Packed distributivity

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

@@ -34,16 +34,65 @@ theorem Eqv.packed_in_coprod_dist {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   {l : Eqv φ (⟨A, ⊥⟩::Γ) L} {r : Eqv φ (⟨B, ⊥⟩::Γ) L}
   : (l.coprod r).packed_in (Δ := Δ) = case (Term.Eqv.distl_inv (e := ⊥)) l.packed_in r.packed_in
   := by
-  rw [coprod, packed_in_case_split]
-  sorry
+  rw [coprod, packed_in_case_split, packed_var, pi_n_zero', Term.Eqv.pi_r]
+  simp only [List.length_cons, Fin.zero_eta, List.get_eq_getElem, Fin.val_zero,
+    List.getElem_cons_zero, wk_res_self]
+  rw [<-Term.Eqv.pi_r, Term.Eqv.split_rtimes_pi_r_distl_packed]
+  conv => rhs; rw [case_bind, <-coprod]
+  rw [case_bind, <-coprod, Term.Eqv.seq, let1_let1]
+  apply congrArg
+  simp [
+    Term.Eqv.sum, Term.Eqv.coprod, let1_case, coprod, let1_beta, Term.Eqv.wk1_seq,
+    Term.Eqv.wk2_seq, Term.Eqv.seq_inj_l, Term.Eqv.seq_inj_r, case_case, case_inl, case_inr
+  ]
+  congr 1 <;> {
+    simp [packed_in, vsubst_vsubst, vwk1, <-vsubst_fromWk]
+    congr; ext k; cases k using Fin.cases with
+    | zero =>
+      simp only [List.get_eq_getElem, List.length_cons, Fin.val_zero, List.getElem_cons_zero,
+        Term.Subst.Eqv.get_comp, Term.Subst.Eqv.get_fromWk, Fin.zero_eta, Set.mem_setOf_eq,
+        Ctx.InS.coe_wk1, Nat.liftWk_zero, subst_var, id_eq, Term.Subst.Eqv.get_unpack, wk_res_self]
+      rw [<-let1_beta_pure, <-wk1_pi_n, <-Term.Eqv.seq, Term.Eqv.wk1_wk2]
+      simp only [List.get_eq_getElem, List.length_cons, Fin.val_zero, List.getElem_cons_zero, split,
+        Term.Eqv.ltimes, pair_tensor_pure, Term.Eqv.nil_seq, Term.Eqv.seq_nil, wk1_rtimes, wk1_pair,
+        wk1_inj_l, wk1_nil]
+      simp only [Term.Eqv.rtimes, tensor, wk1_nil, wk1_pair, wk1_inj_l, seq_assoc_inv,
+        reassoc_inv_let2, reassoc_inv_beta, seq_let2, wk1_pi_n, pi_n_zero, Term.Eqv.pi_r, pr]
+      congr
+      exact Term.Eqv.pair_pi_r_pure _ _
+    | succ k =>
+      simp only [List.get_eq_getElem, List.length_cons, Fin.val_succ, List.getElem_cons_succ, split,
+        pair_ltimes_pure, Term.Eqv.nil_seq, wk1_wk2, Term.Subst.Eqv.get_comp,
+        Term.Subst.Eqv.get_fromWk, Set.mem_setOf_eq, Ctx.InS.coe_wk1, Nat.liftWk_succ,
+        Nat.succ_eq_add_one, subst_var, id_eq, Term.Subst.Eqv.get_unpack, wk_res_self]
+      simp only [wk1_rtimes, wk1_pair, wk1_inj_l, wk1_nil]
+      simp only [Term.Eqv.rtimes, tensor, Term.Eqv.nil, wk1_var0, List.length_cons, Fin.zero_eta,
+        List.get_eq_getElem, Fin.val_zero, List.getElem_cons_zero, wk0_var, zero_add, wk1_pair,
+        wk1_inj_l, seq_assoc_inv, reassoc_inv_let2, reassoc_inv_beta]
+      rw [pi_n_succ2']
+      conv => lhs; rhs; rw [<-Term.Eqv.seq_assoc, Term.Eqv.seq]
+      simp only [List.get_eq_getElem, wk1_seq, wk1_pi_l, wk1_pi_n, subst_let1, subst_lift_seq,
+        subst_lift_pi_l, subst_lift_pi_n]
+      conv => lhs; lhs; rw [Term.Eqv.pi_l]
+      simp only [subst_pl, nil_subst0, wk_eff_let2, wk_eff_var, wk_eff_pair, wk_eff_inj_l, pl_let2]
+      rw [Term.Eqv.Pure.pl_pair (hb := by exact ⟨var 0 Ctx.Var.shead, rfl⟩)]
+      rw [
+        <-Term.Eqv.wk1_pi_l, <-Term.Eqv.wk1_pi_n, <-Term.Eqv.wk1_seq, <-Term.Eqv.seq,
+        Term.Eqv.seq_assoc, Term.Eqv.seq_let2
+      ]
+      simp only [wk1_inj_r, wk_eff_inj_r, wk1_pi_l, Term.Eqv.Pure.inj_r, pair_pi_l, pi_n_succ,
+        Term.Eqv.Pure.inj_l, List.get_eq_getElem]
+      rfl
+  }
 
 theorem Eqv.packed_in_coprod_arr {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   {l : Eqv φ (⟨A, ⊥⟩::Γ) (C::L)} {r : Eqv φ (⟨B, ⊥⟩::Γ) (C::L)}
   : (l.coprod r).packed_in (Δ := Δ)
   = distl_inv ;; coprod l.packed_in r.packed_in
   := by
-  rw [coprod, packed_in_case_split, coprod]
-  sorry
+  rw [packed_in_coprod_dist, coprod, distl_inv_eq_ret, ret_seq]
+  simp
+  congr <;> exact vsubst_lift_packed_in.symm
 
 theorem Eqv.packed_in_pack_coprod_arr {Γ : Ctx α ε} {R L : LCtx α}
   {G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) (A::L)}

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

@@ -163,6 +163,15 @@ theorem Eqv.split_rtimes_pi_r_distl_pure {X A B : Ty α}
     rw [<-Pure.let2_dist_pair (ha := by simp)]
     simp [seq, let1_beta_pure, inj_r]
 
+theorem Eqv.split_rtimes_pi_r_distl {X A B : Ty α}
+  : split (φ := φ) (A := X.prod (A.coprod B)) (e := e) (Γ := Γ)
+  ;;' _ ⋊' pi_r ;;' distl_inv
+  = distl_inv
+  ;;' sum
+    (_ ⋊' (split ;;' inj_l ⋉' _) ;;' assoc_inv)
+    (_ ⋊' (split ;;' inj_r ⋉' _) ;;' assoc_inv)
+  := congrArg (wk_eff (he := bot_le)) (split_rtimes_pi_r_distl_pure)
+
 --   rw [seq_distl_inv]
 --   simp [
 --     seq_rtimes, split, distl_inv, seq_let2, coprod_seq, sum, wk1_seq, wk1_coprod,

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

@@ -1054,14 +1054,26 @@ def Eqv.assoc {A B C : Ty α} {Γ : Ctx α ε}
 def Eqv.assoc_inv {A B C : Ty α} {Γ : Ctx α ε}
   : Eqv (φ := φ) (⟨A.prod (B.prod C), ⊥⟩::Γ) ⟨(A.prod B).prod C, e⟩ := nil.reassoc_inv
 
+@[simp]
 theorem Eqv.wk1_assoc {A B C : Ty α} {Γ : Ctx α ε}
   : (assoc (φ := φ) (Γ := Γ) (A := A) (B := B) (C := C) (e := e)).wk1 (inserted := inserted) = assoc
   := rfl
 
+@[simp]
+theorem Eqv.wk2_assoc {A B C : Ty α} {Γ : Ctx α ε}
+  : (assoc (φ := φ) (Γ := V::Γ) (A := A) (B := B) (C := C) (e := e)).wk2 (inserted := inserted)
+  = assoc := rfl
+
+@[simp]
 theorem Eqv.wk1_assoc_inv {A B C : Ty α} {Γ : Ctx α ε}
   : (assoc_inv (φ := φ) (Γ := Γ) (A := A) (B := B) (C := C) (e := e)).wk1 (inserted := inserted)
   = assoc_inv := rfl
 
+@[simp]
+theorem Eqv.wk2_assoc_inv {A B C : Ty α} {Γ : Ctx α ε}
+  : (assoc_inv (φ := φ) (Γ := V::Γ) (A := A) (B := B) (C := C) (e := e)).wk2 (inserted := inserted)
+  = assoc_inv := rfl
+
 theorem Eqv.seq_prod_assoc {A B C : Ty α} {Γ : Ctx α ε}
   (r : Eqv φ (⟨X, ⊥⟩::Γ) ⟨(A.prod B).prod C, e⟩)
   : r ;;' assoc = r.reassoc := by rw [assoc, seq_reassoc, seq_nil]
@@ -1319,3 +1331,7 @@ theorem Eqv.rtimes_pi_r {A B : Ty α} {Γ : Ctx α ε} {r : Eqv φ ((A, ⊥)::Γ
   simp only [rtimes, tensor, wk1_nil, seq_let2, wk1_pi_r, pi_r_seq]
   rw [pair_pi_r]
   exact ⟨(var 1 Ctx.Var.shead.step), rfl⟩
+
+theorem Eqv.pl_let2 {A B C : Ty α} {Γ : Ctx α ε}
+  {a : Eqv φ Γ ⟨A.prod B, e⟩} {r : Eqv φ ((B, ⊥)::(A, ⊥)::Γ) ⟨C.prod B, e⟩}
+  : (let2 a r).pl = let2 a r.pl := by simp [pl, let2_let2]

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

@@ -312,6 +312,10 @@ theorem Eqv.subst_lift_coprod {A B C : Ty α} {Γ Δ : Ctx α ε} {ρ : Subst.Eq
 def Eqv.inj_l {A B : Ty α} {Γ : Ctx α ε} : Eqv (φ := φ) (⟨A, ⊥⟩::Γ) ⟨A.coprod B, e⟩
   := inl nil
 
+@[simp]
+theorem Eqv.Pure.inj_l {A B : Ty α} {Γ : Ctx α ε}
+  : Pure (inj_l (φ := φ) (A := A) (B := B) (Γ := Γ) (e := e)) := ⟨Eqv.inj_l, rfl⟩
+
 @[simp]
 theorem Eqv.wk1_inj_l {A B : Ty α} {Γ : Ctx α ε}
   : (inj_l (φ := φ) (e := e) (A := A) (B := B) (Γ := Γ)).wk1 (inserted := inserted) = inj_l
@@ -345,6 +349,10 @@ theorem Eqv.seq_inj_l {A B C : Ty α} {Γ : Ctx α ε} {f : Eqv φ (⟨A, ⊥⟩
 def Eqv.inj_r {A B : Ty α} {Γ : Ctx α ε} : Eqv (φ := φ) (⟨B, ⊥⟩::Γ) ⟨A.coprod B, e⟩
   := inr nil
 
+@[simp]
+theorem Eqv.Pure.inj_r {A B : Ty α} {Γ : Ctx α ε}
+  : Pure (inj_r (φ := φ) (A := A) (B := B) (Γ := Γ) (e := e)) := ⟨Eqv.inj_r, rfl⟩
+
 @[simp]
 theorem Eqv.wk1_inj_r {A B : Ty α} {Γ : Ctx α ε}
   : (inj_r (φ := φ) (e := e) (A := A) (B := B) (Γ := Γ)).wk1 (inserted := inserted) = inj_r

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

@@ -13,31 +13,14 @@ def Eqv.distl_pack {Γ : Ctx α ε} {R : LCtx α} {X : Ty α}
   | [] => pi_r
   | _::_ => distl_inv ;;' coprod (distl_pack ;;' inj_l) inj_r
 
--- theorem Eqv.split_rtimes_nil_packed_distl_pure {A B C : Ty α} {Γ : Ctx α ε}
---   : split (φ := φ) (A := Ctx.pack ((A.coprod B, ⊥)::Γ)) (e := ⊥) (Γ := Δ)
---   ;;' _ ⋊' Term.Eqv.nil.packed ;;' distl_inv
---   = distl_inv
---   ;;' sum
---     (_ ⋊' (split ;;' inj_l ⋉' _) ;;' assoc_inv)
---     (_ ⋊' (split ;;' inj_r ⋉' _) ;;' assoc_inv) := by
---   rw [seq_distl_inv]
---   simp [
---     seq_rtimes, split, distl_inv, seq_let2, coprod_seq, sum, wk1_seq, wk1_coprod,
---     inl_coprod, inr_coprod, seq_assoc, seq_ltimes, wk1_rtimes, let2_let2, let2_pair,
---     wk1_assoc_inv
---   ]
---   simp [
---     nil, inj_l, inj_r, let1_beta_var0, let1_beta_var1, let2_pair, subst_lift_coprod, pi_n_zero,
---     pi_r, pr,
---   ]
---   simp [
---     coprod, let1_let2, let1_beta_var0, wk2, Nat.liftnWk, nil, seq_assoc_inv, reassoc_inv_beta,
---     wk1_seq
---   ]
---   simp [seq, let1_beta_pure]
---   rw [<-Eqv.pair_eta_pure (p := var 0 _)]
---   simp [let2_pair, wk0_pl, wk0_pr, let1_beta_pure]
---   sorry
+theorem Eqv.split_rtimes_pi_r_distl_packed {A B : Ty α} {Γ : Ctx α ε}
+  : split (φ := φ) (e := e) (Γ := Δ)
+  ;;' Ctx.pack ((A.coprod B, ⊥)::Γ) ⋊' pi_r ;;' distl_inv
+  = distl_inv
+  ;;' sum
+    (_ ⋊' (split ;;' inj_l ⋉' _) ;;' assoc_inv)
+    (_ ⋊' (split ;;' inj_r ⋉' _) ;;' assoc_inv)
+  := split_rtimes_pi_r_distl
 
 -- theorem Eqv.split_rtimes_nil_packed_distl {A B C : Ty α} {Γ : Ctx α ε}
 --   : split (φ := φ) (A := Ctx.pack ((A.coprod B, ⊥)::Γ)) (e := e) (Γ := Δ)