From 9ffb2e4b614a023566bc920339e820cbbda143e7 Mon Sep 17 00:00:00 2001
From: Jad Ghalayini <jad.ghalayini@protonmail.com>
Date: Fri, 6 Sep 2024 17:20:20 +0100
Subject: [PATCH] Work on lsubst lore

---
 .../BinSyntax/Rewrite/Region/LSubst.lean      | 45 ++++++++++++++++++-
 .../BinSyntax/Rewrite/Region/Setoid.lean      | 17 ++++---
 .../Syntax/Rewrite/Region/Reduce.lean         | 16 +++++++
 .../Syntax/Rewrite/Region/Rewrite.lean        | 20 ++++++++-
 .../BinSyntax/Typing/Region/LSubst.lean       |  4 +-
 5 files changed, 93 insertions(+), 9 deletions(-)

diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/LSubst.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/LSubst.lean
index 1504c67..e6dee69 100644
--- a/DeBruijnSSA/BinSyntax/Rewrite/Region/LSubst.lean
+++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/LSubst.lean
@@ -15,8 +15,51 @@ instance Subst.InS.instSetoid {Γ : Ctx α ε} {L K : LCtx α}
     trans := (λhl hr i => Setoid.trans (hl i) (hr i))
   }
 
+theorem Subst.InS.vlift_congr {Γ : Ctx α ε} {L K : LCtx α}
+  {σ τ : Subst.InS φ Γ L K} (h : σ ≈ τ) : σ.vlift (head := head) ≈ τ.vlift
+  := sorry
+
+theorem Subst.InS.vliftn₂_congr {Γ : Ctx α ε} {L K : LCtx α}
+  {σ τ : Subst.InS φ Γ L K} (h : σ ≈ τ) : σ.vliftn₂ (left := left) (right := right) ≈ τ.vliftn₂
+  := by simp only [vliftn₂_eq_vlift_vlift]; exact vlift_congr <| vlift_congr h
+
+theorem Subst.InS.liftn_append_congr {Γ : Ctx α ε} {L K J : LCtx α}
+  {σ τ : Subst.InS φ Γ L K} (h : σ ≈ τ) : σ.liftn_append J ≈ τ.liftn_append J := by
+  intro i
+  simp only [List.get_eq_getElem, get, liftn_append, liftn]
+  split
+  · rfl
+  · stop
+    convert InS.lwk_congr_right _ (h ⟨i - J.length, sorry⟩) using 1
+    sorry
+    sorry
+    sorry
+    sorry
+    sorry
+
+open Subst.InS
+
 theorem InS.lsubst_congr_subst {Γ : Ctx α ε} {L K : LCtx α} {σ τ : Subst.InS φ Γ L K}
-  (h : σ ≈ τ) (r : InS φ Γ L) : r.lsubst σ ≈ r.lsubst τ := sorry
+  (h : σ ≈ τ) (r : InS φ Γ L) : r.lsubst σ ≈ r.lsubst τ := by
+  induction r using InS.induction generalizing K with
+  | br ℓ a hℓ =>
+    simp only [lsubst_br, List.get_eq_getElem, vwk_id_eq_vwk]
+    apply InS.vsubst_congr_right
+    apply InS.vwk_congr_right
+    apply h
+  | case e r s Ir Is =>
+    simp only [lsubst_case]
+    exact InS.case_congr (by rfl) (Ir (vlift_congr h)) (Is (vlift_congr h))
+  | let1 a r Ir =>
+    simp only [lsubst_let1]
+    exact InS.let1_congr (by rfl) (Ir (vlift_congr h))
+  | let2 a r Ir =>
+    simp only [lsubst_let2]
+    exact InS.let2_congr (by rfl) (Ir (vliftn₂_congr h))
+  | cfg R β G Iβ IG =>
+    simp only [lsubst_cfg]
+    exact InS.cfg_congr _ (Iβ (liftn_append_congr h))
+      (λi => IG i (vlift_congr (liftn_append_congr h)))
 
 theorem InS.lsubst_congr_right {Γ : Ctx α ε} {L K : LCtx α} (σ : Subst.InS φ Γ L K)
   {r r' : InS φ Γ L} (h : r ≈ r') : r.lsubst σ ≈ r'.lsubst σ := sorry
