Remove some redundancy in the proof for presup

theories/LibTactics.v

@@ -27,9 +27,26 @@ Ltac destruct_all := repeat destruct_logic.
 Tactic Notation "mauto" :=
   eauto with mcltt core.
 
+Tactic Notation "mauto" int_or_var(pow) :=
+  eauto pow with mcltt core.
+
 Tactic Notation "mauto" "using" uconstr(use) :=
   eauto using use with mcltt core.
 
+Tactic Notation "mauto" "using" uconstr(use1) "," uconstr(use2) :=
+  eauto using use1, use2 with mcltt core.
+
+Tactic Notation "mauto" "using" uconstr(use1) "," uconstr(use2) "," uconstr(use3) :=
+  eauto using use1, use2, use3 with mcltt core.
+
+Tactic Notation "mauto" "using" uconstr(use1) "," uconstr(use2) "," uconstr(use3) "," uconstr(use4) :=
+  eauto using use1, use2, use3, use4 with mcltt core.
+
 Tactic Notation "mauto" int_or_var(pow) "using" uconstr(use) :=
   eauto pow using use with mcltt core.
 
+Tactic Notation "mauto" int_or_var(pow) "using" uconstr(use1) "," uconstr(use2) :=
+  eauto pow using use1, use2 with mcltt core.
+
+Tactic Notation "mauto" int_or_var(pow) "using" uconstr(use1) "," uconstr(use2) "," uconstr(use3) "," uconstr(use4) :=
+  eauto pow using use1, use2, use3, use4 with mcltt core.

theories/Presup.v

@@ -11,211 +11,135 @@ Require Import Setoid.
 Ltac breakdown_goal :=
   let rec splitting :=
     match goal with
-    | [H : _ |- ?X ∧ ?Y] => split;splitting
-    | [H : _ |- _ ] => mauto
+    | [|- ?X ∧ ?Y] => split;splitting
+    | [|- _] => mauto
     end
   in splitting
 .
 
+Ltac gen_presup_H :=
+  let rec ctx_eq_helper :=
+    match goal with
+    | [H : ⊢ ?Γ ≈ ?Δ |- _] =>
+        let HΓ := fresh "HΓ" in
+        let HΔ := fresh "HΔ" in
+        pose proof presup_ctx_eq _ _ H as [HΓ HΔ]; gen H; ctx_eq_helper; intro
+    | _ => idtac
+    end
+  in
+  let rec sb_helper :=
+    match goal with
+    | [H : ?Γ ⊢s ?σ : ?Δ |- _] =>
+        let HΓ := fresh "HΓ" in
+        let HΔ := fresh "HΔ" in
+        pose proof presup_sb_ctx _ _ _ H as [HΓ HΔ]; gen H; sb_helper; intro
+    | _ => idtac
+    end
+  in
+  ctx_eq_helper; sb_helper.
+
+Ltac gen_presup_IH presup_tm presup_eq presup_sb_eq :=
+  let rec tm_helper :=
+    match goal with
+    | [H : ?Γ ⊢ ?t : a_typ ?i |- _] => gen H; tm_helper; intro
+    | [H : ?Γ ⊢ ?t : ?T |- _] =>
+        let HΓ := fresh "HΓ" in
+        let i := fresh "i" in
+        let HTi := fresh "HTi" in
+        pose proof presup_tm _ _ _ H as [HΓ [i HTi]]; gen H; tm_helper; intro
+    | _ => idtac
+    end
+  in
+  let rec sb_eq_helper :=
+    match goal with
+    | [H : ?Γ ⊢s ?σ ≈ ?τ : ?Δ |- _] =>
+        let HΓ := fresh "HΓ" in
+        let Hσ := fresh "Hσ" in
+        let Hτ := fresh "Hτ" in
+        let HΔ := fresh "HΔ" in
+        pose proof presup_sb_eq _ _ _ _ H as [HΓ [Hσ [Hτ HΔ]]]; gen H; sb_eq_helper; intro
+    | _ => idtac
+    end
+  in
+  let rec eq_helper :=
+    match goal with
+    | [H : ?Γ ⊢ ?s ≈ ?t : ?T |- _] =>
+        let HΓ := fresh "HΓ" in
+        let i := fresh "i" in
+        let Hs := fresh "Hs" in
+        let Ht := fresh "Ht" in
+        let HTi := fresh "HTi" in
+        pose proof presup_eq _ _ _ _ H as [HΓ [Hs [Ht [i HTi]]]]; gen H; eq_helper; intro
+    | _ => idtac
+    end
+  in
+  tm_helper; sb_eq_helper; eq_helper.
+
+Ltac gen_presup presup_tm presup_eq presup_sb_eq := gen_presup_IH presup_tm presup_eq presup_sb_eq; gen_presup_H.
+
 Lemma presup_tm (Γ : Ctx) (t : exp) (T : Typ) (g_tm : Γ ⊢ t : T) :  ⊢ Γ ∧ ∃ i, Γ ⊢ T : typ i
 with presup_eq  (Γ : Ctx) (s t : exp) (T : Typ) (g_eq : Γ ⊢ s ≈ t : T) :  ⊢ Γ ∧ Γ ⊢ s : T ∧ Γ ⊢ t : T ∧ ∃ i,Γ ⊢ T : typ i
 with presup_sb_eq (Γ Δ : Ctx) (σ τ : Sb) (g_seq : Γ ⊢s σ ≈ τ : Δ) : ⊢ Γ ∧ Γ ⊢s σ : Δ ∧ Γ ⊢s τ : Δ ∧ ⊢ Δ.                        
