Merge pull request #39 from Beluga-lang/PR-syntax-update

Update notations

theories/CtxEqLemmas.v

@@ -3,26 +3,26 @@ Require Import Mcltt.Syntax.
 Require Export Mcltt.System.
 Require Export Mcltt.LibTactics.
 
-Lemma ctx_decomp : forall {Γ T}, ⊢ T :: Γ -> (⊢ Γ ∧ ∃ i, Γ ⊢ T : typ i).
+Lemma ctx_decomp : forall {Γ T}, {{ ⊢ Γ , T }} -> {{ ⊢ Γ }} ∧ ∃ i, {{ Γ ⊢ T : Type@i }}.
 Proof with mauto.
   intros * HTΓ.
   inversion HTΓ; subst...
 Qed.
 
 (* Corresponds to presup-⊢≈ in the Agda proof *)
-Lemma presup_ctx_eq : forall {Γ Δ}, ⊢ Γ ≈ Δ -> ⊢ Γ ∧ ⊢ Δ.
+Lemma presup_ctx_eq : forall {Γ Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ ⊢ Γ }} ∧ {{ ⊢ Δ }}.
 Proof with mauto.
   intros * HΓΔ.
   induction HΓΔ as [|* ? [? ?]]...
 Qed.
 
-(* Corresponds to ≈-refl in the Agda code*)
-Lemma tm_eq_refl : forall {Γ t T}, Γ ⊢ t : T -> Γ ⊢ t ≈ t : T.
+(* Corresponds to ≈-refl in the Agda code *)
+Lemma tm_eq_refl : forall {Γ t T}, {{ Γ ⊢ t : T }} -> {{ Γ ⊢ t ≈ t : T }}.
 Proof.
   mauto.
 Qed.
 
-Lemma sb_eq_refl : forall {Γ Δ σ}, Γ ⊢s σ : Δ -> Γ ⊢s σ ≈ σ : Δ.
+Lemma sb_eq_refl : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢s σ ≈ σ : Δ }}.
 Proof.
   mauto.
 Qed.
@@ -31,22 +31,22 @@ Qed.
 Hint Resolve ctx_decomp presup_ctx_eq tm_eq_refl sb_eq_refl : mcltt.
 
 (* Corresponds to t[σ]-Se in the Agda proof *)
-Lemma sub_lvl : forall {Δ Γ T σ i}, Δ ⊢ T : typ i -> Γ ⊢s σ : Δ -> Γ ⊢ a_sub T σ : typ i.
+Lemma exp_sub_typ : forall {Δ Γ T σ i}, {{ Δ ⊢ T : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ T[σ] : Type@i }}.
 Proof.
   mauto.
 Qed.
 
 (* Corresponds to []-cong-Se′ in the Agda proof*)
