Began work on lsubst sorries

DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Structural.lean

@@ -130,6 +130,17 @@ theorem Subst.Eqv.pack_comp_unpack {Γ : Ctx α ε} {R : LCtx α}
     get_id, Fin.coe_fin_one]
   rfl
 
+def Eqv.unpacked {Γ : Ctx α ε} {R : LCtx α} (h : Eqv φ Γ [R.pack]) : Eqv φ Γ R
+  := h.lsubst Subst.Eqv.unpack
+
+def Eqv.packed {Γ : Ctx α ε} {R : LCtx α} (h : Eqv φ Γ R) : Eqv φ Γ [R.pack]
+  := h.lsubst Subst.Eqv.pack
+
+theorem Eqv.unpacked_packed {Γ : Ctx α ε} {R : LCtx α} (h : Eqv φ Γ R)
+  : h.packed.unpacked = h := by
+  rw [Eqv.unpacked, packed, lsubst_lsubst, Subst.Eqv.unpack_comp_pack]
+  sorry
+
 end Region
 
 end BinSyntax

DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean

@@ -1169,6 +1169,22 @@ theorem Eqv.cfg_zero {Γ : Ctx α ε} {L : LCtx α}
 
 -- TODO: case_eta
 
+-- TODO: factor out to discretion as general helper...
+
+theorem Eqv.choiceInduction {ι : Type _} {Γs : ι → Ctx α ε} {L : LCtx α}
+  (motive : ((i : ι) → Eqv φ (Γs i) L) → Prop)
+  (choice : ∀G : (i : ι) → InS φ (Γs i) L, motive (λi => ⟦G i⟧))
+  : ∀G : (i : ι) → Eqv φ (Γs i) L, motive G
+  := λG => by
+  generalize hG : Quotient.choice G = G'
+  induction G' using Quotient.inductionOn with
+  | h G' =>
+    have hG := Quotient.forall_of_choice_eq hG
+    have hG' : G = λi => G i := rfl
+    rw [hG']
+    simp only [hG]
+    apply choice
+
 theorem Eqv.wk_cfg {Γ : Ctx α ε} {L : LCtx α}
   (R S : LCtx α) (β : Eqv φ Γ (R ++ L))
   (G : (i : Fin S.length) → Eqv φ ((List.get S i, ⊥)::Γ) (R ++ L))
@@ -1177,17 +1193,12 @@ theorem Eqv.wk_cfg {Γ : Ctx α ε} {L : LCtx α}
   : cfg S (β.lwk ⟨Fin.toNatWk ρ, hρ⟩) (λi => (G i).lwk ⟨Fin.toNatWk ρ, hρ⟩)
   = cfg R β (λi => (G (ρ i)).vwk_id (Ctx.Wkn.id.toFinWk_id hρ i))
   := by
-  induction β using Quotient.inductionOn with
-  | h β =>
-    simp only [cfg]
-    generalize hG : Quotient.finChoice G = G'
-    induction G' using Quotient.inductionOn with
-    | h G' =>
-      have hG := Quotient.forall_of_finChoice_eq hG
-      simp only [Set.mem_setOf_eq, lwk_quot, List.get_eq_getElem, hG, Fin.getElem_fin, vwk_id_quot,
-        Quotient.finChoice_eq, Eqv.cfg_inner_quot]
-      apply Eqv.sound
-      apply InS.wk_cfg
+  induction β using Quotient.inductionOn
+  induction G using Eqv.choiceInduction
+  simp only [cfg, Set.mem_setOf_eq, lwk_quot, List.get_eq_getElem, Fin.getElem_fin, vwk_id_quot,
+    Quotient.finChoice_eq, Eqv.cfg_inner_quot]
+  apply Eqv.sound
+  apply InS.wk_cfg
 
 theorem Eqv.let1_let1_case {Γ : Ctx α ε}
   {a : Term.Eqv φ Γ ⟨Ty.coprod A B, e⟩}

DeBruijnSSA/BinSyntax/Rewrite/Region/LSubst.lean

@@ -66,6 +66,16 @@ theorem Subst.InS.liftn_append_congr {Γ : Ctx α ε} {L K J : LCtx α}
     rw [List.getElem_append_right _ _ h']
     apply heq_prop
 
+theorem Subst.InS.slift_congr {Γ : Ctx α ε} {L K : LCtx α}
+  {σ τ : Subst.InS φ Γ L K} (h : σ ≈ τ) : σ.slift (head := head) ≈ τ.slift
+  := λi => by cases i using Fin.cases with
+  | zero => rfl
+  | succ i =>
+    simp only [List.get_eq_getElem, List.length_cons, Fin.val_succ, List.getElem_cons_succ,
+      get_slift_succ, InS.lwk0]
+    apply InS.lwk_congr_right
+    apply h
+
 theorem Subst.InS.extend_congr {Γ : Ctx α ε} {L K R : LCtx α}
   {σ τ : Subst.InS φ Γ L K} (h : σ ≈ τ) : σ.extend (R := R) ≈ τ.extend
   := λi => by
@@ -109,7 +119,8 @@ theorem InS.lsubst_congr_subst {Γ : Ctx α ε} {L K : LCtx α} {σ τ : Subst.I
       (λ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
+  {r r' : InS φ Γ L} (h : r ≈ r') : r.lsubst σ ≈ r'.lsubst σ
+  := Uniform.lsubst TStep.lsubst σ.prop h
 
 theorem InS.lsubst_congr {Γ : Ctx α ε} {L K : LCtx α} {σ σ' : Subst.InS φ Γ L K}
   {r r' : InS φ Γ L} (hσ : σ ≈ σ') (hr : r ≈ r') : r.lsubst σ ≈ r'.lsubst σ'
@@ -208,7 +219,8 @@ theorem Eqv.lsubst_toSubst {Γ : Ctx α ε} {L K : LCtx α} {σ : LCtx.InS L K}
   simp [InS.lsubst_toSubst]
 
 def Subst.Eqv.comp {Γ : Ctx α ε} {L K J : LCtx α} (σ : Subst.Eqv φ Γ K J) (τ : Subst.Eqv φ Γ L K)
-  : Subst.Eqv φ Γ L J := Quotient.liftOn₂ σ τ (λσ τ => ⟦σ.comp τ⟧) sorry
+  : Subst.Eqv φ Γ L J := Quotient.liftOn₂ σ τ (λσ τ => ⟦σ.comp τ⟧)
+    (λ_ _ _ _ hσ hτ => Quotient.sound (Subst.InS.comp_congr hσ hτ))
 
 @[simp]
 theorem Subst.Eqv.comp_quot {Γ : Ctx α ε} {L K : LCtx α} {J : LCtx α}
@@ -274,7 +286,7 @@ def Subst.Eqv.slift {Γ : Ctx α ε} {L K : LCtx α} (σ : Subst.Eqv φ Γ L K)
   : Subst.Eqv φ Γ (head::L) (head::K)
   := Quotient.liftOn σ
     (λσ => ⟦σ.slift⟧)
-    sorry
+    (λ_ _ h => Quotient.sound (Subst.InS.slift_congr h))
 
 @[simp]
 theorem Subst.Eqv.slift_quot {Γ : Ctx α ε} {L K : LCtx α} {σ : Subst.InS φ Γ L K}
@@ -317,7 +329,7 @@ def Subst.Eqv.liftn_append {Γ : Ctx α ε} {L K : LCtx α} (J) (σ : Subst.Eqv
   : Subst.Eqv φ Γ (J ++ L) (J ++ K)
   := Quotient.liftOn σ
     (λσ => ⟦σ.liftn_append J⟧)
-    sorry
+    (λ_ _ h => Quotient.sound <| Subst.InS.liftn_append_congr h)
 
 theorem Subst.Eqv.vwk1_lsubst_vlift {Γ : Ctx α ε} {L K : LCtx α}
   {σ : Subst.Eqv φ Γ L K} {r : Region.Eqv φ (head::Γ) L}
@@ -356,8 +368,18 @@ theorem Eqv.lsubst_cfg {Γ : Ctx α ε} {L : LCtx α}
   {σ : Subst.Eqv φ Γ L K}
   : (cfg R β G).lsubst σ
   = cfg R (β.lsubst (σ.liftn_append _)) (λi => (G i).lsubst (σ.liftn_append _).vlift) := by
+  induction σ using Quotient.inductionOn
   induction β using Quotient.inductionOn
-  sorry
+  generalize hG : Quotient.finChoice G = G'
+  induction G' using Quotient.inductionOn with
+  | h G' =>
+    have hG := Quotient.forall_of_finChoice_eq hG
+    have hG' : G = (λi => G i) := rfl
+    simp only [cfg]
+    rw [hG']
+    simp only [Set.mem_setOf_eq, lsubst_quot, List.get_eq_getElem, hG, Fin.getElem_fin, vwk_id_quot,
+      Subst.Eqv.liftn_append_quot, Subst.Eqv.vlift_quot, Quotient.finChoice_eq, Eqv.cfg_inner_quot]
+    rfl
 
 def Subst.Eqv.vsubst {Γ Δ : Ctx α ε} {L K : LCtx α}
   (ρ : Term.Subst.Eqv φ Γ Δ) (σ : Subst.Eqv φ Δ L K) : Subst.Eqv φ Γ L K
@@ -631,3 +653,12 @@ theorem Subst.Eqv.comp_id {Γ : Ctx α ε} {L : LCtx α} {σ : Subst.Eqv φ Γ L
 theorem Subst.Eqv.get_id {Γ : Ctx α ε} {L : LCtx α} {i : Fin L.length}
   : (id : Subst.Eqv φ Γ L L).get i = Eqv.br i (Term.Eqv.var 0 Ctx.Var.shead) (by simp) := by
   rfl
+
+@[simp]
+theorem Eqv.lsubst_id {Γ : Ctx α ε} {L : LCtx α} {r : Eqv φ Γ L}
+  : r.lsubst Subst.Eqv.id = r := by
+  induction r using Quotient.inductionOn
+  simp [Subst.Eqv.id]
+
+theorem Eqv.lsubst_id' {Γ : Ctx α ε} {L : LCtx α} {r : Eqv φ Γ L} {σ : Subst.Eqv φ Γ L L}
+  (h : σ = Subst.Eqv.id) : r.lsubst σ = r := by cases h; simp

DeBruijnSSA/BinSyntax/Rewrite/Region/Step.lean

@@ -200,7 +200,7 @@ theorem TStep.vwk {Γ Δ : Ctx α ε} {L r r' ρ} (hρ : Γ.Wkn Δ ρ)
   | rewrite d d' p => rewrite (d.vwk hρ) (d'.vwk hρ) (p.vwk ρ)
   | reduce d d' p => reduce (d.vwk hρ) (d'.vwk hρ) (p.vwk ρ)
   | initial di d d' => initial (di.wk hρ) (d.vwk hρ) (d'.vwk hρ)
-  | let1_equiv da dr => let1_equiv (da.wk sorry hρ) (dr.vwk hρ.slift)
+  | let1_equiv da dr => let1_equiv (Term.Uniform.wk Term.TStep.wk hρ da) (dr.vwk hρ.slift)
 
 theorem TStep.lwk {Γ : Ctx α ε} {L K r r' ρ} (hρ : L.Wkn K ρ)
   : TStep (φ := φ) Γ L r r' → TStep Γ K (r.lwk ρ) (r'.lwk ρ)
@@ -214,9 +214,15 @@ theorem TStep.lwk {Γ : Ctx α ε} {L K r r' ρ} (hρ : L.Wkn K ρ)
 
 theorem TStep.lsubst {Γ : Ctx α ε} {L K} {r r' : Region φ} {σ : Subst φ}
   (hσ : σ.Wf Γ L K) : (h : TStep Γ L r r') → TStep Γ K (r.lsubst σ) (r'.lsubst σ)
-  | let1_beta de dr => (let1_beta de (dr.lsubst hσ.vlift)).cast_trg sorry
-  | rewrite d d' p => sorry--rewrite (d.lsubst hσ) (d'.lsubst hσ) (p.lsubst σ)
-  | reduce d d' p => sorry
+  | let1_beta de dr => (let1_beta de (dr.lsubst hσ.vlift)).cast_trg (by
+    --TODO: factor out...
+    rw [vsubst_lsubst]; congr; funext k
+    simp only [Subst.vlift, vwk1, ← vsubst_fromWk, Function.comp_apply, vsubst_vsubst]
+    apply vsubst_id'
+    funext k; cases k <;> rfl
+  )
+  | rewrite d d' p => rewrite (d.lsubst hσ) (d'.lsubst hσ) (p.lsubst σ)
+  | reduce d d' p => reduce (d.lsubst hσ) (d'.lsubst hσ) (p.lsubst σ)
   | initial di d d' => initial di (d.lsubst hσ) (d'.lsubst hσ)
   | let1_equiv da dr => let1_equiv da (dr.lsubst hσ.vlift)
 

DeBruijnSSA/BinSyntax/Rewrite/Region/Uniform.lean

@@ -434,6 +434,12 @@ theorem Uniform.vsubst_flatten {P : Ctx α ε → LCtx α → Region φ → Regi
   (p : (Uniform P Δ L) r r') : Uniform P Γ L (r.vsubst σ) (r'.vsubst σ)
   := (p.vsubst (Q := Uniform P) toVsubst hσ).flatten
 
+theorem Uniform.lsubst_flatten {P : Ctx α ε → LCtx α → Region φ → Region φ → Prop} {Γ L K r r'}
+  (toLsubst : ∀{Γ L K σ r r'}, σ.Wf Γ L K → P Γ L r r' → Uniform P Γ K (r.lsubst σ) (r'.lsubst σ))
+  (hσ : σ.Wf Γ L K)
+  (p : (Uniform P Γ L) r r') : Uniform P Γ K (r.lsubst σ) (r'.lsubst σ)
+  := (p.lsubst (Q := Uniform P) toLsubst hσ).flatten
+
 def Uniform.Setoid (P : Ctx α ε → LCtx α → Region φ → Region φ → Prop) (Γ : Ctx α ε) (L : LCtx α)
   : Setoid (InS φ Γ L) where
   r x y := Uniform P Γ L x y

DeBruijnSSA/BinSyntax/Typing/Region/LSubst.lean

@@ -450,6 +450,13 @@ theorem Region.InS.coe_lsubst {Γ : Ctx α ε} (σ : Region.Subst.InS φ Γ L K)
   : (r.lsubst σ : Region φ) = (r : Region φ).lsubst σ
   := rfl
 
+@[simp]
+theorem Region.InS.lsubst_id {Γ : Ctx α ε} {L : LCtx α} {r : InS φ Γ L}
+  : r.lsubst Subst.InS.id = r := by ext; simp
+
+theorem Region.InS.lsubst_id' {Γ : Ctx α ε} {L : LCtx α} {r : InS φ Γ L} {σ : Subst.InS φ Γ L L}
+  (h : σ = Subst.InS.id) : r.lsubst σ = r := by cases h; simp
+
 def Region.Subst.WfD.comp {Γ : Ctx α ε} {σ : Region.Subst φ} {τ : Region.Subst φ}
   (hσ : σ.WfD Γ K J) (hτ : τ.WfD Γ L K) : (σ.comp τ).WfD Γ L J
   := λi => (hτ i).lsubst hσ.vlift