Distributivity lore

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

@@ -17,123 +17,33 @@ theorem Eqv.packed_in_case_split {Γ : Ctx α ε} {R : LCtx α}
   {a : Term.Eqv φ Γ (A.coprod B, e)} {r : Eqv φ ((A, ⊥)::Γ) R} {s : Eqv φ ((B, ⊥)::Γ) R}
   : (case a r s).packed_in (Δ := Δ)
   = case (Term.Eqv.split ;;' _ ⋊' a.packed ;;' Term.Eqv.distl_inv) r.packed_in s.packed_in := by
-  rw [
-    packed_in_case, split, Term.Eqv.seq_rtimes, Term.Eqv.seq_let2, case_let2, let2_pair,
-    <-wk_eff_nil (h := bot_le), wk0_wk_eff, let1_wk_eff, let1_wk_eff
-  ]
-  simp [let1_beta, Term.Eqv.nil]
-  simp [
-    Term.Eqv.distl_inv, Term.Eqv.seq, Term.Eqv.wk1, Term.Eqv.coprod,
-    Nat.liftnWk, Term.Eqv.nil, Term.Eqv.case_inl, Term.Eqv.case_inr,
-    case_let1, case_let2,
-  ]
-  conv => rhs; rw [let1_pair, <-wk_eff_var (hn := Ctx.Var.shead) (he := bot_le), let1_wk_eff]
-  simp only [Set.mem_setOf_eq, let1_beta, vsubst_let1]
-  sorry
-
-theorem Eqv.packed_in_coprod {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
-  {l : Eqv φ (⟨A, ⊥⟩::Γ) L} {r : Eqv φ (⟨B, ⊥⟩::Γ) L}
-  : (l.coprod r).packed_in (Δ := Δ)
-  = let2 (var 0 Ctx.Var.shead) (
-      coprod
-        (let1 (pair (var 1 Ctx.Var.shead.step) (var 0 Ctx.Var.shead)) l.packed_in)
-        (let1 (pair (var 1 Ctx.Var.shead.step) (var 0 Ctx.Var.shead)) r.packed_in)
-  )
-  := by
-  simp only [packed_in, coprod, vsubst_case, subst_var, List.getElem_cons_zero, List.length_cons,
-    Fin.zero_eta, Term.Subst.Eqv.get_unpack, List.get_eq_getElem, Fin.val_zero, pi_n_zero,
-    Term.Eqv.pi_r, pr, wk_res_self, case_let2]
-  sorry
-  -- congr <;> {
-  --   simp [vwk1, <-vsubst_fromWk, vsubst_vsubst]
-  --   congr 1; ext k;
-  --   cases k using Fin.cases with
-  --   | zero =>
-  --     simp [Term.Subst.Eqv.get_comp, subst_fromWk, pi_n_zero, Term.Eqv.pi_r, Term.Eqv.Pure.pr_pair]
-  --   | succ i =>
-  --     simp only [List.get_eq_getElem, List.length_cons, Fin.val_succ, List.getElem_cons_succ,
-  --       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_lift_var_succ, subst_fromWk,
-  --       Term.Subst.Eqv.get_unpack]
-  --     simp only [subst_var, Set.mem_setOf_eq, List.length_cons, Fin.val_succ, Ctx.InS.coe_wk1,
-  --       Nat.liftWk_succ, Nat.succ_eq_add_one, id_eq, List.getElem_cons_succ,
-  --       Term.Subst.Eqv.get_unpack, List.get_eq_getElem, wk_res_self]
-  --     conv => rhs; rw [<-Term.Eqv.let1_beta, <-wk1_pi_n, <-Term.Eqv.seq]
-  --     rw [
-  --       pi_n_succ, Term.Eqv.seq_assoc, Term.Eqv.seq_pi_l, wk_eff_pair,
-  --       Term.Eqv.Pure.pl_pair ⟨_, rfl⟩, pi_n_succ', Term.Eqv.seq,
-  --       wk1_pi_n, wk0_let1, wk1_pi_n, wk_let1, <-wk1, Ctx.InS.lift_wk1, <-wk2, wk2_pi_n,
-  --       Term.Eqv.seq, wk1_pi_n
-  --     ]
-  --     sorry
-  -- }
+  rw [Term.Eqv.seq_distl_inv, Term.Eqv.seq_rtimes, Term.Eqv.split]
+  simp only [Term.Eqv.nil, wk1_packed, Term.Eqv.let2_pair, wk0_var, zero_add, let1_beta_var0,
+    subst_let1, var_succ_subst0, subst_pair, subst_lift_var_succ, var0_subst0, List.length_cons,
+    Nat.reduceAdd, Fin.zero_eta, List.get_eq_getElem, Fin.val_zero, List.getElem_cons_zero,
+    wk_res_eff, wk_eff_var, subst_lift_packed, subst0_var0_packed, subst0_wk0, subst_lift_coprod,
+    subst_inl, subst_lift_var_zero, subst_inr]
+  rw [case_let1, packed_in_case, case_bind]
+  congr 1
+  simp only [vwk1_let1, wk1_pair, wk1_var_succ, zero_add, wk1_var0, List.length_cons, Fin.zero_eta,
+    List.get_eq_getElem, Fin.val_zero, List.getElem_cons_zero, vwk2_packed_in, Term.Eqv.coprod,
+    wk1_inl, Nat.add_zero, Nat.zero_eq, wk1_inr, vwk1_packed_in, case_case, case_inl, case_inr]
+  rfl
 
 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 [
-    packed_in, coprod, vsubst_case, subst_var, wk_res_self, Term.Subst.Eqv.get_unpack,
-    Term.Eqv.pi_n_zero', Term.Eqv.distl_inv, case_let2, Term.Eqv.pi_r, Term.Eqv.pr, case_let2,
-  ]
-  simp [Term.Eqv.nil, Term.Eqv.coprod, case_case, case_inl, case_inr]
-  stop
-  simp [packed_in, vwk1, <-vsubst_fromWk, vsubst_vsubst]
-  congr 3 <;> {
-    ext k; cases k using Fin.cases with
-    | zero =>
-      simp [Term.Subst.Eqv.get_comp, subst_fromWk, pi_n_zero, Term.Eqv.pi_r, Term.Eqv.Pure.pr_pair]
-    | succ k =>
-      simp only [List.get_eq_getElem, List.length_cons, Fin.val_succ, List.getElem_cons_succ,
-        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_lift_var_succ, subst_fromWk,
-        Term.Subst.Eqv.get_unpack]
-      simp only [subst_var, Set.mem_setOf_eq, List.length_cons, Fin.val_succ, Ctx.InS.coe_wk1,
-        Nat.liftWk_succ, Nat.succ_eq_add_one, id_eq, List.getElem_cons_succ,
-        Term.Subst.Eqv.get_unpack, List.get_eq_getElem, wk_res_self]
-      conv => rhs; rw [<-Term.Eqv.let1_beta, <-wk1_pi_n, <-Term.Eqv.seq]
-      rw [
-        pi_n_succ, Term.Eqv.seq_assoc, Term.Eqv.seq_pi_l, wk_eff_pair,
-        Term.Eqv.Pure.pl_pair ⟨_, rfl⟩, pi_n_succ', Term.Eqv.seq,
-        wk1_pi_n, wk0_let1, wk1_pi_n, wk_let1, <-wk1, Ctx.InS.lift_wk1, <-wk2, wk2_pi_n
-      ]
-      sorry
-  }
+  rw [coprod, packed_in_case_split]
+  sorry
 
 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
-  := sorry
-
--- theorem Eqv.packed_in_pack_coprod {Γ : Ctx α ε} {R L : LCtx α}
---   {G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) L}
---   : (pack_coprod G).packed_in (Δ := Δ)
---   = vsubst (distl_pack (e := ⊥) (R := R) (X := Γ.pack)).subst0 (
---     pack_coprod (λi => ((G (i.cast R.length_dist)).packed_in).cast (by rw [LCtx.get_dist]; rfl) rfl)
---   )
---   := by induction R generalizing Γ Δ with
---   | nil => simp [pack_coprod_empty, packed_in]
---   | cons A R I =>
---     conv => lhs; rw [pack_coprod_cons, coprod, packed_in_case, vwk1_pack_coprod, I]
---     conv =>
---       rhs
---       simp only [
---         packed_var, wk_res_self, pack_coprod_cons, coprod, vwk1_packed_in, vsubst_case, var0_subst0
---       ]
---       arg 1
---       rw [distl_pack, distl_inv, Term.Eqv.seq_let2]
---     sorry
-
--- theorem Eqv.packed_in_pack_coprod_arr {Γ : Ctx α ε} {R L : LCtx α}
---   {G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) (A::L)}
---   : (pack_coprod G).packed_in (Δ := Δ)
---   = ret (distl_pack (X := Γ.pack))
---     ;; pack_coprod (λi => acast R.get_dist ;; (G (i.cast R.length_dist)).packed_in)
---   := by
---     rw [packed_in_pack_coprod, ret_seq]; congr;
---     rw [vwk1_pack_coprod]; congr; funext i
---     rw [vwk1_seq, vwk1_packed_in, vwk1_acast, acast_seq]
+  := by
+  rw [coprod, packed_in_case_split, coprod]
+  sorry
 
 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/Region/Structural/Product.lean