diff --git a/DeBruijnSSA/BinSyntax/Rewrite/Region/Setoid.lean b/DeBruijnSSA/BinSyntax/Rewrite/Region/Setoid.lean
index c511dc6..34957ad 100644
--- a/DeBruijnSSA/BinSyntax/Rewrite/Region/Setoid.lean
+++ b/DeBruijnSSA/BinSyntax/Rewrite/Region/Setoid.lean
@@ -156,11 +156,18 @@ theorem InS.initial' {Γ : Ctx α ε} (i : Term.InS φ Γ ⟨Ty.empty, ⊥⟩) (
 
 theorem TStep.vsubst {Γ Δ : Ctx α ε} {L} {r r' : Region φ} {σ : Term.Subst φ}
   (hσ : σ.Wf Γ Δ) : TStep Δ L r r' → Uniform TStep Γ L (r.vsubst σ) (r'.vsubst σ)
-  | TStep.let1_beta de dr => sorry
-  | TStep.rewrite d d' p => sorry
-  | TStep.reduce d d' p => sorry
-  | TStep.initial di d d' => sorry
-  | TStep.let1_equiv p dr => sorry
+  | let1_beta de dr => Uniform.rel <| by
+    convert let1_beta (de.subst hσ) (dr.vsubst hσ.slift) using 1
+    simp only [vsubst_vsubst]
+    congr; funext k; cases k <;> simp [Term.Subst.comp]
+  | rewrite d d' p => Uniform.rel (rewrite (d.vsubst hσ) (d'.vsubst hσ) (p.vsubst σ))
+  | reduce d d' p => Uniform.rel (reduce (d.vsubst hσ) (d'.vsubst hσ) (p.vsubst σ))
+  | initial di d d' =>
+    let ⟨di⟩ := di.term (φ := φ);
+    InS.initial' (di.subst ⟨_, hσ⟩) ⟨_, d.vsubst hσ⟩ ⟨_, d'.vsubst hσ⟩
+  | let1_equiv p dr => Uniform.rel <| let1_equiv
+    (Term.Uniform.subst_flatten Term.TStep.subst hσ p)
+    (dr.vsubst hσ.slift)
 
 theorem TStep.vsubst_to_congr {Γ Δ : Ctx α ε} {L}
   {r r' : InS φ Δ L} (σ : Term.Subst.InS φ Γ Δ) (h : TStep Δ L (r : Region φ) (↑r'))
