Tap

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

@@ -1,6 +1,7 @@
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Structural
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Functor
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Elgot
+import DeBruijnSSA.BinSyntax.Rewrite.Term.Structural.Distrib
 
 namespace BinSyntax
 
@@ -145,4 +146,16 @@ theorem Eqv.packed_case_den {Γ : Ctx α ε} {R : LCtx α}
       rfl
     }
 
--- TODO: cfg: needs Böhm-Jacopini lore
+theorem Eqv.packed_cfg_den {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R ++ L)} {G}
+  : (cfg R β G).packed (Δ := Δ)
+  = ret Term.Eqv.split ;; _ ⋊ (β.packed ;; ret Term.Eqv.pack_app) ;; distl_inv
+  ;; coprod pi_r (fixpoint (ret Term.Eqv.distl_pack ;; unpack.lsubst (Subst.Eqv.fromFCFG (λi =>
+    ret (Term.Eqv.nil.cast
+      (V := ((R.dist Γ.pack).get i, ⊥))
+      (V' := (Γ.pack.prod (R.get (i.cast R.length_dist)), ⊥)) rfl (by simp [R.getElem_dist]))
+    ;; ret Term.Eqv.split ⋉ _
+    ;; assoc
+    ;; _ ⋊ ((G (i.cast R.length_dist)).packed ;; ret Term.Eqv.pack_app)
+    ;; sorry
+  ))))
+  := sorry

DeBruijnSSA/BinSyntax/Rewrite/Region/Structural.lean

@@ -1,5 +1,6 @@
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Structural.Sum
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Structural.Product
+import DeBruijnSSA.BinSyntax.Rewrite.Region.Structural.Distrib
 import DeBruijnSSA.BinSyntax.Rewrite.Term.Structural
 
 namespace BinSyntax
@@ -118,7 +119,15 @@ theorem Eqv.packed_case {Γ : Ctx α ε} {R : LCtx α}
     (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
+theorem Eqv.packed_cfg {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R ++ L)} {G}
+  : (cfg R β G).packed (Δ := Δ)
+  = gloop R.pack β.packed.unpacked_app_out
+      (unpack.lsubst (Subst.Eqv.fromFCFG (λi =>
+        (let1 (pair (var 2 (by simp)) (var 0 Ctx.Var.shead)) (G i).packed.unpacked_app_out)))) := by
+  rw [packed_def', packed_in_cfg, packed_out_cfg_gloop, <-packed_def']
+  congr; funext i
+  rw [vwk1_unpacked_app_out, packed_out_let1, <-packed_def', <-unpacked_app_out_let1]
+  simp
 
 end Region
 

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

@@ -0,0 +1,8 @@
+import DeBruijnSSA.BinSyntax.Rewrite.Region.Structural.Sum
+import DeBruijnSSA.BinSyntax.Rewrite.Region.Structural.Product
+
+namespace BinSyntax
+
+variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [OrderBot ε]
+
+namespace Region

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

@@ -0,0 +1,8 @@
+import DeBruijnSSA.BinSyntax.Rewrite.Region.Structural.Gloop
+import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Elgot
+
+namespace BinSyntax
+
+variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [OrderBot ε]
+
+namespace Region

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

@@ -1,4 +1,4 @@
-import DeBruijnSSA.BinSyntax.Rewrite.Region.LSubst
+import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Seq
 
 namespace BinSyntax
 
@@ -77,3 +77,8 @@ theorem Eqv.dinaturality_gloop {Γ : Ctx α ε} {L : LCtx α}
   = gloop A β ((σ.get (0 : Fin 1)).lsubst
     (Subst.Eqv.fromFCFG_append (K := [A]) (Fin.elim1 G)).vlift)
   := dinaturality (Γ := Γ) (R := [A]) (R' := [B]) (L := L) (σ := σ) (β := β) (G := Fin.elim1 G)
+
+theorem Eqv.uniform_gloop {Γ : Ctx α ε} {L : LCtx α}
+  {β : Eqv φ Γ (A::L)} {e : Term.Eqv φ ((A, ⊥)::Γ) (B, ⊥)}
+  {r : Eqv φ ((B, ⊥)::Γ) (B::L)} {s : Eqv φ ((A, ⊥)::Γ) (A::L)}
+  (hrs : (ret e) ;; r = s ;; (ret e)) : gloop B (β.wrseq (ret e)) r = gloop A β s := Eqv.uniform hrs

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

@@ -1,6 +1,7 @@
 import DeBruijnSSA.BinSyntax.Rewrite.Region.LSubst
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Seq
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Sum
+import DeBruijnSSA.BinSyntax.Rewrite.Region.Structural.Gloop
 import DeBruijnSSA.BinSyntax.Rewrite.Term.Structural.Product
 import DeBruijnSSA.BinSyntax.Typing.Region.Structural
 
@@ -114,6 +115,32 @@ theorem Eqv.packed_in_cfg {Γ : Ctx α ε} {R L : LCtx α}
   rw [packed_in, vsubst_cfg]; apply congrArg; funext i
   rw [packed_in, let1_beta, vsubst_vsubst, Term.Subst.Eqv.lift_unpack]
 
+theorem Eqv.packed_in_gloop {Γ : Ctx α ε}
+  {β : Eqv φ Γ (A::L)} {G : Eqv φ ((A, ⊥)::Γ) (A::L)}
+  : (gloop A β G).packed_in (Δ := Δ)
+  = gloop A β.packed_in (let1 (pair (var 1 (by simp)) (var 0 Ctx.Var.shead)) G.packed_in)
+  := by
+  rw [packed_in, vsubst_gloop]; apply congrArg
+  rw [packed_in, let1_beta, vsubst_vsubst, Term.Subst.Eqv.lift_unpack]
+
+theorem Eqv.packed_in_gloop_uniform {Γ : Ctx α ε}
+  {β : Eqv φ Γ (A::L)} {G : Eqv φ ((A, ⊥)::Γ) (A::L)}
+  : (gloop A β G).packed_in (Δ := Δ)
+  = gloop (Γ.pack.prod A)
+      (β.packed_in.wrseq (ret (pair (var 1 (by simp)) (var 0 Ctx.Var.shead))))
+      (G.packed_in.vwk1 ;; (ret (pair (var 1 (by simp)) (var 0 Ctx.Var.shead)))) := by
+  rw [packed_in_gloop]
+  apply (uniform_gloop _).symm
+  rw [ret_seq, let1_beta, vwk1_seq, seq, vsubst_lsubst, seq]
+  congr 1
+  · ext k; apply eq_of_reg_eq; cases k using Fin.cases <;> simp [Region.alpha, Subst.id]
+  · simp only [vwk1, packed_in, ← vsubst_fromWk, vsubst_vsubst]
+    congr; ext k
+    simp only [List.get_eq_getElem, List.length_cons, Term.Subst.Eqv.get_comp,
+      Term.Subst.Eqv.get_unpack, subst_fromWk]
+    rw [<-Term.Eqv.wk1, <-Term.Eqv.wk1]
+    simp [Term.Eqv.wk1_pi_n]
+
 end Region
 
 end BinSyntax

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

@@ -25,6 +25,18 @@ theorem Eqv.unpack_def {Γ : Ctx α ε} {R : LCtx α}
     simp [
       Region.unpack, Region.nil, Region.ret, Region.lwk0, Region.vwk_lwk, Region.vwk_lift_unpack]
 
+-- def Eqv.pack_case {Γ : Ctx α ε} {R : LCtx α} {X : Ty α}
+--   (r : Eqv φ ((X.prod R, ⊥)::Γ) (R.dist X, e)) : Eqv φ ((R.dist X, ⊥)::Γ) (R.pack, e) :=
+--   case (Term.Eqv.dist X)
+--     (br (List.length R) Term.Eqv.pi_r (by simp))
+--     (lwk_id LCtx.Wkn.id_right_dist r)
+
+def Eqv.pack_coprod {Γ : Ctx α ε} {R : LCtx α}
+  (G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) (A::L)) : Eqv φ ((R.pack, ⊥)::Γ) (A::L) :=
+  match R with
+  | [] => zero
+  | _::R => coprod (pack_coprod (λi => G i.succ)) (G (0 : Fin (R.length + 1)))
+
 @[simp]
 theorem Eqv.vwk_lift_unpack {Γ Δ : Ctx α ε} {R : LCtx α} (ρ : Γ.InS Δ)
   : Eqv.vwk (ρ.lift (le_refl _)) (Eqv.unpack (φ := φ) (R := R)) = unpack := by
@@ -396,6 +408,26 @@ theorem Eqv.vwk1_unpacked_app_out {Γ : Ctx α ε} {R L : LCtx α} {r : Eqv φ (
     unpacked_app_out, <-Subst.Eqv.vlift_unpack_app_out, Subst.Eqv.vwk1_lsubst_vlift,
     Subst.Eqv.vlift_unpack_app_out, Subst.Eqv.vlift_unpack_app_out, <-unpacked_app_out]
 
+theorem Eqv.vwk1_packed_out {Γ : Ctx α ε} {R : LCtx α} {r : Eqv φ (V::Γ) R}
+  : r.packed_out.vwk1 (inserted := inserted) = r.vwk1.packed_out := by
+  rw [packed_out, packed_out, <-Subst.Eqv.vlift_pack, Subst.Eqv.vwk1_lsubst_vlift,
+      Subst.Eqv.vlift_pack, Subst.Eqv.vlift_pack, <-packed_out]
+
+theorem Eqv.unpacked_app_out_let1 {Γ : Ctx α ε} {R L : LCtx α}
+  {a : Term.Eqv φ Γ (A, e)} {r : Eqv φ ((A, ⊥)::Γ) [(R ++ L).pack]}
+  : (let1 a r).unpacked_app_out = let1 a r.unpacked_app_out := by simp [unpacked_app_out]
+
+theorem Eqv.unpacked_app_out_let2 {Γ : Ctx α ε} {R L : LCtx α}
+  {a : Term.Eqv φ Γ (A.prod B, e)} {r : Eqv φ ((B, ⊥)::(A, ⊥)::Γ) [(R ++ L).pack]}
+  : (let2 a r).unpacked_app_out = let2 a r.unpacked_app_out
+  := by simp [unpacked_app_out, Subst.Eqv.vliftn₂_eq_vlift_vlift]
+
+theorem Eqv.unpacked_app_out_case {Γ : Ctx α ε} {R L : LCtx α}
+  {a : Term.Eqv φ Γ (A.coprod B, e)}
+  {l : Eqv φ ((A, ⊥)::Γ) [(R ++ L).pack]} {r : Eqv φ ((B, ⊥)::Γ) [(R ++ L).pack]}
+  : (case a l r).unpacked_app_out = case a l.unpacked_app_out r.unpacked_app_out
+  := by simp [unpacked_app_out]
+
 theorem Eqv.extend_unpack_unpacked_app_out
   {Γ : Ctx α ε} {R L : LCtx α} {r : Eqv φ Γ [(R ++ L).pack]}
   : r.unpacked_app_out.lsubst Subst.Eqv.unpack.extend = r.unpacked_right_out := by
@@ -405,17 +437,23 @@ theorem Eqv.packed_out_cfg_gloop {Γ : Ctx α ε} {R L : LCtx α}
   {β : Eqv φ Γ (R ++ L)} {G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ L)}
   : (cfg R β G).packed_out
   = gloop R.pack β.packed_out.unpacked_app_out
-      (unpack.lsubst (Subst.Eqv.fromFCFG (λi => (G i).vwk1.packed_out.unpacked_app_out))) := calc
+      (unpack.lsubst (Subst.Eqv.fromFCFG (λi => (G i).packed_out.unpacked_app_out.vwk1))) := calc
   _ = (cfg R (β.packed_out.unpacked_app_out.lsubst Subst.Eqv.unpack.extend)
               (λi => (G i).packed_out.unpacked_app_out.lsubst Subst.Eqv.unpack.extend.vlift))
       := by simp [packed_out_cfg, extend_unpack_unpacked_app_out, Subst.Eqv.vlift_extend]
   _ = _ := by
     rw [dinaturality_to_gloop_rec]
     congr
     · ext k; simp [Subst.Eqv.get_fromFCFG]
-      sorry
     · simp [Subst.Eqv.unpack]
 
+-- theorem Eqv.packed_out_gloop {Γ : Ctx α ε} {R L : LCtx α}
+--   {β : Eqv φ Γ (A::L)} {G : Eqv φ (⟨A, ⊥⟩::Γ) (A::L)}
+--   : (gloop A β G).packed_out
+--   = gloop (Ty.empty.coprod A)
+--     (β.packed_out.unpacked_app_out (R := [A]))
+--     (coprod zero nil ;; G.packed_out.unpacked_app_out (R := [A])) := by sorry
+
 end Region
 
 end BinSyntax

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

@@ -0,0 +1,14 @@
+import DeBruijnSSA.BinSyntax.Rewrite.Term.Structural.Sum
+import DeBruijnSSA.BinSyntax.Rewrite.Term.Structural.Product
+import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Distrib
+
+namespace BinSyntax
+
+variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [OrderBot ε]
+
+namespace Term
+
+def Eqv.distl_pack {Γ : Ctx α ε} {R : LCtx α} {X : Ty α}
+  : Eqv φ ((X.prod R.pack, ⊥)::Γ) ((R.dist X).pack, e) := match R with
+  | [] => pi_r
+  | _::_ => distl_inv ;;' coprod (distl_pack ;;' inj_l) inj_r

DeBruijnSSA/BinSyntax/Typing/LCtx.lean

@@ -383,6 +383,9 @@ theorem LCtx.get_dist {X : Ty α} {L : LCtx α} {i}
   : (L.dist X).get i = Ty.prod X (L.get <| i.cast L.length_dist)
   := getElem_dist
 
+theorem LCtx.dist_append {X : Ty α} {L K : LCtx α} : (L ++ K).dist X = L.dist X ++ K.dist X
+  := by induction L <;> simp [*]
+
 @[simp]
 def LCtx.dpack (X : Ty α) : LCtx α → Ty α
   | [] => Ty.empty