@@ -51,12 +51,12 @@ theorem Eqv.vwk_liftn₂_packed_in {Γ Δ Δ' : Ctx α ε} {R : LCtx α} {r : Eq
   simp [<-Ctx.InS.lift_lift]
 
 @[simp]
-theorem Eqv.vwk1_packed_in {Γ Δ : Ctx α ε} {R : LCtx α} {r : Eqv φ (V::Γ) R}
+theorem Eqv.vwk1_packed_in {Γ Δ : Ctx α ε} {R : LCtx α} {r : Eqv φ Γ R}
   : r.packed_in.vwk1 (inserted := inserted) = r.packed_in (Δ := _::Δ) := by
   rw [vwk1, <-Ctx.InS.lift_wk0, vwk_slift_packed_in]
 
 @[simp]
-theorem Eqv.vwk2_packed_in {Γ Δ : Ctx α ε} {R : LCtx α} {r : Eqv φ (V::V::Γ) R}
+theorem Eqv.vwk2_packed_in {Γ Δ : Ctx α ε} {R : LCtx α} {r : Eqv φ Γ R}
   : r.packed_in.vwk2 (inserted := inserted) = r.packed_in (Δ := head::_::Δ) := by
   rw [vwk2, <-Ctx.InS.lift_wk1, vwk_slift_packed_in]
 

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

@@ -95,6 +95,11 @@ theorem Eqv.distl_inv_distl {A B C : Ty α} {Γ : Ctx α ε}
     distl_inv_distl_pure, wk_eff_nil
   ]
 
