Work on the final semantic rule for equality

theories/Core/Soundness/EqualityCases.v

@@ -93,6 +93,27 @@ Qed.
   Hint Resolve glu_rel_eq_refl : mctt.
 
 
+Lemma glu_rel_exp_eq_clean_inversion : forall {i Γ Sb M1 M2 A N},
+    {{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
+    {{ Γ ⊩ A : Type@i }} ->
+    {{ Γ ⊩ M1 : A }} ->
+    {{ Γ ⊩ M2 : A }} ->
+    {{ Γ ⊩ N : Eq A M1 M2 }} ->
+    glu_rel_exp_resp_sub_env i Sb N {{{Eq A M1 M2}}}.
+Proof.
+  intros * ? HA HM1 HM2 HN.
+  assert {{ Γ ⊩ Eq A M1 M2 : Type@i }} by mauto.
+  eapply glu_rel_exp_clean_inversion2 in HN; eassumption.
+Qed.
+
+
+#[global]
+  Ltac invert_glu_rel_exp H ::=
+  directed (unshelve eapply (glu_rel_exp_eq_clean_inversion _) in H; shelve_unifiable; try eassumption;
+   simpl in H)
+  + universe_invert_glu_rel_exp H.
+
+
 Lemma glu_rel_eq_eqrec : forall Γ A i M1 M2 B j BR N,
     {{ Γ ⊩ A : Type@i }} ->
     {{ Γ ⊩ M1 : A }} ->
@@ -101,6 +122,104 @@ Lemma glu_rel_eq_eqrec : forall Γ A i M1 M2 B j BR N,
     {{ Γ, A ⊩ BR : B[Id,,#0,,refl A[Wk] #0] }} ->
     {{ Γ ⊩ N : Eq A M1 M2 }} ->
     {{ Γ ⊩ eqrec N as Eq A M1 M2 return B | refl -> BR end : B[Id,,M1,,M2,,N] }}.
+Proof.
+  intros * HA HM1 HM2 HB HBR HN.
+  assert {{ ⊩ Γ }} by mauto.
+  assert {{ ⊩ Γ }} as [SbΓ] by mauto.
+  saturate_syn_judge.
+
+  assert {{ Γ ⊩s Id,,M1 : Γ, A }} by (eapply glu_rel_sub_extend; mauto 3; bulky_rewrite).
+  assert {{ ⊩ Γ , A }} by mauto.
+  assert {{ ⊩ Γ , A }} as [SbΓA] by mauto.
+  assert {{ Γ ⊩s Id,,M1,,M2 : Γ, A, A[Wk] }} by (eapply glu_rel_sub_extend; mauto 4).
+  assert {{ ⊩ Γ , A, A[Wk] }} by mauto.
+  assert {{ ⊩ Γ , A, A[Wk] }} as [SbΓAA] by mauto.
+  assert {{ Γ ⊩s Id,,M1,,M2,,N : Γ, A, A[Wk], Eq A[Wk ∘ Wk] #1 #0 }}.
+  {
+    eapply glu_rel_sub_extend; mauto 4.
+    eapply glu_rel_eq.
+    - mauto.
+    - rewrite <- @exp_eq_sub_compose_typ with (i := i); mauto 3.
+    - rewrite <- @exp_eq_sub_compose_typ with (i := i); mauto 3.
+  }
+  assert {{ ⊩ Γ, A, A[Wk], Eq A[Wk ∘ Wk] #1 #0 }} as [SbΓAAEq] by mauto.
+  assert {{ Γ, A ⊩s Id,,#0 : Γ, A, A[Wk] }} by
+    (eapply glu_rel_sub_extend; mauto 3; bulky_rewrite).
+  saturate_syn_judge.
+
+  assert {{ Γ, A ⊢ (Eq A[Wk∘Wk] #1 #0)[Id,,#0] ≈ Eq A[Wk] #0 #0 : Type@i }} by admit.
+
+  assert {{ Γ, A ⊩s Id,,#0,,refl A[Wk] #0 : Γ, A, A[Wk], Eq A[Wk∘Wk] #1 #0 }}.
+  {
+    eapply glu_rel_sub_extend; mauto 3.
+    - eapply glu_rel_eq;
+        try rewrite <- @exp_eq_sub_compose_typ with (A:=A); mauto.
+    - bulky_rewrite.
+      mauto 3.
+  }
+  saturate_syn_judge.
+
+  invert_sem_judge.
+
+  eexists; split; eauto.
+  exists j; intros.
+  assert {{ Δ ⊢s σ : Γ }} by mauto 4.
+  apply_glu_rel_judge.
+  apply_glu_rel_exp_judge.
+  simpl in *.
+
+  repeat invert_glu_rel1.
+  clear_dups.
+  saturate_glu_typ_from_el.
+  unify_glu_univ_lvl i.
+
+  deepexec (glu_univ_elem_per_univ i) ltac:(fun H => pose proof H).
+  match_by_head per_univ ltac:(fun H => destruct H).
+  do 2 deepexec (glu_univ_elem_per_elem i) ltac:(fun H => pose proof H; fail_at_if_dup ltac:(4)).
+  saturate_glu_info.
+
+  (* eassert (exists mr, {{ ⟦ eqrec N as Eq A M1 M2 return B | refl -> BR end ⟧ ρ ↘ ^ mr }} *)
+  (*                /\ {{ Γ0 ⊢ eqrec N as Eq A M1 M2 return B | refl -> BR end[σ] : B[Id,,M1,,M2,,N][σ] ® mr ∈ H53 }}). *)
+  (* { *)
+  (*   destruct_glu_eq. *)
+  (*   - assert {{ Γ0 ⊢w Id : Γ0 }} as HId by mauto. *)
+  (*     pose proof (H78 _ _ HId) as HM''. *)
+
+  (*     match goal with *)
+  (*     | H1 : glu_univ_elem _ _ ?El _, H2 : glu_univ_elem i ?P _ _, H3 : ?P _ _, H4 : ?El _ _ _ _ *)
+  (*       |- _ => *)
+  (*         idtac H1 H2 H3 H4 *)
+  (*     end. *)
+
+  (*     pose proof (glu_univ_elem_exp_conv' H62 H51 HM'' H55). *)
+
+  (*     unify_glu_univ_lvl1 i. *)
+
+  (*     unify_glu_univ_lvl i. *)
+  (*     saturate_glu_info. *)
+  (*     assert {{ Γ0 ⊢ M'' : B1 }} by mauto. *)
+  (*     assert {{ Γ0 ⊢ M'' : B1 ® m' ∈ El2 }} by bulky_rewrite_in HM''. *)
+  (*     eassert {{ Γ0 ⊢ M'' : B1 ® m' ∈ glu_elem_top _ _ }} as [] by mauto. *)
+  (*     match_by_head1 per_top ltac:(fun H => specialize (H (length Γ0)) as [? []]). *)
+
+  (*     assert (SbΓA Γ0 {{{σ ,, M''}}} d{{{ρ ↦ m'}}}). *)
+  (*     { *)
+  (*       match_by_head1 (glu_ctx_env SbΓA) invert_glu_ctx_env. *)
+  (*       apply_equiv_left. *)
+  (*       econstructor; mauto 3. *)
+  (*       destruct_all. *)
+  (*       handle *)
+  (*     } *)
+
+
+  (*     eexists; split. *)
+  (*     + econstructor; mauto 3. *)
+  (*       econstructor. *)
+  (* } *)
+
+  econstructor; mauto.
+
+
 Admitted.
 
 #[export]

theories/Core/Soundness/LogicalRelation/CoreLemmas.v

@@ -132,7 +132,7 @@ Qed.
 
 #[global]
   Ltac destruct_glu_eq :=
-  match_by_head1 glu_eq ltac:(fun H => destruct H).
+  match_by_head1 glu_eq ltac:(fun H => dependent destruction H).
 
 Lemma glu_univ_elem_trm_resp_typ_exp_eq : forall i P El a,
     {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
@@ -802,12 +802,12 @@ Proof.
       symmetry. trivial.
   - simpl_glu_rel.
     econstructor; eauto.
-    destruct_glu_eq; progressive_invert H20; econstructor; mauto 3; intros.
+    destruct_glu_eq; match_by_head1 per_eq progressive_invert; econstructor; mauto 3; intros.
     + etransitivity; mauto.
     + etransitivity; eauto.
       symmetry. eauto.
     + resp_per_IH.
-    + specialize (H20 (length Δ)).
+    + match_by_head1 per_bot ltac:(fun H => specialize (H (length Δ))).
       destruct_all.
       functional_read_rewrite_clear.
       mauto.
@@ -1064,7 +1064,7 @@ Proof.
       * assert {{ Δ0 ⊢w σ ∘ σ0 : Γ }} by mauto 4.
         bulky_rewrite.
         etransitivity;
-          [| deepexec H14 ltac:(fun H => apply H)].
+          [| deepexec H13 ltac:(fun H => apply H)].
         mauto 4.
   - destruct_conjs.
     split; [mauto 3 |].

theories/Core/Soundness/LogicalRelation/Lemmas.v

@@ -1227,15 +1227,20 @@ Proof.
   eapply glu_univ_elem_exp_conv; revgoals; mauto 3.
 Qed.
 
+
 #[global]
-Ltac invert_glu_rel_exp H :=
+Ltac basic_invert_glu_rel_exp H :=
   (unshelve eapply (glu_rel_exp_clean_inversion2 _ _) in H; shelve_unifiable; [eassumption | eassumption |];
    simpl in H)
   + (unshelve eapply (glu_rel_exp_clean_inversion1 _) in H; shelve_unifiable; [eassumption |];
      destruct H as [])
   + (inversion H as [? [? [? ?]]]; subst).
 
 
+#[global]
+Ltac invert_glu_rel_exp H :=
+  basic_invert_glu_rel_exp H.
+
 Lemma glu_rel_exp_to_wf_exp : forall {Γ A M},
     {{ Γ ⊩ M : A }} ->
     {{ Γ ⊢ M : A }}.
@@ -1304,7 +1309,7 @@ Proof.
 Qed.
 
 Ltac invert_glu_rel_sub H :=
-  (unshelve eapply (glu_rel_sub_clean_inversion3 _ _) in H; shelve_unifiable; [eassumption | eassumption |])
+  (unshelve eapply (glu_rel_sub_clean_inversion3 _ _) in H; shelve_unifiable; [eassumption | eassumption |]; simpl in H)
   + (unshelve eapply (glu_rel_sub_clean_inversion2 _) in H; shelve_unifiable; [eassumption |];
      destruct H as [? []])
   + (unshelve eapply (glu_rel_sub_clean_inversion1 _) in H; shelve_unifiable; [eassumption |];
@@ -1365,6 +1370,16 @@ Ltac apply_glu_rel_judge :=
   clear_dups.
 
 
+Ltac apply_glu_rel_exp_judge :=
+  destruct_glu_rel_exp_with_sub;
+  simplify_evals;
+  match_by_head glu_univ_elem ltac:(fun H => directed invert_glu_univ_elem H);
+  handle_functional_glu_univ_elem;
+  unfold univ_glu_exp_pred' in *;
+  destruct_conjs;
+  clear_dups.
+
+
 Lemma glu_rel_exp_preserves_lvl : forall Γ Sb M A i,
     {{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
     (forall Δ σ ρ,
@@ -1388,19 +1403,22 @@ Qed.
 Hint Resolve glu_rel_exp_preserves_lvl : mctt.
 
 
-
 Ltac saturate_syn_judge1 :=
   match goal with
   | H : {{ ^?Γ ⊩ ^?M : ^?A }} |- _ =>
       assert {{ Γ ⊢ M : A }} by mauto; fail_if_dup
   | H : {{ ^?Γ ⊩s ^?τ : ^?Γ' }} |- _ =>
       assert {{ Γ ⊢s τ : Γ' }} by mauto; fail_if_dup
+  | H : {{ ⊩ ^?Γ }} |- _ =>
+      assert {{ ⊢ Γ }} by mauto; fail_if_dup
   end.
 
+
 #[global]
   Ltac saturate_syn_judge :=
   repeat saturate_syn_judge1.
 
+#[global]
 Ltac invert_sem_judge1 :=
   match goal with
   | H : {{ ^?Γ ⊩ ^?M : ^?A }} |- _ =>

theories/Core/Soundness/Realizability.v

@@ -325,7 +325,7 @@ Proof.
     saturate_weakening_escape.
     destruct_glu_eq;
       dir_inversion_clear_by_head read_nf.
-    + pose proof (PER_refl1 _ _ _ _ _ H25).
+    + pose proof (PER_refl1 _ _ _ _ _ H21).
       gen_presups.
       assert {{ Γ ⊢w Id : Γ }} by mauto 4.
       assert (P Γ {{{ B[Id] }}}) as HB by mauto 3.

theories/Core/Soundness/UniverseCases.v

@@ -53,15 +53,6 @@ Proof.
   eapply glu_rel_exp_clean_inversion2 in HM; mauto 3.
 Qed.
 
-#[local]
-  Ltac invert_glu_rel_exp_old H :=
-  invert_glu_rel_exp H.
-
-#[global]
-  Ltac invert_glu_rel_exp H :=
-  (unshelve eapply (glu_rel_exp_clean_inversion2' _) in H; shelve_unifiable; [eassumption |];
-   simpl in H)
-  + invert_glu_rel_exp_old H.
 
 Lemma glu_rel_exp_sub_typ : forall {Γ σ Δ i A},
     {{ Γ ⊩s σ : Δ }} ->
@@ -77,3 +68,29 @@ Qed.
 
 #[export]
 Hint Resolve glu_rel_exp_sub_typ : mctt.
+
+
+Lemma glu_rel_exp_typ_sub_clean_inversion : forall {Γ σ Δ Sb M A i},
+    {{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
+    {{ Δ ⊩ A : Type@i }} ->
+    {{ Γ ⊩s σ : Δ }} ->
+    {{ Γ ⊩ M : A[σ] }} ->
+    glu_rel_exp_resp_sub_env i Sb M {{{A[σ]}}}.
+Proof.
+  intros * ? ? ? HM.
+  assert {{ Γ ⊩ A[σ] : Type@i }} by mauto.
+  eapply glu_rel_exp_clean_inversion2 in HM; eassumption.
+Qed.
+
+
+#[global]
+  Ltac universe_invert_glu_rel_exp H :=
+  directed (unshelve eapply (glu_rel_exp_typ_sub_clean_inversion _) in H; shelve_unifiable; try eassumption;
+   simpl in H)
+  + (unshelve eapply (glu_rel_exp_clean_inversion2' _) in H; shelve_unifiable; [eassumption |];
+   simpl in H)
+  + basic_invert_glu_rel_exp H.
+
+
+#[global]
+  Ltac invert_glu_rel_exp H ::= universe_invert_glu_rel_exp H.