Behavior.lean

1 import Mathlib.Data.Fintype.Card
2 import Mathlib.Data.Set.Image
3 
4 /-!
5 # Evidence and initialized behavioral state
6 
7 Reviewed Core v0.2, Proposition 1.1 and Theorem 1.2.
8 Words are executed left to right. Operations are total on the declared state type.
9 An invariant domain can be represented by a subtype carrying its restricted operations.
10 The factorization theorems use attained records, so impossible records need no decoder.
11 -/
12 
13 namespace Komorebi.MachineTheory
14 
15 universe u v w z
16 
17 /-- Exactly the record values produced by at least one state. -/
18 def Attained {X : Type u} {H : Type v} (r : X → H) :=
19   {h : H // ∃ x, r x = h}
20 
21 def record {X : Type u} {H : Type v} (r : X → H) (x : X) : Attained r :=
22   ⟨r x, x, rfl⟩
23 
24 def FiberConstant {X : Type u} {H : Type v} {Y : Type w}
25     (r : X → H) (t : X → Y) : Prop :=
26   ∀ x y, r x = r y → t x = t y
27 
28 /-- Core 1.1: exact factorization through the actual observation record. -/
29 theorem decoder_exists_iff {X : Type u} {H : Type v} {Y : Type w}
30     (r : X → H) (t : X → Y) :
31     (∃ d : Attained r → Y, ∀ x, d (record r x) = t x) ↔ FiberConstant r t := by
32   constructor
33   · rintro ⟨d, hd⟩ x y h
34     have he : record r x = record r y := Subtype.ext h
35     rw [← hd x, ← hd y, he]
36   · intro h
37     classical
38     let d : Attained r → Y := fun a => t (Classical.choose a.property)
39     refine ⟨d, ?_⟩
40     intro x
41     exact h _ _ (Classical.choose_spec (record r x).property)
42 
43 /-- A concrete collision excludes every decoder, not just one algorithm. -/
44 theorem no_decoder_of_collision {X : Type u} {H : Type v} {Y : Type w}
45     {r : X → H} {t : X → Y} (x y : X)
46     (hr : r x = r y) (ht : t x ≠ t y) :
47     ¬ ∃ d : Attained r → Y, ∀ x, d (record r x) = t x := by
48   intro hd
49   exact ht ((decoder_exists_iff r t).mp hd x y hr)
50 
51 /-- First execute the head action, then the remaining word. -/
52 def run {X : Type u} {A : Type v} (F : A → X → X) : List A → X → X
53   | [], x => x
54   | a :: w, x => run F w (F a x)
55 
56 @[simp] theorem run_nil {X : Type u} {A : Type v} (F : A → X → X) (x : X) :
57     run F [] x = x := rfl
58 
59 @[simp] theorem run_cons {X : Type u} {A : Type v} (F : A → X → X)
60     (a : A) (w : List A) (x : X) : run F (a :: w) x = run F w (F a x) := rfl
61 
62 theorem run_append {X : Type u} {A : Type v} (F : A → X → X)
63     (s t : List A) (x : X) : run F (s ++ t) x = run F t (run F s x) := by
64   induction s generalizing x with
65   | nil => rfl
66   | cons a s ih => exact ih (F a x)
67 
68 def SameBehavior {X : Type u} {A : Type v} {Y : Type w}
69     (F : A → X → X) (q : X → Y) (x y : X) : Prop :=
70   ∀ word, q (run F word x) = q (run F word y)
71 
72 def behaviorSetoid {X : Type u} {A : Type v} {Y : Type w}
73     (F : A → X → X) (q : X → Y) : Setoid X where
74   r := SameBehavior F q
75   iseqv := ⟨fun _ _ => rfl, fun h w => (h w).symm,
76     fun h₁ h₂ w => (h₁ w).trans (h₂ w)⟩
77 
78 abbrev BehavioralState {X : Type u} {A : Type v} {Y : Type w}
79     (F : A → X → X) (q : X → Y) := Quotient (behaviorSetoid F q)
80 
81 def behaviorClass {X : Type u} {A : Type v} {Y : Type w}
82     (F : A → X → X) (q : X → Y) (x : X) : BehavioralState F q :=
83   Quotient.mk _ x
84 
85 theorem sameBehavior_step {X : Type u} {A : Type v} {Y : Type w}
86     {F : A → X → X} {q : X → Y} {x y : X} (h : SameBehavior F q x y) (a : A) :
87     SameBehavior F q (F a x) (F a y) := by
88   intro word
89   exact h (a :: word)
90 
91 def quotientStep {X : Type u} {A : Type v} {Y : Type w}
92     (F : A → X → X) (q : X → Y) (a : A) : BehavioralState F q → BehavioralState F q :=
93   Quotient.map (F a) (fun _ _ h => sameBehavior_step h a)
94 
95 def quotientRead {X : Type u} {A : Type v} {Y : Type w}
96     (F : A → X → X) (q : X → Y) : BehavioralState F q → Y :=
97   Quotient.lift q (fun _ _ h => h [])
98 
99 @[simp] theorem quotientStep_class {X : Type u} {A : Type v} {Y : Type w}
100     (F : A → X → X) (q : X → Y) (a : A) (x : X) :
101     quotientStep F q a (behaviorClass F q x) = behaviorClass F q (F a x) := rfl
102 
103 @[simp] theorem quotientRead_class {X : Type u} {A : Type v} {Y : Type w}
104     (F : A → X → X) (q : X → Y) (x : X) :
105     quotientRead F q (behaviorClass F q x) = q x := rfl
106 
107 theorem quotient_run {X : Type u} {A : Type v} {Y : Type w}
108     (F : A → X → X) (q : X → Y) (word : List A) (x : X) :
109     run (quotientStep F q) word (behaviorClass F q x) = behaviorClass F q (run F word x) := by
110   induction word generalizing x with
111   | nil => rfl
112   | cons a word ih => exact ih (F a x)
113 
114 /-- A predictor's guarantee covers all finite words, not sampled continuations. -/
115 structure Predictor {X : Type u} {A : Type v} {Y : Type w} {H : Type z}
116     (F : A → X → X) (q : X → Y) (r : X → H) (Z : Type*) where
117   initState : Attained r → Z
118   step : A → Z → Z
119   read : Z → Y
120   correct : ∀ word x, read (run step word (initState (record r x))) = q (run F word x)
121 
122 /-- Any exact predictor separates behaviorally inequivalent initial states. -/
123 theorem Predictor.equal_initial_states {X : Type u} {A : Type v} {Y : Type w}
124     {H : Type z} {Z : Type*} {F : A → X → X} {q : X → Y} {r : X → H}
125     (p : Predictor F q r Z) {x y : X}
126     (h : p.initState (record r x) = p.initState (record r y)) : SameBehavior F q x y := by
127   intro word
128   rw [← p.correct word x, ← p.correct word y, h]
129 
130 theorem Predictor.record_sufficient {X : Type u} {A : Type v} {Y : Type w}
131     {H : Type z} {Z : Type*} {F : A → X → X} {q : X → Y} {r : X → H}
132     (p : Predictor F q r Z) : ∀ x y, r x = r y → SameBehavior F q x y := by
133   intro x y h
134   apply p.equal_initial_states
135   exact congrArg p.initState (Subtype.ext h)
136 
137 /-- The actual quotient predictor is constructed, not assumed as a structure field. -/
138 noncomputable def canonicalPredictor {X : Type u} {A : Type v} {Y : Type w}
139     {H : Type z} (F : A → X → X) (q : X → Y) (r : X → H)
140     (h : ∀ x y, r x = r y → SameBehavior F q x y) :
141     Predictor F q r (BehavioralState F q) := by
142   have hf : FiberConstant r (behaviorClass F q) := fun x y he => Quotient.sound (h x y he)
143   let d := Classical.choose ((decoder_exists_iff r (behaviorClass F q)).mpr hf)
144   have hd : ∀ x, d (record r x) = behaviorClass F q x :=
145     Classical.choose_spec ((decoder_exists_iff r (behaviorClass F q)).mpr hf)
146   refine ⟨d, quotientStep F q, quotientRead F q, ?_⟩
147   intro word x
148   rw [hd x, quotient_run]
149   rfl
150 
151 /-- Core 1.2, existence part. State cardinality is handled separately below. -/
152 theorem evidence_initialized_predictor_iff {X : Type u} {A : Type v} {Y : Type w}
153     {H : Type z} (F : A → X → X) (q : X → Y) (r : X → H) :
154     Nonempty (Predictor F q r (BehavioralState F q)) ↔
155       (∀ x y, r x = r y → SameBehavior F q x y) := by
156   constructor
157   · rintro ⟨p⟩
158     exact p.record_sufficient
159   · intro h
160     exact ⟨canonicalPredictor F q r h⟩
161 
162 /-- A surjection from initialized states to behavioral classes proves minimality. -/
163 theorem Predictor.initialized_state_surjection {X : Type u} {A : Type v} {Y : Type w}
164     {H : Type z} {Z : Type*} {F : A → X → X} {q : X → Y} {r : X → H}
165     (p : Predictor F q r Z) :
166     ∃ d : Attained (fun x => p.initState (record r x)) → BehavioralState F q,
167       Function.Surjective d := by
168   let e := fun x => p.initState (record r x)
169   have hf : FiberConstant e (behaviorClass F q) := by
170     intro x y he
171     exact Quotient.sound (p.equal_initial_states he)
172   obtain ⟨d, hd⟩ := (decoder_exists_iff e (behaviorClass F q)).mpr hf
173   refine ⟨d, ?_⟩
174   intro z₀
175   refine Quotient.inductionOn z₀ ?_
176   intro x
177   exact ⟨record e x, hd x⟩
178 
179 
180 noncomputable instance attainedFintype {X : Type u} {H : Type v} [Fintype X]
181     (r : X → H) : Fintype (Attained r) := by
182   classical
183   apply Fintype.ofSurjective (record r)
184   intro h
185   obtain ⟨x, hx⟩ := h.property
186   exact ⟨x, Subtype.ext hx⟩
187 
188 noncomputable instance behavioralFintype {X : Type u} {A : Type v} {Y : Type w}
189     [Fintype X] (F : A → X → X) (q : X → Y) : Fintype (BehavioralState F q) := by
190   classical
191   apply Fintype.ofSurjective (behaviorClass F q)
192   intro z₀
193   exact Quotient.inductionOn z₀ (fun x => ⟨x, rfl⟩)
194 
195 /-- Core 1.2, minimality among the *initialized* states, including redundant predictors. -/
196 theorem Predictor.minimal_initialized_card {X : Type u} {A : Type v} {Y : Type w}
197     {H : Type z} {Z : Type*} [Fintype X] {F : A → X → X} {q : X → Y} {r : X → H}
198     (p : Predictor F q r Z) :
199     Fintype.card (BehavioralState F q) ≤
200       Fintype.card (Attained (fun x => p.initState (record r x))) := by
201   obtain ⟨d, hd⟩ := p.initialized_state_surjection
202   exact Fintype.card_le_of_surjective d hd
203 
204 /-- Every behavioral class is initialized in the canonical realization. -/
205 theorem canonical_initialization_surjective {X : Type u} {A : Type v} {Y : Type w}
206     {H : Type z} (F : A → X → X) (q : X → Y) (r : X → H)
207     (h : ∀ x y, r x = r y → SameBehavior F q x y) :
208     Function.Surjective (fun x => (canonicalPredictor F q r h).initState (record r x)) := by
209   intro z₀
210   refine Quotient.inductionOn z₀ ?_
211   intro x
212   refine ⟨x, ?_⟩
213   exact Classical.choose_spec
214     ((decoder_exists_iff r (behaviorClass F q)).mpr
215       (fun x y he => Quotient.sound (h x y he))) x
216 
217 
218 /-- The canonical predictor attains the lower bound on initialized finite states. -/
219 theorem canonical_initialized_card {X : Type u} {A : Type v} {Y : Type w}
220     {H : Type z} [Fintype X] (F : A → X → X) (q : X → Y) (r : X → H)
221     (h : ∀ x y, r x = r y → SameBehavior F q x y) :
222     Fintype.card (Attained (fun x => (canonicalPredictor F q r h).initState (record r x))) =
223       Fintype.card (BehavioralState F q) := by
224   apply le_antisymm
225   · exact Fintype.card_le_of_injective Subtype.val Subtype.val_injective
226   · exact (canonicalPredictor F q r h).minimal_initialized_card
227 
228 end Komorebi.MachineTheory
229 

Back to source controls