PacketTree.lean

1 import Mathlib.Algebra.BigOperators.Group.Finset.Basic
2 import Mathlib.Data.Fintype.Sum
3 import Mathlib.Data.Fintype.Sigma
4 import Mathlib.Data.Fintype.BigOperators
5 
6 /-! Finite rooted trees and path-complete cuts. A selection is arbitrary
7 on nodes. Completeness means exactly one selected node on each full
8 root-to-leaf path. Reconstruction is derived from local conservation,
9 not included in the definition of a cut. -/
10 set_option autoImplicit false
11 open scoped BigOperators
12 namespace Komorebi.LSM
13 
14 /-- Every internal node has a finite nonempty child family. -/
15 inductive PacketTree where
16   | leaf : PacketTree
17   | branch (n : ℕ) (child : Fin (n + 1) → PacketTree) : PacketTree
18 
19 namespace PacketTree
20 
21 /-- Nodes have structural addresses, even when labels coincide. -/
22 @[reducible] def Node : PacketTree → Type
23   | .leaf => Unit
24   | .branch n child => Unit ⊕ (Σ i : Fin (n + 1), Node (child i))
25 
26 /-- Full root-to-leaf paths are indexed by the leaf they reach. -/
27 @[reducible] def Leaf : PacketTree → Type
28   | .leaf => Unit
29   | .branch n child => Σ i : Fin (n + 1), Leaf (child i)
30 
31 def root : (t : PacketTree) → Node t
32   | .leaf => ()
33   | .branch _ _ => Sum.inl ()
34 
35 /-- A canonical leaf proves that no descendant branch is empty. -/
36 def firstLeaf : (t : PacketTree) → Leaf t
37   | .leaf => ()
38   | .branch _ child => ⟨0, firstLeaf (child 0)⟩
39 
40 /-- Counts every selected node along a full path, including the root. -/
41 def pathCount : (t : PacketTree) → (Node t → Bool) → Leaf t → ℕ
42   | .leaf, s, _ => (s ()).toNat
43   | .branch _ child, s, p => (s (Sum.inl ())).toNat +
44       pathCount (child p.1) (fun v => s (Sum.inr ⟨p.1, v⟩)) p.2
45 
46 def IsCompleteCut (t : PacketTree) (s : Node t → Bool) : Prop :=
47   ∀ p : Leaf t, pathCount t s p = 1
48 
49 /-- Canonical recursive finite sum over every node. -/
50 def nodeSum {A : Type*} [AddCommMonoid A] : (t : PacketTree) → (Node t → A) → A
51   | .leaf, f => f ()
52   | .branch _ child, f => f (Sum.inl ()) +
53       ∑ i, nodeSum (child i) (fun v => f (Sum.inr ⟨i, v⟩))
54 
55 def selectedSum {A : Type*} [AddCommMonoid A]
56     (t : PacketTree) (s : Node t → Bool) (f : Node t → A) : A :=
57   nodeSum t (fun v => if s v then f v else 0)
58 
59 /-- Local conservation imposes no condition on terminal node labels. -/
60 def Conservative {A : Type*} [AddCommMonoid A] :
61     (t : PacketTree) → (Node t → A) → Prop
62   | .leaf, _ => True
63   | .branch _ child, f =>
64       f (Sum.inl ()) = ∑ i, f (Sum.inr ⟨i, root (child i)⟩) ∧
65       ∀ i, Conservative (child i) (fun v => f (Sum.inr ⟨i, v⟩))
66 
67 theorem nodeSum_zero {A : Type*} [AddCommMonoid A] (t : PacketTree) :
68     nodeSum t (fun _ => (0 : A)) = 0 := by
69   induction t with
70   | leaf => rfl
71   | branch n child ih => simp [nodeSum, ih]
72 
73 theorem pathCount_zero_iff (t : PacketTree) (s : Node t → Bool) :
74     (∀ p, pathCount t s p = 0) ↔ (∀ v, s v = false) := by
75   induction t with
76   | leaf =>
77       constructor
78       · intro h v
79         cases v
80         simpa [pathCount] using h ()
81       · intro h p
82         cases p
83         simp [pathCount, h ()]
84   | branch n child ih =>
85       constructor
86       · intro h
87         have hroot : s (Sum.inl ()) = false := by
88           have h0 := h ⟨0, firstLeaf (child 0)⟩
89           cases hs : s (Sum.inl ()) <;> simp [pathCount, hs] at h0 ⊢
90         intro v
91         cases v with
92         | inl u => cases u; exact hroot
93         | inr p =>
94             apply (ih p.1 (fun v => s (Sum.inr ⟨p.1, v⟩))).mp
95             · intro q
96               simpa [pathCount, hroot] using h ⟨p.1, q⟩
97       · intro h p
98         have hi := (ih p.1 (fun v => s (Sum.inr ⟨p.1, v⟩))).mpr
99           (fun v => h (Sum.inr ⟨p.1, v⟩))
100         simp [pathCount, h (Sum.inl ()), hi]
101 
102 theorem completeCut_leaf (s : Node .leaf → Bool) :
103     IsCompleteCut .leaf s ↔ s () = true := by
104   simp [IsCompleteCut, pathCount, Leaf]
105 
106 /-- The path criterion forces either a root-only cut or full child cuts. -/
107 theorem completeCut_branch {n : ℕ} {child : Fin (n+1) → PacketTree}
108     (s : Node (.branch n child) → Bool) :
109     IsCompleteCut (.branch n child) s ↔
110       (s (Sum.inl ()) = true ∧ ∀ i v, s (Sum.inr ⟨i, v⟩) = false) ∨
111       (s (Sum.inl ()) = false ∧ ∀ i,
112         IsCompleteCut (child i) (fun v => s (Sum.inr ⟨i, v⟩))) := by
113   constructor
114   · intro h
115     cases hs : s (Sum.inl ()) with
116     | false =>
117         right
118         refine ⟨rfl, ?_⟩
119         intro i p
120         simpa [pathCount, hs] using h ⟨i, p⟩
121     | true =>
122         left
123         refine ⟨rfl, ?_⟩
124         intro i
125         apply (pathCount_zero_iff (child i) _).mp
126         intro p
127         have hp := h ⟨i, p⟩
128         simpa [pathCount, hs] using hp
129   · rintro (⟨hr, hz⟩ | ⟨hr, hc⟩) p
130     · have hp := (pathCount_zero_iff (child p.1) _).mpr (hz p.1) p.2
131       simp [pathCount, hr, hp]
132     · simpa [pathCount, hr] using hc p.1 p.2
133 
134 /-- Complete cuts conserve any additive label with conservative splits. -/
135 theorem selectedSum_eq_root {A : Type*} [AddCommMonoid A]
136     (t : PacketTree) (s : Node t → Bool) (f : Node t → A)
137     (cut : IsCompleteCut t s) (hf : Conservative t f) :
138     selectedSum t s f = f (root t) := by
139   induction t with
140   | leaf =>
141       have hs := (completeCut_leaf s).mp cut
142       simp [selectedSum, nodeSum, root, hs]
143   | branch n child ih =>
144       rcases (completeCut_branch s).mp cut with ⟨hr, hz⟩ | ⟨hr, hc⟩
145       · simp [selectedSum, nodeSum, hr, hz, nodeSum_zero, root]
146       · have hh (i : Fin (n+1)) := ih i
147           (fun v => s (Sum.inr ⟨i, v⟩)) (fun v => f (Sum.inr ⟨i, v⟩))
148           (hc i) (hf.2 i)
149         simp only [selectedSum] at hh
150         simp only [selectedSum, nodeSum, hr, Bool.false_eq_true, ↓reduceIte,
151           zero_add, hh]
152         exact hf.1.symm
153 
154 /-- An explicit enumeration of all structural node addresses. -/
155 @[instance_reducible] def nodeFintype : (t : PacketTree) → Fintype (Node t)
156   | .leaf => inferInstanceAs (Fintype Unit)
157   | .branch n child => by
158       letI (i : Fin (n+1)) : Fintype (Node (child i)) := nodeFintype (child i)
159       exact inferInstanceAs (Fintype (Unit ⊕ (Σ i : Fin (n+1), Node (child i))))
160 
161 instance instFintypeNode (t : PacketTree) : Fintype (Node t) := nodeFintype t
162 
163 theorem nodeSum_eq_sum {A : Type*} [AddCommMonoid A]
164     (t : PacketTree) (f : Node t → A) :
165     nodeSum t f = ∑ v, f v := by
166   induction t with
167   | leaf =>
168       change f () = ∑ v : Unit, f v
169       simp
170   | branch n child ih =>
171       change f (Sum.inl ()) + ∑ i, nodeSum (child i) (fun v => f (Sum.inr ⟨i,v⟩)) = _
172       rw [Fintype.sum_sum_type, Fintype.sum_sigma]
173       simp only [Finset.univ_unique, PUnit.default_eq_unit, Finset.sum_singleton]
174       congr 1
175       exact Finset.sum_congr rfl (fun i _ => ih i _)
176 
177 /-- Standard finite-sum form of the complete-antichain conservation law. -/
178 theorem complete_cut_sum {A : Type*} [AddCommMonoid A]
179     (t : PacketTree) (s : Node t → Bool) (f : Node t → A)
180     (cut : IsCompleteCut t s) (hf : Conservative t f) :
181     (∑ v, if s v then f v else 0) = f (root t) := by
182   rw [← nodeSum_eq_sum]
183   exact selectedSum_eq_root t s f cut hf
184 
185 end PacketTree
186 end Komorebi.LSM

Back to source controls