diff --git a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Reduce.lean b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Reduce.lean
index 1fd4ada..ecbed09 100644
--- a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Reduce.lean
+++ b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Reduce.lean
@@ -149,6 +149,22 @@ def ReduceD.lwk {r r' : Region φ} (ρ : ℕ → ℕ) (d : ReduceD r r') : Reduc
 theorem Reduce.lwk {r r' : Region φ} (ρ : ℕ → ℕ) (p : Reduce r r') : Reduce (r.lwk ρ) (r'.lwk ρ)
   := let ⟨d⟩ := p.nonempty; (d.lwk ρ).reduce
 
+def ReduceD.vsubst {r r' : Region φ} (σ : Term.Subst φ) (d : ReduceD r r')
+  : ReduceD (r.vsubst σ) (r'.vsubst σ)
+  := sorry
+
+theorem Reduce.vsubst
+  {r r' : Region φ} (σ : Term.Subst φ) (p : Reduce r r') : Reduce (r.vsubst σ) (r'.vsubst σ)
+  := let ⟨d⟩ := p.nonempty; (d.vsubst σ).reduce
+
+def ReduceD.lsubst {r r' : Region φ} (σ : Subst φ) (d : ReduceD r r')
+  : ReduceD (r.lsubst σ) (r'.lsubst σ)
+  := sorry
+
+theorem Reduce.lsubst
+  {r r' : Region φ} (σ : Subst φ) (p : Reduce r r') : Reduce (r.lsubst σ) (r'.lsubst σ)
+  := let ⟨d⟩ := p.nonempty; (d.lsubst σ).reduce
+
 theorem ReduceD.effect_le {Γ : ℕ → ε} {r r' : Region φ} (p : ReduceD r r')
   : r'.effect Γ ≤ r.effect Γ := by
   cases p with
diff --git a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Rewrite.lean b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Rewrite.lean
index 6597b33..1ac7cd9 100644
--- a/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Rewrite.lean
+++ b/DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Rewrite.lean
@@ -451,4 +451,22 @@ def RewriteD.lwk {r r' : Region φ} (ρ : ℕ → ℕ) (d : RewriteD r r') : Rew
 theorem Rewrite.lwk {r r' : Region φ} (ρ : ℕ → ℕ) (p : Rewrite r r') : Rewrite (r.lwk ρ) (r'.lwk ρ)
   := let ⟨d⟩ := p.nonempty; (d.lwk ρ).rewrite
 
--- TODO: vsubst, lsubst
+def RewriteD.vsubst {r r' : Region φ} (σ : Term.Subst φ) (p : Rewrite r r')
+  : RewriteD (r.vsubst σ) (r'.vsubst σ)
+  := sorry
+
+theorem Rewrite.vsubst {r r' : Region φ} (σ : Term.Subst φ) (p : Rewrite r r')
+  : Rewrite (r.vsubst σ) (r'.vsubst σ)
+  := sorry
+
+def RewriteD.lsubst {r r' : Region φ} (σ : Subst φ) (p : Rewrite r r')
+  : RewriteD (r.lsubst σ) (r'.lsubst σ)
+  := sorry
+
+theorem Rewrite.lsubst {r r' : Region φ} (σ : Subst φ) (p : Rewrite r r')
+  : Rewrite (r.lsubst σ) (r'.lsubst σ)
+  := sorry
+
+end Region
+
+end BinSyntax
diff --git a/DeBruijnSSA/BinSyntax/Typing/Region/LSubst.lean b/DeBruijnSSA/BinSyntax/Typing/Region/LSubst.lean
index 4c9569f..4da1404 100644
--- a/DeBruijnSSA/BinSyntax/Typing/Region/LSubst.lean
+++ b/DeBruijnSSA/BinSyntax/Typing/Region/LSubst.lean
@@ -526,7 +526,7 @@ theorem Region.InS.lsubst_br {Γ : Ctx α ε} {L K : LCtx α} {σ : Subst.InS φ
 
 @[simp]
 theorem Region.InS.lsubst_case {Γ : Ctx α ε} {L K : LCtx α} {σ : Subst.InS φ Γ L K}
-  {e : Term.InS φ Γ (A.coprod B, ⊥)}
+  {e : Term.InS φ Γ (A.coprod B, e)}
   {s : Region.InS φ ((A, ⊥)::Γ) L} {t : Region.InS φ ((B, ⊥)::Γ) L}
   : (case e s t).lsubst σ = case e (s.lsubst σ.vlift) (t.lsubst σ.vlift)
   := rfl
@@ -599,7 +599,7 @@ theorem Region.InS.extend_comp {Γ : Ctx α ε} {L K J R : LCtx α}
   simp only [Set.mem_setOf_eq, Subst.InS.coe_extend, Subst.InS.coe_comp, Subst.comp, Subst.extend]
   split
   · simp [Subst.vlift]
-    sorry -- TODO: fv_eq lore...
+    sorry -- TODO: fl_eq lore...
   · simp [Subst.vlift]
 
 theorem Region.Wf.csubst {Γ : Ctx α ε} {L : LCtx α} {r : Region φ} {hr : Wf ((A, ⊥)::Γ) r L}