Restore presup

theories/Core/Syntactic/Presup.v

@@ -26,82 +26,112 @@ Ltac gen_presup_ctx H :=
   | {{ ?Γ ⊢s ?σ : ?Δ }} =>
       let HΓ := fresh "HΓ" in
       let HΔ := fresh "HΔ" in
-      pose proof presup_sb_ctx H as [HΓ HΔ]
+      pose proof presup_sub_ctx H as [HΓ HΔ]
   | _ => idtac
   end.
 
-Ltac gen_presup_IH presup_tm presup_eq presup_sb_eq H :=
+Ltac gen_presup_IH presup_exp presup_exp_eq presup_sub_eq H :=
   match type of H with
   | {{ ?Γ ⊢ ?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]]
-  | {{ ?Γ ⊢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Δ]]]
+      pose proof presup_exp _ _ _ H as [HΓ [i HTi]]
   | {{ ?Γ ⊢ ?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]]]]
+      pose proof presup_exp_eq _ _ _ _ H as [HΓ [Hs [Ht [i HTi]]]]
+  | {{ ?Γ ⊢s ?σ ≈ ?τ : ?Δ }} =>
+      let HΓ := fresh "HΓ" in
+      let Hσ := fresh "Hσ" in
+      let Hτ := fresh "Hτ" in
+      let HΔ := fresh "HΔ" in
+      pose proof presup_sub_eq _ _ _ _ H as [HΓ [Hσ [Hτ HΔ]]]
   | _ => gen_presup_ctx H
   end.
 
-Lemma presup_tm : forall {Γ t T}, {{ Γ ⊢ t : T }} -> {{ ⊢ Γ }} ∧ ∃ i, {{ Γ ⊢ T : Type@i }}
-with presup_eq : forall {Γ s t T}, {{ Γ ⊢ s ≈ t : T }} -> {{ ⊢ Γ }} ∧ {{ Γ ⊢ s : T }} ∧ {{ Γ ⊢ t : T }} ∧ ∃ i, {{ Γ ⊢ T : Type@i }}
-with presup_sb_eq : forall {Γ Δ σ τ}, {{ Γ ⊢s σ ≈ τ : Δ }} -> {{ ⊢ Γ }} ∧ {{ Γ ⊢s σ : Δ }} ∧ {{ Γ ⊢s τ : Δ }} ∧ {{ ⊢ Δ }}.
+Lemma presup_exp : forall {Γ t T}, {{ Γ ⊢ t : T }} -> {{ ⊢ Γ }} ∧ ∃ i, {{ Γ ⊢ T : Type@i }}
+with presup_exp_eq : forall {Γ s t T}, {{ Γ ⊢ s ≈ t : T }} -> {{ ⊢ Γ }} ∧ {{ Γ ⊢ s : T }} ∧ {{ Γ ⊢ t : T }} ∧ ∃ i, {{ Γ ⊢ T : Type@i }}
+with presup_sub_eq : forall {Γ Δ σ τ}, {{ Γ ⊢s σ ≈ τ : Δ }} -> {{ ⊢ Γ }} ∧ {{ Γ ⊢s σ : Δ }} ∧ {{ Γ ⊢s τ : Δ }} ∧ {{ ⊢ Δ }}.
 Proof with mauto.
+  (* presup_exp *)
   - intros * Ht.
-    inversion_clear Ht; (on_all_hyp: gen_presup_IH presup_tm presup_eq presup_sb_eq); clear presup_tm presup_eq presup_sb_eq; breakdown_goal.
-    -- eexists.
-       eapply exp_sub_typ...
-       econstructor...
-    -- eexists.
-       pose proof (lift_tm_max_left i0 H).
-       pose proof (lift_tm_max_right i HTi).
-       econstructor...
+    inversion_clear Ht; (on_all_hyp: gen_presup_IH presup_exp presup_exp_eq presup_sub_eq); clear presup_exp presup_exp_eq presup_sub_eq; breakdown_goal.
+    + eexists.
+      eapply exp_sub_typ...
+      econstructor...
+    + eexists.
+      pose proof (lift_exp_max_left i0 H).
+      pose proof (lift_exp_max_right i HTi).
+      econstructor...
+    + eexists.
+      eapply exp_sub_typ...
+      econstructor...
 
   - intros * Hst.
