From c24cc7c9b0c65dd705ec1332837b0ebf96f85a44 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <liuyiyun@seas.upenn.edu>
Date: Thu, 6 Feb 2025 00:08:02 -0500
Subject: [PATCH] Finish ST Conv

---
 theories/fp_red.v | 46 ++++++++++++++++++++++++++++++++++++++++++++++
 theories/logrel.v | 15 +++++++++++++++
 2 files changed, 61 insertions(+)

diff --git a/theories/fp_red.v b/theories/fp_red.v
index 5af61f4..e22e759 100644
--- a/theories/fp_red.v
+++ b/theories/fp_red.v
@@ -107,6 +107,10 @@ Module EPar.
     all : hauto lq:on ctrs:R use:morphing_up.
   Qed.
 
+  Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) :
+    R a b -> R (subst_PTm ρ a) (subst_PTm ρ b).
+  Proof. hauto l:on use:morphing, refl. Qed.
+
 End EPar.
 
 Inductive SNe {n} : PTm n -> Prop :=
@@ -572,6 +576,15 @@ Module RRed.
     RRed.R a b.
   Proof. induction 1; hauto lq:on ctrs:RRed.R. Qed.
 
+  Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) :
+    R a b -> R (subst_PTm ρ a) (subst_PTm ρ b).
+  Proof.
+    move => h. move : m ρ. elim : n a b / h => n.
+    move => a b m ρ /=.
+    eapply AppAbs'; eauto; cycle 1. by asimpl.
+    all : hauto lq:on ctrs:R.
+  Qed.
+
 End RRed.
 
 Module RPar.
@@ -1482,6 +1495,15 @@ Module ERed.
       sauto lq:on.
   Admitted.
 
+  Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) :
+    R a b -> R (subst_PTm ρ a) (subst_PTm ρ b).
+  Proof.
+    move => h. move : m ρ. elim : n a b /h => n.
+    move => a m ρ /=.
+    eapply AppEta'; eauto. by asimpl.
+    all : hauto lq:on ctrs:R.
+  Qed.
+
 End ERed.
 
 Module EReds.
@@ -1546,6 +1568,12 @@ Module EReds.
     rtc ERed.R a b.
   Proof. induction 1; hauto l:on use:FromEPar, @relations.rtc_transitive. Qed.
 
+  Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) :
+    rtc ERed.R a b -> rtc ERed.R (subst_PTm ρ a) (subst_PTm ρ b).
+  Proof.
+    induction 1; hauto lq:on ctrs:rtc use:ERed.substing.
+  Qed.
+
 End EReds.
 
 #[export]Hint Constructors ERed.R RRed.R EPar.R : red.
@@ -1632,6 +1660,12 @@ Module RERed.
     hauto q:on use:ToBetaEtaPar, RPar.FromRRed use:red_sn_preservation, epar_sn_preservation.
   Qed.
 
+  Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) :
+    RERed.R a b -> RERed.R (subst_PTm ρ a) (subst_PTm ρ b).
+  Proof.
+    hauto q:on use:ToBetaEta, FromBeta, FromEta, RRed.substing, ERed.substing.
+  Qed.
+
 End RERed.
 
 Module REReds.
@@ -1716,6 +1750,12 @@ Module REReds.
     hauto lq:on rew:off ctrs:rtc inv:RERed.R.
   Qed.
 
+  Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) :
+    rtc RERed.R a b -> rtc RERed.R (subst_PTm ρ a) (subst_PTm ρ b).
+  Proof.
+    induction 1; hauto lq:on ctrs:rtc use:RERed.substing.
+  Qed.
+
 End REReds.
 
 Module LoRed.
@@ -2207,4 +2247,10 @@ Module DJoin.
     hauto lq:on ctrs:rtc use:REReds.FromRReds unfold:R.
   Qed.
 
+  Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) :
+    R a b -> R (subst_PTm ρ a) (subst_PTm ρ b).
+  Proof.
+    hauto lq:on rew:off ctrs:rtc unfold:R use:REReds.substing.
+  Qed.
+
 End DJoin.
diff --git a/theories/logrel.v b/theories/logrel.v
index e88449b..5377dfb 100644
--- a/theories/logrel.v
+++ b/theories/logrel.v
@@ -735,3 +735,18 @@ Proof.
       hauto lq:on ctrs:rtc unfold:BJoin.R.
     + hauto lq:on use:@relations.rtc_r, InterpUniv_back_closs.
 Qed.
+
+Lemma ST_Conv n Γ (a : PTm n) A B i :
+  Γ ⊨ a ∈ A ->
+  Γ ⊨ B ∈ PUniv i ->
+  DJoin.R A B ->
+  Γ ⊨ a ∈ B.
+Proof.
+  move => ha /SemWt_Univ h h0.
+  move => ρ hρ.
+  have {}h0 : DJoin.R (subst_PTm ρ A) (subst_PTm ρ B) by eauto using DJoin.substing.
+  move /ha : (hρ){ha} => [m [PA [h1 h2]]].
+  move /h : (hρ){h} => [S hS].
+  have ? : PA = S by eauto using InterpUniv_Join'. subst.
+  eauto.
+Qed.