Reduced packed_cfg_split to distributivity lore

DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean

@@ -823,7 +823,8 @@ theorem Eqv.vsubst0_var0_vwk1 {Γ : Ctx α ε} {L : LCtx α} {r : Eqv φ (head::
   : (r.vwk1 (inserted := _)).vsubst (Term.Eqv.var 0 Ctx.Var.shead).subst0 = r := by
   induction r using Quotient.inductionOn
   apply eq_of_reg_eq
-  simp
+  simp only [Set.mem_setOf_eq, InS.coe_vsubst, Term.InS.coe_subst0, Term.InS.coe_var, InS.coe_vwk,
+    Ctx.InS.coe_wk1]
   exact Region.vsubst0_var0_vwk1 _
 
 def Eqv.vswap01

DeBruijnSSA/BinSyntax/Rewrite/Region/LSubst.lean

@@ -459,6 +459,12 @@ theorem Subst.Eqv.vwk_quot {Γ Δ : Ctx α ε} {L K : LCtx α}
   {ρ : Γ.InS Δ} {σ : Subst.InS φ Δ L K}
   : vwk ρ ⟦σ⟧ = ⟦σ.vwk ρ⟧ := rfl
 
+theorem Subst.Eqv.get_vwk {Γ Δ : Ctx α ε} {L K : LCtx α}
+  {ρ : Γ.InS Δ} {σ : Subst.Eqv φ Δ L K} {i : Fin L.length}
+  : (σ.vwk ρ).get i = (σ.get i).vwk ρ.slift := by
+  induction σ using Quotient.inductionOn
+  rfl
+
 theorem Subst.Eqv.vwk_wk0 {Γ : Ctx α ε} {σ : Subst.Eqv φ Γ L K}
   : (σ.vwk <| Ctx.InS.wk0 (head := head)) = σ.vlift := by
   induction σ using Quotient.inductionOn; rfl
@@ -498,6 +504,13 @@ theorem Eqv.vsubst_lsubst {Γ Δ : Ctx α ε}
   induction r using Quotient.inductionOn
   simp [InS.vsubst_lsubst]
 
+theorem Subst.Eqv.get_vsubst {Γ Δ : Ctx α ε} {L K : LCtx α}
+  {ρ : Term.Subst.Eqv φ Γ Δ} {σ : Subst.Eqv φ Δ L K} {i : Fin L.length}
+  : (σ.vsubst ρ).get i = (σ.get i).vsubst (ρ.lift (le_refl _)) := by
+  induction σ using Quotient.inductionOn
+  induction ρ using Quotient.inductionOn
+  rfl
+
 theorem InS.cfgSubstCongr {Γ : Ctx α ε} {L : LCtx α}
   {R : LCtx α} {G G' : ∀i, InS φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)} (hG : G ≈ G')
   : cfgSubst R G ≈ cfgSubst R G' := λi => by

DeBruijnSSA/BinSyntax/Rewrite/Region/Structural.lean

@@ -42,6 +42,11 @@ theorem Eqv.packed_out_packed_in {Γ : Ctx α ε} {R : LCtx α}
   {r : Eqv φ Γ R} : r.packed_in.packed_out = r.packed_out.packed_in (Δ := Δ) := by
   apply unpacked_out_injective; simp [unpacked_out_packed_in]
 
+theorem Eqv.packed_in_unpacked_app_out {Γ : Ctx α ε} {R L : LCtx α}
+  {r : Eqv φ Γ [(R ++ L).pack]}
+  : r.unpacked_app_out.packed_in (Δ := Δ) = r.packed_in.unpacked_app_out := by
+  simp [unpacked_app_out, packed_in, vsubst_lsubst, unpacked_app_out]
+
 theorem Eqv.packed_def' {Γ : Ctx α ε} {R : LCtx α}
   {r : Eqv φ Γ R} : r.packed (Δ := Δ) = r.packed_in.packed_out
   := by simp [packed, packed_out_packed_in]
@@ -151,7 +156,10 @@ theorem Eqv.packed_cfg_split {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R
         ;; _ ⋊ (ret Term.Eqv.distl_pack
           ;; pack_coprod (λi => acast R.get_dist
             ;; (G (i.cast R.length_dist)).packed.unpacked_app_out))) := by
-  sorry
+  rw [packed, packed_out_cfg_letc, packed_in_letc_split]
+  congr 3
+  · rw [packed_in_unpacked_app_out, <-packed]
+  · rw [packed_in_pack_coprod_arr]; congr; funext i; rw [packed_in_unpacked_app_out, <-packed]
 
 -- TODO: unpacked_app_out ltimes dinaturality
 

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

@@ -1,8 +1,27 @@
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Structural.Sum
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Structural.Product
+import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Cast
+import DeBruijnSSA.BinSyntax.Rewrite.Term.Structural.Distrib
 
 namespace BinSyntax
 
 variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [OrderBot ε]
 
 namespace Region
+
+open Term.Eqv
+
+theorem Eqv.packed_in_pack_coprod {Γ : Ctx α ε} {R L : LCtx α}
+  {G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) L}
+  : (pack_coprod G).packed_in (Δ := Δ)
+  = vsubst (distl_pack (e := ⊥) (R := R) (X := Γ.pack)).subst0 (
+    pack_coprod (λi => ((G (i.cast R.length_dist)).packed_in).cast (by rw [LCtx.get_dist]; rfl) rfl)
+  )
+  := sorry
+
+theorem Eqv.packed_in_pack_coprod_arr {Γ : Ctx α ε} {R L : LCtx α}
+  {G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) (A::L)}
+  : (pack_coprod G).packed_in (Δ := Δ)
+  = ret (distl_pack (X := Γ.pack))
+    ;; pack_coprod (λi => acast R.get_dist ;; (G (i.cast R.length_dist)).packed_in)
+  := by rw [packed_in_pack_coprod, ret_seq]; congr; sorry

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