+theorem Eqv.distl_seq_injective {A B C : Ty α} {Γ : Ctx α ε}
+  {r s : Eqv φ (⟨A.prod (B.coprod C), ⊥⟩::Γ) ⟨X, e⟩} (h : distl ;;' r = distl ;;' s)
+  : r = s := by
+  rw [<-nil_seq r, <-nil_seq s, <-distl_inv_distl, <-seq_assoc, h, seq_assoc]
+
 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)
@@ -104,6 +109,44 @@ theorem Eqv.distl_braid {A B C : Ty α} {Γ : Ctx α ε}
   = 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.rtimes_seq_distr {X Y A B C : Ty α} {Γ : Ctx α ε}
+--   {a : Eqv φ ((Y, ⊥)::Γ) ⟨A.coprod B, e⟩}
+--   : X ⋊' a ;;' distl_inv
+--   = pi_r ;;' a ;;' sum sorry sorry := by
+--   sorry
+
+theorem Eqv.split_rtimes_pi_r_distl_pure {X A B C : Ty α} {Γ : Ctx α ε}
+  : split (φ := φ) (A := X.prod (A.coprod B)) (e := ⊥) (Γ := Δ)
+  ;;' _ ⋊' pi_r ;;' distl_inv
+  = distl_inv
+  ;;' sum
+    (_ ⋊' (split ;;' inj_l ⋉' _) ;;' assoc_inv)
+    (_ ⋊' (split ;;' inj_r ⋉' _) ;;' assoc_inv) := by
+  apply distl_seq_injective
+  conv => rhs; rw [seq_assoc, distl_distl_inv, nil_seq]
+  rw [distl, coprod_seq]
+  sorry
+--   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_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]
+--   conv => lhs; rw [<-case_eta (a := (var 0 _).pr)]
+--   simp [case_case]
+--   sorry
+
 theorem Eqv.distr_braid {A B C : Ty α} {Γ : Ctx α ε}
   : distr ;;' braid
   = sum braid braid ;;' distl (φ := φ) (Γ := Γ) (A := A) (B := B) (C := C) (e := e)

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