-    inversion_clear Hst; (on_all_hyp: gen_presup_IH presup_tm presup_eq presup_sb_eq); clear presup_tm presup_eq presup_sb_eq; breakdown_goal.
-    -- econstructor...
-       eapply exp_sub_typ...
-       econstructor...
-       eapply wf_conv...
-       eapply wf_eq_conv; mauto 6.
-
-    -- econstructor...
-       eapply wf_eq_conv...
-
-    -- eapply wf_exp_sub...
-       econstructor...
-       inversion H...
-
-    -- eapply wf_conv; [|eapply wf_eq_conv]...
-
-    -- eapply wf_conv; [econstructor; mauto|].
-       eapply wf_eq_trans.
-       + eapply wf_eq_sym.
-         eapply wf_eq_conv.
-         ++ eapply wf_eq_exp_sub_compose...
-         ++ econstructor...
-       + do 2 econstructor...
-
-    -- eapply wf_conv; [econstructor; mauto|].
-       eapply wf_eq_trans.
-       + eapply wf_eq_sym.
-         eapply wf_eq_conv.
-         ++ eapply wf_eq_exp_sub_compose...
-         ++ econstructor...
-       + do 2 econstructor...
+    inversion_clear Hst; (on_all_hyp: gen_presup_IH presup_exp presup_exp_eq presup_sub_eq); clear presup_exp presup_exp_eq presup_sub_eq; breakdown_goal.
+    + assert {{ Γ ⊢ Type@i[Id,,M] ≈ Type@i : Type@(S i) }}; [econstructor; econstructor|]...
+      assert {{ Γ ⊢ A[Id,,M] ≈ A'[Id,,M'] : Type@i }}; [eapply wf_exp_eq_conv; econstructor; econstructor|]...
+      assert {{ Γ ⊢ A[Id,,zero] ≈ A'[Id,,zero] : Type@i }}; [eapply exp_eq_sub_cong_typ; econstructor|]...
+      assert {{ Γ, ℕ, A ⊢ ℕ[Wk∘Wk] ≈ ℕ : Type@i }}...
+      assert {{ Γ, ℕ, A ⊢ A[Wk∘Wk,,succ(#1)] ≈ A'[Wk∘Wk,,succ(#1)] : Type@i }}.
+      {
+        eapply exp_eq_sub_cong_typ...
+        econstructor...
+        eapply wf_conv...
+        econstructor...
+        assert {{ Γ, ℕ, A ⊢ ℕ ≈ ℕ[Wk∘Wk] : Type@i }}...
+        eapply wf_conv...
+        eapply wf_exp_eq_trans...
+      }
+      econstructor...
+      econstructor...
+    + econstructor...
+      eapply exp_sub_typ...
+      econstructor...
+    + assert {{ Γ ⊢s Id∘σ,,M[σ] ≈ σ,,M[σ] : Δ,ℕ }}; [eapply wf_sub_eq_sym; econstructor|]...
+      assert {{ Γ ⊢s (Id,,M)∘σ ≈ Id∘σ,,M[σ] : Δ,ℕ }}; [econstructor|]...
+      assert {{ Γ ⊢s (Id,,M)∘σ ≈ σ,,M[σ] : Δ,ℕ }}...
+      assert {{ Γ ⊢ A[(Id,,M)][σ] ≈ A[(Id,,M)∘σ] : Type@i }}.
+      {
+        eapply wf_exp_eq_sym. econstructor.
+        - eapply wf_exp_eq_sub_compose... econstructor...
+        - do 3 (econstructor; mauto).
+      }
+      assert {{ Γ ⊢ A[(Id,,M)][σ] ≈ A[σ,,M[σ]] : Type@i }} by (eapply wf_exp_eq_trans; mauto; do 4 (econstructor; mauto)).
+      econstructor; econstructor...
+    + assert {{ Γ ⊢ A[~(q σ)][Id,,M[σ]] ≈ A[σ,,M[σ]] : Type@i }}.
+      {  }
+    + econstructor...
+      eapply wf_eq_conv...
+
+    + eapply wf_exp_sub...
+      econstructor...
+      inversion H...
+
+    + eapply wf_conv; [|eapply wf_eq_conv]...
+
+    + eapply wf_conv; [econstructor; mauto|].
+      eapply wf_eq_trans.
+      * eapply wf_eq_sym.
+        eapply wf_eq_conv.
+        { eapply wf_eq_exp_sub_compose... }
+        { econstructor... }
+      * do 2 econstructor...
+
+    + eapply wf_conv; [econstructor; mauto|].
+      eapply wf_eq_trans.
+      * eapply wf_eq_sym.
+        eapply wf_eq_conv.
+        { eapply wf_eq_exp_sub_compose... }
+        { econstructor... }
+      * do 2 econstructor...
 
   - intros * Hστ.
-    inversion_clear Hστ; (on_all_hyp: gen_presup_IH presup_tm presup_eq presup_sb_eq); clear presup_tm presup_eq presup_sb_eq; breakdown_goal.
+    inversion_clear Hστ; (on_all_hyp: gen_presup_IH presup_exp presup_exp_eq presup_sub_eq); clear presup_exp presup_exp_eq presup_sub_eq; breakdown_goal.
     -- inversion_clear H...
 
     -- econstructor...
@@ -121,6 +151,6 @@ Proof with mauto.
 Qed.
 
 #[export]
-Hint Resolve presup_tm presup_eq presup_sb_eq : mcltt.
+Hint Resolve presup_exp presup_exp_eq presup_sub_eq : mcltt.
 
-Ltac gen_presup H := gen_presup_IH presup_tm presup_eq presup_sb_eq H; gen_presup_ctx H.
+Ltac gen_presup H := gen_presup_IH presup_exp presup_exp_eq presup_sub_eq H; gen_presup_ctx H.