PrefixScan.lean

1 import Mathlib.Data.List.Count
2 import Mathlib.Data.Int.Basic
3 
4 /-!
5 # Core 6.4: capacity completion and a literal short-circuit root scan
6 
7 The scan reads one Boolean report per row, retains both ordered sublists on
8 success, and stops at the first excessive prefix. Counts are natural numbers;
9 the source's nonnegative integer formulation is supplied separately.
10 -/
11 namespace Komorebi.MachineTheory.PrefixScan
12 
13 /-- A completion assigns every unread row to exactly one of the two branches. -/
14 def Completable (m C a b : ℕ) : Prop :=
15   ∃ u v : ℕ, u + v = m - (a+b) ∧ a+u ≤ C ∧ b+v ≤ C
16 
17 /-- Core 6.4's numerical iff. Capacity feasibility is not query realizability. -/
18 theorem completion_iff (m C a b : ℕ) (hread : a+b ≤ m) (hsize : m ≤ 2*C) :
19     Completable m C a b ↔ max a b ≤ C := by
20   constructor
21   · rintro ⟨u,v,_,ha,hb⟩
22     omega
23   · intro h
24     let u := min (m-(a+b)) (C-a)
25     refine ⟨u,m-(a+b)-u,?_,?_,?_⟩ <;> dsimp [u] <;> omega
26 
27 /-- The exact integer statement in the book, including its declared range. -/
28 theorem integer_completion_iff (m C a b : ℤ) (_hC : 1 ≤ C)
29     (_hm : 2 ≤ m) (hsize : m ≤ 2*C) (_ha : 0 ≤ a) (_hb : 0 ≤ b) (hread : a+b ≤ m) :
30     (∃ u v : ℤ, 0 ≤ u ∧ 0 ≤ v ∧ u+v=m-a-b ∧ a+u≤C ∧ b+v≤C) ↔ max a b ≤ C := by
31   constructor
32   · rintro ⟨u,v,hu,hv,_,h1,h2⟩; omega
33   · intro h
34     refine ⟨min (m-a-b) (C-a),m-a-b-min (m-a-b) (C-a),?_,?_,?_,?_,?_⟩ <;> omega
35 
36 variable {X : Type}
37 
38 /-- Preserve original order within each report branch. -/
39 def prepend (x : X) (o : Bool) (p : List X × List X) : List X × List X :=
40   if o then (p.1,x::p.2) else (x::p.1,p.2)
41 
42 def partition (report : X → Bool) : List X → List X × List X
43   | [] => ([],[])
44   | x::xs => prepend x (report x) (partition report xs)
45 
46 /-- Counters refer only to report-table reads and capacity-predicate evaluations. -/
47 structure Result (X : Type) where
48   branches : Option (List X × List X)
49   reads : ℕ
50   checks : ℕ
51   deriving Repr, DecidableEq
52 
53 def full (report : X → Bool) (C a b : ℕ) (xs : List X) : Result X :=
54   let p := partition report xs
55   ⟨if max (a+p.1.length) (b+p.2.length) ≤ C then some p else none,xs.length,1⟩
56 
57 /-- A predicate is tested before another row is read, also at the final prefix. -/
58 def stream (report : X → Bool) (C a b : ℕ) : List X → Result X
59   | [] => ⟨if max a b ≤ C then some ([],[]) else none,0,1⟩
60   | x::xs =>
61       if max a b ≤ C then
62         let o := report x
63         let r := if o then stream report C a (b+1) xs else stream report C (a+1) b xs
64         ⟨r.branches.map (prepend x o),r.reads+1,r.checks+1⟩
65       else ⟨none,0,1⟩
66 
67 @[simp] theorem partition_nil (report : X → Bool) : partition report [] = ([],[]) := rfl
68 
69 theorem partition_filters (report : X → Bool) (xs : List X) :
70     partition report xs = (xs.filter (fun x => !report x),xs.filter report) := by
71   induction xs with
72   | nil => rfl
73   | cons x xs ih =>
74     simp only [partition,ih,prepend,List.filter_cons]
75     cases report x <;> rfl
76 
77 theorem partition_length (report : X → Bool) (xs : List X) :
78     (partition report xs).1.length + (partition report xs).2.length = xs.length := by
79   induction xs with
80   | nil => rfl
81   | cons x xs ih =>
82     simp only [partition,prepend]
83     cases report x <;> simp_all <;> omega
84 
85 /-- The literal streaming scan preserves the full scan's returned ordered branches. -/
86 theorem stream_branches (report : X → Bool) (C a b : ℕ) (xs : List X) :
87     (stream report C a b xs).branches = (full report C a b xs).branches := by
88   induction xs generalizing a b with
89   | nil => rfl
90   | cons x xs ih =>
91     by_cases hab : max a b ≤ C
92     · cases ho : report x
93       · simp only [stream,hab,ite_true,ho,Bool.false_eq_true,ite_false,ih,full,
94           partition,prepend,Option.map_ite,
95           List.length_cons]
96         simp only [Nat.add_assoc,Nat.add_comm]
97       · simp only [stream,hab,ite_true,ho,ih,full,partition,prepend,
98           Option.map_ite,List.length_cons]
99         simp only [Nat.add_assoc,Nat.add_comm]
100     · have hn : ¬ max (a+(partition report (x::xs)).1.length)
101           (b+(partition report (x::xs)).2.length) ≤ C := by omega
102       simp only [stream,hab,ite_false,full,hn]
103 
104 /-- Early rejection can only omit a suffix of table reads. -/
105 theorem stream_reads_le (report : X → Bool) (C a b : ℕ) (xs : List X) :
106     (stream report C a b xs).reads ≤ xs.length := by
107   induction xs generalizing a b with
108   | nil => exact Nat.zero_le _
109   | cons x xs ih =>
110     by_cases hab : max a b ≤ C
111     · cases ho : report x <;> simp only [stream,hab,ite_true,ho,Bool.false_eq_true,ite_false]
112       · exact Nat.succ_le_succ (ih (a+1) b)
113       · exact Nat.succ_le_succ (ih a (b+1))
114     · simp only [stream,hab,ite_false]; exact Nat.zero_le _
115 
116 /-- The added capacity tests are metered; they are not free inference. -/
117 theorem stream_checks (report : X → Bool) (C a b : ℕ) (xs : List X) :
118     (stream report C a b xs).checks = (stream report C a b xs).reads + 1 := by
119   induction xs generalizing a b with
120   | nil => rfl
121   | cons x xs ih =>
122     by_cases hab : max a b ≤ C
123     · cases ho : report x <;> simp only [stream,hab,ite_true,ho,Bool.false_eq_true,ite_false]
124       · rw [ih]
125       · rw [ih]
126     · simp only [stream,hab,ite_false]
127 
128 /-- Success cannot be claimed without reading the complete candidate query. -/
129 theorem successful_reads (report : X → Bool) (C a b : ℕ) (xs : List X)
130     (p : List X × List X) (hs : (stream report C a b xs).branches = some p) :
131     (stream report C a b xs).reads = xs.length := by
132   induction xs generalizing a b p with
133   | nil => rfl
134   | cons x xs ih =>
135     by_cases hab : max a b ≤ C
136     · cases ho : report x
137       · simp only [stream,hab,ite_true,ho,Bool.false_eq_true,ite_false] at hs ⊢
138         obtain ⟨q,hq,_⟩ := Option.map_eq_some_iff.mp hs
139         exact congrArg (fun n => n+1) (ih (a+1) b q hq)
140       · simp only [stream,hab,ite_true,ho] at hs ⊢
141         obtain ⟨q,hq,_⟩ := Option.map_eq_some_iff.mp hs
142         exact congrArg (fun n => n+1) (ih a (b+1) q hq)
143     · simp only [stream,hab,ite_false] at hs
144       cases hs
145 
146 end Komorebi.MachineTheory.PrefixScan

Back to source controls