Began swapped completeness

DeBruijnSSA/BinSyntax/Rewrite/Region/Compose.lean

@@ -3,3 +3,4 @@ import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Product
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Sum
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Structural
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Elgot
+import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Completeness

DeBruijnSSA/BinSyntax/Rewrite/Term/Compose.lean

@@ -2,19 +2,5 @@ import DeBruijnSSA.BinSyntax.Rewrite.Term.Eqv
 import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Seq
 import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Product
 import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Sum
+import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Completeness
 import DeBruijnSSA.BinSyntax.Typing.Term.Compose
-
-import Discretion.Utils.Quotient
-
-
-namespace BinSyntax
-
-variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [OrderBot ε]
-
-namespace Term
-
--- TODO: distributor
-
--- TODO: inverse distributor
-
--- TODO: distributor is iso; this gives us the desired categorical structure! yay!

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

@@ -0,0 +1,40 @@
+import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Structural.Product
+import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Structural.Sum
+import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Distrib
+
+namespace BinSyntax
+
+variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [OrderBot ε]
+
+namespace Term
+
+-- theorem Eqv.packed_let1_den {Γ : Ctx α ε} {A B : Ty α}
+--   {a : Eqv φ Γ (A, e)} {b : Eqv φ ((A, ⊥)::Γ) (B, e)}
+--   : (let1 a b).packed (Δ := Δ)
+--   = Eqv.split ;;' (a.packed ⋉' _) ;;' b.packed
+--   := by
+--   sorry
+
+-- theorem Eqv.packed_let2_den {Γ : Ctx α ε} {A B C : Ty α}
+--   {a : Eqv φ Γ (A.prod B, e)} {b : Eqv φ ((B, ⊥)::(A, ⊥)::Γ) (C, e)}
+--   : (let2 a b).packed (Δ := Δ)
+--   = Eqv.split ;;' ((a.packed ;;' braid) ⋉' _) ;;' assoc ;;' b.packed := by
+--   sorry
+
+-- theorem Eqv.packed_case_den {Γ : Ctx α ε} {A B : Ty α}
+--   {a : Eqv φ Γ (A.coprod B, e)} {l : Eqv φ ((A, ⊥)::Γ) (C, e)} {r : Eqv φ ((B, ⊥)::Γ) (C, e)}
+--   : (case a l r).packed (Δ := Δ)
+--   = Eqv.split ;;' (a.packed ⋉' _) ;;' distr_inv ;;' sorry := by
+--   sorry
+
+-- @[simp]
+-- theorem Eqv.packed_inl_den {Γ : Ctx α ε} {A B : Ty α} {a : Eqv φ Γ (A, e)}
+--   : (inl (B := B) a).packed (Δ := Δ) = inl a.packed := sorry
+
+-- @[simp]
+-- theorem Eqv.packed_inr_den {Γ : Ctx α ε} {A B : Ty α} {a : Eqv φ Γ (B, e)}
+--   : (inr (A := A) a).packed (Δ := Δ) = inr a.packed := sorry
+
+-- @[simp]
+-- theorem Eqv.packed_abort_den {Γ : Ctx α ε} {A : Ty α} {a : Eqv φ Γ (Ty.empty, e)}
+--   : (abort a A).packed (Δ := Δ) = abort a.packed A := sorry

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

@@ -75,3 +75,34 @@ theorem Eqv.distl_inv_distl {A B C : Ty α} {Γ : Ctx α ε}
     <-wk_eff_distl (h := bot_le), <-wk_eff_distl_inv (h := bot_le), <-wk_eff_seq,
     distl_inv_distl_pure, wk_eff_nil
   ]
