Prove per escape lemma along gluing (#151)

* Prove per escape lemma along gluing

* Fix CI errors

* Remove some explicit Id rewriting

* Simplify the proof a bit

theories/Core/Soundness/Cumulativity.v

@@ -107,9 +107,9 @@ Section glu_univ_elem_cumulativity.
       assert (exists ac, {{ $| a0 & c |↘ ac }} /\ {{ Δ ⊢ m[σ] m' : OT0[σ,,m'] ® ac ∈ OEl' c equiv_c }}) by mauto.
       destruct_conjs.
       functional_eval_rewrite_clear.
-      enough {{ Δ ⊢ OT[σ,,m'] ≈ OT0[σ,,m'] : Type@j }} by (rewrite glu_univ_elem_elem_morphism_iff1; mauto).
-      assert {{ DG b ∈ glu_univ_elem i ↘ OP c equiv_c ↘ OEl c equiv_c }} by mauto.
       assert {{ DG b ∈ glu_univ_elem j ↘ OP' c equiv_c ↘ OEl' c equiv_c }} by mauto.
+      enough {{ Δ ⊢ OT[σ,,m'] ≈ OT0[σ,,m'] : Type@j }} as -> by mauto.
+      assert {{ DG b ∈ glu_univ_elem i ↘ OP c equiv_c ↘ OEl c equiv_c }} by mauto.
       assert {{ Δ ⊢ OT0[σ,,m'] ® OP' c equiv_c }} by (eapply glu_univ_elem_trm_typ; mauto).
       assert {{ Δ ⊢ OT[σ,,m'] ® glu_typ_top i b }} as [] by mauto 3.
       assert {{ Δ ⊢ OT0[σ,,m'] ® glu_typ_top j b }} as [] by mauto 3.

theories/Core/Soundness/EquivalenceLemmas.v

@@ -0,0 +1,82 @@
+From Coq Require Import Morphisms Morphisms_Prop Morphisms_Relations Relation_Definitions RelationClasses.
+
+From Mcltt Require Import Base LibTactics.
+From Mcltt.Core.Syntactic Require Import Corollaries.
+From Mcltt.Core.Semantic Require Import Realizability.
+From Mcltt.Core.Soundness Require Import Realizability.
+From Mcltt.Core.Soundness Require Export LogicalRelation.
+Import Domain_Notations.
+
+Lemma glu_univ_elem_per_univ_typ_escape : forall {i a a' P P' El El' Γ A A'},
+    {{ Dom a ≈ a' ∈ per_univ i }} ->
+    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    {{ DG a' ∈ glu_univ_elem i ↘ P' ↘ El' }} ->
+    {{ Γ ⊢ A ® P }} ->
+    {{ Γ ⊢ A' ® P' }} ->
+    {{ Γ ⊢ A ≈ A' : Type@i }}.
+Proof.
+  intros * [? Hper] Hglu Hglu' HA HA'.
+  gen A' A Γ. gen El' El P' P.
+  induction Hper using per_univ_elem_ind; intros; subst;
+    saturate_refl_for per_univ_elem;
+    invert_glu_univ_elem Hglu;
+    handle_functional_glu_univ_elem;
+    handle_per_univ_elem_irrel;
+    destruct_by_head pi_glu_typ_pred;
+    saturate_glu_by_per;
+    invert_glu_univ_elem Hglu';
+    handle_functional_glu_univ_elem;
+    try solve [simpl in *; mauto 4].
+  - destruct_by_head pi_glu_typ_pred.
+    rename x into IP. rename x0 into IEl. rename x1 into OP. rename x2 into OEl.
+    rename M0 into M'. rename IT0 into IT'. rename OT0 into OT'.
+    rename x4 into OP'. rename x5 into OEl'.
+    assert {{ Γ ⊢ IT ® IP }}.
+    {
+      assert {{ Γ ⊢ IT[Id] ® IP }} by mauto.
+      simpl in *.
+      autorewrite with mcltt in *; mauto.
+    }
+    assert {{ Γ ⊢ IT' ® IP }}.
+    {
+      assert {{ Γ ⊢ IT'[Id] ® IP }} by mauto.
+      simpl in *.
+      autorewrite with mcltt in *; mauto.
+    }
+    do 2 bulky_rewrite1.
+    assert {{ Γ ⊢ IT ≈ IT' : Type@i }} by mauto.
+    enough {{ Γ, IT ⊢ OT ≈ OT' : Type@i }} by mauto 3.
+    assert {{ Dom ⇑! A (length Γ) ≈ ⇑! A' (length Γ) ∈ in_rel }} as equiv_len_len' by (eapply per_bot_then_per_elem; mauto).
+    assert {{ Dom ⇑! A (length Γ) ≈ ⇑! A (length Γ) ∈ in_rel }} as equiv_len_len by (eapply per_bot_then_per_elem; mauto).
+    assert {{ Dom ⇑! A' (length Γ) ≈ ⇑! A' (length Γ) ∈ in_rel }} as equiv_len'_len' by (eapply per_bot_then_per_elem; mauto).
+    destruct_rel_mod_eval.
+    handle_per_univ_elem_irrel.
+    rename a0 into b.
+    rename a' into b'.
+    assert {{ DG b ∈ glu_univ_elem i ↘ OP d{{{ ⇑! A (length Γ) }}} equiv_len_len ↘ OEl d{{{ ⇑! A (length Γ) }}} equiv_len_len }} by mauto.
+    assert {{ DG b' ∈ glu_univ_elem i ↘ OP' d{{{ ⇑! A' (length Γ) }}} equiv_len'_len' ↘ OEl' d{{{ ⇑! A' (length Γ) }}} equiv_len'_len' }} by mauto.
+    assert {{ Γ, IT ⊢ OT ® OP d{{{ ⇑! A (length Γ) }}} equiv_len_len }}.
+    {
+      assert {{ Γ, IT ⊢ #0 : IT[Wk] ® !(length Γ) ∈ glu_elem_bot i A }} by eauto using var_glu_elem_bot.
+      assert {{ Γ, IT ⊢ #0 : IT[Wk] ® ⇑! A (length Γ) ∈ IEl }} by (eapply realize_glu_elem_bot; mauto).
+      assert {{ Γ, IT ⊢ OT[Wk,,#0] ≈ OT : Type@i }} as <- by (bulky_rewrite1; mauto 3).
+      mauto.
+    }
+    assert {{ Γ, IT ⊢ OT' ® OP' d{{{ ⇑! A' (length Γ) }}} equiv_len'_len' }}.
+    {
+      assert {{ Γ, IT' ⊢ #0 : IT'[Wk] ® !(length Γ) ∈ glu_elem_bot i A' }} by eauto using var_glu_elem_bot.
+      assert {{ Γ, IT' ⊢ #0 : IT'[Wk] ® ⇑! A' (length Γ) ∈ IEl }} by (eapply realize_glu_elem_bot; mauto).
+      assert {{ Γ, IT' ⊢ OT'[Wk,,#0] ® OP' d{{{ ⇑! A' (length Γ) }}} equiv_len'_len' }} by mauto.
+      assert {{ ⊢ Γ, IT' ≈ Γ, IT }} as <- by mauto.
+      assert {{ Γ, IT' ⊢ OT'[Wk,,#0] ≈ OT' : Type@i }} as <- by (bulky_rewrite1; mauto 3).
+      mauto.
+    }
+    mauto 3.
+  - match_by_head (per_bot b b') ltac:(fun H => specialize (H (length Γ)) as [V []]).
+    simpl in *.
+    destruct_conjs.
+    assert {{ Γ ⊢ A[Id] ≈ A : Type@i }} as <- by mauto 4.
+    assert {{ Γ ⊢ A'[Id] ≈ A' : Type@i }} as <- by mauto 4.
+    assert {{ Γ ⊢ A'[Id] ≈ V : Type@i }} as -> by mauto 4.
+    mauto 4.
+Qed.

theories/Core/Soundness/LogicalRelation/Lemmas.v

@@ -48,7 +48,7 @@ Qed.
 #[export]
 Hint Resolve glu_nat_escape : mcltt.
 
-Lemma glu_nat_resp_equiv : forall Γ m a,
+Lemma glu_nat_resp_exp_eq : forall Γ m a,
     glu_nat Γ m a ->
     forall m',
     {{ Γ ⊢ m ≈ m' : ℕ }} ->
@@ -61,7 +61,18 @@ Proof.
 Qed.
 
 #[local]
-Hint Resolve glu_nat_resp_equiv : mcltt.
+Hint Resolve glu_nat_resp_exp_eq : mcltt.
+
+Lemma glu_nat_resp_ctx_eq : forall Γ m a Δ,
+    glu_nat Γ m a ->
+    {{ ⊢ Γ ≈ Δ }} ->
+    glu_nat Δ m a.
+Proof.
+  induction 1; intros; mauto.
+Qed.
+
+#[local]
+Hint Resolve glu_nat_resp_ctx_eq : mcltt.
 
 Lemma glu_nat_readback : forall Γ m a,
     glu_nat Γ m a ->
@@ -97,7 +108,7 @@ Proof.
     simpl_glu_rel; trivial.
 Qed.
 
-Lemma glu_univ_elem_typ_resp_equiv : forall i P El A,
+Lemma glu_univ_elem_typ_resp_exp_eq : forall i P El A,
     {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} ->
     forall Γ T T',
       {{ Γ ⊢ T ® P }} ->
@@ -118,12 +129,12 @@ Add Parametric Morphism i P El A (H : glu_univ_elem i P El A) Γ : (P Γ)
     with signature wf_exp_eq Γ {{{Type@i}}} ==> iff as glu_univ_elem_typ_morphism_iff1.
 Proof.
   intros. split; intros;
-    eapply glu_univ_elem_typ_resp_equiv;
+    eapply glu_univ_elem_typ_resp_exp_eq;
     mauto 2.
 Qed.
 
 
-Lemma glu_univ_elem_trm_resp_typ_equiv : forall i P El A,
+Lemma glu_univ_elem_trm_resp_typ_exp_eq : forall i P El A,
     {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} ->
     forall Γ t T a T',
       {{ Γ ⊢ t : T ® a ∈ El }} ->
@@ -139,14 +150,14 @@ Proof.
 Qed.
 
 Add Parametric Morphism i P El A (H : glu_univ_elem i P El A) Γ : (El Γ)
-    with signature wf_exp_eq Γ {{{Type@i}}} ==> eq ==> eq ==> iff as glu_univ_elem_elem_morphism_iff1.
+    with signature wf_exp_eq Γ {{{Type@i}}} ==> eq ==> eq ==> iff as glu_univ_elem_trm_morphism_iff1.
 Proof.
   split; intros;
-    eapply glu_univ_elem_trm_resp_typ_equiv;
+    eapply glu_univ_elem_trm_resp_typ_exp_eq;
     mauto 2.
 Qed.
 
-Lemma glu_univ_elem_typ_resp_ctx_equiv : forall i P El A,
+Lemma glu_univ_elem_typ_resp_ctx_eq : forall i P El A,
     {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} ->
     forall Γ T Δ,
       {{ Γ ⊢ T ® P }} ->
@@ -163,10 +174,36 @@ Add Parametric Morphism i P El A (H : glu_univ_elem i P El A) : P
     with signature wf_ctx_eq ==> eq ==> iff as glu_univ_elem_typ_morphism_iff2.
 Proof.
   intros. split; intros;
-    eapply glu_univ_elem_typ_resp_ctx_equiv;
+    eapply glu_univ_elem_typ_resp_ctx_eq;
     mauto 2.
 Qed.
 
+Lemma glu_univ_elem_trm_resp_ctx_eq : forall i P El A,
+    {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    forall Γ T M m Δ,
+      {{ Γ ⊢ M : T ® m ∈ El }} ->
+      {{ ⊢ Γ ≈ Δ }} ->
+      {{ Δ ⊢ M : T ® m ∈ El }}.
+Proof.
+  simpl.
+  induction 1 using glu_univ_elem_ind; intros;
+    simpl_glu_rel; mauto 2;
+    econstructor; mauto using glu_nat_resp_ctx_eq.
+
+  - split; mauto.
+    do 2 eexists.
+    split; mauto.
+    eapply glu_univ_elem_typ_resp_ctx_eq; mauto.
+  - split; mauto.
+Qed.
+
+Add Parametric Morphism i P El A (H : glu_univ_elem i P El A) : El
+    with signature wf_ctx_eq ==> eq ==> eq ==> eq ==> iff as glu_univ_elem_trm_morphism_iff2.
+Proof.
+  intros. split; intros;
+    eapply glu_univ_elem_trm_resp_ctx_eq;
+    mauto 2.
+Qed.
 
 Lemma glu_nat_resp_wk' : forall Γ m a,
     glu_nat Γ m a ->
@@ -273,7 +310,7 @@ 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,
+Lemma glu_univ_elem_trm_resp_exp_eq : forall i P El A,
     {{ DG A ∈ glu_univ_elem i ↘ P ↘ El }} ->
     forall Γ t T a t',
       {{ Γ ⊢ t : T ® a ∈ El }} ->
@@ -286,7 +323,7 @@ Proof.
     repeat split; mauto 3.
 
   - repeat eexists; try split; eauto.
-    eapply glu_univ_elem_typ_resp_equiv; mauto.
+    eapply glu_univ_elem_typ_resp_exp_eq; mauto.
 
   - econstructor; eauto.
     invert_per_univ_elem H3.
@@ -308,16 +345,14 @@ Proof.
     mauto 4.
 Qed.
 
-
 Add Parametric Morphism i P El A (H : glu_univ_elem i P El A) Γ T : (El Γ T)
-    with signature wf_exp_eq Γ T ==> eq ==> iff as glu_univ_elem_elem_morphism_iff2.
+    with signature wf_exp_eq Γ T ==> eq ==> iff as glu_univ_elem_trm_morphism_iff3.
 Proof.
   split; intros;
-    eapply glu_univ_elem_trm_resp_equiv;
+    eapply glu_univ_elem_trm_resp_exp_eq;
     mauto 2.
 Qed.
 
-
 Lemma glu_univ_elem_core_univ' : forall j i typ_rel el_rel,
     j < i ->
     (typ_rel <∙> univ_glu_typ_pred j i) ->
@@ -327,6 +362,7 @@ Proof.
   intros.
   unshelve basic_glu_univ_elem_econstructor; mautosolve.
 Qed.
+
 #[export]
 Hint Resolve glu_univ_elem_core_univ' : mcltt.
 
@@ -489,7 +525,7 @@ Ltac handle_functional_glu_univ_elem :=
   apply_predicate_equivalence;
   clear_dups.
 
-Lemma glu_univ_elem_pi_clean_inversion : forall {i a p B in_rel typ_rel el_rel},
+Lemma glu_univ_elem_pi_clean_inversion1 : forall {i a p B in_rel typ_rel el_rel},
   {{ DF a ≈ a ∈ per_univ_elem i ↘ in_rel }} ->
   {{ DG Π a p B ∈ glu_univ_elem i ↘ typ_rel ↘ el_rel }} ->
   exists IP IEl (OP : forall c (equiv_c_c : {{ Dom c ≈ c ∈ in_rel }}), glu_typ_pred)
@@ -563,10 +599,34 @@ Proof.
     intuition.
 Qed.
 
-Arguments glu_univ_elem_pi_clean_inversion _ _ _ _ _ _ _ _ _ &.
+Lemma glu_univ_elem_pi_clean_inversion2 : forall {i a p B in_rel IP IEl typ_rel el_rel},
+  {{ DF a ≈ a ∈ per_univ_elem i ↘ in_rel }} ->
+  {{ DG a ∈ glu_univ_elem i ↘ IP ↘ IEl }} ->
+  {{ DG Π a p B ∈ glu_univ_elem i ↘ typ_rel ↘ el_rel }} ->
+  exists (OP : forall c (equiv_c_c : {{ Dom c ≈ c ∈ in_rel }}), glu_typ_pred)
+     (OEl : forall c (equiv_c_c : {{ Dom c ≈ c ∈ in_rel }}), glu_exp_pred) elem_rel,
+    (forall c (equiv_c : {{ Dom c ≈ c ∈ in_rel }}) b,
+        {{ ⟦ B ⟧ p ↦ c ↘ b }} ->
+        {{ DG b ∈ glu_univ_elem i ↘ OP _ equiv_c ↘ OEl _ equiv_c }}) /\
+      {{ DF Π a p B ≈ Π a p B ∈ per_univ_elem i ↘ elem_rel }} /\
+      (typ_rel <∙> pi_glu_typ_pred i in_rel IP IEl OP) /\
+      (el_rel <∙> pi_glu_exp_pred i in_rel IP IEl elem_rel OEl).
+Proof.
+  intros *.
+  simpl.
+  intros Hinper Hinglu Hglu.
+  unshelve eapply (glu_univ_elem_pi_clean_inversion1 _) in Hglu; shelve_unifiable; [eassumption |];
+    destruct Hglu as [? [? [? [? [? [? [? [? []]]]]]]]].
+  handle_functional_glu_univ_elem.
+  do 3 eexists.
+  repeat split; try eassumption;
+    intros []; econstructor; mauto.
+Qed.
 
 Ltac invert_glu_univ_elem H :=
-  (unshelve eapply (glu_univ_elem_pi_clean_inversion _) in H; shelve_unifiable; [eassumption |];
+  (unshelve eapply (glu_univ_elem_pi_clean_inversion2 _ _) in H; shelve_unifiable; [eassumption | eassumption |];
+   destruct H as [? [? [? [? [? []]]]]])
+  + (unshelve eapply (glu_univ_elem_pi_clean_inversion1 _) in H; shelve_unifiable; [eassumption |];
    destruct H as [? [? [? [? [? [? [? [? []]]]]]]]])
   + basic_invert_glu_univ_elem H.
 
@@ -615,6 +675,22 @@ Proof with mautosolve.
   symmetry; mauto.
 Qed.
 
+Ltac saturate_glu_by_per1 :=
+  match goal with
+  | H : glu_univ_elem ?i ?P ?El ?a,
+      H1 : per_univ_elem ?i _ ?a ?a' |- _ =>
+      assert (glu_univ_elem i P El a') by (rewrite <- H1; eassumption);
+      fail_if_dup
+  | H : glu_univ_elem ?i ?P ?El ?a',
+      H1 : per_univ_elem ?i _ ?a ?a' |- _ =>
+      assert (glu_univ_elem i P El a) by (rewrite H1; eassumption);
+      fail_if_dup
+  end.
+
+Ltac saturate_glu_by_per :=
+  clear_dups;
+  repeat saturate_glu_by_per1.
+
 Lemma per_univ_glu_univ_elem : forall i a,
     {{ Dom a ≈ a ∈ per_univ i }} ->
     exists P El, {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }}.

theories/Core/Syntactic/System/Lemmas.v

@@ -343,6 +343,23 @@ Qed.
 #[export]
 Hint Resolve sub_eq_extend_cong_typ' sub_eq_extend_compose_typ sub_eq_p_extend_typ : mcltt.
 
+Lemma sub_eq_wk_var0_id : forall Γ A i,
+    {{ Γ ⊢ A : Type@i }} ->
+    {{ Γ, A ⊢s Wk,,#0 ≈ Id : Γ, A }}.
+Proof.
+  intros * ?.
+  assert {{ ⊢ Γ, A }} by mauto 3.
+  assert {{ Γ, A ⊢s (Wk∘Id),,#0[Id] ≈ Id : Γ, A }} by mauto.
+  assert {{ Γ, A ⊢s Wk ≈ Wk∘Id : Γ }} by mauto.
+  assert {{ Γ, A ⊢ #0 ≈ #0[Id] : A[Wk] }} by mauto.
+  mauto 4.
+Qed.
+
+#[export]
+Hint Resolve sub_eq_wk_var0_id : mcltt.
+#[export]
+Hint Rewrite -> sub_eq_wk_var0_id using mauto 4 : mcltt.
+
 Lemma exp_eq_sub_sub_compose_cong_typ : forall {Γ Δ Δ' Ψ σ τ σ' τ' A i}, {{ Ψ ⊢ A : Type@i }} -> {{ Δ ⊢s σ : Ψ }} -> {{ Δ' ⊢s σ' : Ψ }} -> {{ Γ ⊢s τ : Δ }} -> {{ Γ ⊢s τ' : Δ' }} -> {{ Γ ⊢s σ∘τ ≈ σ'∘τ' : Ψ }} -> {{ Γ ⊢ A[σ][τ] ≈ A[σ'][τ'] : Type@i }}.
 Proof with mautosolve.
   intros.

theories/_CoqProject

@@ -53,6 +53,7 @@
 ./Core/Syntactic/SystemOpt.v
 ./Core/Soundness.v
 ./Core/Soundness/Cumulativity.v
+./Core/Soundness/EquivalenceLemmas.v
 ./Core/Soundness/LogicalRelation.v
 ./Core/Soundness/LogicalRelation/CoreTactics.v
 ./Core/Soundness/LogicalRelation/Definitions.v