Work on region densem

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

@@ -0,0 +1,76 @@
+import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Structural
+import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Functor
+import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Elgot
+
+namespace BinSyntax
+
+variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [OrderBot ε]
+
+namespace Region
+
+theorem Eqv.packed_br_den {Γ : Ctx α ε} {L : LCtx α}
+  {ℓ} {a : Term.Eqv φ Γ (A, ⊥)} {hℓ}
+  : (br (L := L) ℓ a hℓ).packed (Δ := Δ)
+  = ret ((a.packed.wk_res ⟨hℓ.get, by rfl⟩)) ;; ret (Term.Eqv.inj_n _ ⟨ℓ, hℓ.length⟩) := by
+  rw [<-ret_of_seq, Term.Eqv.seq_inj_n, packed_br]
+
+theorem Eqv.packed_let1_den {Γ : Ctx α ε} {R : LCtx α}
+  {a : Term.Eqv φ Γ (A, e)} {r : Eqv φ ((A, ⊥)::Γ) R}
+  : (let1 a r).packed (Δ := Δ)
+  = ret Term.Eqv.split ;; _ ⋊ lret a.packed ;; r.packed := by
+  rw [<-lret_rtimes, ret_seq, lret]
+  simp only [Term.Eqv.rtimes, Term.Eqv.tensor, Term.Eqv.wk1_nil, Term.Eqv.wk1_packed, let1_let2,
+    InS.nil_vwk1, vwk1_let2, vwk3, vwk_let1, Term.Eqv.wk_pair, vwk_quot,
+    InS.nil_vwk_lift, vsubst_let2, Term.Eqv.nil_subst0, Term.Eqv.wk_eff_split, vsubst_let1,
+    Term.Eqv.subst_pair]
+  rw [<-Term.Eqv.wk_eff_split (lo := ⊥) (h := bot_le), let2_wk_eff, Term.Eqv.split, let2_pair]
+  simp only [vwk1_quot, InS.nil_vwk1, vwk_quot, InS.nil_vwk_lift, let1_beta, vsubst_let1,
+    Term.Eqv.subst_pair, let1_seq]
+  rw [packed_let1, <-nil, <-ret_nil, vsubst_ret]
+  simp only [Term.Eqv.nil, Term.Eqv.wk0_var, zero_add, ← Ctx.InS.lift_wk2, Term.Eqv.wk_var,
+    Set.mem_setOf_eq, Ctx.InS.coe_lift, Ctx.InS.coe_wk2, Nat.liftWk_succ, Term.Eqv.wk_lift_packed,
+    Term.Eqv.subst_liftn₂_packed, Term.Eqv.subst_lift_var_zero, vsubst_br]
+  conv =>
+    rhs
+    rw [let1_pair, let1_pair]
+    simp only [let1_beta, Nat.liftnWk, Nat.ofNat_pos, ↓reduceIte, zero_add,
+    Term.Eqv.subst_liftn₂_var_one, Term.Eqv.var_succ_subst0, Term.Eqv.var0_subst0, List.length_cons,
+    ↓dreduceIte, Nat.reduceAdd, Set.mem_setOf_eq, Ctx.InS.coe_lift, Ctx.InS.coe_wk2,
+    Nat.liftWk_succ, id_eq, Nat.reduceSub, Nat.succ_eq_add_one, Fin.zero_eta, List.get_eq_getElem,
+    Fin.val_zero, List.getElem_cons_zero, Term.Eqv.wk_res_eff, Term.Eqv.wk_eff_var
+    ]
+    rw [<-Term.Eqv.wk_eff_var (lo := ⊥) (hn := by simp) (he := bot_le), let1_wk_eff, let1_beta]
+  simp only [Term.Eqv.wk_var, Nat.succ_eq_add_one, zero_add, vsubst_let1]
+  congr
+  · induction a using Quotient.inductionOn
+    apply Term.Eqv.eq_of_term_eq
+    simp [Term.subst_subst]
+    congr
+    funext n
+    simp only [Term.Subst.pi_n, Term.pi_n, Term.Subst.comp, Term.subst_pn]
+    rfl
+  · conv => rhs; rhs; rhs; rhs; rhs; rw [<-ret, <-Term.Eqv.nil, ret_nil, nil_seq]
+    simp only [let1_beta, vwk1, vsubst_vsubst]
+    simp only [<-vsubst_fromWk, vsubst_vsubst, packed, packed_out, packed_in]
+    congr 1
+    ext k
+    simp [Term.Subst.Eqv.get_comp, Term.Eqv.subst_fromWk, <-Ctx.InS.lift_wk0]
+    apply Term.Eqv.eq_of_term_eq
+    simp only [Term.InS.coe_subst, Term.InS.coe_subst0, Term.InS.coe_pi_n, Term.pi_n, Term.subst_pn,
+      Term.wk_pn, Term.InS.coe_wk,
+      Term.InS.coe_pair, Term.InS.coe_var, List.length_cons, Term.Subst.liftn, Nat.ofNat_pos,
+      ↓reduceIte, Ctx.InS.lift_wk0, Term.Subst.InS.coe_comp, Term.Subst.InS.coe_lift, Ctx.InS.coe_wk1,
+      Nat.liftnWk]
+    rfl
+
+-- theorem Eqv.packed_let2_den {Γ : Ctx α ε} {R : LCtx α}
+--   {a : Term.Eqv φ Γ (A.prod B, e)} {r : Eqv φ ((B, ⊥)::(A, ⊥)::Γ) R}
+--   : (let2 a r).packed (Δ := Δ)
+--   = ret Term.Eqv.split ;; _ ⋊ lret a.packed ;; assoc_inv ;; r.packed := by sorry
+
+-- theorem Eqv.packed_case_den {Γ : Ctx α ε} {R : LCtx α}
+--   {a : Term.Eqv φ Γ (A.coprod B, e)} {r : Eqv φ ((A, ⊥)::Γ) R} {s : Eqv φ ((B, ⊥)::Γ) R}
+--   : (case a r s).packed (Δ := Δ)
+--   = ret Term.Eqv.split ;; _ ⋊ lret a.packed ;; distl_inv ;; coprod r.packed s.packed := by sorry
+
+-- TODO: cfg: needs Böhm-Jacopini lore

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