+
+def Eqv.distr {A B C : Ty α} {Γ : Ctx α ε}
+  : Eqv φ (⟨(A.prod C).coprod (B.prod C), ⊥⟩::Γ) ⟨(A.coprod B).prod C, e⟩
+  := coprod (inj_l ⋉' C) (inj_r ⋉' C)
+
+theorem Eqv.distl_braid {A B C : Ty α} {Γ : Ctx α ε}
+  : distl ;;' braid
+  = sum braid braid ;;' distr (φ := φ) (Γ := Γ) (A := A) (B := B) (C := C) (e := e) := by
+  rw [distr, sum_coprod, distl, coprod_seq, rtimes_braid, rtimes_braid]
+
+theorem Eqv.distr_braid {A B C : Ty α} {Γ : Ctx α ε}
+  : distr ;;' braid
+  = sum braid braid ;;' distl (φ := φ) (Γ := Γ) (A := A) (B := B) (C := C) (e := e)
+  := by rw [distl, sum_coprod, distr, coprod_seq, ltimes_braid, ltimes_braid]
+
+def Eqv.distr_inv {A B C : Ty α} {Γ : Ctx α ε}
+  : Eqv φ (⟨(A.coprod B).prod C, ⊥⟩::Γ) ⟨(A.prod C).coprod (B.prod C), e⟩
+  := let2 nil (case (var 1 (by simp))
+    (pair (var 0 Ctx.Var.bhead) (var 1 (by simp))).inl
+    (pair (var 0 Ctx.Var.bhead) (var 1 (by simp))).inr)
+
+-- theorem Eqv.distr_distr_inv {A B C : Ty α} {Γ : Ctx α ε}
+--   : (distr : Eqv φ (⟨(A.prod C).coprod (B.prod C), ⊥⟩::Γ) ⟨(A.coprod B).prod C, e⟩)
+--   ;;' distr_inv = nil := by
+--   rw [distr, coprod_seq]
+  -- simp only [distr, distr_inv, coprod_seq]
+  -- simp [
+  --   seq, let1_beta_pure, coprod, wk1_let2, rtimes, wk1_tensor, let2_tensor, subst_liftn₂_tensor,
+  --   wk2, Nat.liftnWk, nil, inj_l, inj_r, case_inl, case_inr, <-inl_let2, <-inr_let2, let2_eta,
+  --   case_eta
+  -- ]

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

@@ -1,5 +1,3 @@
-import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Seq
-import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Sum
 import DeBruijnSSA.BinSyntax.Rewrite.Term.Compose.Product
 import DeBruijnSSA.BinSyntax.Typing.Term.Structural
 

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

@@ -410,6 +410,29 @@ def Eqv.sum {A A' B B' : Ty α} {Γ : Ctx α ε}
 
 -- TODO: sum is a bifunctor; so that's nil nil and seq!
 
