From c04989587d541cd05efca295a46f5e475c2b8c27 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Sun, 15 Dec 2024 11:00:39 -0800
Subject: [PATCH] proved semantic rule for refl

---
 theories/Core/Soundness/EqualityCases.v       | 30 +++++++++++++++++--
 .../Core/Soundness/LogicalRelation/Lemmas.v   | 24 +++++++++++++++
 2 files changed, 51 insertions(+), 3 deletions(-)

diff --git a/theories/Core/Soundness/EqualityCases.v b/theories/Core/Soundness/EqualityCases.v
index 48ae372..e4ec7f7 100644
--- a/theories/Core/Soundness/EqualityCases.v
+++ b/theories/Core/Soundness/EqualityCases.v
@@ -62,12 +62,36 @@ 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;
+      try (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.
diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
index 4e86989..0c1b6b4 100644
--- a/theories/Core/Soundness/LogicalRelation/Lemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -1234,6 +1234,7 @@ Ltac invert_glu_rel_exp H :=
      destruct H as [])
   + (inversion H; subst).
 
+
 Lemma glu_rel_exp_to_wf_exp : forall {Γ A M},
     {{ Γ ⊩ M : A }} ->
     {{ Γ ⊢ M : A }}.
@@ -1360,3 +1361,26 @@ Ltac applying_glu_rel_judge :=
   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.