@@ -0,0 +1,92 @@
+import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Product
+import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Sum
+
+namespace BinSyntax
+
+variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [OrderBot ε]
+
+namespace Region
+
+def Eqv.lret {Γ : Ctx α ε} {A B : Ty α} (a : Term.Eqv φ ((A, ⊥)::Γ) (B, e))
+  : Eqv φ ((A, ⊥)::Γ) (B::L) := let1 a nil
+
+theorem Eqv.lret_pure {Γ : Ctx α ε} {A B : Ty α} {a : Term.Eqv φ ((A, ⊥)::Γ) (B, ⊥)}
+  : lret (L := L) a = ret a := by simp [lret, ret, let1_beta, <-ret_nil]
+
+@[simp]
+theorem Eqv.lret_wk_eff {Γ : Ctx α ε} {A B : Ty α}
+  {a : Term.Eqv φ ((A, ⊥)::Γ) (B, lo)} {h : lo ≤ hi} : (lret (L := L) (a.wk_eff h)) = lret a
+  := by simp [lret]
+
+@[simp]
+theorem Eqv.vwk_slift_lret {Γ Δ : Ctx α ε} {A B : Ty α} {a : Term.Eqv φ ((A, ⊥)::Δ) (B, e)}
+  {ρ : Γ.InS Δ} : (lret (L := L) a).vwk ρ.slift = lret (a.wk ρ.slift)
+  := by simp [lret]
+
+@[simp]
+theorem Eqv.vwk1_lret {Γ : Ctx α ε} {A B : Ty α} {a : Term.Eqv φ ((A, ⊥)::Γ) (B, e)}
+  : (lret (L := L) a).vwk1 (inserted := inserted) = lret (a.wk1)
+  := by simp only [lret, vwk1_let1]; rfl
+
+@[simp]
+theorem Eqv.lret_nil {Γ : Ctx α ε} {A : Ty α}
+  : (lret (L := L) <| Term.Eqv.nil (φ := φ) (Γ := Γ) (A := A) (e := e)) = nil := by
+  rw [lret, <-Term.Eqv.wk_eff_nil (lo := ⊥) (h := bot_le), let1_wk_eff, Term.Eqv.nil, let1_0_nil]
+
+theorem Eqv.lret_lret {Γ : Ctx α ε}
+  {f : Term.Eqv φ ((A, ⊥)::Γ) (B, e)} {g : Term.Eqv φ ((B, ⊥)::Γ) (C, e)}
+  : lret f ;; lret g = lret (L := L) (f ;;' g)
+  := by simp only [lret, let1_seq, vwk1_let1, nil_seq, Term.Eqv.seq, let1_let1]; rfl
+
+theorem Eqv.lret_of_seq {Γ : Ctx α ε}
+  {f : Term.Eqv φ ((A, ⊥)::Γ) (B, e)} {g : Term.Eqv φ ((B, ⊥)::Γ) (C, e)}
+  : lret (L := L) (f ;;' g) = lret f ;; lret g := lret_lret.symm
+
+theorem Eqv.lret_rtimes {Γ : Ctx α ε}
+  {f : Term.Eqv φ ((A, ⊥)::Γ) (B, e)}
+  : lret (L := L) (C ⋊' f) = C ⋊ lret f := by
+  rw [lret, Term.Eqv.rtimes, Term.Eqv.tensor, let1_let2, rtimes]
+  apply congrArg
+  simp only [Term.Eqv.wk1_nil, InS.nil_vwk1, vwk1_lret, Term.Eqv.wk0_nil]
+  rw [lret, let1_seq, nil_seq, vwk1_ret]
+  simp only [InS.nil_vwk1, Term.Eqv.wk1_pair, Term.Eqv.wk1_var_succ, zero_add,
+    Term.Eqv.wk1_var0, List.length_cons, Fin.zero_eta, List.get_eq_getElem, Fin.val_zero,
+    List.getElem_cons_zero]
+  rw [
+    let1_pair, let1_beta,
+    <-Term.Eqv.wk_eff_var (lo := ⊥) (hn := by simp) (he := bot_le), let1_wk_eff, let1_beta
+  ]
+  simp only [vsubst_let1]
+  congr
+  induction f using Quotient.inductionOn
+  apply Term.Eqv.eq_of_term_eq
+  simp
+
+theorem Eqv.lret_braid {Γ : Ctx α ε}
+  : lret (Γ := Γ) (L := L) (e := e) (Term.Eqv.braid) = braid (φ := φ) (left := A) (right := B) := by
+  rw [<-Term.Eqv.wk_eff_braid (lo := ⊥) (h := bot_le), lret_wk_eff, lret_pure, braid_eq_ret]
+
+theorem Eqv.lret_ltimes {Γ : Ctx α ε}
+  {f : Term.Eqv φ ((A, ⊥)::Γ) (B, e)}
+  : lret (L := L) (f ⋉' C) = lret f ⋉ C := by
+  rw [<-Term.Eqv.braid_rtimes_braid]
+  simp [lret_of_seq, lret_braid, lret_rtimes, braid_rtimes_braid]
+
+theorem Eqv.lret_assoc {Γ : Ctx α ε}
+  : lret (Γ := Γ) (L := L) (e := e) (Term.Eqv.assoc)
+  = assoc (φ := φ) (A := A) (B := B) (C := C) := by
+  rw [<-Term.Eqv.wk_eff_assoc (lo := ⊥) (h := bot_le), lret_wk_eff, lret_pure, assoc_eq_ret]
+
+theorem Eqv.lret_inj_l {Γ : Ctx α ε}
+  : lret (L := L) (Term.Eqv.inj_l (e := e)) = inj_l (φ := φ) (Γ := Γ) (A := A) (B := B) := by
+  rw [<-Term.Eqv.wk_eff_inj_l (lo := ⊥) (h := bot_le), lret_wk_eff, lret_pure]; rfl
+
+theorem Eqv.lret_inj_r {Γ : Ctx α ε}
+  : lret (L := L) (Term.Eqv.inj_r (e := e)) = inj_r (φ := φ) (Γ := Γ) (A := A) (B := B) := by
+  rw [<-Term.Eqv.wk_eff_inj_r (lo := ⊥) (h := bot_le), lret_wk_eff, lret_pure]; rfl
+
+theorem Eqv.lret_coprod {Γ : Ctx α ε}
+  {f : Term.Eqv φ ((A, ⊥)::Γ) (C, e)} {g : Term.Eqv φ ((B, ⊥)::Γ) (C, e)}
+  : lret (L := L) (f.coprod g) = coprod (lret f) (lret g) := by
+  rw [lret, Term.Eqv.coprod, let1_case, coprod]
+  simp only [vwk1_lret]; rfl

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

@@ -73,6 +73,14 @@ theorem Eqv.nil_vwk1 {Γ : Ctx α ε} {L : LCtx α}
   : (Eqv.nil (φ := φ) (ty := ty) (rest := Γ) (targets := L)).vwk1 (inserted := inserted)
   = Eqv.nil := rfl
 
+theorem Eqv.nil_vwk2 {Γ : Ctx α ε} {L : LCtx α}
+  : (Eqv.nil (φ := φ) (ty := ty) (rest := head::Γ) (targets := L)).vwk2 (inserted := inserted)
+  = Eqv.nil := rfl
+
+theorem Eqv.nil_vsubst_lift {Γ Δ : Ctx α ε} {L : LCtx α} {σ : Term.Subst.Eqv φ Γ Δ}
+  : (Eqv.nil (φ := φ) (ty := ty) (rest := Δ) (targets := L)).vsubst (σ.lift (le_refl _))
+  = Eqv.nil := by induction σ using Quotient.inductionOn; rfl
+
 @[simp]
 theorem Eqv.nil_lwk1 {Γ : Ctx α ε} {L : LCtx α}
   : (Eqv.nil (φ := φ) (ty := ty) (rest := Γ) (targets := L)).lwk1 (inserted := inserted)

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

@@ -513,6 +513,14 @@ theorem Eqv.pi_l_runit {A : Ty α} {Γ : Ctx α ε}
 def Eqv.braid {A B : Ty α} {Γ : Ctx α ε} : Eqv φ (⟨A.prod B, ⊥⟩::Γ) ⟨B.prod A, e⟩
   := let2 nil $ pair (var 0 (by simp)) (var 1 (by simp))
 
+@[simp]
+theorem Eqv.wk_eff_braid {A B : Ty α} {Γ : Ctx α ε} {h : lo ≤ hi}
+  : (braid : Eqv φ (⟨A.prod B, ⊥⟩::Γ) ⟨B.prod A, lo⟩).wk_eff h = braid := rfl
+
+@[simp]
+theorem Eqv.Pure.braid {A B : Ty α} {Γ : Ctx α ε}
+  : (braid : Eqv φ (⟨A.prod B, ⊥⟩::Γ) ⟨B.prod A, e⟩).Pure := ⟨Eqv.braid, rfl⟩
+
 theorem Eqv.wk1_braid {A B : Ty α} {Γ : Ctx α ε}
   : (braid : Eqv φ (⟨A.prod B, ⊥⟩::Γ) ⟨B.prod A, e⟩).wk1 (inserted := inserted) = braid := rfl
 
@@ -855,9 +863,9 @@ theorem Eqv.Pure.right_central {A A' B B' : Ty α} {Γ : Ctx α ε}
   := by
   apply Eq.symm
   rw [
-    <-braid_ltimes_braid, <-seq_assoc, braid_ltimes (l := l), seq_assoc, <-seq_assoc (a := braid),
-    hr.left_central, seq_assoc, braid_rtimes, <-seq_assoc, ltimes_braid (l := r), seq_assoc,
-    <-seq_assoc (c := braid), braid_braid, seq_nil
+    <-braid_ltimes_braid, <-seq_assoc, braid_ltimes (l := l), seq_assoc,
+    <-seq_assoc (a := Eqv.braid), hr.left_central, seq_assoc, braid_rtimes, <-seq_assoc,
+    ltimes_braid (l := r), seq_assoc, <-seq_assoc (c := Eqv.braid), braid_braid, seq_nil
   ]
 
 theorem Eqv.tensor_seq_of_comm {A₀ A₁ A₂ B₀ B₁ B₂ : Ty α} {Γ : Ctx α ε}

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

@@ -84,6 +84,21 @@ theorem Eqv.inj_n_def {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length}
 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
 
+theorem Eqv.wk1_inj_n {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length}
+  : (inj_n (φ := φ) (Γ := Γ) (e := e) R i).wk1 (inserted := inserted) = inj_n R i := by
+  rw [inj_n_def', wk1_inj, wk1_nil, inj_n_def']
+
+theorem Eqv.seq_inj_n  {Γ : Ctx α ε} {R : LCtx α} {i : Fin R.length}
+  {a : Eqv φ ((X, ⊥)::Γ) (R.get i, e)}
+  : a ;;' Eqv.inj_n R i = a.inj := by
+  rw [seq, wk1_inj_n]
+  induction R generalizing Γ with
+  | nil => exact i.elim0
+  | cons _ _ I =>
+    cases i using Fin.cases with
+    | zero => simp [inj_n, <-inr_let1, nil, let1_eta]
+    | succ i => simp [inj_n, <-inl_let1, I, inj]
+
 -- 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/Rewrite/Term/Compose/Sum.lean

@@ -302,6 +302,11 @@ theorem Eqv.wk2_inj_l {A B : Ty α} {Γ : Ctx α ε}
   : (inj_l (φ := φ) (e := e) (A := A) (B := B) (Γ := head::Γ)).wk2 (inserted := inserted) = inj_l
   := by simp [inj_l]
 
+@[simp]
+theorem Eqv.wk_eff_inj_l {A B : Ty α} {Γ : Ctx α ε} {h : lo ≤ hi}
+  : (inj_l (φ := φ) (A := A) (B := B) (Γ := Γ)).wk_eff h = inj_l
+  := by simp [inj_l]
+
 theorem Eqv.seq_inj_l {A B C : Ty α} {Γ : Ctx α ε} {f : Eqv φ (⟨A, ⊥⟩::Γ) ⟨B, e⟩}
   : f ;;' inj_l (B := C) = f.inl := by
   rw [seq, wk1_inj_l, inj_l]
@@ -320,6 +325,11 @@ theorem Eqv.wk2_inj_r {A B : Ty α} {Γ : Ctx α ε}
   : (inj_r (φ := φ) (e := e) (A := A) (B := B) (Γ := head::Γ)).wk2 (inserted := inserted) = inj_r
   := by simp [inj_r]
 
+@[simp]
+theorem Eqv.wk_eff_inj_r {A B : Ty α} {Γ : Ctx α ε} {h : lo ≤ hi}
+  : (inj_r (φ := φ) (A := A) (B := B) (Γ := Γ)).wk_eff h = inj_r
+  := by simp [inj_r]
+
 theorem Eqv.seq_inj_r {Γ : Ctx α ε} {f : Eqv φ (⟨B, ⊥⟩::Γ) ⟨C, e⟩}
   : f ;;' inj_r (A := A) = f.inr := by
   rw [seq, wk1_inj_r, inj_r]

DeBruijnSSA/BinSyntax/Typing/Ctx.lean

@@ -391,6 +391,10 @@ theorem InS.lift_wk1 {left right inserted} {Γ : Ctx α ε}
   : wk1.lift (le_refl _) = (wk2 : InS (left::right::inserted::Γ) (left::right::Γ))
   := by ext; simp [Nat.liftnWk_two]
 
+theorem InS.lift_wk2 {left middle right inserted} {Γ : Ctx α ε}
+  : wk2.lift (le_refl _) = (wk3 : InS (left::middle::right::inserted::Γ) (left::middle::right::Γ))
+  := by ext; simp [Nat.liftnWk_succ, Nat.liftnWk_zero]
+
 theorem Wkn.liftn_append (Ξ) (h : Γ.Wkn Δ ρ)
   : Wkn (Ξ ++ Γ) (Ξ ++ Δ) (Nat.liftnWk Ξ.length ρ)
   := Wkn_iff.mpr ((Wkn_iff.mp h).liftn_append Ξ)