finished semantic well-formedness of equality type

theories/Core/Soundness/FunctionCases.v

@@ -47,7 +47,7 @@ Proof.
   intros.
   assert {{ Δ ⊢s σ : Γ }} by mauto 4.
   split; mauto 3.
-  applying_glu_rel_judge.
+  apply_glu_rel_judge.
   rename m into a.
   assert {{ Γ ⊨ Π A B : Type@i }} as [env_relΓ]%rel_exp_of_typ_inversion1 by mauto 3 using completeness_fundamental_exp.
   assert {{ Γ, A ⊨ B : Type@i }} as [env_relΓA]%rel_exp_of_typ_inversion1 by mauto 3 using completeness_fundamental_exp.

theories/Core/Soundness/LogicalRelation/Lemmas.v

@@ -650,7 +650,7 @@ Proof.
     handle_functional_glu_univ_elem.
     trivial.
 Qed.
-
+xb
 Lemma glu_univ_elem_per_subtyp_trm_conv : forall {i j k a a' P P' El El' Γ A A' M m},
     {{ Sub a <: a' at i }} ->
     {{ DG a ∈ glu_univ_elem j ↘ P ↘ El }} ->
@@ -1227,12 +1227,13 @@ Proof.
   eapply glu_univ_elem_exp_conv; revgoals; mauto 3.
 Qed.
 
+#[global]
 Ltac 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; subst).
+  + (inversion H as [? [? [? ?]]]; subst).
 
 
 Lemma glu_rel_exp_to_wf_exp : forall {Γ A M},
@@ -1352,7 +1353,8 @@ Ltac unify_glu_univ_lvl i :=
   fail_if_dup;
   repeat unify_glu_univ_lvl1 i.
 
-Ltac applying_glu_rel_judge :=
+Ltac apply_glu_rel_judge :=
+  destruct_glu_rel_typ_with_sub;
   destruct_glu_rel_exp_with_sub;
   destruct_glu_rel_sub_with_sub;
   simplify_evals;

theories/Core/Soundness/SubtypingCases.v

@@ -54,18 +54,58 @@ Qed.
 #[export]
 Hint Resolve glu_rel_sub_subtyp : mctt.
 
+
+#[local]
+Lemma glu_rel_exp_conv' : forall {Γ M A A' i},
+    {{ Γ ⊩ M : A }} ->
+    {{ Γ ⊢ A ≈ A' : Type@i }} -> (** proof trick, will discharge. see the next lemma. *)
+    {{ Γ ⊢ A ≈ A' : Type@i }} ->
+    {{ Γ ⊩ M : A' }}.
+Proof.
+  intros * [? [? [k ?]]] [env_relΓ [? [? ?]]]%completeness_fundamental_exp_eq ?.
+  econstructor; split; [eassumption |].
+  exists (max i k); intros.
+  assert {{ Δ ⊢s σ : Γ }} by mauto 4.
+
+  destruct_glu_rel_exp_with_sub.
+  assert {{ Dom ρ ≈ ρ ∈ env_relΓ }} by (eapply glu_ctx_env_per_env; mauto).
+  (on_all_hyp: destruct_rel_by_assumption env_relΓ).
+  destruct_by_head rel_typ.
+  match_by_head eval_exp ltac:(fun H => directed dependent destruction H).
+  destruct_by_head rel_exp.
+  saturate_refl.
+  invert_per_univ_elems.
+  apply_equiv_left.
+  destruct_all.
+  handle_per_univ_elem_irrel.
+  assert (i <= max i k) by lia.
+  assert (k <= max i k) by lia.
+  assert {{ Δ ⊢ A'[σ] ≈ A[σ] : Type@(max i k) }} by mauto 4.
+  eapply mk_glu_rel_exp_with_sub''; intuition mauto using per_univ_elem_cumu_max_left, per_univ_elem_cumu_max_right.
+  bulky_rewrite.
+  eapply glu_univ_elem_exp_cumu_ge; try eassumption.
+  eapply glu_univ_elem_resp_per_univ; eauto.
+  symmetry. mauto.
+Qed.
+
 Lemma glu_rel_exp_conv : forall {Γ M A A' i},
     {{ Γ ⊩ M : A }} ->
-    {{ Γ ⊩ A' : Type@i }} ->
     {{ Γ ⊢ A ≈ A' : Type@i }} ->
     {{ Γ ⊩ M : A' }}.
 Proof.
-  mauto 3.
+  eauto using glu_rel_exp_conv'.
 Qed.
 
 #[export]
 Hint Resolve glu_rel_exp_conv : mctt.
 
+Add Parametric Morphism i Γ M : (glu_rel_exp Γ M)
+    with signature (wf_exp_eq Γ {{{Type@i}}}) ==> iff as foo.
+Proof.
+  split; mauto 3.
+Qed.
+
+
 Lemma glu_rel_sub_conv : forall {Γ σ Δ Δ'},
     {{ Γ ⊩s σ : Δ }} ->
     {{ ⊩ Δ' }} ->

theories/Core/Soundness/UniverseCases.v

@@ -53,14 +53,15 @@ Proof.
   eapply glu_rel_exp_clean_inversion2 in HM; mauto 3.
 Qed.
 
-Ltac invert_glu_rel_exp H ::=
+#[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)
-  + (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; subst).
+  + invert_glu_rel_exp_old H.
 
 Lemma glu_rel_exp_sub_typ : forall {Γ σ Δ i A},
     {{ Γ ⊩s σ : Δ }} ->