-Proof.
-  - inversion g_tm;clear g_tm.
-    1-4,8-9 : mauto.
-    -- pose proof (wf_vlookup _ _ _ H H0).
-       breakdown_goal.
-    -- pose proof presup_tm _ _ _ H0 as [AG [i0 AGi]].
-       pose proof ctx_decomp _ _ AG as [G [i1 GTi1]].
-       breakdown_goal.
-       exists i.
-       eapply (sub_lvl _ _ _ _ _ H0).
-       econstructor;mauto.
-
-    -- pose proof presup_tm _ _ _ H as [G [i0 GAi]].
-       pose proof presup_tm _ _ _ H0 as [AG [i1 AGi1]].
-       breakdown_goal.
-       exists (max i i1).
-       pose proof (lift_tm_max _ _ _ _ _ _ H AGi1) as [Ga AGB].
-       econstructor;auto.
-
-    -- pose proof presup_sb_ctx _ _ _ H as [G D].
-       pose proof presup_tm _ _ _ H0 as [_ [i0 DAi0]].
-       breakdown_goal.
-    -- pose proof presup_eq _ _ _ _ H0 as [G [_ [GT _]]].
-       breakdown_goal.
-    -- pose proof presup_tm_ctx _ _ _ H.
-       breakdown_goal.
+Proof with breakdown_goal.
+  - inversion g_tm; clear g_tm; subst; gen_presup presup_tm presup_eq presup_sb_eq; breakdown_goal.
+    -- exists i.
+       eapply sub_lvl...
+       econstructor...
+
+    -- exists (max i i0).
+       pose proof (lift_tm_max _ _ _ _ _ _ H HTi) as [Ga AGB].
+       econstructor...
 
-  - inversion g_eq;clear g_eq.    
-    -- pose proof presup_sb_ctx _ _ _ H as [G D].
-       clear presup_eq.
-       breakdown_goal.
-
-    -- pose proof presup_sb_ctx _ _ _ H as [G D].
-       clear presup_eq.
-       breakdown_goal.
-
-    -- pose proof presup_sb_ctx _ _ _ H as [G D].
-       pose proof (wf_pi _ _ _ _ H0 H1).
-       breakdown_goal.
-       econstructor;mauto.
+  - inversion g_eq; clear g_eq; subst; gen_presup presup_tm presup_eq presup_sb_eq; breakdown_goal.
+    -- pose proof (wf_pi _ _ _ _ H0 H1)...
+       econstructor...
        eapply (sub_lvl _ _ _ _ _ H1).
