More packing lore

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

@@ -1 +1,94 @@
-import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Structural.Basic
+import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Structural.Sum
+import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Structural.Product
+import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Structural
+
+namespace BinSyntax
+
+variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [OrderBot ε]
+
+namespace Region
+
+def Eqv.packed {Γ Δ : Ctx α ε} {R : LCtx α} (r : Eqv φ Γ R) : Eqv φ ((Γ.pack, ⊥)::Δ) [R.pack]
+  := r.packed_out.packed_in
+
+def Eqv.unpacked {Γ : Ctx α ε} {R : LCtx α} (r : Eqv φ [(Γ.pack, ⊥)] [R.pack]) (h : Γ.Pure)
+  : Eqv φ Γ R := r.unpacked_out.unpacked_in h
+
+theorem Eqv.unpacked_out_unpacked_in {Γ : Ctx α ε} {R : LCtx α}
+  {r : Eqv φ [(Γ.pack, ⊥)] [R.pack]} {h : Γ.Pure}
+  : (r.unpacked_in h).unpacked_out = r.unpacked_out.unpacked_in h := by
+  simp only [unpacked_in, unpacked_out_let1]
+  induction r using Quotient.inductionOn
+  simp only [Term.Eqv.packE_def', vwk_id_quot, unpacked_out_quot, let1_quot]
+  rfl
+
+theorem Eqv.unpacked_out_packed_in {Γ : Ctx α ε} {R : LCtx α}
+  {r : Eqv φ Γ [R.pack]} : r.packed_in.unpacked_out = r.unpacked_out.packed_in (Δ := Δ) := by
+  simp only [unpacked_out, packed_in, vsubst_lsubst]
+  congr
+  simp only [Subst.Eqv.unpack, unpack_def, InS.unpack, Set.mem_setOf_eq, csubst_quot,
+    Term.Subst.Eqv.unpack, Subst.Eqv.vsubst_quot]
+  congr; ext; simp
+
+theorem Eqv.packed_out_unpacked_in {Γ : Ctx α ε} {R : LCtx α}
+  {r : Eqv φ [(Γ.pack, ⊥)] R} {h : Γ.Pure}
+  : (r.unpacked_in h).packed_out = r.packed_out.unpacked_in h := by
+  apply unpacked_out_injective; simp [unpacked_out_unpacked_in]
+
+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_def' {Γ : Ctx α ε} {R : LCtx α}
+  {r : Eqv φ Γ R} : r.packed (Δ := Δ) = r.packed_in.packed_out
+  := by simp [packed, packed_out_packed_in]
+
+theorem Eqv.unpacked_def' {Γ : Ctx α ε} {R : LCtx α}
+  {r : Eqv φ [(Γ.pack, ⊥)] [R.pack]} {h : Γ.Pure}
+  : r.unpacked h = r.unpacked_out.unpacked_in h := by simp [unpacked, unpacked_out_unpacked_in]
+
+theorem Eqv.packed_unpacked {Γ : Ctx α ε} {R : LCtx α}
+  {r : Eqv φ [(Γ.pack, ⊥)] [R.pack]} {h : Γ.Pure} : (r.unpacked h).packed = r
+  := by rw [unpacked, packed_def', packed_in_unpacked_in, packed_out_unpacked_out]
+
+theorem Eqv.unpacked_packed {Γ : Ctx α ε} {R : LCtx α}
+  {r : Eqv φ Γ R} {h : Γ.Pure} : r.packed.unpacked h = r
+  := by rw [unpacked, packed_def', unpacked_out_packed_out, unpacked_in_packed_in]
+
+open Term.Eqv
+
+theorem Eqv.packed_br {Γ : Ctx α ε} {L : LCtx α}
+  {ℓ} {a : Term.Eqv φ Γ (A, ⊥)} {hℓ}
+  : (br (L := L) ℓ a hℓ).packed (Δ := Δ) = ret ((a.packed.wk_res ⟨hℓ.get, by rfl⟩).inj) := by
+  rw [packed, packed_out_br, packed_in_br, Term.Eqv.packed_of_inj, ret]
+  congr
+  induction a using Quotient.inductionOn
+  apply Term.Eqv.eq_of_term_eq; rfl
+
+theorem Eqv.packed_let1 {Γ : Ctx α ε} {R : LCtx α}
+  {a : Term.Eqv φ Γ (A, e)} {r : Eqv φ ((A, ⊥)::Γ) R}
+  : (let1 a r).packed (Δ := Δ)
+  = let1 a.packed (let1 (pair (var 1 (by simp)) (var 0 Ctx.Var.shead)) r.packed) := by
+  rw [packed, packed_out_let1, packed_in_let1, <-packed]
+
+theorem Eqv.packed_let2 {Γ : Ctx α ε} {R : LCtx α}
+  {a : Term.Eqv φ Γ (A.prod B, e)} {r : Eqv φ ((B, ⊥)::(A, ⊥)::Γ) R}
+  : (let2 a r).packed (Δ := Δ)
+  = let2 a.packed (let1
+    (pair (pair (var 2 (by simp)) (var 1 (by simp))) (var 0 Ctx.Var.shead))
+    r.packed) := by
+  rw [packed, packed_out_let2, packed_in_let2, <-packed]
+
+theorem Eqv.packed_case {Γ : Ctx α ε} {R : LCtx α}
+  {a : Term.Eqv φ Γ (A.coprod B, e)} {r : Eqv φ ((A, ⊥)::Γ) R} {s : Eqv φ ((B, ⊥)::Γ) R}
+  : (case a r s).packed (Δ := Δ)
+  = case a.packed
+    (let1 (pair (var 1 (by simp)) (var 0 Ctx.Var.shead)) r.packed)
+    (let1 (pair (var 1 (by simp)) (var 0 Ctx.Var.shead)) s.packed) := by
+  simp only [packed, packed_out_case, packed_in_case]
+
+-- TODO: cfg
+
+end Region
+
+end BinSyntax

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

@@ -34,7 +34,10 @@ theorem Eqv.packed_in_unpacked_in
 
 open Term.Eqv
 
--- TODO: br
+theorem Eqv.packed_in_br {Γ : Ctx α ε} {L : LCtx α}
+  {ℓ} {a : Term.Eqv φ Γ (A, ⊥)} {hℓ}
+  : (br (L := L) ℓ a hℓ).packed_in (Δ := Δ) = br ℓ a.packed hℓ := by
+  simp [packed_in, Term.Eqv.packed]
 
 theorem Eqv.packed_in_let1 {Γ : Ctx α ε} {R : LCtx α}
   {a : Term.Eqv φ Γ (A, e)} {r : Eqv φ ((A, ⊥)::Γ) R}

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

@@ -129,7 +129,16 @@ def Eqv.packed_out {Γ : Ctx α ε} {R : LCtx α} (h : Eqv φ Γ R) : Eqv φ Γ
 theorem Eqv.packed_out_quot {Γ : Ctx α ε} {R : LCtx α} (r : InS φ Γ R)
   : packed_out ⟦r⟧ = ⟦r.packed_out⟧ := rfl
 
--- TODO: br becomes an injection
+theorem Eqv.packed_out_br {Γ : Ctx α ε} {L : LCtx α}
+  {ℓ} {a : Term.Eqv φ Γ (A, ⊥)} {hℓ}
+  : (br (L := L) ℓ a hℓ).packed_out = br 0 (a.wk_res ⟨hℓ.get, by rfl⟩).inj (by simp) := by
+  simp [packed_out]
+  induction a using Quotient.inductionOn
+  simp only [Term.Eqv.subst0_quot, Term.Eqv.inj_n_def, List.get_eq_getElem, Term.Eqv.wk_id_quot,
+    Term.Eqv.subst_quot, br_quot, Term.Eqv.wk_res_quot]
+  rw [Term.Eqv.inj_quot]
+  simp only [br_quot]
+  congr; ext; simp [Term.inj_n]
 
 theorem Eqv.packed_out_let1 {Γ : Ctx α ε} {R : LCtx α}
   (a : Term.Eqv φ Γ (A, e)) (r : Eqv φ ((A, ⊥)::Γ) R)

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

@@ -1,2 +1,12 @@
 import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Structural.Sum
 import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Structural.Product
+
+namespace BinSyntax
+
+variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [OrderBot ε]
+
+namespace Term
+
+theorem Eqv.packed_of_inj
+  {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} {a : Eqv φ Γ (R.get i, e)}
+  : a.inj.packed (Δ := Δ) = a.packed.inj := by simp [packed]

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

@@ -15,15 +15,61 @@ def Eqv.inj
   | [] => i.elim0
   | _::R => by cases i using Fin.cases with | zero => exact a.inr | succ i => exact inl (inj a)
 
--- TODO: pack_inj is just inj (nil)
+@[simp]
+theorem Eqv.inj_quot {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} {a : InS φ Γ (R.get i, e)}
+  : Eqv.inj ⟦a⟧ = ⟦Term.InS.inj a⟧ := by
+  induction R generalizing Γ with
+  | nil => exact i.elim0
+  | cons _ _ I =>
+    cases i using Fin.cases with
+    | zero => rfl
+    | succ i =>
+      simp only [inj, I, inl_quot, Fin.cases_succ]
+      apply congrArg
+      ext
+      simp [Term.inj, Term.Wf.inj, -Function.iterate_succ, Function.iterate_succ']
+
+@[simp]
+theorem Eqv.wk_inj {Γ Δ : Ctx α ε} {R : LCtx α} {i : Fin R.length}
+  {a : Eqv φ Δ (R.get i, e)} {ρ : Γ.InS Δ}
+  : a.inj.wk ρ = (a.wk ρ).inj := by
+  induction a using Quotient.inductionOn
+  simp only [inj_quot, wk_quot]
+  congr; ext; simp
+
+@[simp]
+theorem Eqv.wk0_inj {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length}
+  {a : Eqv φ Γ (R.get i, e)} : a.inj.wk0 (head := head) = (a.wk0).inj := wk_inj
+
+@[simp]
+theorem Eqv.wk1_inj {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length}
+  {a : Eqv φ (V::Γ) (R.get i, e)} : a.inj.wk1 (inserted := inserted) = (a.wk1).inj := wk_inj
+
+@[simp]
+theorem Eqv.subst_inj {Γ Δ : Ctx α ε} {R : LCtx α} {i : Fin R.length}
+  {a : Eqv φ Δ (R.get i, e)} {σ : Subst.Eqv φ Γ Δ}
+  : a.inj.subst σ = (a.subst σ).inj := by
+  induction a using Quotient.inductionOn
+  induction σ using Quotient.inductionOn
+  simp only [inj_quot, subst_quot]
+  congr; ext; simp
+
+@[simp]
+theorem Eqv.inj_zero {Γ : Ctx α ε} {R : LCtx α}
+  {a : Eqv φ Γ (List.get (A::R) (0 : Fin (R.length + 1)), e)}
+  : a.inj = a.inr := rfl
+
+theorem Eqv.inj_succ {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length}
+  {a : Eqv φ Γ (List.get (A::R) i.succ, e)}
+  : a.inj = (a.inj (R := R)).inl := rfl
 
 def Eqv.inj_n {Γ : Ctx α ε} (R : LCtx α) (i : Fin R.length) : Eqv φ ((R.get i, ⊥)::Γ) (R.pack, e)
   := match R with
   | [] => i.elim0
   | _::R => i.cases (inr nil) (λi => inl (inj_n R i))
 
 theorem Eqv.inj_n_def {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length}
-  : Eqv.inj_n (φ := φ) (Γ := Γ) R i = ⟦Term.InS.inj_n R i⟧ := by
+  : Eqv.inj_n (φ := φ) (Γ := Γ) (e := e) R i = ⟦Term.InS.inj_n R i⟧ := by
   induction R generalizing Γ with
   | nil => exact i.elim0
   | cons _ _ I =>
@@ -35,6 +81,9 @@ theorem Eqv.inj_n_def {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length}
       ext
       simp [Term.inj_n, Term.inj, Term.Wf.inj_n, -Function.iterate_succ, Function.iterate_succ']
 
+theorem Eqv.inj_n_def' {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length}
+  : Eqv.inj_n (φ := φ) (Γ := Γ) (e := e) R i = nil.inj := by rw [inj_n_def, nil, var, inj_quot]; rfl
+
 -- def Eqv.pack_case {Γ : Ctx α ε} {R : LCtx α}
 --   (d : Eqv φ Γ (R.pack, e)) (G : ∀i : Fin R.length, Eqv φ ((R.get i, ⊥)::Γ) (A, e))
 --   : Eqv φ Γ (C, e) := sorry

DeBruijnSSA/BinSyntax/Typing/Term/Basic.lean

@@ -401,6 +401,10 @@ theorem Term.Wf.wk_res {Γ : Ctx α ε} {a : Term φ} {V V'} (h : Wf Γ a V) (hV
 def Term.InS.wk_res {Γ : Ctx α ε} {V V'} (hV : V ≤ V') (a : InS φ Γ V) : InS φ Γ V'
   := ⟨a, a.prop.wk_res hV⟩
 
+@[simp]
+theorem Term.InS.coe_wk_res {Γ : Ctx α ε} {V V'} {a : InS φ Γ V} (hV : V ≤ V')
+  : (a.wk_res hV : Term φ) = (a : Term φ) := rfl
+
 theorem Term.Wf.to_op' {Γ : Ctx α ε} {a : Term φ}
   (h : Wf Γ (Term.op f a) V)
   (hV : ⟨Φ.src f, V.2⟩ ≤ V')

DeBruijnSSA/BinSyntax/Typing/Term/Structural.lean

@@ -386,12 +386,12 @@ theorem subst_lift_inj_n {ℓ : ℕ} {σ : Subst φ} : (inj_n ℓ).subst σ.lift
 
 @[simp]
 theorem Wf.inj_n {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length}
-  : Term.Wf (φ := φ) ((R.get i, ⊥)::Γ) (inj_n i) (R.pack, ⊥)  := by
+  : Term.Wf (φ := φ) ((R.get i, ⊥)::Γ) (inj_n i) (R.pack, e)  := by
   induction R generalizing Γ with
   | nil => exact i.elim0
   | cons _ _ I =>
     cases i using Fin.cases with
-    | zero => exact Wf.inr $ Wf.var Ctx.Var.shead
+    | zero => exact Wf.inr $ Wf.var Ctx.Var.bhead
     | succ i =>
       simp only [
         Fin.val_succ, BinSyntax.Term.inj_n, Function.iterate_succ', Function.comp_apply, LCtx.pack,
@@ -400,32 +400,33 @@ theorem Wf.inj_n {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length}
       apply I
 
 def InS.inj_n {Γ : Ctx α ε} (R : LCtx α) (i : Fin R.length)
-  : Term.InS φ ((R.get i, ⊥)::Γ) (R.pack, ⊥) :=
+  : Term.InS φ ((R.get i, ⊥)::Γ) (R.pack, e) :=
   ⟨Term.inj_n i, Term.Wf.inj_n⟩
 
 @[simp]
 theorem InS.coe_inj_n {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length}
-  : (InS.inj_n (φ := φ) (Γ := Γ) (R := R) i : Term φ) = Term.inj_n i := rfl
+  : (InS.inj_n (φ := φ) (Γ := Γ) (R := R) (e := e) i : Term φ) = Term.inj_n i := rfl
 
 @[simp]
 theorem InS.wk_lift_inj_n {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} {ρ : Γ.InS Δ}
-  : (InS.inj_n (φ := φ) R i).wk (ρ.lift (le_refl _)) = inj_n R i := by ext; simp
+  : (InS.inj_n (φ := φ) (e := e) R i).wk (ρ.lift (le_refl _)) = inj_n R i := by ext; simp
 
 @[simp]
 theorem InS.wk_slift_inj_n {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} {ρ : Γ.InS Δ}
-  : (InS.inj_n (φ := φ) R i).wk (ρ.slift) = inj_n R i := by ext; simp
+  : (InS.inj_n (φ := φ) (e := e) R i).wk (ρ.slift) = inj_n R i := by ext; simp
 
 @[simp]
 theorem InS.subst_lift_inj_n {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} {σ : Subst.InS φ Γ Δ}
-  : (InS.inj_n (φ := φ) R i).subst (σ.lift (le_refl _)) = inj_n R i := by ext; simp
+  : (InS.inj_n (φ := φ) (e := e) R i).subst (σ.lift (le_refl _)) = inj_n R i := by ext; simp
 
 @[simp]
 theorem InS.subst_slift_inj_n {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length} {σ : Subst.InS φ Γ Δ}
-  : (InS.inj_n (φ := φ) R i).subst σ.slift = inj_n R i := by ext; simp
+  : (InS.inj_n (φ := φ) (e := e) R i).subst σ.slift = inj_n R i := by ext; simp
 
 @[simp]
 theorem InS.wk1_inj_n {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length}
-  : (InS.inj_n (φ := φ) (Γ := Γ) R i).wk1 (inserted := inserted) = inj_n R i := by ext; simp
+  : (InS.inj_n (φ := φ) (Γ := Γ) (e := e) R i).wk1 (inserted := inserted) = inj_n R i
+  := by ext; simp
 
 end Sum