From 86f48d948352683b1c6c28413db5d1d2894c5d0d Mon Sep 17 00:00:00 2001
From: "Junyoung/\"Clare\" Jang" <jjc9310@gmail.com>
Date: Mon, 29 Jul 2024 11:08:17 -0400
Subject: [PATCH] Provide more soundness lemmas (#141)

* Prove more

* Add placeholders for monotonicities of gluing model predicates
---
 .../Soundness/LogicalRelation/Definitions.v   |  5 +-
 .../Core/Soundness/LogicalRelation/Lemmas.v   | 54 +++++++++++++++++++
 2 files changed, 55 insertions(+), 4 deletions(-)

diff --git a/theories/Core/Soundness/LogicalRelation/Definitions.v b/theories/Core/Soundness/LogicalRelation/Definitions.v
index 32e0376e..9cc28eed 100644
--- a/theories/Core/Soundness/LogicalRelation/Definitions.v
+++ b/theories/Core/Soundness/LogicalRelation/Definitions.v
@@ -303,13 +303,10 @@ Variant cons_glu_sub_pred i Γ A (TSb : glu_sub_pred) : glu_sub_pred :=
 | mk_cons_glu_sub_pred :
   `{ forall P El,
         {{ Δ ⊢s σ : Γ, A }} ->
-        (* Do we need the following argument?
-           In other words, is it possible to prove that "TSb" respects
-           wf_sub_eq without the following condition? *)
-        {{ Δ ⊢s Wk ∘ σ ≈ Wk∘σ : Γ }} ->
         {{ ⟦ A ⟧ ρ ↯ ↘ a }} ->
         {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
         {{ Δ ⊢ #0[σ] : A[Wk∘σ] ® ~(ρ 0) ∈ El }} ->
+        {{ Δ ⊢s Wk ∘ σ ® ρ ↯ ∈ TSb }} ->
         {{ Δ ⊢s σ ® ρ ∈ cons_glu_sub_pred i Γ A TSb }} }.
 
 Inductive glu_ctx_env : glu_sub_pred -> ctx -> Prop :=
diff --git a/theories/Core/Soundness/LogicalRelation/Lemmas.v b/theories/Core/Soundness/LogicalRelation/Lemmas.v
index 0d25e497..bb5c5a2b 100644
--- a/theories/Core/Soundness/LogicalRelation/Lemmas.v
+++ b/theories/Core/Soundness/LogicalRelation/Lemmas.v
@@ -619,3 +619,57 @@ Proof.
   - do 2 eexists.
     glu_univ_elem_econstructor; try reflexivity; mauto.
 Qed.
+
+(* TODO: strengthen the result (implication from P to P' / El to El') *)
+Lemma glu_univ_elem_cumu_ge : forall {i j a P El},
+    i <= j ->
+    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    exists P' El', {{ DG a ∈ glu_univ_elem j ↘ P' ↘ El' }}.
+Proof.
+  simpl.
+  intros * Hge Hglu. gen j.
+  induction Hglu using glu_univ_elem_ind; intros;
+    handle_functional_glu_univ_elem; try solve [do 2 eexists; glu_univ_elem_econstructor; try (reflexivity + lia); mauto].
+
+  edestruct IHHglu; [eassumption |].
+  destruct_conjs.
+  do 2 eexists.
+  glu_univ_elem_econstructor; try reflexivity; mauto.
+  instantiate (1 := fun c equiv_c Γ M A m => forall b Pb Elb,
+                        {{ ⟦ B ⟧ p ↦ c ↘ b }} ->
+                        glu_univ_elem j Pb Elb b ->
+                        {{ Γ ⊢ M : A ® m ∈ Elb }}).
+  instantiate (1 := fun c equiv_c Γ A => forall b Pb Elb,
+                        {{ ⟦ B ⟧ p ↦ c ↘ b }} ->
+                        glu_univ_elem j Pb Elb b ->
+                        {{ Γ ⊢ A ® Pb }}).
+  intros.
+  assert (exists (P' : ctx -> typ -> Prop) (El' : ctx -> typ -> typ -> domain -> Prop), glu_univ_elem j P' El' b) as [] by mauto.
+  destruct_conjs.
+  rewrite simple_glu_univ_elem_morphism_iff; try (eassumption + reflexivity);
+    split; intros; handle_functional_glu_univ_elem; intuition.
+Qed.
+
+Lemma glu_univ_elem_typ_monotone : forall {i a P El Δ σ Γ A},
+    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    {{ Γ ⊢ A ® P }} ->
+    {{ Δ ⊢w σ : Γ }} ->
+    {{ Δ ⊢ A[σ] ® P }}.
+Admitted.
+
+Lemma glu_univ_elem_exp_monotone : forall {i a P El Δ σ Γ M A m},
+    {{ DG a ∈ glu_univ_elem i ↘ P ↘ El }} ->
+    {{ Γ ⊢ M : A ® m ∈ El }} ->
+    {{ Δ ⊢w σ : Γ }} ->
+    {{ Δ ⊢ M[σ] : A[σ] ® m ∈ El }}.
+Admitted.
+
+(* Simple Morphism instance for "glu_ctx_env" *)
+Add Parametric Morphism : glu_ctx_env
+    with signature glu_sub_pred_equivalence ==> eq ==> iff as simple_glu_ctx_env_morphism_iff.
+Proof with mautosolve.
+  intros Sb Sb' HSbSb' a.
+  split; intro Horig; [gen Sb' | gen Sb];
+    induction Horig; econstructor;
+    try (etransitivity; [symmetry + idtac|]; eassumption); eauto.
+Qed.