@@ -1033,6 +1033,10 @@ theorem Eqv.wk1_assoc {A B C : Ty α} {Γ : Ctx α ε}
   : (assoc (φ := φ) (Γ := Γ) (A := A) (B := B) (C := C) (e := e)).wk1 (inserted := inserted) = assoc
   := rfl
 
+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
+
 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]

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

@@ -462,6 +462,10 @@ def Eqv.sum {A A' B B' : Ty α} {Γ : Ctx α ε}
   (l : Eqv φ (⟨A, ⊥⟩::Γ) ⟨A', e⟩) (r : Eqv φ (⟨B, ⊥⟩::Γ) ⟨B', e⟩)
   : Eqv φ (⟨A.coprod B, ⊥⟩::Γ) ⟨A'.coprod B', e⟩ := coprod (l.seq inj_l) (r.seq inj_r)
 
+theorem Eqv.sum_def' {A A' B B' : Ty α} {Γ : Ctx α ε}
+  (l : Eqv φ (⟨A, ⊥⟩::Γ) ⟨A', e⟩) (r : Eqv φ (⟨B, ⊥⟩::Γ) ⟨B', e⟩)
+  : sum l r = coprod l.inl r.inr := by simp [sum, seq_inj_l, seq_inj_r]
+
 -- TODO: sum is a bifunctor; so that's nil nil and seq!
 
 @[simp]

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

@@ -12,3 +12,44 @@ 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
+
+-- 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_nil_packed_distl {A B C : Ty α} {Γ : Ctx α ε}
+--   : split (φ := φ) (A := Ctx.pack ((A.coprod B, ⊥)::Γ)) (e := 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, seq_rtimes,
+--     let2_pair
+--   ]
+--   simp [nil, let1_beta_var0]

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

@@ -137,6 +137,16 @@ theorem Eqv.pi_n_succ' {Γ Δ : Ctx α ε} (i : Fin Γ.length)
   : pi_n (φ := φ) (Γ := V::Γ) (Δ := Δ) (e := e) ⟨i + 1, by simp⟩ = pi_l ;;' pi_n i
   := pi_n_succ i
 
+theorem Eqv.pi_n_succ2' {Γ Δ : Ctx α ε} (i : Fin Γ.length)
+  : pi_n (φ := φ) (Γ := V'::V::Γ) (Δ := Δ) (e := e) ⟨i + 1 + 1, by simp⟩ = pi_l ;;' pi_l ;;' pi_n i
+  := by
+  rw [<-seq_assoc, seq, wk1_seq, wk1_pi_l, wk1_pi_n, seq, wk1_pi_n]
+  rw [let1_beta' (a' := pi_l) (h := by simp)]
+  rw [let1_beta' (a' := pi_l) (h := by simp)]
+  apply eq_of_term_eq;
+  simp only [InS.coe_pi_n, <-Term.subst0_nil_pl_pi_n]
+  rfl
+
 theorem Eqv.pi_n_one {Γ Δ : Ctx α ε}
   : Eqv.pi_n (φ := φ) (Γ := V::V'::Γ) (Δ := Δ) (e := e) (1 : Fin (Γ.length + 2))
   = pi_l ;;' pi_r := by exact pi_n_succ (Γ := V'::Γ) (0 : Fin (Γ.length + 1))

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2ce0037d487217469a1efeb9ea8196fe15ab9c46",
+   "rev": "e0b13c946e9c3805f1eec785c72955e103a9cbaf",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "61fb4d1a2a6a4fe4be260ca31c58af1234ff298b",
+   "rev": "a895713f7701e295a015b1087f3113fd3d615272",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "ba3db161926d69d9d7b6629b38a98630a32204bb",
+   "rev": "418c53780957030e8fd99d2007872a87ad82d9e6",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,