need a few lemmas to push through this proof (#99)

* need a few lemmas to push through this proof

* fix issues

* more lemmas

* add more gluing lemmas

* TODO: write a workhorse tactic that simplifies substitutions

* make use of autorewrite

* add a bunch of hints for rewrite

* fix export issue

* add a few more morphisms

* fix mistakes

* rewrites are very annoying. tactics are needed to get rid of some proofs

* exploit autorewrites

* address comments

theories/Core/Semantic/PER/CoreTactics.v

@@ -18,20 +18,26 @@ Ltac destruct_rel_mod_eval :=
     match goal with
     | H : (forall c c' (equiv_c_c' : {{ Dom c ≈ c' ∈ ?in_rel }}), rel_mod_eval _ _ _ _ _ _) |- _ =>
         destruct_rel_by_assumption in_rel H; mark H
+    | H : rel_mod_eval _ _ _ _ _ _ |- _ =>
+        dependent destruction H
     end;
   unmark_all.
 Ltac destruct_rel_mod_app :=
   repeat
     match goal with
     | H : (forall c c' (equiv_c_c' : {{ Dom c ≈ c' ∈ ?in_rel }}), rel_mod_app _ _ _ _ _) |- _ =>
         destruct_rel_by_assumption in_rel H; mark H
+    | H : rel_mod_app _ _ _ _ _ |- _ =>
+        dependent destruction H
     end;
   unmark_all.
 Ltac destruct_rel_typ :=
   repeat
     match goal with
     | H : (forall c c' (equiv_c_c' : {{ Dom c ≈ c' ∈ ?in_rel }}), rel_typ _ _ _ _ _ _) |- _ =>
         destruct_rel_by_assumption in_rel H; mark H
+    | H : rel_typ _ _ _ _ _ _ |- _ =>
+        dependent destruction H
     end;
   unmark_all.
 

theories/Core/Soundness/LogicalRelation.v

@@ -1 +1 @@
-From Mcltt.Core.Soundness Require Export LogicalRelation.Definitions.
+From Mcltt.Core.Soundness Require Export LogicalRelation.Definitions LogicalRelation.Lemmas.

theories/Core/Soundness/LogicalRelation/Definitions.v

@@ -84,6 +84,8 @@ Inductive pi_glu_pred i
                    exists ab, {{ $| a & b |↘ ab }} /\ OEl _ _ Ha Δ {{{ m [ σ ] m' }}} {{{ OT [ σ ,, m' ] }}} ab) ->
     pi_glu_pred i IR IP IEl elem_rel OEl Γ m M a.
 
+#[export]
+ Hint Constructors neut_glu_pred pi_typ_pred pi_glu_pred : mcltt.
 
 Lemma pi_glu_pred_pi_typ_pred : forall i IR IP IEl (OP : forall c c' (equiv_c_c' : {{ Dom c ≈ c' ∈ IR }}),  typ_pred) elem_rel OEl Γ m M a,
     pi_glu_pred i IR IP IEl elem_rel OEl Γ m M a ->
@@ -162,12 +164,14 @@ Equations glu_univ_elem (i : nat) : typ_pred -> glu_pred -> domain -> domain ->
 
 Definition glu_univ (i : nat) (A : domain) : typ_pred :=
   fun Γ M => exists P El, glu_univ_elem i P El A A /\ P Γ M.
+Arguments glu_univ i A Γ M/.
 
 Definition univ_glu_pred j i : glu_pred :=
     fun Γ m M A =>
       {{ Γ ⊢ m : M }} /\ {{ Γ ⊢ M ≈ Type@j : Type@i }} /\
         per_univ j A A /\
         glu_univ j A Γ m.
+Arguments univ_glu_pred j i Γ t T a/.
 
 Section GluingInduction.
 
@@ -272,3 +276,16 @@ Inductive glu_typ i Γ M A B : Prop :=
     per_top_typ A B ->
     (forall Δ σ a, {{ Δ ⊢w σ : Γ }} -> {{ Rtyp A in length Δ ↘ a }} -> {{ Δ ⊢ M [ σ ] ≈  a : Type@i }}) ->
     glu_typ i Γ M A B.
+
+
+Ltac invert_glu_rel1 :=
+  match goal with
+  | H : pi_typ_pred _ _ _ _ _ _ _ |- _ =>
+      progressive_invert H
+  | H : pi_glu_pred _ _ _ _ _ _ _ _ _ _ |- _ =>
+      progressive_invert H
+  | H : neut_typ_pred _ _ _ _ |- _ =>
+      progressive_invert H
+  | H : neut_glu_pred _ _ _ _ _ _ |- _ =>
+      progressive_invert H
+  end.

theories/Core/Soundness/LogicalRelation/Lemmas.v

@@ -1,6 +1,6 @@
 From Coq Require Import Morphisms Morphisms_Relations.
 From Mcltt Require Import Base LibTactics.
-From Mcltt.Core Require Import Evaluation PER Presup Readback Syntactic.Corollaries.
+From Mcltt.Core Require Import Evaluation PER Presup CtxEq Readback Syntactic.Corollaries System.Lemmas.
 
 From Mcltt.Core.Soundness Require Import LogicalRelation.Definitions.
 From Mcltt.Core.Soundness Require Export Weakening.Lemmas.
@@ -13,6 +13,9 @@ Proof.
   induction 1; mauto.
 Qed.
 
+#[local]
+ Hint Resolve glu_nat_per_nat : mcltt.
+
 Lemma glu_nat_escape : forall Γ m a,
     glu_nat Γ m a ->
     {{ ⊢ Γ }} ->
@@ -45,18 +48,8 @@ Proof.
   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; intros s; mauto.
-  - specialize (IHglu_nat s).
-    destruct_conjs.
-    mauto.
-  - specialize (H s).
-    destruct_conjs.
-    mauto.
-Qed.
+#[local]
+ Hint Resolve glu_nat_resp_equiv : mcltt.
 
 Lemma glu_nat_readback : forall Γ m a,
     glu_nat Γ m a ->
@@ -73,19 +66,208 @@ Proof.
   - mauto.
 Qed.
 
+#[global]
+  Ltac simpl_glu_rel :=
+  apply_equiv_left;
+  repeat invert_glu_rel1;
+  apply_equiv_left;
+  destruct_all;
+  gen_presups.
+
+
 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.
-  (* 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...
+Proof.
+  induction 1 using glu_univ_elem_ind; intros;
+    simpl_glu_rel; trivial.
+Qed.
+
+
+Lemma glu_univ_elem_typ_resp_equiv : forall i P El A B,
+    glu_univ_elem i P El A B ->
+    forall Γ T T',
+      P Γ T ->
+      {{ Γ ⊢ T ≈ T' : Type@i }} ->
+      P Γ T'.
+Proof.
+  induction 1 using glu_univ_elem_ind; intros;
+    simpl_glu_rel; mauto.
+
+  split; [trivial |].
+  intros.
+  specialize (H4 _ _ _ H2 H5); mauto.
+Qed.
+
+
+Lemma glu_univ_elem_trm_resp_typ_equiv : forall i P El A B,
+    glu_univ_elem i P El A B ->
+    forall Γ t T a T',
+      El Γ t T a ->
+      {{ Γ ⊢ T ≈ T' : Type@i }} ->
+      El Γ t T' a.
+Proof.
+  induction 1 using glu_univ_elem_ind; intros;
+    simpl_glu_rel; repeat split; mauto.
+
+  intros.
+  specialize (H4 _ _ _ H2 H7); mauto.
+Qed.
+
+
+Lemma glu_univ_elem_typ_resp_ctx_equiv : forall i P El A B,
+    glu_univ_elem i P El A B ->
+    forall Γ T Δ,
+      P Γ T ->
+      {{ ⊢ Γ ≈ Δ }} ->
+      P Δ T.
+Proof.
+  induction 1 using glu_univ_elem_ind; intros;
+    simpl_glu_rel; mauto 2;
+    econstructor; mauto.
+Qed.
+
+
+Lemma glu_nat_resp_wk' : forall Γ m a,
+    glu_nat Γ m a ->
+    forall Δ σ,
+      {{ Γ ⊢ m : ℕ }} ->
+      {{ Δ ⊢w σ : Γ }} ->
+      glu_nat Δ {{{ m [ σ ]}}} a.
+Proof.
+  induction 1; intros; gen_presups.
+  - econstructor.
+    transitivity {{{ zero [ σ ]}}}; mauto.
+  - econstructor; [ |mauto].
+    transitivity {{{ (succ m') [σ]}}}; mauto 4.
+  - econstructor; trivial.
+    intros. gen_presups.
+    assert {{ Δ0 ⊢w σ ∘ σ0 : Γ }} by mauto.
+    specialize (H0 _ _ _ H5 H4).
+    transitivity {{{ m [ σ ∘ σ0 ]}}}; mauto 4.
+Qed.
+
+Lemma glu_nat_resp_wk : forall Γ m a,
+    glu_nat Γ m a ->
+    forall Δ σ,
+      {{ Δ ⊢w σ : Γ }} ->
+      glu_nat Δ {{{ m [ σ ]}}} a.
+Proof.
+  mauto using glu_nat_resp_wk'.
+Qed.
+#[export]
+ Hint Resolve glu_nat_resp_wk : mcltt.
+
+Lemma glu_univ_elem_trm_escape : forall i P El A B,
+    glu_univ_elem i P El A B ->
+    forall Γ t T a,
+      El Γ t T a ->
+      {{ Γ ⊢ t : T }}.
+Proof.
+  induction 1 using glu_univ_elem_ind; intros;
+    simpl_glu_rel; mauto 4.
+
+  specialize (H4 (length Γ)).
+  specialize (H (length Γ)).
+  assert {{ Γ ⊢w Id : Γ }} by mauto.
+  destruct_all.
+  specialize (H5 _ _ _ _ H6 H9 H7).
+  gen_presup H5.
+  mauto.
+Qed.
+
+Lemma glu_univ_elem_per : forall i P El A B,
+    glu_univ_elem i P El A B ->
+    exists R, per_univ_elem i R A B.
+Proof.
+  induction 1 using glu_univ_elem_ind; intros; eexists;
+    try solve [per_univ_elem_econstructor; try reflexivity; trivial].
+
+  - subst. eapply per_univ_elem_core_univ'; trivial.
+    reflexivity.
+  - invert_per_univ_elem H3. mauto.
+Qed.
+
+Lemma glu_univ_elem_trm_per : forall i P El A B,
+    glu_univ_elem i P El A B ->
+    forall Γ t T a R,
+      El Γ t T a ->
+      per_univ_elem i R A B ->
+      R a a.
+Proof.
+  induction 1 using glu_univ_elem_ind; intros;
+    try do 2 match_by_head1 per_univ_elem ltac:(fun H => invert_per_univ_elem H);
+    simpl_glu_rel;
+    mauto 4.
+
+  intros.
+  destruct_rel_mod_app.
+  destruct_rel_mod_eval.
+  functional_eval_rewrite_clear.
+  do_per_univ_elem_irrel_assert.
+
+  econstructor; firstorder eauto.
+Qed.
+
+Lemma glu_univ_elem_trm_typ : forall i P El A B,
+    glu_univ_elem i P El A B ->
+    forall Γ t T a,
+      El Γ t T a ->
+      P Γ T.
+Proof.
+  induction 1 using glu_univ_elem_ind; intros;
+    simpl_glu_rel;
+    mauto 4.
+
+  econstructor; eauto.
+  invert_per_univ_elem H3.
+  intros.
+  destruct_rel_mod_eval.
+  edestruct H11 as [? []]; eauto.
+Qed.
+
+Lemma glu_univ_elem_trm_univ_lvl : forall i P El A B,
+    glu_univ_elem i P El A B ->
+    forall Γ t T a,
+      El Γ t T a ->
+      {{ Γ ⊢ T : Type@i }}.
+Proof.
+  intros. eapply glu_univ_elem_univ_lvl; [| eapply glu_univ_elem_trm_typ]; eassumption.
+Qed.
+
+
+Lemma glu_univ_elem_trm_resp_equiv : forall i P El A B,
+    glu_univ_elem i P El A B ->
+    forall Γ t T a t',
+      El Γ t T a ->
+      {{ Γ ⊢ t ≈ t' : T }} ->
+      El Γ t' T a.
+Proof.
+  induction 1 using glu_univ_elem_ind; intros;
+    simpl_glu_rel;
+    repeat split; mauto 3.
+
+  - repeat eexists; try split; eauto.
+    eapply glu_univ_elem_typ_resp_equiv; mauto.
+
+  - econstructor; eauto.
+    invert_per_univ_elem H3.
+    intros.
+    destruct_rel_mod_eval.
+    assert {{ Δ ⊢ m' : IT [ σ ]}} by eauto using glu_univ_elem_trm_escape.
+    edestruct H12 as [? []]; eauto.
+    eexists; split; eauto.
+    eapply H2; eauto.
+    assert {{ Γ ⊢ m ≈ t' : Π IT OT }} as Hty by mauto.
+    assert {{ Δ ⊢ IT [ σ ] : Type @ i4 }} by mauto 3.
+    eapply wf_exp_eq_sub_cong with (Γ := Δ) in Hty; [|mauto 4].
+    autorewrite with mcltt in Hty.
+    eapply wf_exp_eq_app_cong with (N := m') (N' := m') in Hty; try pi_univ_level_tac; [|mauto 2].
+    autorewrite with mcltt in Hty.
+    eassumption.
+  - intros.
+    assert {{ Δ ⊢ m [ σ ] ≈ t' [ σ ] : M [ σ ] }} by mauto 4.
+    mauto.
 Qed.

theories/Core/Soundness/Weakening/Lemmas.v

@@ -70,6 +70,9 @@ Proof with mautosolve.
     eapply wf_sub_eq_compose_assoc; revgoals...
 Qed.
 
+#[export]
+Hint Resolve weakening_compose : mcltt.
+
 Lemma weakening_id : forall Γ,
     {{ ⊢ Γ }} ->
     {{ Γ ⊢w Id : Γ }}.

theories/Core/Syntactic/Corollaries.v

@@ -1,3 +1,4 @@
+From Coq Require Import Setoid.
 From Mcltt Require Import Base LibTactics.
 From Mcltt.Core Require Import CtxEq Presup.
 Import Syntax_Notations.
@@ -35,3 +36,9 @@ Qed.
 
 #[export]
 Hint Resolve invert_sub_id : mcltt.
+
+Add Parametric Morphism i Γ Δ t (H : {{ Δ ⊢ t : Type@i }}) : (a_sub t)
+    with signature wf_sub_eq Γ Δ ==> wf_exp_eq Γ {{{ Type@i }}} as sub_typ_cong1.
+Proof.
+  intros. gen_presups. mauto 4.
+Qed.

theories/Core/Syntactic/Presup.v

@@ -233,7 +233,37 @@ Proof with mautosolve 4.
 Qed.
 
 #[export]
-Hint Resolve presup_exp presup_exp_eq presup_sub_eq : mcltt.
+  Hint Resolve presup_exp presup_exp_eq presup_sub_eq : mcltt.
+
+
+#[local]
+  Ltac invert_wf_ctx1 H :=
+  match type of H with
+  | {{ ⊢ ~_ , ~_ }} =>
+      let H' := fresh "H" in
+      pose proof H as H';
+      progressive_invert H'
+  end.
+
+Ltac invert_wf_ctx :=
+  (on_all_hyp: fun H => invert_wf_ctx1 H);
+  clear_dups.
 
 Ltac gen_presup H := gen_presup_IH @presup_exp @presup_exp_eq @presup_sub_eq H.
-Ltac gen_presups := on_all_hyp: fun H => gen_presup H.
+
+Ltac gen_presups := (on_all_hyp: fun H => gen_presup H); invert_wf_ctx;  clear_dups.
+
+
+Lemma wf_ctx_eq_extend' : forall (Γ Δ : ctx) (A : typ) (i : nat) (A' : typ),
+    {{ ⊢ Γ ≈ Δ }} ->
+    {{ Γ ⊢ A ≈ A' : Type@i }} ->
+    {{ ⊢ Γ , A ≈ Δ , A' }}.
+Proof.
+  intros. gen_presups.
+  econstructor; mauto.
+Qed.
+
+#[export]
+  Hint Resolve wf_ctx_eq_extend' : mcltt.
+#[export]
+  Remove Hints wf_ctx_eq_extend : mcltt.