-Lemma sub_lvl_eq : forall {Δ Γ T T' σ i}, Δ ⊢ T ≈ T' : typ i -> Γ ⊢s σ : Δ -> Γ ⊢ a_sub T σ ≈ a_sub T' σ : typ i.
+Lemma eq_exp_sub_typ : forall {Δ Γ T T' σ i}, {{ Δ ⊢ T ≈ T' : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ T[σ] ≈ T'[σ] : Type@i }}.
 Proof.
   mauto.
 Qed.
 
 #[export]
-Hint Resolve sub_lvl sub_lvl_eq : mcltt.
+Hint Resolve exp_sub_typ eq_exp_sub_typ : mcltt.
 
 (* Corresponds to ∈!⇒ty-wf in Agda proof *)
-Lemma var_in_wf : forall {Γ T x}, ⊢ Γ -> x : T ∈! Γ -> ∃ i, Γ ⊢ T : typ i.
+Lemma var_in_wf : forall {Γ T x}, {{ ⊢ Γ }} -> {{ #x : T ∈ Γ }} -> ∃ i, {{ Γ ⊢ T : Type@i }}.
 Proof with mauto.
   intros * HΓ Hx. gen x T.
   induction HΓ; intros; inversion_clear Hx as [|? ? ? ? Hx']...
@@ -56,7 +56,7 @@ Qed.
 #[export]
 Hint Resolve var_in_wf : mcltt.
 
-Lemma presup_sb_ctx : forall {Γ Δ σ}, Γ ⊢s σ : Δ -> ⊢ Γ ∧ ⊢ Δ.
+Lemma presup_sb_ctx : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ ⊢ Γ }} ∧ {{ ⊢ Δ }}.
 Proof with mauto.
   intros * Hσ.
   induction Hσ...
@@ -70,7 +70,7 @@ Qed.
 #[export]
 Hint Resolve presup_sb_ctx : mcltt.
 
-Lemma presup_tm_ctx : forall {Γ t T}, Γ ⊢ t : T -> ⊢ Γ.
+Lemma presup_tm_ctx : forall {Γ t T}, {{ Γ ⊢ t : T }} -> {{ ⊢ Γ }}.
 Proof with mauto.
   intros * Ht.
   induction Ht...
@@ -81,7 +81,7 @@ Qed.
 Hint Resolve presup_tm_ctx : mcltt.
 
 (* Corresponds to ∈!⇒ty≈ in Agda proof *)
-Lemma var_in_eq : forall {Γ Δ T x}, ⊢ Γ ≈ Δ -> x : T ∈! Γ -> ∃ S i, x : S ∈! Δ ∧ Γ ⊢ T ≈ S : typ i ∧ Δ ⊢ T ≈ S : typ i.
+Lemma var_in_eq : forall {Γ Δ T x}, {{ ⊢ Γ ≈ Δ }} -> {{ #x : T ∈ Γ }} -> ∃ S i, {{ #x : S ∈ Δ }} ∧ {{ Γ ⊢ T ≈ S : Type@i }} ∧ {{ Δ ⊢ T ≈ S : Type@i }}.
 Proof with mauto.
   intros * HΓΔ Hx.
   gen Δ; induction Hx; intros; inversion_clear HΓΔ as [|? ? ? ? ? HΓΔ'].
@@ -91,7 +91,7 @@ Proof with mauto.
 Qed.
 
 (* Corresponds to ⊢≈-sym in Agda proof *)
-Lemma ctx_eq_sym : forall {Γ Δ}, ⊢ Γ ≈ Δ -> ⊢ Δ ≈ Γ.
+Lemma ctx_eq_sym : forall {Γ Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ ⊢ Δ ≈ Γ }}.
 Proof with mauto.
   intros.
   induction H...
@@ -100,7 +100,7 @@ Qed.
 #[export]
 Hint Resolve var_in_eq ctx_eq_sym : mcltt.
 
-Lemma presup_sb_eq_ctx : forall {Γ Δ σ σ'}, Γ ⊢s σ ≈ σ' : Δ -> ⊢ Γ.
+Lemma presup_sb_eq_ctx : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Γ }}.
 Proof with mauto.
   intros.
   induction H; mauto; now (eapply proj1; mauto).
@@ -109,12 +109,12 @@ Qed.
 #[export]
 Hint Resolve presup_sb_eq_ctx : mcltt.
 
-Lemma presup_tm_eq_ctx : forall {Γ t t' T}, Γ ⊢ t ≈ t' : T -> ⊢ Γ.
+Lemma presup_tm_eq_ctx : forall {Γ t t' T}, {{ Γ ⊢ t ≈ t' : T }} -> {{ ⊢ Γ }}.
 Proof with mauto.
   intros.
   induction H...
   Unshelve.
-  exact 0%nat.
+  constructor.
 Qed.
 
 #[export]

theories/CtxEquiv.v

@@ -4,31 +4,26 @@ Require Import Mcltt.System.
 Require Import Mcltt.CtxEqLemmas.
 Require Import Mcltt.LibTactics.
 
-Lemma ctxeq_tm : forall {Γ Δ t T}, ⊢ Γ ≈ Δ -> Γ ⊢ t : T -> Δ ⊢ t : T
+Lemma ctxeq_tm : forall {Γ Δ t T}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢ t : T }} -> {{ Δ ⊢ t : T }}
 with
-ctxeq_eq : forall {Γ Δ t t' T}, ⊢ Γ ≈ Δ -> Γ ⊢ t ≈ t' : T -> Δ ⊢ t ≈ t' : T
+ctxeq_eq : forall {Γ Δ t t' T}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢ t ≈ t' : T }} -> {{ Δ ⊢ t ≈ t' : T }}
 with
-ctxeq_s : forall {Γ Γ' Δ σ}, ⊢ Γ ≈ Δ -> Γ ⊢s σ : Γ' -> Δ ⊢s σ : Γ'
+ctxeq_s : forall {Γ Γ' Δ σ}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢s σ : Γ' }} -> {{ Δ ⊢s σ : Γ' }}
 with
-ctxeq_s_eq : forall {Γ Γ' Δ σ σ'}, ⊢ Γ ≈ Δ -> Γ ⊢s σ ≈ σ' : Γ' -> Δ ⊢s σ ≈ σ' : Γ'.
+ctxeq_s_eq : forall {Γ Γ' Δ σ σ'}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢s σ ≈ σ' : Γ' }} -> {{ Δ ⊢s σ ≈ σ' : Γ' }}.
 Proof with mauto.
   (*ctxeq_tm*)
   - clear ctxeq_tm.
     intros * HΓΔ Ht.
     gen Δ.
     induction Ht; intros; destruct (presup_ctx_eq HΓΔ)...
-    -- destruct (presup_ctx_eq HΓΔ) as [G D].
-       pose proof (IHHt1 _ HΓΔ).
-       assert (⊢ a :: Γ ≈ a :: Δ)...
-    -- destruct (presup_ctx_eq HΓΔ) as [G D].
-       pose proof (IHHt1 _ HΓΔ).
-       assert (⊢ A :: Γ ≈ A :: Δ)...
+    -- pose proof (IHHt1 _ HΓΔ).
+       assert ({{ ⊢ Γ , A ≈ Δ , A }})...
     -- destruct (var_in_eq HΓΔ H0) as [T' [i [xT'G [GTT' DTT']]]].
        eapply wf_conv...
-    -- destruct (presup_ctx_eq HΓΔ) as [G D].
-       assert (⊢ A :: Γ ≈ A :: Δ); mauto 6.
+    -- assert ({{ ⊢ Γ , A ≈ Δ , A }}); mauto 6.
     -- pose proof (IHHt1 _ HΓΔ).
-       assert (⊢ A :: Γ ≈ A :: Δ)...
+       assert ({{ ⊢ Γ , A ≈ Δ , A }})...
   (*ctxeq_eq*)
   - clear ctxeq_eq.
     intros * HΓΔ Htt'.
@@ -37,7 +32,7 @@ Proof with mauto.
     1-4,6-19: mauto.
     -- pose proof (IHHtt'1 _ HΓΔ).
        pose proof (ctxeq_tm _ _ _ _ HΓΔ H).
-       assert (⊢ M :: Γ ≈ M :: Δ)...
+       assert ({{ ⊢ Γ , M ≈ Δ , M }})...
     -- inversion_clear HΓΔ.
        pose proof (var_in_eq H3 H0) as [T'' [n [xT'' [GTT'' DTT'']]]].
        destruct (presup_ctx_eq H3).

theories/Presup.v

@@ -19,11 +19,11 @@ Ltac breakdown_goal :=
 
 Ltac gen_presup_ctx H :=
   match type of H with
-  | ⊢ ?Γ ≈ ?Δ =>
+  | {{ ⊢ ?Γ ≈ ?Δ }} =>
       let HΓ := fresh "HΓ" in
       let HΔ := fresh "HΔ" in
       pose proof presup_ctx_eq H as [HΓ HΔ]
-  | ?Γ ⊢s ?σ : ?Δ =>
+  | {{ ?Γ ⊢s ?σ : ?Δ }} =>
       let HΓ := fresh "HΓ" in
       let HΔ := fresh "HΔ" in
       pose proof presup_sb_ctx H as [HΓ HΔ]
@@ -32,18 +32,18 @@ Ltac gen_presup_ctx H :=
 
 Ltac gen_presup_IH presup_tm presup_eq presup_sb_eq H :=
   match type of H with
-  | (?Γ ⊢ ?t : ?T) =>
+  | {{ ?Γ ⊢ ?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 ?σ ≈ ?τ : ?Δ =>
+  | {{ ?Γ ⊢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Δ]]]
-  | ?Γ ⊢ ?s ≈ ?t : ?T =>
+  | {{ ?Γ ⊢ ?s ≈ ?t : ?T }} =>
       let HΓ := fresh "HΓ" in
       let i := fresh "i" in
       let Hs := fresh "Hs" in
@@ -53,32 +53,32 @@ Ltac gen_presup_IH presup_tm presup_eq presup_sb_eq H :=
   | _ => gen_presup_ctx H
   end.
 
-Lemma presup_tm : forall {Γ t T}, Γ ⊢ t : T -> ⊢ Γ ∧ ∃ i, Γ ⊢ T : typ i
-with presup_eq : forall {Γ s t T}, Γ ⊢ s ≈ t : T -> ⊢ Γ ∧ Γ ⊢ s : T ∧ Γ ⊢ t : T ∧ ∃ i,Γ ⊢ T : typ i
-with presup_sb_eq : forall {Γ Δ σ τ}, Γ ⊢s σ ≈ τ : Δ -> ⊢ Γ ∧ Γ ⊢s σ : Δ ∧ Γ ⊢s τ : Δ ∧ ⊢ Δ.
+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 τ : Δ }} ∧ {{ ⊢ Δ }}.
 Proof with mauto.
   - intros * Ht.
-    inversion_clear Ht; (on_all_hyp: gen_presup_IH presup_tm presup_eq presup_sb_eq); breakdown_goal.
+    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 sub_lvl...
+       eapply exp_sub_typ...
        econstructor...
     -- eexists.
        pose proof (lift_tm_max_left i0 H).
        pose proof (lift_tm_max_right i HTi).
        econstructor...
 
   - intros * Hst.
-    inversion_clear Hst; (on_all_hyp: gen_presup_IH presup_tm presup_eq presup_sb_eq); breakdown_goal.
+    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 sub_lvl...
+       eapply exp_sub_typ...
        econstructor...
        eapply wf_conv...
        eapply wf_eq_conv; mauto 6.
 
     -- econstructor...
        eapply wf_eq_conv...
 
-    -- eapply wf_sub...
+    -- eapply wf_exp_sub...
        econstructor...
        inversion H...
 
@@ -88,20 +88,20 @@ Proof with mauto.
        eapply wf_eq_trans.
        + eapply wf_eq_sym.
          eapply wf_eq_conv.
-         ++ eapply wf_eq_sub_comp...
+         ++ 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_sub_comp...
+         ++ 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); breakdown_goal.
+    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...
 
     -- econstructor...
@@ -116,8 +116,8 @@ Proof with mauto.
        eapply wf_conv...
        eapply wf_eq_conv...
 
-  Unshelve.
-  all: exact 0.
+    Unshelve.
+    all: constructor.
 Qed.
 
 #[export]

theories/PresupLemmas.v

@@ -8,7 +8,7 @@ Require Import Setoid.
 
 (*Type lifting lemmas*)
 
-Lemma lift_tm_ge : forall {Γ T n m}, n <= m -> Γ ⊢ T : typ n -> Γ ⊢ T : typ m.
+Lemma lift_tm_ge : forall {Γ T n m}, n <= m -> {{ Γ ⊢ T : Type@n }} -> {{ Γ ⊢ T : Type@m }}.
 Proof with mauto.
   intros * Hnm HT.
   induction m; inversion Hnm; subst...
@@ -17,19 +17,19 @@ Qed.
 #[export]
 Hint Resolve lift_tm_ge : mcltt.
 
-Lemma lift_tm_max_left : forall {Γ T n} m, Γ ⊢ T : typ n -> Γ ⊢ T : typ (max n m).
+Lemma lift_tm_max_left : forall {Γ T n} m, {{ Γ ⊢ T : Type@n }} -> {{ Γ ⊢ T : 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 : typ m -> Γ ⊢ T : typ (max n m).
+Lemma lift_tm_max_right : forall {Γ T} n {m}, {{ Γ ⊢ T : Type@m }} -> {{ Γ ⊢ T : 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': typ n -> Γ ⊢ T ≈ T' : typ m.
+Lemma lift_eq_ge : forall {Γ T T' n m}, n <= m -> {{ Γ ⊢ T ≈ T': Type@n }} -> {{ Γ ⊢ T ≈ T' : Type@m }}.
 Proof with mauto.
   intros * Hnm HTT'.
   induction m; inversion Hnm; subst...
@@ -38,13 +38,13 @@ Qed.
 #[export]
 Hint Resolve lift_eq_ge : mcltt.
 
-Lemma lift_eq_max_left : forall {Γ T T' n} m, Γ ⊢ T ≈ T' : typ n -> Γ ⊢ T ≈ T' : typ (max n m).
+Lemma lift_eq_max_left : forall {Γ T T' n} m, {{ Γ ⊢ T ≈ T' : Type@n }} -> {{ Γ ⊢ T ≈ T' : 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' : typ m -> Γ ⊢ T ≈ T' : typ (max n m).
+Lemma lift_eq_max_right : forall {Γ T T'} n {m}, {{ Γ ⊢ T ≈ T' : Type@m }} -> {{ Γ ⊢ T ≈ T' : Type@(max n m) }}.
 Proof with mauto.
   intros.
   assert (m <= max n m) by lia...

theories/Relations.v

@@ -8,7 +8,7 @@ Require Import Mcltt.PresupLemmas.
 Require Import Setoid.
 Require Import Coq.Program.Equality.
 
-Lemma ctx_eq_refl : forall {Γ}, ⊢ Γ -> ⊢ Γ ≈ Γ.
+Lemma ctx_eq_refl : forall {Γ}, {{ ⊢ Γ }} -> {{ ⊢ Γ ≈ Γ }}.
 Proof with mauto.
   intros * HΓ.
   induction HΓ...
@@ -17,7 +17,7 @@ Qed.
 #[export]
 Hint Resolve ctx_eq_refl : mcltt.
 
-Lemma ctx_eq_trans : forall {Γ0 Γ1 Γ2}, ⊢ Γ0 ≈ Γ1 -> ⊢ Γ1 ≈ Γ2 -> ⊢ Γ0 ≈ Γ2.
+Lemma ctx_eq_trans : forall {Γ0 Γ1 Γ2}, {{ ⊢ Γ0 ≈ Γ1 }} -> {{ ⊢ Γ1 ≈ Γ2 }} -> {{ ⊢ Γ0 ≈ Γ2 }}.
 Proof with mauto.
   intros * HΓ01 HΓ12.
   gen Γ2.
@@ -31,17 +31,17 @@ Proof with mauto.
   econstructor...
 Qed.
 
-Add Relation (Ctx) (wf_ctx_eq)
+Add Relation (ctx) (wf_ctx_eq)
     symmetry proved by @ctx_eq_sym
     transitivity proved by @ctx_eq_trans
     as ctx_eq.
 
-Add Parametric Relation (Γ : Ctx) (T : Typ) : (exp) (λ t t', Γ ⊢ t ≈ t' : T)
+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.                                                
 
-Add Parametric Relation (Γ Δ : Ctx) : (Sb) (λ σ τ, Γ ⊢s σ ≈ τ : Δ)
+Add Parametric Relation (Γ Δ : ctx) : (sub) (λ σ τ, {{ Γ ⊢s σ ≈ τ : Δ }})
     symmetry proved by (λ σ τ, wf_sub_eq_sym Γ σ τ Δ)
     transitivity proved by (λ σ τ ρ, wf_sub_eq_trans Γ σ τ Δ ρ)
     as sb_eq.