@@ -472,6 +472,16 @@ theorem Eqv.vwk1_unpack_app_out {Γ : Ctx α ε} {R L : LCtx α}
   : (unpack_app_out (φ := φ) (Γ := Γ) (R := R) (L := L)).vwk1 (inserted := inserted)
   = unpack_app_out := by simp only [unpack_app_out, vwk1_case, Term.Eqv.wk1_pack_app]; rfl
 
+@[simp]
+theorem Eqv.vwk_lift_unpack_app_out {Γ Δ : Ctx α ε} {R L : LCtx α} {ρ : Γ.InS Δ}
+  : (unpack_app_out (φ := φ) (R := R) (L := L)).vwk ρ.slift
+  = unpack_app_out := by simp [unpack_app_out]
+
+@[simp]
+theorem Eqv.vsubst_lift_unpack_app_out {Γ Δ : Ctx α ε} {R L : LCtx α} {σ : Term.Subst.Eqv φ Γ Δ}
+  : (unpack_app_out (φ := φ) (R := R) (L := L)).vsubst (σ.lift (le_refl _)) = unpack_app_out := by
+  simp [unpack_app_out, <-ret_nil]
+
 def Subst.Eqv.unpack_app_out {Γ : Ctx α ε} {R L : LCtx α}
   : Subst.Eqv φ Γ [(R ++ L).pack] [R.pack, L.pack] := Region.Eqv.unpack_app_out.csubst
 
@@ -482,6 +492,18 @@ theorem Subst.Eqv.vlift_unpack_app_out {Γ : Ctx α ε} {R L : LCtx α}
   ext k; cases k using Fin.elim1
   simp [unpack_app_out]
 
+@[simp]
+theorem Subst.Eqv.vwk_unpack_app_out {Γ : Ctx α ε} {R L : LCtx α} {ρ : Γ.InS Δ}
+  : (Subst.Eqv.unpack_app_out (φ := φ) (R := R) (L := L)).vwk ρ = unpack_app_out := by
+  ext k; cases k using Fin.elim1
+  simp [unpack_app_out, Subst.Eqv.get_vwk]
+
+@[simp]
+theorem Subst.Eqv.vsubst_unpack_app_out {Γ Δ : Ctx α ε} {R L : LCtx α} {σ : Term.Subst.Eqv φ Δ Γ}
+  : (Subst.Eqv.unpack_app_out (φ := φ) (R := R) (L := L)).vsubst σ = unpack_app_out := by
+  ext k; cases k using Fin.elim1
+  simp [unpack_app_out, Subst.Eqv.get_vsubst]
+
 theorem Subst.Eqv.extend_unpack_comp_unpack_app_out {Γ : Ctx α ε} {R L : LCtx α}
   : Subst.Eqv.unpack.extend.comp Subst.Eqv.unpack_app_out
   = Subst.Eqv.unpack_right_out (φ := φ) (Γ := Γ) (R := R) (L := L) := by

DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Sum.lean

@@ -294,6 +294,21 @@ theorem Eqv.wk_lift_coprod {A B C : Ty α} {Γ Δ : Ctx α ε} {ρ : Γ.InS Δ}
   : wk ρ.slift (coprod l r) = coprod (wk ρ.slift l) (wk ρ.slift r)
   := by simp [coprod, wk1, wk_wk]; congr 2 <;> ext k <;> cases k <;> rfl
 
