Restore all except Presup

Beluga-lang · Jan 13, 2024 · aa4508e · aa4508e
1 parent e6a2ca6
commit aa4508e
Show file tree

Hide file tree

Showing 3 changed files with 109 additions and 88 deletions.
diff --git a/theories/Core/Syntactic/CtxEquiv.v b/theories/Core/Syntactic/CtxEquiv.v
@@ -5,58 +5,79 @@ Require Import Syntactic.Syntax.
 Require Import Syntactic.System.
 Require Import Syntactic.SystemLemmas.
 
-Lemma ctxeq_tm : forall {Γ Δ t T}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢ t : T }} -> {{ Δ ⊢ t : T }}
+Ltac gen_ctxeq_helper_IH ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper H :=
+  match type of H with
+  | {{ ?Γ ⊢ ?M : ?A }} => pose proof ctxeq_exp_helper _ _ _ H
+  | {{ ?Γ ⊢ ?M ≈ ?N : ?A }} => pose proof ctxeq_exp_eq_helper _ _ _ _ H
+  | {{ ?Γ ⊢s ?σ : ?Δ }} => pose proof ctxeq_sub_helper _ _ _ H
+  | {{ ?Γ ⊢s ?σ ≈ ?τ : ?Δ }} => pose proof ctxeq_sub_eq_helper _ _ _ _ H
+  | _ => idtac
+  end.
+
+Lemma ctxeq_exp_helper : forall {Γ M A}, {{ Γ ⊢ M : A }} -> ∀ {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢ M : A }}
 with
-ctxeq_eq : forall {Γ Δ t t' T}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢ t ≈ t' : T }} -> {{ Δ ⊢ t ≈ t' : T }}
+ctxeq_exp_eq_helper : forall {Γ M M' A}, {{ Γ ⊢ M ≈ M' : A }} -> ∀ {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢ M ≈ M' : A }}
 with
-ctxeq_s : forall {Γ Γ' Δ σ}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢s σ : Γ' }} -> {{ Δ ⊢s σ : Γ' }}
+ctxeq_sub_helper : forall {Γ Γ' σ}, {{ Γ ⊢s σ : Γ' }} -> ∀ {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢s σ : Γ' }}
 with
-ctxeq_s_eq : forall {Γ Γ' Δ σ σ'}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢s σ ≈ σ' : Γ' }} -> {{ Δ ⊢s σ ≈ σ' : Γ' }}.
+ctxeq_sub_eq_helper : forall {Γ Γ' σ σ'}, {{ Γ ⊢s σ ≈ σ' : Γ' }} -> ∀ {Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ Δ ⊢s σ ≈ σ' : Γ' }}.
 Proof with mauto.
