add lemmas for weakenings (#92)

* add lemmas for weakenings

* update

theories/Core/Completeness/FundamentalTheorem.v

@@ -15,9 +15,9 @@ Section completeness_fundamental.
   Let ctx_prop Γ (_ : {{ ⊢ Γ }}) : Prop := {{ ⊨ Γ }}.
   Let ctx_eq_prop Γ Γ' (_ : {{ ⊢ Γ ≈ Γ' }}) : Prop := {{ ⊨ Γ ≈ Γ' }}.
   Let exp_prop Γ M A (_ : {{ Γ ⊢ M : A }}) : Prop := {{ Γ ⊨ M : A }}.
-  Let exp_eq_prop Γ M M' A (_ : {{ Γ ⊢ M ≈ M' : A }}) : Prop := {{ Γ ⊨ M ≈ M' : A }}.
+  Let exp_eq_prop Γ A M M' (_ : {{ Γ ⊢ M ≈ M' : A }}) : Prop := {{ Γ ⊨ M ≈ M' : A }}.
   Let sub_prop Γ σ Δ (_ : {{ Γ ⊢s σ : Δ }}) : Prop := {{ Γ ⊨s σ : Δ }}.
-  Let sub_eq_prop Γ σ σ' Δ (_ : {{ Γ ⊢s σ ≈ σ' : Δ }}) : Prop := {{ Γ ⊨s σ ≈ σ' : Δ }}.
+  Let sub_eq_prop Γ Δ σ σ' (_ : {{ Γ ⊢s σ ≈ σ' : Δ }}) : Prop := {{ Γ ⊨s σ ≈ σ' : Δ }}.
 
   #[local]
   Ltac unfold_prop :=
@@ -61,7 +61,7 @@ Section completeness_fundamental.
       (P4 := sub_eq_prop)...
   Qed.
 
-  Theorem completeness_fundamental_exp_eq : forall Γ M M' A (HMM' : {{ Γ ⊢ M ≈ M' : A }}), exp_eq_prop Γ M M' A HMM'.
+  Theorem completeness_fundamental_exp_eq : forall Γ M M' A (HMM' : {{ Γ ⊢ M ≈ M' : A }}), exp_eq_prop Γ A M M' HMM'.
   Proof with solve_completeness_fundamental using.
     induction 1 using wf_exp_eq_mut_ind
       with
@@ -83,7 +83,7 @@ Section completeness_fundamental.
       (P4 := sub_eq_prop)...
   Qed.
 
-  Theorem completeness_fundamental_sub_eq : forall Γ σ σ' Δ (Hσσ' : {{ Γ ⊢s σ ≈ σ' : Δ }}), sub_eq_prop Γ σ σ' Δ Hσσ'.
+  Theorem completeness_fundamental_sub_eq : forall Γ σ σ' Δ (Hσσ' : {{ Γ ⊢s σ ≈ σ' : Δ }}), sub_eq_prop Γ Δ σ σ' Hσσ'.
   Proof with solve_completeness_fundamental using.
     induction 1 using wf_sub_eq_mut_ind
       with

theories/Core/Soundness/Weakening/Lemmas.v

@@ -0,0 +1,100 @@
+Require Import Coq.Program.Equality.
+
+From Mcltt Require Import Base System.Definitions System.Lemmas Weakening.Definition Presup CtxEq LibTactics.
+Import Syntax_Notations.
+
+
+Lemma weakening_escape : forall Γ σ Δ,
+    {{ Γ ⊢w σ : Δ }} ->
+    {{ Γ ⊢s σ : Δ }}.
+Proof.
+  induction 1;
+    match goal with
+    | H : _ |- _ =>
+        solve [gen_presup H; trivial]
+    end.
+Qed.
+
+#[export]
+  Hint Resolve weakening_escape : mcltt.
+
+
+Lemma weakening_resp_equiv : forall Γ σ σ' Δ,
+    {{ Γ ⊢w σ : Δ }} ->
+    {{ Γ ⊢s σ ≈ σ' : Δ }} ->
+    {{ Γ ⊢w σ' : Δ }}.
+Proof.
+  induction 1; mauto.
+Qed.
+
+
+Lemma ctxeq_weakening : forall Γ σ Δ,
+    {{ Γ ⊢w σ : Δ }} ->
+    forall Γ',
+      {{ ⊢ Γ ≈ Γ' }} ->
+      {{ Γ' ⊢w σ : Δ }}.
+Proof.
+  induction 1; mauto.
+Qed.
+
+
+Lemma weakening_conv : forall Γ σ Δ,
+    {{ Γ ⊢w σ : Δ }} ->
+    forall Δ',
+      {{ ⊢ Δ ≈ Δ' }} ->
+      {{ Γ ⊢w σ : Δ' }}.
+Proof.
+  induction 1; intros; mauto.
+  eapply wk_p.
+  - eapply IHweakening.
+    apply weakening_escape in H.
+    gen_presup H.
+    progressive_invert HΔ.
+    econstructor; [ | | eapply ctxeq_exp | ..]; mauto.
+  - mauto.
+Qed.
+
+#[export]
+ Hint Resolve weakening_conv : mcltt.
+
+Lemma invert_id : forall Γ Δ,
+    {{ Γ ⊢s Id : Δ }} ->
+    {{ ⊢ Γ ≈ Δ }}.
+Proof.
+  intros. dependent induction H; intros; try congruence; mauto.
+Qed.
+
+
+Lemma weakening_compose : forall Γ' σ' Γ'',
+    {{ Γ' ⊢w σ' : Γ'' }} ->
+    forall Γ σ,
+      {{ Γ ⊢w σ : Γ' }} ->
+      {{ Γ ⊢w σ' ∘ σ : Γ'' }}.
+Proof.
+  induction 1; intros.
+  - gen_presup H.
+    apply invert_id in Hτ.
+    eapply weakening_resp_equiv; [ mauto | ].
+    transitivity {{{ Id ∘ σ0 }}}; mauto.
+  - eapply wk_p; [eauto |].
+    apply weakening_escape in H.
+    transitivity {{{ Wk ∘ τ ∘ σ0 }}}; mauto.
+Qed.
+
+
+Lemma weakening_id : forall Γ,
+    {{ ⊢ Γ }} ->
+    {{ Γ ⊢w Id : Γ }}.
+Proof.
+  mauto.
+Qed.
+
+Lemma weakening_wk : forall Γ T,
+    {{ ⊢ Γ , T }} ->
+    {{ Γ , T ⊢w Wk : Γ }}.
+Proof.
+  intros. eapply wk_p; mauto.
+Qed.
+
+#[export]
+ Hint Resolve weakening_id weakening_wk : mcltt.

theories/Core/Syntactic/Presup.v

@@ -199,4 +199,4 @@ Qed.
 #[export]
 Hint Resolve presup_exp presup_exp_eq presup_sub_eq : mcltt.
 
-Ltac gen_presup H := gen_presup_IH presup_exp presup_exp_eq presup_sub_eq H; gen_presup_ctx H.
+Ltac gen_presup H := gen_presup_IH @presup_exp @presup_exp_eq @presup_sub_eq H.

theories/Core/Syntactic/System/Definitions.v

@@ -1,4 +1,4 @@
-From Coq Require Import List.
+From Coq Require Import List Classes.RelationClasses.
 From Mcltt Require Import Base LibTactics.
 From Mcltt Require Export Syntax.
 Import Syntax_Notations.
@@ -105,7 +105,7 @@ with wf_sub : ctx -> sub -> ctx -> Prop :=
      {{ ⊢ Δ ≈ Δ' }} ->
      {{ Γ ⊢s σ : Δ' }} )
 where "Γ ⊢s σ : Δ" := (wf_sub Γ σ Δ) (in custom judg) : type_scope
-with wf_exp_eq : ctx -> exp -> exp -> typ -> Prop :=
+with wf_exp_eq : ctx -> typ -> exp -> exp -> Prop :=
 | wf_exp_eq_typ_sub :
   `( {{ Γ ⊢s σ : Δ }} ->
      {{ Γ ⊢ Type@i[σ] ≈ Type@i : Type@(S i) }} )
@@ -236,8 +236,9 @@ with wf_exp_eq : ctx -> exp -> exp -> typ -> Prop :=
   `( {{ Γ ⊢ M ≈ M' : A }} ->
      {{ Γ ⊢ M' ≈ M'' : A }} ->
      {{ Γ ⊢ M ≈ M'' : A }} )
-where "Γ ⊢ M ≈ M' : A" := (wf_exp_eq Γ M M' A) (in custom judg) : type_scope
-with wf_sub_eq : ctx -> sub -> sub -> ctx -> Prop :=
+where "Γ ⊢ M ≈ M' : A" := (wf_exp_eq Γ A M M') (in custom judg) : type_scope
+
+with wf_sub_eq : ctx -> ctx -> sub -> sub -> Prop :=
 | wf_sub_eq_id :
   `( {{ ⊢ Γ }} ->
      {{ Γ ⊢s Id ≈ Id : Γ }} )
@@ -289,7 +290,7 @@ with wf_sub_eq : ctx -> sub -> sub -> ctx -> Prop :=
   `( {{ Γ ⊢s σ ≈ σ' : Δ }} ->
      {{ ⊢ Δ ≈ Δ' }} ->
      {{ Γ ⊢s σ ≈ σ' : Δ' }} )
-where "Γ ⊢s S1 ≈ S2 : Δ" := (wf_sub_eq Γ S1 S2 Δ) (in custom judg) : type_scope.
+where "Γ ⊢s S1 ≈ S2 : Δ" := (wf_sub_eq Γ Δ S1 S2) (in custom judg) : type_scope.
 
 Scheme wf_ctx_mut_ind := Induction for wf_ctx Sort Prop
 with wf_ctx_eq_mut_ind := Induction for wf_ctx_eq Sort Prop
@@ -300,3 +301,19 @@ with wf_sub_eq_mut_ind := Induction for wf_sub_eq Sort Prop.
 
 #[export]
 Hint Constructors wf_ctx wf_ctx_eq wf_exp wf_sub wf_exp_eq wf_sub_eq ctx_lookup: mcltt.
+
+#[export]
+  Instance WfExpPER Γ A : PER (wf_exp_eq Γ A).
+Proof.
+  split.
+  - eauto using wf_exp_eq_sym.
+  - eauto using wf_exp_eq_trans.
+Qed.
+
+#[export]
+  Instance WfSubPER Γ Δ : PER (wf_sub_eq Γ Δ).
+Proof.
+  split.
+  - eauto using wf_sub_eq_sym.
+  - eauto using wf_sub_eq_trans.
+Qed.

theories/_CoqProject

@@ -41,6 +41,7 @@
 ./Core/Soundness/LogicalRelation.v
 ./Core/Soundness/Weakening.v
 ./Core/Soundness/Weakening/Definition.v
+./Core/Soundness/Weakening/Lemmas.v
 ./Frontend/Elaborator.v
 ./Frontend/Parser.v
 ./Frontend/ParserExtraction.v