+theorem Eqv.subst_lift_coprod {A B C : Ty α} {Γ Δ : Ctx α ε} {ρ : Subst.Eqv φ Γ Δ}
+  {l : Eqv φ ((A, ⊥)::Δ) ⟨C, e⟩} {r : Eqv φ ((B, ⊥)::Δ) ⟨C, e⟩}
+  : subst (ρ.lift (le_refl _)) (coprod l r)
+  = coprod (subst (ρ.lift (le_refl _)) l) (subst (ρ.lift (le_refl _)) r) := by
+  induction l using Quotient.inductionOn; induction r using Quotient.inductionOn;
+  induction ρ using Quotient.inductionOn;
+  apply eq_of_term_eq
+  simp only [Set.mem_setOf_eq, InS.coe_subst, Term.subst, Subst.InS.coe_lift, Subst.lift_zero,
+    InS.coe_wk, Ctx.InS.coe_wk1, ← Term.subst_fromWk, Term.subst_subst, InS.coe_case, InS.coe_var,
+    ]
+  congr <;> {
+    funext k; cases k <;> simp only [Subst.comp, Term.subst, Nat.liftWk_succ, Nat.succ_eq_add_one,
+      Subst.lift_succ, Term.wk_wk, Term.subst_fromWk, Nat.liftWk_succ_comp_succ] <;> rfl
+  }
+
 def Eqv.inj_l {A B : Ty α} {Γ : Ctx α ε} : Eqv (φ := φ) (⟨A, ⊥⟩::Γ) ⟨A.coprod B, e⟩
   := inl nil
 
@@ -307,6 +322,11 @@ theorem Eqv.wk_lift_inj_l {A B : Ty α} {Γ Δ : Ctx α ε} {ρ : Γ.InS Δ}
   : wk ρ.slift (inj_l (φ := φ) (e := e) (A := A) (B := B)) = inj_l
   := by simp [inj_l]
 
+@[simp]
+theorem Eqv.subst_lift_inj_l {A B : Ty α} {Γ Δ : Ctx α ε} {ρ : Subst.Eqv φ Γ Δ}
+  : subst (ρ.lift (le_refl _)) (inj_l (φ := φ) (e := e) (A := A) (B := B)) = inj_l
+  := by simp [inj_l]
+
 @[simp]
 theorem Eqv.wk2_inj_l {A B : Ty α} {Γ : Ctx α ε}
   : (inj_l (φ := φ) (e := e) (A := A) (B := B) (Γ := head::Γ)).wk2 (inserted := inserted) = inj_l
@@ -335,6 +355,11 @@ theorem Eqv.wk_lift_inj_r {A B : Ty α} {Γ Δ : Ctx α ε} {ρ : Γ.InS Δ}
   : wk ρ.slift (inj_r (φ := φ) (e := e) (A := A) (B := B)) = inj_r
   := by simp [inj_r]
 
+@[simp]
+theorem Eqv.subst_lift_inj_r {A B : Ty α} {Γ Δ : Ctx α ε} {ρ : Subst.Eqv φ Γ Δ}
+  : subst (ρ.lift (le_refl _)) (inj_r (φ := φ) (e := e) (A := A) (B := B)) = inj_r
+  := by simp [inj_r]
+
 @[simp]
 theorem Eqv.wk2_inj_r {A B : Ty α} {Γ : Ctx α ε}
   : (inj_r (φ := φ) (e := e) (A := A) (B := B) (Γ := head::Γ)).wk2 (inserted := inserted) = inj_r

DeBruijnSSA/BinSyntax/Rewrite/Term/Structural/Sum.lean

@@ -138,6 +138,13 @@ theorem Eqv.wk1_pack_app {Γ : Ctx α ε} {L R : LCtx α}
   : (pack_app (φ := φ) (Γ := Γ) (L := L) (R := R) (e := e)).wk1 (inserted := inserted) = pack_app
   := by rw [wk1, <-Ctx.InS.lift_wk0, wk_lift_pack_app]
 
+@[simp]
+theorem Eqv.subst_lift_pack_app {Γ Δ : Ctx α ε} {L R : LCtx α} {ρ : Subst.Eqv φ Γ Δ}
+  : (pack_app (φ := φ) (Γ := Δ) (L := L) (R := R) (e := e)).subst (ρ.lift (le_refl _)) = pack_app
+  := by induction L generalizing R with
+  | nil => induction ρ using Quotient.inductionOn; rfl
+  | cons A L I => simp [pack_app, subst_lift_seq, Term.Eqv.subst_lift_coprod, Term.Eqv.sum, I]
+
 theorem Eqv.pack_app_coprod {Γ : Ctx α ε} {L R : LCtx α}
   : pack_app (φ := φ) (Γ := Γ) (L := L) (R := R) (e := e) ;;' coprod pack_app_inl pack_app_inr = nil
   := by induction L generalizing R with