Refactoring and optimizing proofs (#98)

* Some refactoring

* Bit more refactoring

* Optimize proofs

* Update minor

* Update Lemmas.v a bit

theories/Core/Semantic/PER/Lemmas.v

@@ -4,13 +4,6 @@ From Mcltt Require Import Base LibTactics.
 From Mcltt.Core Require Import Evaluation PER.Definitions PER.CoreTactics Readback.
 Import Domain_Notations.
 
-Add Parametric Morphism A : (@all A)
-    with signature forall_relation (fun (x : A) => iff) ==> iff as all_iff_moprhism'.
-Proof.
-  unfold forall_relation.
-  split; intros ** ?; intuition.
-Qed.
-
 Add Parametric Morphism A : PER
     with signature (@relation_equivalence A) ==> iff as PER_morphism.
 Proof.

theories/Core/Soundness/LogicalRelation/Definitions.v

@@ -12,7 +12,9 @@ Global Open Scope predicate_scope.
 Generalizable All Variables.
 
 Notation "'typ_pred'" := (predicate (Tcons ctx (Tcons typ Tnil))).
+Notation "'typ_pred_equivalence'" := (@predicate_equivalence (Tcons ctx (Tcons typ Tnil))).
 Notation "'glu_pred'" := (predicate (Tcons ctx (Tcons exp (Tcons typ (Tcons domain Tnil))))).
+Notation "'glu_pred_equivalence'" := (@predicate_equivalence (Tcons ctx (Tcons exp (Tcons typ (Tcons domain Tnil))))).
 
 Definition univ_typ_pred j i : typ_pred := fun Γ T => {{ Γ ⊢ T ≈ Type@j :  Type@i }}.
 Arguments univ_typ_pred j i Γ T/.

theories/Core/Soundness/LogicalRelation/Lemmas.v

@@ -1,43 +1,18 @@
+From Coq Require Import Morphisms Morphisms_Relations.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import System.Definitions Presup CtxEq Evaluation Readback PER.
+From Mcltt.Core Require Import Evaluation PER Presup Readback Syntactic.Corollaries.
 
 From Mcltt.Core.Soundness Require Import LogicalRelation.Definitions.
 From Mcltt.Core.Soundness Require Export Weakening.Lemmas.
 Import Domain_Notations.
 
-
 Lemma glu_nat_per_nat : forall Γ m a,
     glu_nat Γ m a ->
     per_nat a a.
 Proof.
   induction 1; mauto.
 Qed.
 
-Lemma sub_id_typ : forall Γ M A,
-    {{ Γ ⊢ M : A }} ->
-    {{ Γ ⊢ M : A [ Id ] }}.
-Proof.
-  intros. gen_presups. mauto 6.
-Qed.
-
-#[export]
- Hint Resolve invert_id sub_id_typ : mcltt.
-
-Lemma invert_sub_id : forall Γ M A,
-    {{ Γ ⊢ M [ Id ] : A }} ->
-    {{ Γ ⊢ M : A }}.
-Proof.
-  intros. remember {{{ M [ Id ]}}} as M'.
-  gen M.
-  induction H; intros; try congruence;
-    gen_presups;
-    progressive_inversion;
-    mauto.
-Qed.
-
-#[export]
- Hint Resolve invert_sub_id : mcltt.
-
 Lemma glu_nat_escape : forall Γ m a,
     glu_nat Γ m a ->
     {{ ⊢ Γ }} ->
@@ -49,14 +24,14 @@ Proof.
     end.
   assert {{ Γ ⊢w Id : Γ }} by mauto.
   specialize (H (length Γ)).
-  destruct_all.
+  destruct_conjs.
   specialize (H0 _ _ _ H2 H3).
   gen_presups.
   mauto.
 Qed.
 
 #[export]
- Hint Resolve glu_nat_escape : mcltt.
+Hint Resolve glu_nat_escape : mcltt.
 
 Lemma glu_nat_resp_equiv : forall Γ m a,
     glu_nat Γ m a ->
@@ -67,21 +42,19 @@ Proof.
   induction 1; intros; mauto.
   econstructor; trivial.
   intros.
-  specialize (H0 _ _ _ H2 H3).
-  mauto.
+  transitivity {{{ m[σ] }}}; mauto.
 Qed.
 
-
 Lemma glu_nat_per_top : forall Γ m a,
     glu_nat Γ m a ->
     per_top d{{{ ⇓ ℕ a }}} d{{{ ⇓ ℕ a }}}.
 Proof.
-  induction 1; unfold per_top in *; intros; mauto.
+  induction 1; intros s; mauto.
   - specialize (IHglu_nat s).
-    destruct_all.
+    destruct_conjs.
     mauto.
   - specialize (H s).
-    destruct_all.
+    destruct_conjs.
     mauto.
 Qed.
 
@@ -95,21 +68,24 @@ Proof.
   induction 1; intros; progressive_inversion; gen_presups.
   - transitivity {{{ zero [ σ ] }}}; mauto.
   - specialize (IHglu_nat _ _ _ H1 H5).
-    transitivity {{{ (succ m') [ σ ]}}}; [mauto |].
-    transitivity {{{ succ m' [ σ ] }}}; mauto 6.
+    transitivity {{{ (succ m') [ σ ]}}}; mauto.
+    transitivity {{{ succ m' [ σ ] }}}; mauto.
   - mauto.
 Qed.
 
-
 Lemma glu_univ_elem_univ_lvl : forall i P El A B,
     glu_univ_elem i P El A B ->
     forall Γ T,
       P Γ T ->
       {{ Γ ⊢ T : Type@i }}.
 Proof with (simpl in *; destruct_all; gen_presups; trivial).
+  pose proof iff_impl_subrelation.
+  assert (Proper (typ_pred_equivalence ==> pointwise_relation ctx (pointwise_relation typ iff)) id)
+    by apply predicate_equivalence_pointwise.
   induction 1 using glu_univ_elem_ind; intros.
-  - apply H1 in H3...
-  - apply H in H1...
-  - apply H4 in H6. progressive_invert H6...
-  - apply H0 in H2...
+  (* Use [apply_relation_equivalence]-like tactic later *)
+  - rewrite H3 in H5...
+  - rewrite H1 in H3...
+  - rewrite H6 in H8. dir_inversion_by_head pi_typ_pred...
+  - rewrite H2 in H4...
 Qed.

theories/Core/Soundness/Weakening/Lemmas.v

@@ -1,9 +1,9 @@
-Require Import Coq.Program.Equality.
+From Coq Require Import Program.Equality.
 
-From Mcltt Require Import Base System.Definitions System.Lemmas Weakening.Definition Presup CtxEq LibTactics.
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core Require Import CtxEq Presup Syntactic.Corollaries System Weakening.Definition.
 Import Syntax_Notations.
 
-
 Lemma weakening_escape : forall Γ σ Δ,
     {{ Γ ⊢w σ : Δ }} ->
     {{ Γ ⊢s σ : Δ }}.
@@ -16,8 +16,7 @@ Proof.
 Qed.
 
 #[export]
-  Hint Resolve weakening_escape : mcltt.
-
+Hint Resolve weakening_escape : mcltt.
 
 Lemma weakening_resp_equiv : forall Γ σ σ' Δ,
     {{ Γ ⊢w σ : Δ }} ->
@@ -27,7 +26,6 @@ Proof.
   induction 1; mauto.
 Qed.
 
-
 Lemma ctxeq_weakening : forall Γ σ Δ,
     {{ Γ ⊢w σ : Δ }} ->
     forall Γ',
@@ -37,7 +35,6 @@ Proof.
   induction 1; mauto.
 Qed.
 
-
 Lemma weakening_conv : forall Γ σ Δ,
     {{ Γ ⊢w σ : Δ }} ->
     forall Δ',
@@ -55,33 +52,24 @@ Proof.
 Qed.
 
 #[export]
- Hint Resolve weakening_conv : mcltt.
-
-Lemma invert_id : forall Γ Δ,
-    {{ Γ ⊢s Id : Δ }} ->
-    {{ ⊢ Γ ≈ Δ }}.
-Proof.
-  intros. dependent induction H; intros; try congruence; mauto.
-Qed.
-
+Hint Resolve weakening_conv : mcltt.
 
 Lemma weakening_compose : forall Γ' σ' Γ'',
     {{ Γ' ⊢w σ' : Γ'' }} ->
     forall Γ σ,
       {{ Γ ⊢w σ : Γ' }} ->
       {{ Γ ⊢w σ' ∘ σ : Γ'' }}.
-Proof.
+Proof with mautosolve.
   induction 1; intros.
   - gen_presup H.
-    apply invert_id in Hτ.
-    eapply weakening_resp_equiv; [ mauto | ].
-    transitivity {{{ Id ∘ σ0 }}}; mauto.
+    assert {{ ⊢ Γ ≈ Δ }} by mauto.
+    eapply weakening_resp_equiv; [mauto 2 |].
+    transitivity {{{ Id ∘ σ0 }}}...
   - eapply wk_p; [eauto |].
-    apply weakening_escape in H.
-    transitivity {{{ Wk ∘ τ ∘ σ0 }}}; mauto.
+    transitivity {{{ Wk ∘ τ ∘ σ0 }}}; mauto 4.
+    eapply wf_sub_eq_compose_assoc; revgoals...
 Qed.
 
-
 Lemma weakening_id : forall Γ,
     {{ ⊢ Γ }} ->
     {{ Γ ⊢w Id : Γ }}.
@@ -93,8 +81,9 @@ Lemma weakening_wk : forall Γ T,
     {{ ⊢ Γ , T }} ->
     {{ Γ , T ⊢w Wk : Γ }}.
 Proof.
-  intros. eapply wk_p; mauto.
+  intros.
+  econstructor; mautosolve.
 Qed.
 
 #[export]
- Hint Resolve weakening_id weakening_wk : mcltt.
+Hint Resolve weakening_id weakening_wk : mcltt.

theories/Core/Syntactic/Corollaries.v

@@ -0,0 +1,37 @@
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core Require Import CtxEq Presup.
+Import Syntax_Notations.
+
+Corollary invert_id : forall Γ Δ,
+    {{ Γ ⊢s Id : Δ }} ->
+    {{ ⊢ Γ ≈ Δ }}.
+Proof.
+  intros * H.
+  dependent induction H; mauto.
+Qed.
+
+#[export]
+Hint Resolve invert_id : mcltt.
+
+Corollary sub_id_typ : forall Γ M A,
+    {{ Γ ⊢ M : A }} ->
+    {{ Γ ⊢ M : A [ Id ] }}.
+Proof.
+  intros.
+  gen_presups.
+  mauto 6.
+Qed.
+
+#[export]
+Hint Resolve sub_id_typ : mcltt.
+
+Corollary invert_sub_id : forall Γ M A,
+    {{ Γ ⊢ M [ Id ] : A }} ->
+    {{ Γ ⊢ M : A }}.
+Proof.
+  intros * H.
+  dependent induction H; mauto.
+Qed.
+
+#[export]
+Hint Resolve invert_sub_id : mcltt.

theories/Core/Syntactic/CtxEq.v

@@ -40,24 +40,26 @@ Module ctxeq_judg.
     all: inversion_clear 1;
       (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 * HΓΔ; destruct (presup_ctx_eq HΓΔ); mauto;
+      intros * HΓΔ; destruct (presup_ctx_eq HΓΔ); mauto 4;
       try (rename B into C); try (rename B' into C'); try (rename A0 into B); try (rename A' into B').
     (* ctxeq_exp_helper & ctxeq_exp_eq_helper recursion cases *)
     1,6-8: assert {{ ⊢ Γ, ℕ ≈ Δ, ℕ }} by (econstructor; mautosolve);
       assert {{ Δ, ℕ ⊢ B : Type@i }} by eauto; econstructor...
     (* ctxeq_exp_helper & ctxeq_exp_eq_helper function cases *)
     1-3,5-9: assert {{ Δ ⊢ B : Type@i }} by eauto; assert {{ ⊢ Γ, B ≈ Δ, B }} by mauto;
-      try econstructor; mautosolve.
+      try econstructor...
     (* ctxeq_exp_helper & ctxeq_exp_eq_helper variable cases *)
-    1-2: assert (exists B i, {{ #x : B ∈ Δ }} /\ {{ Γ ⊢ A ≈ B : Type@i }} /\ {{ Δ ⊢ A ≈ B : Type@i }}); destruct_conjs...
+    1-2: assert (exists B i, {{ #x : B ∈ Δ }} /\ {{ Γ ⊢ A ≈ B : Type@i }} /\ {{ Δ ⊢ A ≈ B : Type@i }}); destruct_conjs; mautosolve 4.
     (* ctxeq_sub_helper & ctxeq_sub_eq_helper weakening cases *)
-    2-3: inversion_clear HΓΔ; econstructor...
+    2-3: inversion_clear HΓΔ; econstructor; mautosolve 4.
 
     (* ctxeq_exp_eq_helper variable case *)
     inversion_clear HΓΔ as [|? Δ0 ? ? C'].
     assert (exists D i', {{ #x : D ∈ Δ0 }} /\ {{ Γ0 ⊢ B ≈ D : Type@i' }} /\ {{ Δ0 ⊢ B ≈ D : Type@i' }}) as [D [i0 ?]] by mauto.
     destruct_conjs.
-    assert {{ Δ0, C' ⊢ B[Wk] ≈ D[Wk] : Type @ i0 }}...
+    assert {{ ⊢ Δ0, C' }} by mauto.
+    assert {{ Δ0 ⊢ D ≈ B : Type@i0 }} by mauto.
+    assert {{ Δ0, C' ⊢ D[Wk] ≈ B[Wk] : Type@i0 }}...
   Qed.
 
   Corollary ctxeq_exp : forall {Γ Δ M A}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢ M : A }} -> {{ Δ ⊢ M : A }}.
@@ -98,6 +100,8 @@ Proof with mautosolve.
   assert {{ Γ2 ⊢ T2 : Type@i }} by mauto using lift_exp_max_right.
   assert {{ Γ0 ⊢ T0 ≈ T1 : Type@i }} by mauto using lift_exp_eq_max_left.
   assert {{ Γ2 ⊢ T1 ≈ T2 : Type@i }} by mauto using lift_exp_eq_max_right.
+  assert {{ ⊢ Γ0 ≈ Γ2 }} by mauto.
+  assert {{ Γ0 ⊢ T0 ≈ T2 : Type@i }} by mauto.
   econstructor...
 Qed.