Packwork

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

@@ -13,9 +13,25 @@ def Eqv.packed {Γ : Ctx α ε} {R : LCtx α} (r : Eqv φ Γ R) : Eqv φ [(Γ.pa
 def Eqv.unpacked {Γ : Ctx α ε} {R : LCtx α} (r : Eqv φ [(Γ.pack, ⊥)] [R.pack]) (h : Γ.Pure)
   : Eqv φ Γ R := r.unpacked_out.unpacked_in h
 
--- TODO: (un)packed_in commutes with (un)packed_out
+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 [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
 
--- TODO: packed_unpacked, unpacked_packed
+-- theorem Eqv.unpacked_out_packed_in {Γ : Ctx α ε} {R : LCtx α}
+--   {r : Eqv φ Γ [R.pack]} : r.packed_in.unpacked_out = r.unpacked_out.packed_in := sorry
+
+-- 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 := sorry
+
+-- theorem Eqv.packed_out_packed_in {Γ : Ctx α ε} {R : LCtx α}
+--   {r : Eqv φ Γ R} : r.packed_in.packed_out = r.packed_out.packed_in := sorry
+
+-- TODO: packed_unpacked, unpacked_packed via commutativity + cancellation
 
 -- TODO: {br, let1, let2, case, cfg}
 

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

@@ -51,6 +51,16 @@ theorem Subst.Eqv.unpack_def {Γ : Ctx α ε} {R : LCtx α}
   : Subst.Eqv.unpack (φ := φ) (Γ := Γ) (R := R) = ⟦InS.unpack (Γ := Γ) (R := R)⟧
   := by rw [unpack, Region.Eqv.unpack_def]; rfl
 
+@[simp]
+theorem Subst.Eqv.vlift_unpack {Γ : Ctx α ε} {R : LCtx α}
+  : (Subst.Eqv.unpack (φ := φ) (Γ := Γ) (R := R)).vlift (head := head) = unpack := by
+  simp [unpack_def]
+
+@[simp]
+theorem Subst.Eqv.vliftn₂_unpack {Γ : Ctx α ε} {R : LCtx α}
+  : (Subst.Eqv.unpack (φ := φ) (Γ := Γ) (R := R)).vliftn₂ (left := left) (right := right)
+  = unpack := by simp [Subst.Eqv.vliftn₂_eq_vlift_vlift]
+
 def Subst.Eqv.pack {Γ : Ctx α ε} {R : LCtx α} : Subst.Eqv φ Γ R [R.pack] := ⟦Subst.InS.pack⟧
 
 @[simp]
@@ -63,6 +73,11 @@ theorem Subst.Eqv.vlift_pack {Γ : Ctx α ε} {R : LCtx α}
   : (pack (φ := φ) (Γ := Γ) (R := R)).vlift (head := head) = pack
   := by simp only [pack, vlift_quot, Subst.InS.vlift_pack]
 
+@[simp]
+theorem Subst.Eqv.vliftn₂_pack {Γ : Ctx α ε} {R : LCtx α}
+  : (Subst.Eqv.pack (φ := φ) (Γ := Γ) (R := R)).vliftn₂ (left := left) (right := right)
+  = pack := by simp [Subst.Eqv.vliftn₂_eq_vlift_vlift]
+
 theorem Eqv.vsubst0_pack_unpack {Γ : Ctx α ε} {R : LCtx α} {ℓ : Fin R.length}
   : (unpack (φ := φ) (Γ := _::Γ) (R := R)).vsubst (Term.Eqv.inj_n R ℓ).subst0
   = br ℓ (Term.Eqv.var 0 Ctx.Var.shead) (by simp) := by
@@ -110,21 +125,62 @@ theorem Subst.Eqv.unpack_comp_pack {Γ : Ctx α ε} {R : LCtx α}
 --     get_id, Fin.coe_fin_one]
 --   rfl
 
-def Eqv.unpacked_out {Γ : Ctx α ε} {R : LCtx α} (h : Eqv φ Γ [R.pack]) : Eqv φ Γ R
-  := h.lsubst Subst.Eqv.unpack
+def Eqv.unpacked_out {Γ : Ctx α ε} {R : LCtx α} (r : Eqv φ Γ [R.pack]) : Eqv φ Γ R
+  := r.lsubst Subst.Eqv.unpack
+
+-- TODO: br here?
+
+@[simp]
+theorem Eqv.unpacked_out_quot {Γ : Ctx α ε} {R : LCtx α} (r : InS φ Γ [R.pack])
+  : unpacked_out ⟦r⟧ = ⟦r.unpacked_out⟧ := by simp only [unpacked_out, Subst.Eqv.unpack,
+    unpack_def, InS.unpack, Set.mem_setOf_eq, csubst_quot, lsubst_quot]; rfl
+
+theorem Eqv.unpacked_out_let1 {Γ : Ctx α ε} {R : LCtx α}
+  (a : Term.Eqv φ Γ (A, e)) (r : Eqv φ ((A, ⊥)::Γ) [R.pack])
+  :  (let1 a r).unpacked_out = let1 a r.unpacked_out := by simp [unpacked_out]
+
+theorem Eqv.unpacked_out_let2 {Γ : Ctx α ε} {R : LCtx α}
+  (a : Term.Eqv φ Γ (A.prod B, e)) (r : Eqv φ ((B, ⊥)::(A, ⊥)::Γ) [R.pack])
+  : (let2 a r).unpacked_out = let2 a r.unpacked_out := by simp [unpacked_out]
+
+theorem Eqv.unpacked_out_case {Γ : Ctx α ε} {R : LCtx α}
+  (a : Term.Eqv φ Γ (A.coprod B, e))
+  (l : Eqv φ ((A, ⊥)::Γ) [R.pack]) (r : Eqv φ ((B, ⊥)::Γ) [R.pack])
+  : (case a l r).unpacked_out = case a l.unpacked_out r.unpacked_out := by simp [unpacked_out]
+
+-- TODO: unpacking a cfg is a quarter of Böhm–Jacopini
 
 def Eqv.packed_out {Γ : Ctx α ε} {R : LCtx α} (h : Eqv φ Γ R) : Eqv φ Γ [R.pack]
   := h.lsubst Subst.Eqv.pack
 
+@[simp]
+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_let1 {Γ : Ctx α ε} {R : LCtx α}
+  (a : Term.Eqv φ Γ (A, e)) (r : Eqv φ ((A, ⊥)::Γ) R)
+  : (let1 a r).packed_out = let1 a r.packed_out := by simp [packed_out]
+
+theorem Eqv.packed_out_let2 {Γ : Ctx α ε} {R : LCtx α}
+  (a : Term.Eqv φ Γ (A.prod B, e)) (r : Eqv φ ((B, ⊥)::(A, ⊥)::Γ) R)
+  : (let2 a r).packed_out = let2 a r.packed_out := by simp [packed_out]
+
+theorem Eqv.packed_out_case {Γ : Ctx α ε} {R : LCtx α}
+  (a : Term.Eqv φ Γ (A.coprod B, e))
+  (l : Eqv φ ((A, ⊥)::Γ) R) (r : Eqv φ ((B, ⊥)::Γ) R)
+  : (case a l r).packed_out = case a l.packed_out r.packed_out := by simp [packed_out]
+
+-- TODO: packing a cfg is half of Böhm–Jacopini, and I believe the best we can do sans dinaturality
+
 -- theorem Eqv.unpacked_out_packed_out {Γ : Ctx α ε} {R : LCtx α} (h : Eqv φ Γ R)
 --   : h.packed_out.unpacked_out = h := by
 --   rw [Eqv.unpacked, packed, lsubst_lsubst, Subst.Eqv.unpack_comp_pack]
 --   sorry
 
 -- TODO: packed_out_unpacked_out
 
--- TODO: {br, let1, let2, case, cfg}
-
 end Region
 
 end BinSyntax

DeBruijnSSA/BinSyntax/Typing/Region/Structural.lean

@@ -27,8 +27,8 @@ def Subst.InS.pack {Γ : Ctx α ε} {R : LCtx α} : Subst.InS φ Γ R [R.pack] :
   ⟨Subst.pack, Subst.Wf.pack⟩
 
 @[simp]
-theorem Subst.InS.coe_pack {Γ : Ctx α ε} {R : LCtx α} (ℓ : ℕ)
-  : (Subst.InS.pack (φ := φ) (Γ := Γ) (R := R) : Region.Subst φ) ℓ = br 0 (Term.inj_n ℓ) := rfl
+theorem Subst.InS.coe_pack {Γ : Ctx α ε} {R : LCtx α}
+  : (Subst.InS.pack (φ := φ) (Γ := Γ) (R := R) : Region.Subst φ) = Subst.pack := rfl
 
 @[simp]
 theorem Subst.vlift_pack
@@ -110,6 +110,29 @@ theorem Subst.InS.vlift_unpack {Γ : Ctx α ε} {R : LCtx α}
   : (Subst.InS.unpack (φ := φ) (Γ := Γ) (R := R)).vlift (head := head) = unpack := by
   ext; simp [Subst.vlift]
 
-open Term
+@[simp]
+theorem Subst.InS.vliftn₂_unpack {Γ : Ctx α ε} {R : LCtx α}
+  : (Subst.InS.unpack (φ := φ) (Γ := Γ) (R := R)).vliftn₂ (left := left) (right := right)
+  = unpack := by simp [Subst.InS.vliftn₂_eq_vlift_vlift]
+
+def InS.unpacked_out {Γ : Ctx α ε} {R : LCtx α} (r : InS φ Γ [R.pack]) : InS φ Γ R
+  := r.lsubst Subst.InS.unpack
+
+@[simp]
+theorem InS.coe_unpacked_out {Γ : Ctx α ε} {R : LCtx α} (r : InS φ Γ [R.pack])
+  : (r.unpacked_out : Region φ) = (r : Region φ).lsubst (Region.csubst (Region.unpack R.length))
+  := rfl
+
+def InS.packed_out {Γ : Ctx α ε} {R : LCtx α} (h : InS φ Γ R) : InS φ Γ [R.pack]
+  := h.lsubst Subst.InS.pack
+
+@[simp]
+theorem InS.coe_packed_out {Γ : Ctx α ε} {R : LCtx α} (r : InS φ Γ R)
+  : (r.packed_out : Region φ) = (r : Region φ).lsubst Subst.pack
+  := rfl
+
+-- theorem InS.unpacked_in_unpacked_out {Γ : Ctx α ε} {R : LCtx α} (r : InS φ Γ [R.pack])
+--   : r.unpacked_out.unpacked_in = r.unpacked_in.unpacked_out := by
+--   ext; simp
 
 end Region