Work on the final semantic rule for equality

theories/Core/Semantic/Evaluation/Definitions.v

@@ -82,7 +82,7 @@ with eval_eqrec : domain -> exp -> exp -> domain -> domain -> domain -> env -> d
   `( {{ ⟦ BR ⟧ ρ ↦ n ↘ br }} ->
      {{ eqrec refl n as Eq a m1 m2 ⟦return B | refl -> BR end⟧ ρ ↘ br }} )
 | eval_eqrec_neut :
-  `( {{ ⟦ B ⟧ ρ ↦ m1 ↦ m2 ↦ ⇑ (Eq a m1 m2) n ↘ b }} ->
+  `( {{ ⟦ B ⟧ ρ ↦ m1 ↦ m2 ↦ ⇑ c n ↘ b }} ->
      {{ eqrec ⇑ c n as Eq a m1 m2 ⟦return B | refl -> BR end⟧ ρ ↘ ⇑ b (eqrec n under ρ as Eq a m1 m2 return B | refl -> BR end) }} )
 where "'eqrec' n 'as' 'Eq' a m1 m2 '⟦return' B | 'refl' -> BR 'end⟧' ρ '↘' r" := (eval_eqrec a B BR m1 m2 n ρ r) (in custom judg)
 with eval_sub : sub -> env -> env -> Prop :=

theories/Core/Soundness/EqualityCases.v

@@ -1,6 +1,5 @@
 From Mctt Require Import LibTactics.
 From Mctt.Core Require Import Base.
-From Mctt.Core.Completeness Require Import FundamentalTheorem.
 From Mctt.Core.Semantic Require Import Realizability.
 From Mctt.Core.Soundness Require Import
   ContextCases
@@ -93,6 +92,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 +121,102 @@ 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.
+
+  repeat invert_glu_rel1.
+  handle_functional_glu_univ_elem.
+  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 ∈ H77 }}) as [? [? ?]].
+  {
+    destruct_glu_eq.
+    - assert {{ Γ0 ⊢w Id : Γ0 }} as HId by mauto.
+      assert {{ Γ0 ⊢ M'' : B1 }} by (gen_presups; trivial).
+      pose proof (H99 _ _ HId) as HM''.
+      saturate_glu_typ_from_el.
+      assert {{ Γ0 ⊢ B1[Id] ≈ B1 : Type@i }} as HrwB1 by mauto 3.
+      rewrite HrwB1 in *.
+      assert {{ Γ0 ⊢ B1 ≈ A[σ] : Type@i }} as HrwB1' by mauto 4.
+      rewrite HrwB1' in *.
+      saturate_glu_info.
+
+      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; bulky_rewrite.
+        admit.
+      }
+      destruct_glu_rel_exp_with_sub.
+      simplify_evals.
+      simpl in *.
+
+      eexists; split; mauto 3.
+      admit.
+
+    - match_by_head1 per_bot ltac:(fun H => pose proof (H (length Γ0)) as [V [HV _]]).
+      assert {{ Γ0 ⊢w Id : Γ0 }} as HId by mauto.
+      pose proof (H54 _ _ V HId HV).
+      assert {{ Γ0 ⊢ N[σ] ≈ V : (Eq A M1 M2)[σ] }} by admit.
+
+      eexists; split; mauto 3.
+
+      admit.
+  }
+
+  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

@@ -1020,11 +1020,14 @@ Proof.
     econstructor; intuition.
 Qed.
 
-Ltac invert_glu_ctx_env H :=
+
+Ltac basic_invert_glu_ctx_env H :=
   (unshelve eapply (glu_ctx_env_cons_clean_inversion _) in H; shelve_unifiable; [eassumption |];
    destruct H as [? [? []]])
   + dependent destruction H.
 
+Ltac invert_glu_ctx_env H := basic_invert_glu_ctx_env H.
+
 Lemma glu_ctx_env_subtyp_sub_if : forall Γ Γ' Sb Sb' Δ σ ρ,
     {{ ⊢ Γ ⊆ Γ' }} ->
     {{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
@@ -1188,6 +1191,7 @@ Ltac destruct_glu_rel_typ_with_sub :=
     end;
   unmark_all.
 
+
 (** *** Lemmas about [glu_rel_exp] *)
 
 Lemma glu_rel_exp_clean_inversion1 : forall {Γ Sb M A},
@@ -1227,15 +1231,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 }}.
@@ -1254,6 +1263,62 @@ Qed.
 #[export]
 Hint Resolve glu_rel_exp_to_wf_exp : mctt.
 
+
+
+Lemma glu_ctx_env_cons_clean_inversion'_helper : forall {Γ TSb A Sb i},
+  {{ EG Γ ∈ glu_ctx_env ↘ TSb }} ->
+  {{ EG Γ, A ∈ glu_ctx_env ↘ Sb }} ->
+  {{ Γ ⊩ A : Type@i }} ->
+  {{ Γ ⊢ A : Type@i }} ->
+  (forall Δ σ ρ,
+      {{ Δ ⊢s σ ® ρ ∈ TSb }} ->
+      glu_rel_typ_with_sub i Δ A σ ρ) /\
+    (Sb <∙> cons_glu_sub_pred i Γ A TSb).
+Proof.
+  intros * HΓ HΓA [? [? [j HA]]] ?.
+  handle_functional_glu_ctx_env.
+  assert (forall Δ σ ρ, {{ Δ ⊢s σ ® ρ ∈ TSb }} -> glu_rel_typ_with_sub i Δ A σ ρ) by
+    (intros; apply_equiv_right; mauto).
+  split; trivial.
+
+  match_by_head glu_ctx_env progressive_invert.
+  handle_functional_glu_ctx_env.
+
+  intros Δ σ ρ.
+  split; intros [].
+  - apply_equiv_left.
+    destruct_glu_rel_typ_with_sub.
+    handle_functional_glu_univ_elem.
+    econstructor; intuition.
+    eapply @glu_univ_elem_exp_conv' with (i:=i0) (j:=i); try eassumption.
+    bulky_rewrite.
+  - rewrite <- H5 in *.
+    destruct_glu_rel_typ_with_sub.
+    handle_functional_glu_univ_elem.
+    econstructor; intuition.
+    eapply @glu_univ_elem_exp_conv' with (i:=i) (j:=i0); try eassumption.
+    bulky_rewrite.
+Qed.
+
+
+Lemma glu_ctx_env_cons_clean_inversion' : forall {Γ TSb A Sb i},
+  {{ EG Γ ∈ glu_ctx_env ↘ TSb }} ->
+  {{ EG Γ, A ∈ glu_ctx_env ↘ Sb }} ->
+  {{ Γ ⊩ A : Type@i }} ->
+  (forall Δ σ ρ,
+      {{ Δ ⊢s σ ® ρ ∈ TSb }} ->
+      glu_rel_typ_with_sub i Δ A σ ρ) /\
+    (Sb <∙> cons_glu_sub_pred i Γ A TSb).
+Proof.
+  mauto using glu_ctx_env_cons_clean_inversion'_helper.
+Qed.
+
+
+Ltac invert_glu_ctx_env H ::=
+  directed (unshelve eapply (glu_ctx_env_cons_clean_inversion' _) in H; shelve_unifiable; try eassumption; destruct H)
+  + basic_invert_glu_ctx_env H.
+
+
 (** *** Lemmas about [glu_rel_sub] *)
 
 Lemma glu_rel_sub_clean_inversion1 : forall {Γ Sb τ Γ'},
@@ -1304,7 +1369,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 +1430,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,27 +1463,36 @@ 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.
 
-Ltac invert_sem_judge1 :=
+#[global]
+  Ltac invert_sem_judge1 :=
   match goal with
   | H : {{ ^?Γ ⊩ ^?M : ^?A }} |- _ =>
-      invert_glu_rel_exp H
+      mark H;
+      let H' := fresh "H" in
+      pose proof H as H';
+      invert_glu_rel_exp H'
   | H : {{ ^?Γ ⊩s ^?τ : ^?Γ' }} |- _ =>
-      invert_glu_rel_sub H
+      mark H;
+      let H' := fresh "H" in
+      pose proof H as H';
+      invert_glu_rel_sub H'
   end.
 
 #[global]
   Ltac invert_sem_judge :=
-  repeat invert_sem_judge1.
+  repeat invert_sem_judge1; unmark_all.

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.