-       econstructor.
-       econstructor;mauto.
-       mauto.
-       eapply wf_conv;mauto.
-       eapply wf_eq_conv.
-       eapply wf_eq_sym.
-       eapply wf_eq_sub_comp;mauto.
-       eapply wf_eq_typ_sub;mauto.   
-
-    -- pose proof (presup_eq _ _ _ _ H0) as [G [GM [GM' _]]].
-       pose proof (presup_eq _ _ _ _ H1) as [MG [MGT0 [MGT' _]]].
-       clear presup_eq.
-       breakdown_goal.
-       econstructor;mauto.
-       eauto using ctxeq_tm, ctx_eq_refl with mcltt.
-
-    -- breakdown_goal.
-
-    -- breakdown_goal.
-
-    -- pose proof (presup_sb_ctx _ _ _ H) as [G D].
-       breakdown_goal.
-
-    -- pose proof (presup_eq _ _ _ _ H) as [G [Gt0 [Gt' GTi]]].
-       breakdown_goal.
-
-    -- pose proof (presup_sb_ctx _ _ _ H) as [G D].
-       breakdown_goal.
-
-    -- pose proof (presup_sb_eq _ _ _ _ H0) as [G [Gs [Gs' D]]].
-       pose proof (presup_eq _ _ _ _ H) as [_ [Dt0 [Dt' [i DT0i]]]].
-       breakdown_goal.
-       econstructor;mauto.
-       eapply wf_eq_conv;mauto using wf_eq_sub_cong.
-
-    -- pose proof (presup_tm _ _ _ H) as [G [i GTi]].
-       breakdown_goal.
-
-    -- pose proof (ctx_decomp _ _ H) as [G0 [i G0M]].
-       breakdown_goal.
-
-    -- pose proof (presup_tm _ _ _ H1) as [_ [i ]].
-       breakdown_goal.
-       econstructor;mauto.
-       eapply wf_eq_conv.
-       eapply wf_eq_sym.
-       eapply wf_eq_sub_comp;mauto.
-       mauto.
-
-    -- pose proof (presup_tm _ _ _ H1) as [G [n ]].
-       breakdown_goal.
-       eapply wf_conv.
-       eapply wf_sub;mauto.
+       econstructor...
+       eapply wf_conv...
+       eapply wf_eq_conv; mauto 6.
+
+    -- econstructor; mauto using ctxeq_tm, ctx_eq_refl.
+
+    -- econstructor...
+       eapply wf_eq_conv; mauto using wf_eq_sub_cong.
+
+    -- eapply wf_sub...
+       econstructor...
+       inversion H...
+
+    -- eapply wf_conv; try now (econstructor; mauto).
+
+    -- eapply wf_conv; try now (econstructor; mauto).
        eapply wf_eq_trans.
-       eapply wf_eq_sym.
-       eapply wf_eq_conv.
-       eapply wf_eq_sub_comp;mauto.
-       econstructor;mauto.
-       econstructor;mauto.
-       econstructor;mauto.
-       econstructor;mauto.
-       econstructor;mauto. 
-
-    -- breakdown_goal.
-       eapply wf_conv.
-       eapply wf_sub;mauto.
-       eapply wf_eq_conv.
+       + eapply wf_eq_sym.
+         eapply wf_eq_conv.
+         ++ eapply wf_eq_sub_comp...
+         ++ do 2 (econstructor; mauto).
+       + do 3 (econstructor; mauto).
+
+    -- eapply wf_conv; try now (econstructor; mauto).
        eapply wf_eq_trans.
-       eapply wf_eq_sym.
-       eapply wf_eq_conv.
-       eapply wf_eq_sub_comp;mauto.
-       eapply wf_eq_typ_sub.
-       econstructor;mauto.
-       eapply wf_eq_conv.
-       eapply wf_eq_sub_cong;mauto.
-       eapply wf_eq_typ_sub.
-       econstructor;mauto.
-       mauto.
-
-    -- pose proof (presup_eq _ _ _ _ H) as [G [Gs [Gt _]]].
-       breakdown_goal.
-
-    -- pose proof (presup_eq _ _ _ _ H) as [G [Gs [Gt [n GT0]]]].
-       pose proof (presup_eq _ _ _ _ H0) as [_ [_ [GT _]]].
-       breakdown_goal.
-
-    -- pose proof (presup_eq _ _ _ _ H) as [G [Gt [Gs [n GTn]]]].
-       breakdown_goal.
-
-    -- pose proof (presup_eq _ _ _ _ H) as [G [Gs [Gt' [n GTn]]]].
-       pose proof (presup_eq _ _ _ _ H0) as [_ [_ [Gt _]]].
-       breakdown_goal.
+       + eapply wf_eq_sym.
+         eapply wf_eq_conv.
+         ++ eapply wf_eq_sub_comp...
+         ++ do 2 (econstructor; mauto).
+       + do 3 (econstructor; mauto).
+
+  - inversion g_seq; clear g_seq; subst; gen_presup presup_tm presup_eq presup_sb_eq; breakdown_goal.
+    -- inversion_clear H as [|D DTi]...
+
+    -- econstructor...
+       eapply wf_conv...
+
+    -- econstructor...
+       eapply wf_conv...
+       eapply wf_eq_conv...
+
+    -- inversion_clear HΔ as [|Γ0' T' i HΓ0 HT]...
+       econstructor...
+       eapply wf_conv...
+       eapply wf_eq_conv...
 
-  - inversion g_seq;clear g_seq.
-    -- breakdown_goal.
-
-    -- pose proof (ctx_decomp _ _ H) as [D [i DTi]].
-       breakdown_goal.
-
-    -- pose proof (presup_sb_eq _ _ _ _ H) as [G [Gt0 [Gt' G']]].
-       pose proof (presup_sb_eq _ _ _ _ H0) as [_ [G's0 [G's' D]]].
-       breakdown_goal.
-
-    -- pose proof (presup_sb_eq _ _ _ _ H) as [G [Gs0 [Gs' D0]]].
-       pose proof (presup_eq _ _ _ _ H1) as [_ [Gt [Gt' [n _]]]].
-       breakdown_goal.
-       econstructor;mauto.
-       eapply (wf_conv _ _ _ _ _ Gt').
-       eapply wf_eq_conv.
-       eapply wf_eq_sub_cong;mauto.
-       mauto.
-
-    -- pose proof (presup_sb_ctx _ _ _ H) as [G D].
-       breakdown_goal.
-
-    -- pose proof (presup_sb_ctx _ _ _ H) as [G D].
-       breakdown_goal.
-
-    -- pose proof (presup_sb_ctx _ _ _ H) as [G' D].
-       pose proof (presup_sb_ctx _ _ _ H0) as [G'' _].
-       breakdown_goal.
-
-    -- breakdown_goal.
-       econstructor.
-       econstructor;mauto.
-       mauto.
-       eapply wf_conv.
-       eapply (wf_sub _ _ _ _ _ H2 H1).
-       eapply wf_eq_conv.
-       eapply wf_eq_sym.
-       eapply wf_eq_sub_comp;mauto.
-       mauto.
-
-    -- pose proof (presup_sb_ctx _ _ _ H) as [G D].
-       breakdown_goal.
-
-    -- pose proof (presup_sb_ctx _ _ _ H) as [G TG0].
-       pose proof (ctx_decomp _ _ TG0) as [G0 [i G0T]].
-       clear presup_sb_eq.
-       breakdown_goal.
-       econstructor;mauto.
-       eapply wf_conv;mauto.
-       mauto.
-       eapply wf_eq_conv;mauto.
-
-    -- pose proof (presup_sb_eq _ _ _ _ H) as [G [Gt [Gs D]]].
-       breakdown_goal.
-
-    -- pose proof (presup_sb_eq _ _ _ _ H) as [G [Gs [Gs' D]]].
-       pose proof (presup_sb_eq _ _ _ _ H0) as [_ [_ [Gt _]]].
-       breakdown_goal.
-
-    -- pose proof (presup_sb_eq _ _ _ _ H) as [G [Gs [Gt _]]].
-       pose proof (presup_ctx_eq _ _ H0) as [D0 D].
-       breakdown_goal.
     Unshelve.
-    1-9: exact 0. 
-Qed.  
+    all: exact 0.
+Qed.

theories/Syntax.v

@@ -62,15 +62,19 @@ Definition exp_to_num e :=
   | None => None
   end.
 
-Declare Custom Entry exp.
-Declare Scope exp_scope.
-Delimit Scope exp_scope with exp.
+#[global] Declare Custom Entry exp.
+#[global] Declare Scope exp_scope.
+#[global] Delimit Scope exp_scope with exp.
+#[global] Bind Scope exp_scope with exp.
+#[global] Bind Scope exp_scope with subst.
+Open Scope exp_scope.
+Open Scope nat_scope.
 
-Notation "{{ e }}" := e (at level 0, e custom exp at level 99) : exp_scope.
+Notation "<{ x }>" := x (at level 0, x custom exp at level 99) : exp_scope.
 Notation "( x )" := x (in custom exp at level 0, x custom exp at level 99) : exp_scope.
 Notation "~{ x }" := x (in custom exp at level 0, x constr at level 0) : exp_scope.
 Notation "x" := x (in custom exp at level 0, x constr at level 0) : exp_scope.
-Notation "e [ s ]" := (a_sub e s) (in custom exp at level 0, s custom exp at level 99) : exp_scope.
+Notation "e |[ s ]|" := (a_sub e s) (in custom exp at level 0, s custom exp at level 99) : exp_scope.
 Notation "'λ' T e" := (a_fn T e) (in custom exp at level 0, T custom exp at level 30, e custom exp at level 30) : exp_scope.
 Notation "f x .. y" := (a_app .. (a_app f x) .. y) (in custom exp at level 40, f custom exp, x custom exp at next level, y custom exp at next level) : exp_scope.
 Notation "'ℕ'" := a_nat (in custom exp) : exp_scope.
@@ -79,8 +83,8 @@ Notation "'Π' T S" := (a_pi T S) (in custom exp at level 0, T custom exp at lev
 Number Notation exp num_to_exp exp_to_num : exp_scope.
 Notation "'suc' e" := (a_succ e) (in custom exp at level 30, e custom exp at level 30) : exp_scope.
 Notation "'#' n" := (a_var n) (in custom exp at level 0, n constr at level 0) : exp_scope.
-Notation "'$id'" := a_id (in custom exp at level 0) : exp_scope.
-Notation "'$wk'" := a_weaken (in custom exp at level 0) : exp_scope.
+Notation "'Id'" := a_id (in custom exp at level 0) : exp_scope.
+Notation "'Wk'" := a_weaken (in custom exp at level 0) : exp_scope.
 Infix "∙" := a_compose (in custom exp at level 70) : exp_scope.
 Infix "," := a_extend (in custom exp at level 80) : exp_scope.