-  (*ctxeq_tm*)
-  - clear ctxeq_tm.
-    intros * HΓΔ Ht.
-    gen Δ.
-    induction Ht; intros; destruct (presup_ctx_eq HΓΔ)...
-    -- pose proof (IHHt1 _ HΓΔ).
-       assert ({{ ⊢ Γ , A ≈ Δ , A }})...
-    -- destruct (var_in_eq HΓΔ H0) as [T' [i [xT'G [GTT' DTT']]]].
-       eapply wf_conv...
-    -- assert ({{ ⊢ Γ , A ≈ Δ , A }}); mauto 6.
-    -- pose proof (IHHt1 _ HΓΔ).
-       assert ({{ ⊢ Γ , A ≈ Δ , A }})...
-  (*ctxeq_eq*)
-  - clear ctxeq_eq.
-    intros * HΓΔ Htt'.
-    gen Δ.
-    induction Htt'; intros; destruct (presup_ctx_eq HΓΔ).
-    1-4,6-19: mauto.
-    -- pose proof (IHHtt'1 _ HΓΔ).
-       pose proof (ctxeq_tm _ _ _ _ HΓΔ H).
-       assert ({{ ⊢ Γ , M ≈ Δ , M }})...
-    -- inversion_clear HΓΔ.
-       pose proof (var_in_eq H3 H0) as [T'' [n [xT'' [GTT'' DTT'']]]].
-       destruct (presup_ctx_eq H3).
-       eapply wf_eq_conv...
-    -- pose proof (var_in_eq HΓΔ H0) as [T'' [n [xT'' [GTT'' DTT'']]]].
-       eapply wf_eq_conv...
-  (*ctxeq_s*)
-  - clear ctxeq_s.
-    intros * HΓΔ Hσ.
-    gen Δ.
-    induction Hσ; intros; destruct (presup_ctx_eq HΓΔ)...
+  (* ctxeq_exp_helper *)
+  - intros * HM * HΓΔ. gen Δ.
+    inversion_clear HM; (on_all_hyp: gen_ctxeq_helper_IH ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper); clear ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper; intros; destruct (presup_ctx_eq HΓΔ)...
+    all: try (rename B into C); try (rename A0 into B).
+    2-4: assert {{ Δ ⊢ B : Type@i }} as HB; eauto.
+    2-4: assert {{ ⊢ Γ, B ≈ Δ, B }}; mauto; clear HB...
+    + assert {{ ⊢ Γ, ℕ ≈ Δ, ℕ }}; [econstructor|]...
+      assert {{ Δ, ℕ ⊢ B : Type@i }}...
+      econstructor...
+    + assert (∃ B i, {{ #x : B ∈ Δ }} ∧ {{ Γ ⊢ A ≈ B : Type@i }} ∧ {{ Δ ⊢ A ≈ B : Type@i }}) as [? [? [? [? ?]]]]...
+  (* ctxeq_exp_eq_helper *)
+  - intros * HMM' * HΓΔ. gen Δ.
+    inversion_clear HMM'; (on_all_hyp: gen_ctxeq_helper_IH ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper); clear ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper; intros; destruct (presup_ctx_eq HΓΔ)...
+    all: try (rename B into C); try (rename B' into C'); try (rename A0 into B); try (rename A' into B').
+    1-3: assert {{ ⊢ Γ, ℕ ≈ Δ, ℕ }}; [econstructor|]...
+    1-3: assert {{ Δ, ℕ ⊢ B : Type@i }}; eauto.
+    1-3: econstructor...
+    1-5: assert {{ Δ ⊢ B : Type@i }}; eauto.
+    1-5: assert {{ ⊢ Γ, B ≈ Δ, B }}...
+    + assert (∃ B i, {{ #x : B ∈ Δ }} ∧ {{ Γ ⊢ A ≈ B : Type@i }} ∧ {{ Δ ⊢ A ≈ B : Type@i }}) as [? [? [? [? ?]]]]...
+    + inversion_clear HΓΔ as [|? ? ? ? C'].
+      assert (∃ D i', {{ #x : D ∈ Δ0 }} ∧ {{ Γ0 ⊢ B ≈ D : Type@i' }} ∧ {{ Δ0 ⊢ B ≈ D : Type@i' }}) as [D [i0 [? [? ?]]]]...
+      assert {{ Δ0, C' ⊢ B[Wk] ≈ D[Wk] : Type @ i0 }}...
+  (* ctxeq_sub_helper *)
+  - intros * Hσ * HΓΔ. gen Δ.
+    inversion_clear Hσ; (on_all_hyp: gen_ctxeq_helper_IH ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper); clear ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper; intros; destruct (presup_ctx_eq HΓΔ)...
     inversion_clear HΓΔ.
     econstructor...
-  (*ctxeq_s_eq*)
-  - clear ctxeq_s_eq.
-    intros * HΓΔ Hσσ'.
-    gen Δ.
-    induction Hσσ'; intros; destruct (presup_ctx_eq HΓΔ).
-    3-9,11-13: mauto.
-    -- inversion_clear HΓΔ; eapply wf_sub_eq_conv...
-    -- inversion_clear HΓΔ; eapply wf_sub_eq_conv...
-    -- econstructor. eapply ctxeq_s...
+  (* ctxeq_sub_eq_helper *)
+  - intros * Hσσ' * HΓΔ. gen Δ.
+    inversion_clear Hσσ'; (on_all_hyp: gen_ctxeq_helper_IH ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper); clear ctxeq_exp_helper ctxeq_exp_eq_helper ctxeq_sub_helper ctxeq_sub_eq_helper; intros; destruct (presup_ctx_eq HΓΔ)...
+    inversion_clear HΓΔ.
+    eapply wf_sub_eq_conv...
+    Unshelve.
+    all: constructor.
+Qed.
+
+Lemma ctxeq_exp : forall {Γ Δ M A}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢ M : A }} -> {{ Δ ⊢ M : A }}.
+Proof.
+  eauto using ctxeq_exp_helper.
+Qed.
+
+Lemma ctxeq_exp_eq : forall {Γ Δ M M' A}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢ M ≈ M' : A }} -> {{ Δ ⊢ M ≈ M' : A }}.
+Proof.
+  eauto using ctxeq_exp_eq_helper.
+Qed.
+
+Lemma ctxeq_sub : forall {Γ Δ σ Γ'}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢s σ : Γ' }} -> {{ Δ ⊢s σ : Γ' }}.
+Proof.
+  eauto using ctxeq_sub_helper.
+Qed.
+
+Lemma ctxeq_sub_eq : forall {Γ Δ σ σ' Γ'}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢s σ ≈ σ' : Γ' }} -> {{ Δ ⊢s σ ≈ σ' : Γ' }}.
+Proof.
+  eauto using ctxeq_sub_eq_helper.
 Qed.
 
 #[export]
-Hint Resolve ctxeq_tm ctxeq_eq ctxeq_s ctxeq_s_eq : mcltt.
+Hint Resolve ctxeq_exp ctxeq_exp_eq ctxeq_sub ctxeq_sub_eq : mcltt.
diff --git a/theories/Core/Syntactic/Relations.v b/theories/Core/Syntactic/Relations.v
@@ -24,10 +24,10 @@ Proof with mauto.
   induction HΓ01 as [|? ? ? i01 * HΓ01 IHΓ01 HΓ0T0 _ HΓ0T01 _]; intros...
   rename HΓ12 into HT1Γ12.
   inversion_clear HT1Γ12 as [|? ? ? i12 * HΓ12' _ HΓ2'T2 _ HΓ2'T12].
-  pose proof (lift_tm_max_left i12 HΓ0T0).
-  pose proof (lift_tm_max_right i01 HΓ2'T2).
-  pose proof (lift_eq_max_left i12 HΓ0T01).
-  pose proof (lift_eq_max_right i01 HΓ2'T12).
+  pose proof (lift_exp_max_left i12 HΓ0T0).
+  pose proof (lift_exp_max_right i01 HΓ2'T2).
+  pose proof (lift_exp_eq_max_left i12 HΓ0T01).
+  pose proof (lift_exp_eq_max_right i01 HΓ2'T12).
   econstructor...
 Qed.
 
@@ -37,11 +37,11 @@ Add Relation (ctx) (wf_ctx_eq)
     as ctx_eq.
 
 Add Parametric Relation (Γ : ctx) (T : typ) : (exp) (λ t t', {{ Γ ⊢ t ≈ t' : T }})
-    symmetry proved by (λ t t', wf_eq_sym Γ t t' T)
-    transitivity proved by (λ t t' t'', wf_eq_trans Γ t t' T t'')
-    as tm_eq.                                                
+    symmetry proved by (λ t t', wf_exp_eq_sym Γ t t' T)
+    transitivity proved by (λ t t' t'', wf_exp_eq_trans Γ t t' T t'')
+    as exp_eq.                                                
 
 Add Parametric Relation (Γ Δ : ctx) : (sub) (λ σ τ, {{ Γ ⊢s σ ≈ τ : Δ }})
     symmetry proved by (λ σ τ, wf_sub_eq_sym Γ σ τ Δ)
     transitivity proved by (λ σ τ ρ, wf_sub_eq_trans Γ σ τ Δ ρ)
-    as sb_eq.
+    as sub_eq.
diff --git a/theories/Core/Syntactic/SystemLemmas.v b/theories/Core/Syntactic/SystemLemmas.v
@@ -4,49 +4,49 @@ Require Import LibTactics.
 Require Import Syntactic.Syntax.
 Require Import Syntactic.System.
 
-Lemma ctx_decomp : forall {Γ T}, {{ ⊢ Γ , T }} -> {{ ⊢ Γ }} ∧ ∃ i, {{ Γ ⊢ T : Type@i }}.
+Lemma ctx_decomp : forall {Γ A}, {{ ⊢ Γ , A }} -> {{ ⊢ Γ }} ∧ ∃ i, {{ Γ ⊢ A : Type@i }}.
 Proof with mauto.
-  intros * HTΓ.
-  inversion HTΓ; subst...
+  intros * HAΓ.
+  inversion HAΓ; subst...
 Qed.
 
-Lemma lift_tm_ge : forall {Γ T n m}, n <= m -> {{ Γ ⊢ T : Type@n }} -> {{ Γ ⊢ T : Type@m }}.
+Lemma lift_exp_ge : forall {Γ A n m}, n <= m -> {{ Γ ⊢ A : Type@n }} -> {{ Γ ⊢ A : Type@m }}.
 Proof with mauto.
-  intros * Hnm HT.
+  intros * Hnm HA.
   induction m; inversion Hnm; subst...
 Qed.
 
 #[export]
-Hint Resolve lift_tm_ge : mcltt.
+Hint Resolve lift_exp_ge : mcltt.
 
-Lemma lift_tm_max_left : forall {Γ T n} m, {{ Γ ⊢ T : Type@n }} -> {{ Γ ⊢ T : Type@(max n m) }}.
+Lemma lift_exp_max_left : forall {Γ A n} m, {{ Γ ⊢ A : Type@n }} -> {{ Γ ⊢ A : Type@(max n m) }}.
 Proof with mauto.
   intros.
   assert (n <= max n m) by lia...
 Qed.
 
-Lemma lift_tm_max_right : forall {Γ T} n {m}, {{ Γ ⊢ T : Type@m }} -> {{ Γ ⊢ T : Type@(max n m) }}.
+Lemma lift_exp_max_right : forall {Γ A} n {m}, {{ Γ ⊢ A : Type@m }} -> {{ Γ ⊢ A : Type@(max n m) }}.
 Proof with mauto.
   intros.
   assert (m <= max n m) by lia...
 Qed.
 
-Lemma lift_eq_ge : forall {Γ T T' n m}, n <= m -> {{ Γ ⊢ T ≈ T': Type@n }} -> {{ Γ ⊢ T ≈ T' : Type@m }}.
+Lemma lift_exp_eq_ge : forall {Γ A A' n m}, n <= m -> {{ Γ ⊢ A ≈ A': Type@n }} -> {{ Γ ⊢ A ≈ A' : Type@m }}.
 Proof with mauto.
-  intros * Hnm HTT'.
+  intros * Hnm HAA'.
   induction m; inversion Hnm; subst...
 Qed.
 
 #[export]
-Hint Resolve lift_eq_ge : mcltt.
+Hint Resolve lift_exp_eq_ge : mcltt.
 
-Lemma lift_eq_max_left : forall {Γ T T' n} m, {{ Γ ⊢ T ≈ T' : Type@n }} -> {{ Γ ⊢ T ≈ T' : Type@(max n m) }}.
+Lemma lift_exp_eq_max_left : forall {Γ A A' n} m, {{ Γ ⊢ A ≈ A' : Type@n }} -> {{ Γ ⊢ A ≈ A' : Type@(max n m) }}.
 Proof with mauto.
   intros.
   assert (n <= max n m) by lia...
 Qed.
 
-Lemma lift_eq_max_right : forall {Γ T T'} n {m}, {{ Γ ⊢ T ≈ T' : Type@m }} -> {{ Γ ⊢ T ≈ T' : Type@(max n m) }}.
+Lemma lift_exp_eq_max_right : forall {Γ A A'} n {m}, {{ Γ ⊢ A ≈ A' : Type@m }} -> {{ Γ ⊢ A ≈ A' : Type@(max n m) }}.
 Proof with mauto.
   intros.
   assert (m <= max n m) by lia...
@@ -60,46 +60,46 @@ Proof with mauto.
 Qed.
 
 (* Corresponds to ≈-refl in the Agda code *)
-Lemma tm_eq_refl : forall {Γ t T}, {{ Γ ⊢ t : T }} -> {{ Γ ⊢ t ≈ t : T }}.
+Lemma exp_eq_refl : forall {Γ M A}, {{ Γ ⊢ M : A }} -> {{ Γ ⊢ M ≈ M : A }}.
 Proof.
   mauto.
 Qed.
 
-Lemma sb_eq_refl : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢s σ ≈ σ : Δ }}.
+Lemma sub_eq_refl : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢s σ ≈ σ : Δ }}.
 Proof.
   mauto.
 Qed.
 
 #[export]
-Hint Resolve ctx_decomp presup_ctx_eq tm_eq_refl sb_eq_refl : mcltt.
+Hint Resolve ctx_decomp presup_ctx_eq exp_eq_refl sub_eq_refl : mcltt.
 
 (* Corresponds to t[σ]-Se in the Agda proof *)
-Lemma exp_sub_typ : forall {Δ Γ T σ i}, {{ Δ ⊢ T : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ T[σ] : Type@i }}.
+Lemma exp_sub_typ : forall {Δ Γ A σ i}, {{ Δ ⊢ A : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ A[σ] : Type@i }}.
 Proof.
   mauto.
 Qed.
 
 (* Corresponds to []-cong-Se′ in the Agda proof*)
-Lemma eq_exp_sub_typ : forall {Δ Γ T T' σ i}, {{ Δ ⊢ T ≈ T' : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ T[σ] ≈ T'[σ] : Type@i }}.
+Lemma exp_eq_sub_cong_typ : forall {Δ Γ A A' σ i}, {{ Δ ⊢ A ≈ A' : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ A[σ] ≈ A'[σ] : Type@i }}.
 Proof.
   mauto.
 Qed.
 
 #[export]
-Hint Resolve exp_sub_typ eq_exp_sub_typ : mcltt.
+Hint Resolve exp_sub_typ exp_eq_sub_cong_typ : mcltt.
 
 (* Corresponds to ∈!⇒ty-wf in Agda proof *)
-Lemma var_in_wf : forall {Γ T x}, {{ ⊢ Γ }} -> {{ #x : T ∈ Γ }} -> ∃ i, {{ Γ ⊢ T : Type@i }}.
+Lemma ctx_lookup_wf : forall {Γ A x}, {{ ⊢ Γ }} -> {{ #x : A ∈ Γ }} -> ∃ i, {{ Γ ⊢ A : Type@i }}.
 Proof with mauto.
-  intros * HΓ Hx. gen x T.
+  intros * HΓ Hx. gen x A.
   induction HΓ; intros; inversion_clear Hx as [|? ? ? ? Hx']...
   destruct (IHHΓ _ _ Hx')...
 Qed.
 
 #[export]
-Hint Resolve var_in_wf : mcltt.
+Hint Resolve ctx_lookup_wf : mcltt.
 
-Lemma presup_sb_ctx : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ ⊢ Γ }} ∧ {{ ⊢ Δ }}.
+Lemma presup_sub_ctx : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ ⊢ Γ }} ∧ {{ ⊢ Δ }}.
 Proof with mauto.
   intros * Hσ.
   induction Hσ...
@@ -111,20 +111,20 @@ Proof with mauto.
 Qed.
 
 #[export]
-Hint Resolve presup_sb_ctx : mcltt.
+Hint Resolve presup_sub_ctx : mcltt.
 
-Lemma presup_tm_ctx : forall {Γ t T}, {{ Γ ⊢ t : T }} -> {{ ⊢ Γ }}.
+Lemma presup_ctx : forall {Γ M A}, {{ Γ ⊢ M : A }} -> {{ ⊢ Γ }}.
 Proof with mauto.
-  intros * Ht.
-  induction Ht...
+  intros * HM.
+  induction HM...
   eapply proj1...
 Qed.
 
 #[export]
-Hint Resolve presup_tm_ctx : mcltt.
+Hint Resolve presup_ctx : mcltt.
 
 (* Corresponds to ∈!⇒ty≈ in Agda proof *)
-Lemma var_in_eq : forall {Γ Δ T x}, {{ ⊢ Γ ≈ Δ }} -> {{ #x : T ∈ Γ }} -> ∃ S i, {{ #x : S ∈ Δ }} ∧ {{ Γ ⊢ T ≈ S : Type@i }} ∧ {{ Δ ⊢ T ≈ S : Type@i }}.
+Lemma ctxeq_ctx_lookup : forall {Γ Δ A x}, {{ ⊢ Γ ≈ Δ }} -> {{ #x : A ∈ Γ }} -> ∃ B i, {{ #x : B ∈ Δ }} ∧ {{ Γ ⊢ A ≈ B : Type@i }} ∧ {{ Δ ⊢ A ≈ B : Type@i }}.
 Proof with mauto.
   intros * HΓΔ Hx.
   gen Δ; induction Hx; intros; inversion_clear HΓΔ as [|? ? ? ? ? HΓΔ'].
@@ -141,18 +141,18 @@ Proof with mauto.
 Qed.
 
 #[export]
-Hint Resolve var_in_eq ctx_eq_sym : mcltt.
+Hint Resolve ctxeq_ctx_lookup ctx_eq_sym : mcltt.
 
-Lemma presup_sb_eq_ctx : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Γ }}.
+Lemma presup_sub_eq_ctx : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Γ }}.
 Proof with mauto.
   intros.
   induction H; mauto; now (eapply proj1; mauto).
 Qed.
 
 #[export]
-Hint Resolve presup_sb_eq_ctx : mcltt.
+Hint Resolve presup_sub_eq_ctx : mcltt.
 
-Lemma presup_tm_eq_ctx : forall {Γ t t' T}, {{ Γ ⊢ t ≈ t' : T }} -> {{ ⊢ Γ }}.
+Lemma presup_exp_eq_ctx : forall {Γ M M' A}, {{ Γ ⊢ M ≈ M' : A }} -> {{ ⊢ Γ }}.
 Proof with mauto.
   intros.
   induction H...
@@ -161,4 +161,4 @@ Proof with mauto.
 Qed.
 
 #[export]
-Hint Resolve presup_tm_eq_ctx : mcltt.
+Hint Resolve presup_exp_eq_ctx : mcltt.