finished semantic well-formedness of equality type

theories/Core/Soundness/EqualityCases.v

@@ -18,17 +18,80 @@ Lemma glu_rel_eq : forall Γ A i M N,
     {{ Γ ⊩ N : A }} ->
     {{ Γ ⊩ Eq A M N : Type@i }}.
 Proof.
-Admitted.
+  intros * HA HM HN.
+  assert {{ ⊩ Γ }} as [SbΓ] by mauto.
+  assert {{ Γ ⊢ A : Type@i }} by mauto.
+  assert {{ Γ ⊢ M : A }} by mauto.
+  assert {{ Γ ⊢ N : A }} by mauto.
+  invert_glu_rel_exp HA.
+  invert_glu_rel_exp HM.
+  invert_glu_rel_exp HN.
+
+  eapply glu_rel_exp_of_typ; mauto 3.
+  intros.
+  assert {{ Δ ⊢s σ : Γ }} by mauto 4.
+  split; mauto 3.
+  applying_glu_rel_judge.
+  saturate_glu_typ_from_el.
+  unify_glu_univ_lvl i.
+  deepexec glu_univ_elem_per_univ ltac:(fun H => pose proof H).
+  match_by_head per_univ ltac:(fun H => destruct H).
+  do 2 deepexec glu_univ_elem_per_elem ltac:(fun H => pose proof H; fail_at_if_dup ltac:(4)).
+
+  eexists; repeat split; mauto.
+  - eexists. per_univ_elem_econstructor; mauto. reflexivity.
+  - intros.
+    match_by_head1 glu_univ_elem invert_glu_univ_elem.
+    handle_per_univ_elem_irrel.
+    handle_functional_glu_univ_elem.
+    econstructor; mauto 3;
+      intros Δ' τ **;
+      assert {{ Δ' ⊢s τ : Δ }} by mauto 2;
+      assert {{ Δ' ⊢s σ ∘ τ ® ρ ∈ SbΓ }} by (eapply glu_ctx_env_sub_monotone; eassumption);
+      assert {{ Δ' ⊢s σ ∘ τ : Γ }} by mauto 2;
+      applying_glu_rel_judge;
+      handle_functional_glu_univ_elem;
+      unify_glu_univ_lvl i.
+    + bulky_rewrite.
+    + assert {{ Δ' ⊢ M[σ][τ] ≈ M[σ ∘ τ] : A[σ ∘ τ] }} by mauto.
+      bulky_rewrite.
+    + assert {{ Δ' ⊢ N[σ][τ] ≈ N[σ ∘ τ] : A[σ ∘ τ] }} by mauto.
+      bulky_rewrite.
+Qed.
 
 #[export]
   Hint Resolve glu_rel_eq : mctt.
 
-Lemma glu_rel_eq_refl : forall Γ A i M,
-    {{ Γ ⊩ A : Type@i }} ->
+Lemma glu_rel_eq_refl : forall Γ A M,
     {{ Γ ⊩ M : A }} ->
     {{ Γ ⊩ refl A M : Eq A M M }}.
 Proof.
-Admitted.
+  intros * HM.
+  assert {{ ⊩ Γ }} as [SbΓ] by mauto.
+  assert {{ Γ ⊢ M : A }} by mauto.
+  invert_glu_rel_exp HM.
+  assert {{ Γ ⊢ A : Type@x }} by mauto.
+  eexists; split; eauto.
+  exists x; intros.
+  assert {{ Δ ⊢s σ : Γ }} by mauto 4.
+  applying_glu_rel_judge.
+  saturate_glu_typ_from_el.
+  deepexec glu_univ_elem_per_univ ltac:(fun H => pose proof H).
+  match_by_head per_univ ltac:(fun H => destruct H).
+  deepexec glu_univ_elem_per_elem ltac:(fun H => pose proof H; fail_at_if_dup ltac:(4)).
+  saturate_glu_info.
+  eexists; repeat split; mauto.
+  - glu_univ_elem_econstructor; mauto 3; reflexivity.
+  - do 2 try econstructor; mauto 3;
+    intros Δ' τ **;
+      assert {{ Δ' ⊢s τ : Δ }} by mauto 2;
+    assert {{ Δ' ⊢s σ ∘ τ ® ρ ∈ SbΓ }} by (eapply glu_ctx_env_sub_monotone; eassumption);
+    assert {{ Δ' ⊢s σ ∘ τ : Γ }} by mauto 2;
+    assert {{ Δ' ⊢ M[σ][τ] ≈ M[σ ∘ τ] : A[σ ∘ τ] }} by mauto;
+    applying_glu_rel_judge;
+    saturate_glu_typ_from_el;
+    bulky_rewrite.
+Qed.
 
 #[export]
   Hint Resolve glu_rel_eq_refl : mctt.

theories/Core/Soundness/FunctionCases.v

@@ -47,12 +47,7 @@ Proof.
   intros.
   assert {{ Δ ⊢s σ : Γ }} by mauto 4.
   split; mauto 3.
-  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.
+  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/Definitions.v

@@ -415,6 +415,12 @@ Variant glu_rel_sub_with_sub Δ τ (Sb : glu_sub_pred) σ ρ : Prop :=
 Definition glu_rel_ctx Γ : Prop := exists Sb, {{ EG Γ ∈ glu_ctx_env ↘ Sb }}.
 Arguments glu_rel_ctx Γ/.
 
+Definition glu_rel_exp_resp_sub_env i Sb M A :=
+  forall Δ σ ρ,
+    {{ Δ ⊢s σ ® ρ ∈ Sb }} ->
+    glu_rel_exp_with_sub i Δ M A σ ρ.
+Arguments glu_rel_exp_resp_sub_env i Sb M A/.
+
 Definition glu_rel_exp Γ M A : Prop :=
   exists Sb,
     {{ EG Γ ∈ glu_ctx_env ↘ Sb }} /\

theories/Core/Soundness/LogicalRelation/Lemmas.v

@@ -464,6 +464,19 @@ Proof.
   eapply glu_univ_elem_exp_lower_max_left; mauto.
 Qed.
 
+Lemma glu_univ_elem_exp_conv' : forall {i j a P P' El El' Γ A M m},
+    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    {{ DG a ∈ glu_univ_elem j ↘ P' ↘ El' }} ->
+    {{ Γ ⊢ M : A ® m ∈ El }} ->
+    {{ Γ ⊢ A ® P' }} ->
+    {{ Γ ⊢ M : A ® m ∈ El' }}.
+Proof.
+  intros.
+  eapply glu_univ_elem_exp_conv; only 2: exact H; eauto.
+  mauto 2.
+Qed.
+
+
 Lemma glu_univ_elem_per_subtyp_typ_escape : forall {i a a' P P' El El' Γ A A'},
     {{ Sub a <: a' at i }} ->
     {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
@@ -637,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 }} ->
@@ -1144,29 +1157,32 @@ Ltac destruct_glu_rel_by_assumption sub_glu_rel H :=
         mark_with H' 1
     end;
   unmark_all_with 1.
+
 Ltac destruct_glu_rel_exp_with_sub :=
   repeat
     match goal with
     | H : (forall Δ σ ρ, {{ Δ ⊢s σ ® ρ ∈ ?sub_glu_rel }} -> glu_rel_exp_with_sub _ _ _ _ _ _) |- _ =>
-        destruct_glu_rel_by_assumption sub_glu_rel H; mark H
+        destruct_glu_rel_by_assumption sub_glu_rel H; fail_if_dup; mark H
     | H : glu_rel_exp_with_sub _ _ _ _ _ _ |- _ =>
         dependent destruction H
     end;
   unmark_all.
+
 Ltac destruct_glu_rel_sub_with_sub :=
   repeat
     match goal with
     | H : (forall Δ σ ρ, {{ Δ ⊢s σ ® ρ ∈ ?sub_glu_rel }} -> glu_rel_sub_with_sub _ _ _ _ _) |- _ =>
-        destruct_glu_rel_by_assumption sub_glu_rel H; mark H
+        destruct_glu_rel_by_assumption sub_glu_rel H; fail_if_dup; mark H
     | H : glu_rel_exp_with_sub _ _ _ _ _ _ |- _ =>
         dependent destruction H
     end;
   unmark_all.
+
 Ltac destruct_glu_rel_typ_with_sub :=
   repeat
     match goal with
     | H : (forall Δ σ ρ, {{ Δ ⊢s σ ® ρ ∈ ?sub_glu_rel }} -> glu_rel_typ_with_sub _ _ _ _ _) |- _ =>
-        destruct_glu_rel_by_assumption sub_glu_rel H; mark H
+        destruct_glu_rel_by_assumption sub_glu_rel H; fail_if_dup; mark H
     | H : glu_rel_exp_with_sub _ _ _ _ _ _ |- _ =>
         dependent destruction H
     end;
@@ -1189,18 +1205,13 @@ Proof.
   mauto.
 Qed.
 
-Definition glu_rel_exp_clean_inversion2_result i Sb M A :=
-  forall Δ σ ρ,
-    {{ Δ ⊢s σ ® ρ ∈ Sb }} ->
-    glu_rel_exp_with_sub i Δ M A σ ρ.
-
 Lemma glu_rel_exp_clean_inversion2 : forall {i Γ Sb M A},
     {{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
     {{ Γ ⊩ A : Type@i }} ->
     {{ Γ ⊩ M : A }} ->
-    glu_rel_exp_clean_inversion2_result i Sb M A.
+    glu_rel_exp_resp_sub_env i Sb M A.
 Proof.
-  unfold glu_rel_exp_clean_inversion2_result.
+  simpl.
   intros * ? HA HM.
   eapply glu_rel_exp_clean_inversion1 in HA; [| eassumption].
   eapply glu_rel_exp_clean_inversion1 in HM; [| eassumption].
@@ -1216,12 +1227,14 @@ 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 |];
-   unfold glu_rel_exp_clean_inversion2_result in H)
+   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},
     {{ Γ ⊩ M : A }} ->
@@ -1315,3 +1328,61 @@ Qed.
 
 #[export]
 Hint Resolve glu_rel_sub_wf_sub : mctt.
+
+
+Ltac saturate_glu_typ_from_el1 :=
+  match goal with
+  | H : glu_univ_elem _ _ ?El _, H1 : ?El _ _ _ _ |- _ =>
+      pose proof (glu_univ_elem_trm_typ _ _ _ _ H _ _ _ _ H1);
+      fail_if_dup
+  end.
+
+Ltac saturate_glu_typ_from_el :=
+  fail_if_dup;
+  repeat saturate_glu_typ_from_el1.
+
+Ltac unify_glu_univ_lvl1 i :=
+  match goal with
+  | H1 : glu_univ_elem _ _ ?El _, H2 : glu_univ_elem i ?P _ _, H3 : ?P _ _, H4 : ?El _ _ _ _
+    |- _ =>
+      pose proof (glu_univ_elem_exp_conv' H1 H2 H4 H3);
+      fail_if_dup
+  end.
+
+Ltac unify_glu_univ_lvl i :=
+  fail_if_dup;
+  repeat unify_glu_univ_lvl1 i.
+
+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;
+  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 Δ σ ρ,
+        {{ Δ ⊢s σ ® ρ ∈ Sb }} ->
+        glu_rel_exp_with_sub i Δ M A σ ρ) ->
+    {{ Γ ⊢ A : Type@i }}.
+Proof.
+  intros.
+  assert (exists env_relΓ, {{ EF Γ ≈ Γ ∈ per_ctx_env ↘ env_relΓ }}) as [env_relΓ] by mauto 3.
+  assert (exists ρ ρ', initial_env Γ ρ /\ initial_env Γ ρ' /\ {{ Dom ρ ≈ ρ' ∈ env_relΓ }}) as [ρ] by mauto 3 using per_ctx_then_per_env_initial_env.
+  destruct_conjs.
+  functional_initial_env_rewrite_clear.
+  assert {{ Γ ⊢s Id ® ρ ∈ Sb }} by (eapply initial_env_glu_rel_exp; mauto 3).
+  destruct_glu_rel_exp_with_sub.
+  saturate_glu_typ_from_el.
+  saturate_glu_info.
+  mauto 3.
+Qed.
+
+#[export]
+Hint Resolve glu_rel_exp_preserves_lvl : mctt.

theories/Core/Soundness/NatCases.v

@@ -51,7 +51,7 @@ Hint Resolve glu_rel_exp_sub_nat : mctt.
 Lemma glu_rel_exp_clean_inversion2'' : forall {Γ Sb M},
     {{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
     {{ Γ ⊩ M : ℕ }} ->
-    glu_rel_exp_clean_inversion2_result 0 Sb M {{{ ℕ }}}.
+    glu_rel_exp_resp_sub_env 0 Sb M {{{ ℕ }}}.
 Proof.
   intros * ? HM.
   assert {{ Γ ⊩ ℕ : Type@0 }} by mauto 3.
@@ -60,11 +60,11 @@ Qed.
 
 Ltac invert_glu_rel_exp H ::=
   (unshelve eapply (glu_rel_exp_clean_inversion2'' _) in H; shelve_unifiable; [eassumption |];
-   unfold glu_rel_exp_clean_inversion2_result in H)
+   unfold glu_rel_exp_resp_sub_env in H)
   + (unshelve eapply (glu_rel_exp_clean_inversion2' _) in H; shelve_unifiable; [eassumption |];
-     unfold glu_rel_exp_clean_inversion2_result in H)
+     unfold glu_rel_exp_resp_sub_env in H)
   + (unshelve eapply (glu_rel_exp_clean_inversion2 _ _) in H; shelve_unifiable; [eassumption | eassumption |];
-     unfold glu_rel_exp_clean_inversion2_result in H)
+     unfold glu_rel_exp_resp_sub_env in H)
   + (unshelve eapply (glu_rel_exp_clean_inversion1 _) in H; shelve_unifiable; [eassumption |];
      destruct H as [])
   + (inversion H; subst).

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

@@ -46,21 +46,22 @@ Hint Resolve glu_rel_exp_typ : mctt.
 Lemma glu_rel_exp_clean_inversion2' : forall {i Γ Sb M},
     {{ EG Γ ∈ glu_ctx_env ↘ Sb }} ->
     {{ Γ ⊩ M : Type@i }} ->
-    glu_rel_exp_clean_inversion2_result (S i) Sb M {{{ Type@i }}}.
+    glu_rel_exp_resp_sub_env (S i) Sb M {{{ Type@i }}}.
 Proof.
   intros * ? HM.
   assert {{ Γ ⊩ Type@i : Type@(S i) }} by mauto 3.
   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 |];
-   unfold glu_rel_exp_clean_inversion2_result in H)
-  + (unshelve eapply (glu_rel_exp_clean_inversion2 _ _) in H; shelve_unifiable; [eassumption | eassumption |];
-     unfold glu_rel_exp_clean_inversion2_result in H)
-  + (unshelve eapply (glu_rel_exp_clean_inversion1 _) in H; shelve_unifiable; [eassumption |];
-     destruct H as [])
-  + (inversion H; subst).
+   simpl in H)
+  + invert_glu_rel_exp_old H.
 
 Lemma glu_rel_exp_sub_typ : forall {Γ σ Δ i A},
     {{ Γ ⊩s σ : Δ }} ->