+@[simp]
+theorem Eqv.sum_nil {A B : Ty α} {Γ : Ctx α ε}
+  : sum (φ := φ) (A := A) (B := B) (Γ := Γ) (e := e) nil nil = nil := by
+  simp [sum, coprod_inl_inr]
+
+theorem Eqv.sum_coprod {A A' B B' C : Ty α} {Γ : Ctx α ε}
+  {l : Eqv φ (⟨A, ⊥⟩::Γ) ⟨A', e⟩}
+  {r : Eqv φ (⟨B, ⊥⟩::Γ) ⟨B', e⟩}
+  {f : Eqv φ (⟨A', ⊥⟩::Γ) ⟨C, e⟩}
+  {g : Eqv φ (⟨B', ⊥⟩::Γ) ⟨C, e⟩}
+  : sum l r ;;' coprod f g = coprod (l ;;' f) (r ;;' g) := by
+  simp [sum, coprod_seq, <-seq_assoc, inj_l_coprod, inj_r_coprod]
+
+theorem Eqv.sum_seq {A₀ A₁ A₂ B₀ B₁ B₂ : Ty α} {Γ : Ctx α ε}
+  {l : Eqv φ (⟨A₀, ⊥⟩::Γ) ⟨A₁, e⟩}
+  {r : Eqv φ (⟨B₀, ⊥⟩::Γ) ⟨B₁, e⟩}
+  {l' : Eqv φ (⟨A₁, ⊥⟩::Γ) ⟨A₂, e⟩}
+  {r' : Eqv φ (⟨B₁, ⊥⟩::Γ) ⟨B₂, e⟩}
+  : sum l r ;;' sum l' r' = sum (l ;;' l') (r ;;' r') := by
+  conv => lhs; rhs; rw [sum]
+  simp only [sum_coprod, seq_assoc]
+  rfl
+
 def Eqv.braid_sum {A B : Ty α} {Γ : Ctx α ε} : Eqv φ (⟨A.coprod B, ⊥⟩::Γ) ⟨B.coprod A, e⟩
   := nil.swap_sum
 

DeBruijnSSA/BinSyntax/Typing/Region/Basic.lean

@@ -152,6 +152,17 @@ theorem InS.cast_inj {Γ Γ' : Ctx α ε} {L L' : LCtx α} {r r' : InS φ Γ L}
 def Wf.toInS {Γ : Ctx α ε} {r : Region φ} {L} (h : r.Wf Γ L) : InS φ Γ L
   := ⟨r, h⟩
 
+@[simp]
+theorem Wf.coe_toInS {Γ : Ctx α ε} {r : Region φ} {L} {h : r.Wf Γ L}
+  : h.toInS.val = r := rfl
+
+def WfD.toInS {Γ : Ctx α ε} {r : Region φ} {L} (h : r.WfD Γ L) : InS φ Γ L
+  := ⟨r, h.toWf⟩
+
+@[simp]
+theorem WfD.coe_toInS {Γ : Ctx α ε} {r : Region φ} {L} {h : r.WfD Γ L}
+  : h.toInS.val = r := rfl
+
 def InS.br {Γ : Ctx α ε} {L : LCtx α} (ℓ) (a : Term.InS φ Γ ⟨A, ⊥⟩)
   (hℓ : L.Trg ℓ A) : InS φ Γ L
   := ⟨Region.br ℓ a, Wf.br hℓ a.2⟩

DeBruijnSSA/BinSyntax/Typing/Term/Basic.lean

@@ -269,6 +269,20 @@ theorem Term.WfD.toWf {Γ : Ctx α ε} {a : Term φ} {V} (h : WfD Γ a V) : Wf 
   | abort da => Wf.abort da.toWf
   | unit e => Wf.unit e
 
+def Term.Wf.toIns {Γ : Ctx α ε} {a : Term φ} {V} (h : Wf Γ a V) : InS φ Γ V
+  := ⟨a, h⟩
+
+@[simp]
+theorem Term.Wf.coe_toInS {Γ : Ctx α ε} {a : Term φ} {V} {h : Wf Γ a V}
+  : (h.toIns : Term φ) = a := rfl
+
+def Term.WfD.toInS {Γ : Ctx α ε} {a : Term φ} (h : WfD Γ a V) : InS φ Γ V
+  := ⟨a, h.toWf⟩
+
+@[simp]
+theorem Term.WfD.coe_toInS {Γ : Ctx α ε} {a : Term φ} {V} {h : WfD Γ a V}
+  : (h.toInS : Term φ) = a := rfl
+
 theorem Term.Wf.nonempty {Γ : Ctx α ε} {a : Term φ} {V} (h : Wf Γ a V) : Nonempty (WfD Γ a V)
   := match h with
   | var dv => ⟨WfD.var dv⟩

DeBruijnSSA/BinSyntax/Typing/Term/Structural.lean

@@ -424,3 +424,19 @@ 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
 
 end Sum
+
+-- section Arrow
+
+-- def arr : Term φ → Term φ
+-- | var x => pi_n x
+-- | op f a => a.arr.seq (op f nil)
+-- | let1 a b => let1 a.arr sorry
+-- | pair a b => sorry
+-- | let2 a b => sorry
+-- | inl a => sorry
+-- | inr a => sorry
+-- | case a l r => sorry
+-- | unit => sorry
+-- | abort a => sorry
+
+-- end Arrow