CompletePrunings.lean

1 import KomorebiPaperV.FiniteAdaptive
2 
3 /-!
4 Author: Komorebi P.
5 Set-valued prunings use node identities, not potentially repeated node labels.
6 Completeness means exactly one selected node on every terminal path. This is
7 proved equivalent to the manuscript's covering antichain definition and to
8 recursive cuts, for arbitrary positive finite branching.
9 -/
10 
11 namespace KomorebiPaperV.CompletePrunings
12 open KomorebiPaperV.FiniteAdaptive
13 
14 variable {A : Type*}
15 
16 inductive Node : FiniteAdaptive.Tree A → Type _ where
17   | root (t : FiniteAdaptive.Tree A) : Node t
18   | down {a : A} {n : ℕ} {children : Fin (n + 1) → FiniteAdaptive.Tree A}
19       (i : Fin (n + 1)) : Node (children i) → Node (.branch a n children)
20 
21 inductive OnPath : {t : FiniteAdaptive.Tree A} → Node t → Terminal t → Prop where
22   | root {t : FiniteAdaptive.Tree A} (p : Terminal t) : OnPath (.root t) p
23   | down {a : A} {n : ℕ} {children : Fin (n + 1) → FiniteAdaptive.Tree A}
24       {i : Fin (n + 1)} {v : Node (children i)} {p : Terminal (children i)} :
25       OnPath v p → OnPath (t := .branch a n children) (.down i v) (.down i p)
26 
27 inductive Selected : {t : FiniteAdaptive.Tree A} → Cut t → Node t → Prop where
28   | stop (t : FiniteAdaptive.Tree A) : Selected (.stop t) (.root t)
29   | split {a : A} {n : ℕ} {children : Fin (n + 1) → FiniteAdaptive.Tree A}
30       {q : ∀ i, Cut (children i)} {i : Fin (n + 1)} {v : Node (children i)} :
31       Selected (q i) v → Selected (t := .branch a n children) (.split q) (.down i v)
32 
33 def Complete {t : FiniteAdaptive.Tree A} (S : Set (Node t)) : Prop :=
34   ∀ p : Terminal t, ∃! v : Node t, OnPath v p ∧ v ∈ S
35 
36 theorem terminal_exists (t : FiniteAdaptive.Tree A) : Nonempty (Terminal t) := by
37   induction t with
38   | leaf a => exact ⟨.here⟩
39   | branch a n children ih =>
40     obtain ⟨p⟩ := ih 0
41     exact ⟨.down 0 p⟩
42 
43 theorem node_on_terminal {t : FiniteAdaptive.Tree A} (v : Node t) : ∃ p : Terminal t, OnPath v p := by
44   induction v with
45   | root t =>
46     obtain ⟨p⟩ := terminal_exists t
47     exact ⟨p, .root p⟩
48   | down i v ih =>
49     obtain ⟨p, hp⟩ := ih
50     exact ⟨.down i p, .down hp⟩
51 
52 theorem selected_stop_iff {t : FiniteAdaptive.Tree A} (v : Node t) :
53     Selected (.stop t) v ↔ v = .root t := by
54   constructor
55   · intro h; cases h; rfl
56   · rintro rfl; exact .stop t
57 
58 theorem selected_split_root_false {a : A} {n : ℕ} {children : Fin (n + 1) → FiniteAdaptive.Tree A}
59     (q : ∀ i, Cut (children i)) : ¬Selected (t := .branch a n children) (.split q) (.root _) := by
60   intro h; cases h
61 
62 theorem selected_split_down_iff {a : A} {n : ℕ} {children : Fin (n + 1) → FiniteAdaptive.Tree A}
63     (q : ∀ i, Cut (children i)) (i : Fin (n + 1)) (v : Node (children i)) :
64     Selected (t := .branch a n children) (.split q) (.down i v) ↔ Selected (q i) v := by
65   constructor
66   · intro h; cases h with | split h => exact h
67   · exact Selected.split
68 
69 theorem cut_complete {t : FiniteAdaptive.Tree A} (q : Cut t) : Complete {v | Selected q v} := by
70   induction q with
71   | stop t =>
72     intro p
73     refine ⟨.root t, ⟨.root p, .stop t⟩, ?_⟩
74     intro v hv
75     exact (selected_stop_iff v).mp hv.2
76   | @split a n children q ih =>
77     intro p
78     cases p with
79     | down i p =>
80       obtain ⟨v, hv, hu⟩ := ih i p
81       refine ⟨.down i v, ⟨.down hv.1, .split hv.2⟩, ?_⟩
82       intro w hw
83       cases hw.1 with
84       | root p => exact False.elim (selected_split_root_false q hw.2)
85       | down hp =>
86         have he := hu _ ⟨hp, (selected_split_down_iff q _ _).mp hw.2⟩
87         cases he
88         rfl
89 
90 /-- Literal rooted-tree ancestry, including equality. -/
91 inductive Ancestor : {t : FiniteAdaptive.Tree A} → Node t → Node t → Prop where
92   | root {t : FiniteAdaptive.Tree A} (v : Node t) : Ancestor (.root t) v
93   | down {a : A} {n : ℕ} {children : Fin (n + 1) → FiniteAdaptive.Tree A}
94       {i : Fin (n + 1)} {u v : Node (children i)} :
95       Ancestor u v → Ancestor (t := .branch a n children) (.down i u) (.down i v)
96 
97 theorem ancestor_onPath {t : FiniteAdaptive.Tree A} {u v : Node t} (h : Ancestor u v)
98     {p : Terminal t} (hp : OnPath v p) : OnPath u p := by
99   induction h with
100   | root v => exact .root p
101   | down h ih =>
102     cases hp with | down hp => exact .down (ih hp)
103 
104 def CoveringAntichain {t : FiniteAdaptive.Tree A} (S : Set (Node t)) : Prop :=
105   (∀ p : Terminal t, ∃ v ∈ S, OnPath v p) ∧
106   (∀ u ∈ S, ∀ v ∈ S, Ancestor u v → u = v)
107 
108 theorem path_nodes_comparable {t : FiniteAdaptive.Tree A} {u v : Node t} {p : Terminal t}
109     (hu : OnPath u p) (hv : OnPath v p) : Ancestor u v ∨ Ancestor v u := by
110   induction hu with
111   | root p => exact Or.inl (.root _)
112   | @down a n children i u p hu ih =>
113     cases hv with
114     | root p => exact Or.inr (.root _)
115     | down hv =>
116       rcases ih hv with h | h
117       · exact Or.inl (.down h)
118       · exact Or.inr (.down h)
119 
120 theorem complete_iff_covering_antichain {t : FiniteAdaptive.Tree A} (S : Set (Node t)) :
121     Complete S ↔ CoveringAntichain S := by
122   constructor
123   · intro h
124     constructor
125     · intro p
126       obtain ⟨v, hv, _⟩ := h p
127       exact ⟨v, hv.2, hv.1⟩
128     · intro u hu v hv huv
129       obtain ⟨p, hp⟩ := node_on_terminal v
130       obtain ⟨w, _, hw⟩ := h p
131       exact (hw u ⟨ancestor_onPath huv hp, hu⟩).trans (hw v ⟨hp, hv⟩).symm
132   · rintro ⟨hcover, hanti⟩ p
133     obtain ⟨v, hv, hp⟩ := hcover p
134     refine ⟨v, ⟨hp, hv⟩, ?_⟩
135     intro u hu
136     rcases path_nodes_comparable hu.1 hp with h | h
137     · exact hanti u hu.2 v hv h
138     · exact (hanti v hv u hu.2 h).symm
139 
140 theorem complete_root_unique {t : FiniteAdaptive.Tree A} (S : Set (Node t)) (h : Complete S)
141     (hr : Node.root t ∈ S) (v : Node t) : v ∈ S ↔ v = .root t := by
142   constructor
143   · intro hv
144     obtain ⟨p, hp⟩ := node_on_terminal v
145     obtain ⟨w, _, hw⟩ := h p
146     exact (hw v ⟨hp, hv⟩).trans (hw (.root t) ⟨.root p, hr⟩).symm
147   · rintro rfl; exact hr
148 
149 theorem complete_child {a : A} {n : ℕ} {children : Fin (n + 1) → FiniteAdaptive.Tree A}
150     (S : Set (Node (.branch a n children))) (h : Complete S)
151     (hr : Node.root _ ∉ S) (i : Fin (n + 1)) :
152     Complete {v | Node.down i v ∈ S} := by
153   intro p
154   obtain ⟨v, hv, hu⟩ := h (.down i p)
155   cases hv.1 with
156   | root p => exact False.elim (hr hv.2)
157   | @down _ _ _ _ v _ hp =>
158     refine ⟨v, ⟨hp, hv.2⟩, ?_⟩
159     intro w hw
160     have he := hu (.down i w) ⟨.down hw.1, hw.2⟩
161     cases he
162     rfl
163 
164 theorem complete_has_cut (t : FiniteAdaptive.Tree A) (S : Set (Node t)) (h : Complete S) :
165     ∃ q : Cut t, ∀ v : Node t, Selected q v ↔ v ∈ S := by
166   classical
167   induction t with
168   | leaf a =>
169     refine ⟨.stop _, ?_⟩
170     intro v
171     cases v with
172     | root t =>
173       have hroot : Node.root (.leaf a) ∈ S := by
174         obtain ⟨w, hw, _⟩ := h .here
175         cases w
176         exact hw.2
177       simp [selected_stop_iff, hroot]
178   | branch a n children ih =>
179     by_cases hr : Node.root (.branch a n children) ∈ S
180     · exact ⟨.stop _, fun v => (selected_stop_iff v).trans
181         (complete_root_unique S h hr v).symm⟩
182     · have hex : ∀ i, ∃ q : Cut (children i), ∀ v,
183           Selected q v ↔ Node.down i v ∈ S :=
184         fun i => ih i _ (complete_child S h hr i)
185       choose q hq using hex
186       refine ⟨.split q, ?_⟩
187       intro v
188       cases v with
189       | root t => simp [selected_split_root_false, hr]
190       | down i v => exact (selected_split_down_iff q i v).trans (hq i v)
191 
192 theorem cut_ext (t : FiniteAdaptive.Tree A) (q r : Cut t)
193     (h : ∀ v, Selected q v ↔ Selected r v) : q = r := by
194   induction q with
195   | stop t =>
196     cases r with
197     | stop t => rfl
198     | split r =>
199       exact False.elim (selected_split_root_false r ((h (.root _)).mp (.stop _)))
200   | @split a n children q ih =>
201     cases r with
202     | stop t =>
203       exact False.elim (selected_split_root_false q ((h (.root _)).mpr (.stop _)))
204     | split r =>
205       have he : q = r := by
206         funext i
207         apply ih i (r i)
208         intro v
209         exact (selected_split_down_iff q i v).symm.trans
210           ((h (.down i v)).trans (selected_split_down_iff r i v))
211       cases he
212       rfl
213 
214 noncomputable def pruningEquiv (t : FiniteAdaptive.Tree A) :
215     Cut t ≃ {S : Set (Node t) // Complete S} where
216   toFun q := ⟨{v | Selected q v}, cut_complete q⟩
217   invFun S := (complete_has_cut t S.1 S.2).choose
218   left_inv q := by
219     apply cut_ext
220     exact (complete_has_cut t _ (cut_complete q)).choose_spec
221   right_inv S := by
222     apply Subtype.ext
223     ext v
224     exact (complete_has_cut t S.1 S.2).choose_spec v
225 
226 theorem complete_pruning_finite (t : FiniteAdaptive.Tree A) :
227     Finite {S : Set (Node t) // Complete S} :=
228   Finite.of_equiv (Cut t) (pruningEquiv t)
229 
230 theorem complete_pruning_minimum (t : FiniteAdaptive.Tree A)
231     (J : {S : Set (Node t) // Complete S} → ℝ) :
232     ∃ S, ∀ T, J S ≤ J T := by
233   obtain ⟨q, hq⟩ := arbitrary_objective_minimum t (J ∘ pruningEquiv t)
234   refine ⟨pruningEquiv t q, ?_⟩
235   intro S
236   simpa only [Function.comp_def, (pruningEquiv t).apply_symm_apply] using
237     hq ((pruningEquiv t).symm S)
238 
239 end KomorebiPaperV.CompletePrunings

Back to source controls