Mathlib.Algorithms.MonotoneWindowDeque
A rightmost-stable monotone deque for maxima over finite streams with nondecreasing contiguous windows, including invariant preservation, scan correctness, and amortized resource bounds.
Basic 9 core · 6 supporting This module gives the paper-independent input model for a monotone-window scan: a finite prefix of an ordered value function, bounded half-open windows, and a finite schedule whose two endpoints are nondecreasing. ★ left_le_of_get_lt
Finite streams and monotone contiguous window schedules
This module gives the paper-independent input model for a monotone-window scan: a finite prefix of an ordered value function, bounded half-open windows, and a finite schedule whose two endpoints are nondecreasing. It also relates predicate, list, and finset views of a window, including empty windows.
structure Stream reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A finite ordered stream of values in a type records its length and value at each natural-number index.
Definition (Lean source)
parameters
α :
Type*
fields
length :
ℕ
value :
ℕ → α
structure Window reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A contiguous half-open window in a stream of given length has a left endpoint no larger than its right endpoint, which does not exceed the stream length.
Definition (Lean source)
parameters
n :
ℕ
fields
left :
ℕ
right :
ℕ
left_le_right :
left ≤ right
right_le_length :
right ≤ n
def ActiveAt reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A left endpoint, a right endpoint, and an index determine whether the index is active in the half-open interval.
Definition (Lean source)
parameters
left right i :
ℕ
def
ActiveAt left right i :
Prop
given by
clause 1
left ≤ i
clause 2
i < right
def Active reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A bounded window and an index determine whether the index is active in that window.
def indices reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque.Window
A bounded window determines its increasing list of active indices.
def indexFinset reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque.Window
A bounded window determines its finite set of active indices.
structure Schedule reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A finite schedule for a stream of given length contains bounded windows with nondecreasing left and right endpoints.
def steps reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque.Schedule
A finite schedule determines its number of scheduled windows.
Definition (Lean source)
parameters
n :
ℕ
schedule :
Schedule n
def
steps schedule :
ℕ
given by
schedule.windows.length
theorem left_le_of_get_lt reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque.Schedule
A finite schedule, two valid schedule positions, and their strict order ensure that the earlier left endpoint is no larger.
Formal statement
6 supporting declarations (lemmas, instances)
-
mem_indices_ifftheorem — A bounded window has the same active indices in its list enumeration and in its active-window condition. -
mem_indexFinset_ifftheorem — A bounded window has the same active indices in its finite-set enumeration and in its active-window condition. -
card_indexFinsettheorem — A bounded window has as many active indices as its width.Proof (Lean source)
theorem Window.card_indexFinset {n : ℕ} (w : Window n) : w.indexFinset.card = w.right - w.left := by simp [Window.indexFinset] -
indices_eq_nil_ifftheorem — A bounded window has an empty index list exactly when its two endpoints coincide.Proof (Lean source)
theorem Window.indices_eq_nil_iff {n : ℕ} (w : Window n) : w.indices = [] ↔ w.left = w.right := by constructor · intro h have hlen : w.indices.length = 0 := by simp [h] rw [Window.indices, List.length_range'] at hlen exact Nat.le_antisymm w.left_le_right (Nat.sub_eq_zero_iff_le.mp hlen) · intro h simp [Window.indices, h] -
indexFinset_nonempty_ifftheorem — A bounded window has an active index exactly when its left endpoint is strictly below its right endpoint.Proof (Lean source)
theorem Window.indexFinset_nonempty_iff {n : ℕ} (w : Window n) : w.indexFinset.Nonempty ↔ w.left < w.right := by simp [Window.indexFinset] -
right_le_of_get_lttheorem — A finite schedule, two valid schedule positions, and their strict order ensure that the earlier right endpoint is no larger.hypothesesn :ℕschedule :Schedule ni j :ℕhi :i < schedule.stepshj :j < schedule.stepshij :i < jconclusion(schedule.windows.get ⟨i, hi⟩).right ≤ (schedule.windows.get ⟨j, hj⟩).rightProof (Lean source)
theorem Schedule.right_le_of_get_lt {n : ℕ} (schedule : Schedule n) {i j : ℕ} (hi : i < schedule.steps) (hj : j < schedule.steps) (hij : i < j) : (schedule.windows.get ⟨i, hi⟩).right ≤ (schedule.windows.get ⟨j, hj⟩).right := by exact schedule.right_mono.rel_get_of_lt hij
Deque 12 core · 10 supporting This module defines the purely functional deque kernel. ★ mem_prunedBack_dominated
Monotone deque operations and invariant
This module defines the purely functional deque kernel. The deterministic tie policy is rightmost-stable: inserting a value deletes every suffix entry with value less than or equal to the new value. Consequently retained values are strictly decreasing from front to back.
abbrev Deque reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A deque is represented by its front-to-back list of natural-number indices. The type itself imposes no ordering or monotonicity; the monotone-deque invariant is carried separately by the validity predicates.
Definition (Lean source)
def
Deque :
Type
given by
List ℕ
def initialDeque reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
The initial deque is empty before any stream index enters.
Definition (Lean source)
def
given by
[]
def expireFront reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A left endpoint and a deque determine the deque after front expiration.
def expiredFront reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A left endpoint and a deque determine the recorded front pops.
def pruneBack reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A stream, a deque, and a new index determine the deque after rightmost-stable back pruning, which removes ties in favor of the newer index.
def prunedBack reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A stream, a deque, and a new index determine the recorded back pops.
def push reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A stream, a deque, and a new index determine the deque after one rightmost-stable insertion.
structure PushBatch reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A batch insertion records its final deque, every pushed index, and every index removed from the back while processing the batch.
def pushAll reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A stream determines the recorded batch insertion from an initial deque and a list of entering indices.
Definition (Lean source)
parameters
α :
Type u_1
stream :
Stream α
given by
clause 1
| q, [] => { state := q, pushed := [], backPopped := [] }
clause 2
| q, i :: is
=> let removed := prunedBack stream q i let rest := pushAll stream (push stream q i) is { state := rest.state, pushed := i :: rest.pushed, backPopped := removed ++ rest.backPopped }
structure ValidAt reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A stream, two raw endpoints, and a deque satisfy the validity invariant when every retained index is active for the endpoints and within the stream, retained indices strictly increase from front to back, their stream values strictly decrease from front to back, and every active in-stream index that is not retained is dominated by a later retained index whose value is at least as large.
Definition (Lean source)
parameters
assumes
def Valid reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A stream, a bounded window, and a deque determine whether the deque is valid for that window.
theorem mem_prunedBack_dominated reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A stream, all old indices being earlier than the new index, and an index recorded as a back pop ensure that the popped index is earlier and no larger in value than the new index.
Formal statement
hypotheses
α :
Type u_1
stream :
Stream α
q :
i j :
ℕ
hindex :
∀ k ∈ q, k < i
hj :
j ∈ prunedBack stream q i
conclusion
conclusion 1
j < i
conclusion 2
stream.value j ≤ stream.value i
Proof (Lean source)
theorem mem_prunedBack_dominated (stream : Stream α) {q : Deque} {i j : ℕ}
(hindex : ∀ k ∈ q, k < i) (hj : j ∈ prunedBack stream q i) :
j < i ∧ stream.value j ≤ stream.value i := by
constructor
· exact hindex j ((List.rtakeWhile_suffix _ _).mem hj)
· have h := List.mem_rtakeWhile_imp hj
simpa [prunedBack] using h
10 supporting declarations (lemmas, instances)
-
initialDeque_validAttheorem — A stream has an empty initial deque satisfying the zero-width invariant.Proof (Lean source)
theorem initialDeque_validAt (stream : Stream α) : ValidAt stream 0 0 initialDeque := by refine ⟨?_, ?_, ?_, ?_⟩ · simp [initialDeque] · simp [initialDeque] · simp [initialDeque] · simp [initialDeque, ActiveAt] -
expiredFront_append_expireFronttheorem — A left endpoint and a deque have a reported front-pop prefix followed by the retained deque exactly equal to the original deque.Proof (Lean source)
theorem expiredFront_append_expireFront (left : ℕ) (q : Deque) : expiredFront left q ++ expireFront left q = q := by exact List.takeWhile_append_dropWhile -
pruneBack_append_prunedBacktheorem — A stream, a deque, and a new index have a retained prefix and reported back-pop suffix exactly equal to the original deque.hypothesesconclusionpruneBack stream q i ++ prunedBack stream q i = qProof (Lean source)
theorem pruneBack_append_prunedBack (stream : Stream α) (q : Deque) (i : ℕ) : pruneBack stream q i ++ prunedBack stream q i = q := by exact List.rdropWhile_append_rtakeWhile -
pruneBack_prefixtheorem — A stream, a deque, and a new index ensure that back pruning retains a prefix of the old deque.hypothesesconclusionpruneBack stream q i <+: qProof (Lean source)
theorem pruneBack_prefix (stream : Stream α) (q : Deque) (i : ℕ) : pruneBack stream q i <+: q := by exact List.rdropWhile_prefix _ _ -
pruneBack_index_orderedtheorem — A stream, a new index, and strictly ordered old deque indices ensure that back pruning preserves strict index order.hypothesesconclusion(pruneBack stream q i).Pairwise (· < ·)Proof (Lean source)
theorem pruneBack_index_ordered (stream : Stream α) {q : Deque} {i : ℕ} (hq : q.Pairwise (· < ·)) : (pruneBack stream q i).Pairwise (· < ·) := by exact hq.sublist (pruneBack_prefix stream q i).sublist -
pruneBack_value_decreasingtheorem — A stream, a new index, and strictly decreasing old deque values ensure that back pruning preserves strict value decrease.hypothesesα :sharedType u_1stream :Stream αq :i :ℕhq :q.Pairwise (fun j k => stream.value k < stream.value j)conclusion(pruneBack stream q i).Pairwise (fun j k => stream.value k < stream.value j)Proof (Lean source)
theorem pruneBack_value_decreasing (stream : Stream α) {q : Deque} {i : ℕ} (hq : q.Pairwise (fun j k => stream.value k < stream.value j)) : (pruneBack stream q i).Pairwise (fun j k => stream.value k < stream.value j) := by exact hq.sublist (pruneBack_prefix stream q i).sublist -
mem_push_ifftheorem — A stream, a deque, a new index, and a queried index have the stated membership characterization after one push.hypotheses -
push_index_orderedtheorem — A stream, strictly ordered old deque indices, and all old indices being earlier than the new one ensure that one push preserves strict index order.hypothesesconclusion(push stream q i).Pairwise (· < ·)Proof (Lean source)
theorem push_index_ordered (stream : Stream α) {q : Deque} {i : ℕ} (hq : q.Pairwise (· < ·)) (hi : ∀ j ∈ q, j < i) : (push stream q i).Pairwise (· < ·) := by rw [push, List.pairwise_append] refine ⟨pruneBack_index_ordered stream hq, List.pairwise_singleton _ _, ?_⟩ intro j hj k hk simp only [List.mem_singleton] at hk subst k exact hi j ((pruneBack_prefix stream q i).mem hj) -
push_value_decreasingtheorem — A stream and strictly decreasing old deque values ensure that one rightmost-stable push leaves strictly decreasing values.hypothesesα :sharedType u_1stream :Stream αq :i :ℕhq :q.Pairwise (fun j k => stream.value k < stream.value j)conclusion(push stream q i).Pairwise (fun j k => stream.value k < stream.value j)Proof (Lean source)
theorem push_value_decreasing (stream : Stream α) {q : Deque} {i : ℕ} (hq : q.Pairwise (fun j k => stream.value k < stream.value j)) : (push stream q i).Pairwise (fun j k => stream.value k < stream.value j) := by rw [push, List.pairwise_append] refine ⟨pruneBack_value_decreasing stream hq, List.pairwise_singleton _ _, ?_⟩ intro j hj k hk simp only [List.mem_singleton] at hk subst k let r := pruneBack stream q i have hr_ne : r ≠ [] := List.ne_nil_of_mem hj have hlast : stream.value i < stream.value (r.getLast hr_ne) := by have h := List.rdropWhile_last_not (fun j => decide (stream.value j ≤ stream.value i)) q hr_ne simpa [r, pruneBack] using h have hr : r.Pairwise (fun a b => stream.value b < stream.value a) := by exact pruneBack_value_decreasing stream (i := i) hq have hr_le : r.Pairwise (fun a b => stream.value b ≤ stream.value a) := by exact hr.imp (fun h => h.le) exact lt_of_lt_of_le hlast (hr_le.rel_getLast hj) -
noduptheorem — A valid raw-window deque has no duplicate indices.hypothesesconclusionq.Nodup
Update 3 core · 7 supporting This module combines front expiration with batch insertion of the newly entered right-endpoint interval. ★ update_preserves
Window update and invariant preservation
This module combines front expiration with batch insertion of the newly entered right-endpoint interval. Its preservation results cover repeated endpoints, empty batches, empty windows, and windows that become empty.
structure StepTrace reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A stream has a step record containing its before and after deques and exact push, front-pop, and back-pop event lists.
def update reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A stream, the prior right endpoint, a new bounded window, and the prior deque determine the recorded monotone-deque update, expiring the front before inserting newly entered active indices.
Definition (Lean source)
parameters
def
given by
expired :
expireFront window.left q
enteredLeft :
max oldRight window.left
entered :
range' enteredLeft (window.right - enteredLeft)
batch :
pushAll stream expired entered
{ oldRight := oldRight window := window before := q afterExpiration := expired after := batch.state pushed := batch.pushed frontPopped := expiredFront window.left q backPopped := batch.backPopped }
theorem update_preserves reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A valid old-window deque, a nondecreasing left endpoint, and a nondecreasing right endpoint ensure that one update produces a valid new-window deque.
Formal statement
Proof (Lean source)
theorem update_preserves {stream : Stream α} {oldWindow newWindow : Window stream.length}
{q : Deque} (hq : Valid stream oldWindow q)
(hleft : oldWindow.left ≤ newWindow.left)
(hright : oldWindow.right ≤ newWindow.right) :
Valid stream newWindow (update stream oldWindow.right newWindow q).after := by
unfold Valid at hq ⊢
unfold update
exact pushAll_interval_preserves
(expireFront_preserves hq hleft)
hright
newWindow.right_le_length
newWindow.left_le_right
7 supporting declarations (lemmas, instances)
-
update_pushedtheorem — A stream, a prior right endpoint, a new window, and a prior deque have an update push log equal to the newly entered active interval.hypotheses -
expireFront_preservestheorem — A valid old raw-window deque and a nondecreasing new left endpoint ensure that front expiration preserves the full raw-window invariant, including an empty intermediate interval.hypothesesconclusionValidAt stream newLeft oldRight (expireFront newLeft q)Proof (Lean source)
theorem expireFront_preserves {stream : Stream α} {oldLeft oldRight newLeft : ℕ} {q : Deque} (hq : ValidAt stream oldLeft oldRight q) (hleft : oldLeft ≤ newLeft) : ValidAt stream newLeft oldRight (expireFront newLeft q) := by by_cases hempty : oldRight < newLeft · have hexp : expireFront newLeft q = [] := by rw [expireFront, List.dropWhile_eq_nil_iff] intro i hi simp only [decide_eq_true_eq] exact lt_trans (hq.active i hi).1.2 hempty rw [hexp] refine ⟨by simp, by simp, by simp, ?_⟩ intro i hactive simp only [ActiveAt] at hactive exfalso omega · have hsub : (expireFront newLeft q).Sublist q := by exact List.dropWhile_sublist _ refine ⟨?_, hq.index_ordered.sublist hsub, hq.value_decreasing.sublist hsub, ?_⟩ · intro i hi have himem : i ∈ q ∧ newLeft ≤ i := by exact (mem_dropWhile_lt_iff newLeft hq.index_ordered i).mp hi have hiold := hq.active i himem.1 exact ⟨⟨himem.2, hiold.1.2⟩, hiold.2⟩ · intro i hi hbound hin have hiold : ActiveAt oldLeft oldRight i := ⟨le_trans hleft hi.1, hi.2⟩ have hiq : i ∉ q := by intro hiq apply hin exact (mem_dropWhile_lt_iff newLeft hq.index_ordered i).mpr ⟨hiq, hi.1⟩ obtain ⟨j, hjq, hij, hvalue⟩ := hq.dominates_omitted i hiold hbound hiq refine ⟨j, ?_, hij, hvalue⟩ exact (mem_dropWhile_lt_iff newLeft hq.index_ordered j).mpr ⟨hjq, le_trans hi.1 (le_of_lt hij)⟩ -
to_max_righttheorem — A valid raw-window deque remains valid when its right endpoint is enlarged to at least its left endpoint.hypothesesProof (Lean source)
theorem ValidAt.to_max_right {stream : Stream α} {left right : ℕ} {q : Deque} (hq : ValidAt stream left right q) : ValidAt stream left (max right left) q := by by_cases hempty : right < left · have hqnil : q = [] := by apply List.eq_nil_iff_forall_not_mem.mpr intro i hi have hactive := (hq.active i hi).1 simp only [ActiveAt] at hactive omega rw [hqnil] refine ⟨by simp, by simp, by simp, ?_⟩ intro i hactive simp only [ActiveAt] at hactive have hmax : max right left = left := max_eq_right (le_of_lt hempty) rw [hmax] at hactive omega · have hle : left ≤ right := Nat.le_of_not_gt hempty simpa [max_eq_left hle] using hq -
push_succ_preservestheorem — A valid raw-window deque, a left endpoint no larger than the current right endpoint, and room for one more stream index ensure that pushing the right-boundary index preserves the invariant for the enlarged window.hypothesesleft right :ℕq :hq :ValidAt stream left right qhleft :left ≤ righthbound :right < stream.lengthProof (Lean source)
theorem push_succ_preserves {stream : Stream α} {left right : ℕ} {q : Deque} (hq : ValidAt stream left right q) (hleft : left ≤ right) (hbound : right < stream.length) : ValidAt stream left (right + 1) (push stream q right) := by have hold_lt : ∀ j ∈ q, j < right := by intro j hj exact (hq.active j hj).1.2 have hright_mem : right ∈ push stream q right := by exact (mem_push_iff stream q right right).mpr (inr rfl) refine ⟨?_, push_index_ordered stream hq.index_ordered hold_lt, push_value_decreasing stream hq.value_decreasing, ?_⟩ · intro i hi rcases (mem_push_iff stream q right i).mp hi with hi | hiEq · have hiq : i ∈ q := (pruneBack_prefix stream q right).mem hi have hactive := hq.active i hiq exact ⟨⟨hactive.1.1, Nat.lt_succ_of_lt hactive.1.2⟩, hactive.2⟩ · subst i exact ⟨⟨hleft, Nat.lt_succ_self right⟩, hbound⟩ · intro i hi hifinite hin have hine : i ≠ right := by intro hiright apply hin simpa [hiright] using hright_mem have hiright : i < right := by simp only [ActiveAt] at hi omega have hiold : ActiveAt left right i := ⟨hi.1, hiright⟩ by_cases hiq : i ∈ q · have hipruned : i ∈ prunedBack stream q right := by have hiappend : i ∈ pruneBack stream q right ++ prunedBack stream q right := by rw [pruneBack_append_prunedBack] exact hiq rcases List.mem_append.mp hiappend with hiretained | hipruned · exact elim (hin ((mem_push_iff stream q right i).mpr (inl hiretained))) · exact hipruned have hidominated := mem_prunedBack_dominated stream hold_lt hipruned exact ⟨right, hright_mem, hidominated.1, hidominated.2⟩ · obtain ⟨j, hjq, hij, hvalue⟩ := hq.dominates_omitted i hiold hifinite hiq by_cases hjretained : j ∈ pruneBack stream q right · exact ⟨j, (mem_push_iff stream q right j).mpr (inl hjretained), hij, hvalue⟩ · have hjpruned : j ∈ prunedBack stream q right := by have hjappend : j ∈ pruneBack stream q right ++ prunedBack stream q right := by rw [pruneBack_append_prunedBack] exact hjq exact (List.mem_append.mp hjappend).resolve_left hjretained have hjdominated := mem_prunedBack_dominated stream hold_lt hjpruned exact ⟨right, hright_mem, lt_trans hij hjdominated.1, le_trans hvalue hjdominated.2⟩ -
pushAll_range_preservestheorem — A valid raw-window deque, a left endpoint no larger than the range start, and a range ending within the stream ensure that pushing the whole consecutive range preserves the invariant.hypothesesleft start count :ℕq :hq :ValidAt stream left start qhleft :left ≤ starthbound :start + count ≤ stream.lengthProof (Lean source)
theorem pushAll_range_preserves {stream : Stream α} {left start count : ℕ} {q : Deque} (hq : ValidAt stream left start q) (hleft : left ≤ start) (hbound : start + count ≤ stream.length) : ValidAt stream left (start + count) (pushAll stream q (range' start count)).state := by induction count generalizing start q with | zero => simpa [pushAll] | succ count ih => rw [List.range'_succ] simp only [pushAll] have hpush : ValidAt stream left (start + 1) (push stream q start) := push_succ_preserves hq hleft (by omega) have hrec := ih (start := start + 1) (q := push stream q start) hpush (by omega) (by omega) simpa only [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using hrec -
pushAll_interval_preservestheorem — A valid deque after front expiration, a nondecreasing right endpoint, a new endpoint within the stream, and a valid new raw interval ensure that inserting newly entered active indices restores the invariant.hypothesesleft oldRight newRight :ℕq :hq :ValidAt stream left oldRight qhright :oldRight ≤ newRighthbound :newRight ≤ stream.lengthhwindow :left ≤ newRightProof (Lean source)
theorem pushAll_interval_preserves {stream : Stream α} {left oldRight newRight : ℕ} {q : Deque} (hq : ValidAt stream left oldRight q) (hright : oldRight ≤ newRight) (hbound : newRight ≤ stream.length) (hwindow : left ≤ newRight) : ValidAt stream left newRight (pushAll stream q (range' (max oldRight left) (newRight - max oldRight left))).state := by have hright? : max oldRight left ≤ newRight := max_le hright hwindow have hq' : ValidAt stream left (max oldRight left) q := hq.to_max_right have hbatch := pushAll_range_preserves (start := max oldRight left) (count := newRight - max oldRight left) hq' (le_max_right oldRight left) (by simpa [Nat.add_sub_of_le hright?] using hbound) simpa [Nat.add_sub_of_le hright?] using hbatch -
update_initial_preservestheorem — A stream and its first bounded window ensure that updating from the empty initial interval produces a valid deque.hypothesesProof (Lean source)
theorem update_initial_preserves (stream : Stream α) (window : Window stream.length) : Valid stream window (update stream 0 window []).after := by unfold Valid unfold update exact pushAll_interval_preserves (expireFront_preserves (initialDeque_validAt stream) (zero_le _)) (zero_le _) window.right_le_length window.left_le_right
Correctness 3 core · 3 supporting The invariant implies that the deque head is an active argmax. ★ head_value_eq_windowMax
Head and finite-window maximum correctness
The invariant implies that the deque head is an active argmax. This module exposes both the argmax witness formulation and equality with the maximum of the finite set of active values, so consumers never need to unfold the internal domination invariant.
def windowValues reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A stream and a bounded window determine the finite set of values observed in that window.
def windowMax reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A stream, a bounded window, and strictly ordered window endpoints determine the window maximum.
Definition (Lean source)
parameters
α :
Type u_1
stream :
Stream α
window :
Window stream.length
hne :
window.left < window.right
def
windowMax stream window hne :
α
given by
(windowValues stream window).max' (windowValues_nonempty stream window hne)
theorem head_value_eq_windowMax reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque.Valid
A valid bounded-window deque and a nonempty window ensure that its head is an active argmax whose value equals the finite-window maximum.
Formal statement
Proof (Lean source)
theorem Valid.head_value_eq_windowMax {stream : Stream α}
{window : Window stream.length} {q : Deque}
(hq : Valid stream window q) (hne : window.left < window.right) :
∃ head tail, q = head :: tail ∧ Active window head ∧
stream.value head = windowMax stream window hne ∧
∀ i, Active window i → stream.value i ≤ stream.value head := by
obtain ⟨head, tail, hqeq, hhead, hmax⟩ := hq.head_argmax hne
refine ⟨head, tail, hqeq, hhead, ?_, hmax⟩
unfold windowMax
symm
apply (Finset.max'_eq_iff _ _ _).mpr
constructor
· rw [windowValues, mem_image]
exact ⟨head, (Window.mem_indexFinset_iff window).mpr hhead, rfl⟩
· intro value hvalue
rw [windowValues, mem_image] at hvalue
obtain ⟨i, hi, rfl⟩ := hvalue
exact hmax i ((Window.mem_indexFinset_iff window).mp hi)
3 supporting declarations (lemmas, instances)
-
windowValues_nonemptytheorem — A stream, a bounded window, and strictly ordered window endpoints ensure that the window's finite value set is nonempty.hypothesesα :sharedType u_1stream :Stream αwindow :Window stream.lengthhne :window.left < window.rightconclusion(windowValues stream window).NonemptyProof (Lean source)
theorem windowValues_nonempty (stream : Stream α) (window : Window stream.length) (hne : window.left < window.right) : (windowValues stream window).Nonempty := by refine ⟨stream.value window.left, ?_⟩ rw [windowValues, mem_image] exact ⟨window.left, (Window.mem_indexFinset_iff window).mpr ⟨le_rfl, hne⟩, rfl⟩ -
head_argmaxtheorem — A valid raw-window deque, a nonempty raw interval, and a right endpoint within the stream ensure that the deque head is active and maximizes the stream value over that interval.hypothesesleft right :ℕq :hq :ValidAt stream left right qhne :left < righthbound :right ≤ stream.lengthProof (Lean source)
theorem ValidAt.head_argmax {stream : Stream α} {left right : ℕ} {q : Deque} (hq : ValidAt stream left right q) (hne : left < right) (hbound : right ≤ stream.length) : ∃ head tail, q = head :: tail ∧ ActiveAt left right head ∧ head < stream.length ∧ ∀ i, ActiveAt left right i → i < stream.length → stream.value i ≤ stream.value head := by have hq_ne : q ≠ [] := by intro hq_nil have hleft_bound : left < stream.length := lt_of_lt_of_le hne hbound obtain ⟨j, hj, -⟩ := hq.dominates_omitted left ⟨le_rfl, hne⟩ hleft_bound (by simp [hq_nil]) simp [hq_nil] at hj obtain ⟨head, tail, rfl⟩ := List.exists_cons_of_ne_nil hq_ne have hhead := hq.active head (by simp) refine ⟨head, tail, rfl, hhead.1, hhead.2, ?_⟩ intro i hi hibound have hmember_le : ∀ j ∈ head :: tail, stream.value j ≤ stream.value head := by intro j hj rcases List.mem_cons.mp hj with rfl | hj · exact le_rfl · exact (List.pairwise_cons.mp hq.value_decreasing).1 j hj |>.le by_cases hiq : i ∈ head :: tail · exact hmember_le i hiq · obtain ⟨j, hjq, -, hij⟩ := hq.dominates_omitted i hi hibound hiq exact le_trans hij (hmember_le j hjq) -
head_argmaxtheorem — A valid bounded-window deque and a nonempty window ensure that its head is an active argmax.hypothesesProof (Lean source)
theorem Valid.head_argmax {stream : Stream α} {window : Window stream.length} {q : Deque} (hq : Valid stream window q) (hne : window.left < window.right) : ∃ head tail, q = head :: tail ∧ Active window head ∧ ∀ i, Active window i → stream.value i ≤ stream.value head := by obtain ⟨head, tail, hqeq, hhead, -, hmax⟩ := ValidAt.head_argmax hq hne window.right_le_length refine ⟨head, tail, hqeq, hhead, ?_⟩ intro i hi exact hmax i hi (lt_of_lt_of_le hi.2 window.right_le_length)
Scan 3 core · 3 supporting This module runs the deque update over every scheduled window. ★ scan_head_value_eq_windowMax
Folding updates across a monotone window schedule
This module runs the deque update over every scheduled window. Its pointwise theorems return the valid state, active head argmax, and exact maximum value at any requested schedule position.
def scanFrom reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A stream determines the scan trace produced from a prior right endpoint, deque, and list of windows.
Definition (Lean source)
parameters
α :
Type u_1
stream :
Stream α
def scan reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A stream and a monotone window schedule determine the complete scan trace from the empty initial state.
Definition (Lean source)
parameters
given by
scanFrom stream 0 initialDeque schedule.windows
theorem scan_head_value_eq_windowMax reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A stream, a monotone window schedule, a valid schedule position, and a nonempty window at that position ensure that the scan head is an active argmax whose value equals the finite-window maximum.
Formal statement
Proof (Lean source)
theorem scan_head_value_eq_windowMax (stream : Stream α)
(schedule : Schedule stream.length) {k : ℕ} (hk : k < schedule.steps)
(hne : (schedule.windows.get ⟨k, hk⟩).left <
(schedule.windows.get ⟨k, hk⟩).right) :
∃ step head tail,
(scan stream schedule)[k]? = some step ∧
step.window = schedule.windows.get ⟨k, hk⟩ ∧
step.after = head :: tail ∧ Active step.window head ∧
stream.value head = windowMax stream (schedule.windows.get ⟨k, hk⟩) hne ∧
∀ i, Active step.window i → stream.value i ≤ stream.value head := by
obtain ⟨step, hstep, hwindow, hvalid⟩ := scan_valid_at stream schedule hk
have hne_step : step.window.left < step.window.right := by
simpa [hwindow] using hne
obtain ⟨head, tail, hafter, hactive, hvalue, hmax⟩ :=
hvalid.head_value_eq_windowMax hne_step
refine ⟨step, head, tail, hstep, hwindow, hafter, hactive, ?_, hmax⟩
simpa [hwindow] using hvalue
3 supporting declarations (lemmas, instances)
-
length_scantheorem — A stream and a monotone window schedule ensure that the scan has exactly one trace step for each scheduled window.hypothesesProof (Lean source)
theorem length_scan (stream : Stream α) (schedule : Schedule stream.length) : (scan stream schedule).length = schedule.steps := by have hlength : ∀ (oldRight : ℕ) (q : Deque) (windows : List (Window stream.length)), (scanFrom stream oldRight q windows).length = windows.length := by intro oldRight q windows induction windows generalizing oldRight q with | nil => rfl | cons window windows ih => simp only [scanFrom, List.length_cons] rw [ih] exact hlength 0 initialDeque schedule.windows -
scan_valid_attheorem — A stream, a monotone window schedule, and a valid schedule position ensure that the corresponding scan step has a valid deque for its window.hypothesesα :sharedType u_1stream :Stream αschedule :Schedule stream.lengthk :ℕhk :k < schedule.stepsProof (Lean source)
theorem scan_valid_at (stream : Stream α) (schedule : Schedule stream.length) {k : ℕ} (hk : k < schedule.steps) : ∃ step, (scan stream schedule)[k]? = some step ∧ step.window = schedule.windows.get ⟨k, hk⟩ ∧ Valid stream step.window step.after := by let emptyWindow : Window stream.length := { left := 0, right := 0, left_le_right := le_rfl, right_le_length := zero_le _ } have hinitial : Valid stream emptyWindow initialDeque := by exact initialDeque_validAt stream have hleft : (emptyWindow :: schedule.windows).Pairwise (fun a b => a.left ≤ b.left) := by rw [List.pairwise_cons] exact ⟨by simp [emptyWindow], schedule.left_mono⟩ have hright : (emptyWindow :: schedule.windows).Pairwise (fun a b => a.right ≤ b.right) := by rw [List.pairwise_cons] exact ⟨by simp [emptyWindow], schedule.right_mono⟩ simpa [scan, Schedule.steps, emptyWindow] using scanFrom_valid_at_of_valid stream hinitial schedule.windows hleft hright hk -
scan_head_argmaxtheorem — A stream, a monotone window schedule, a valid schedule position, and a nonempty window at that position ensure that the scan head is active and maximizes the stream value in that window.hypothesesProof (Lean source)
theorem scan_head_argmax (stream : Stream α) (schedule : Schedule stream.length) {k : ℕ} (hk : k < schedule.steps) (hne : (schedule.windows.get ⟨k, hk⟩).left < (schedule.windows.get ⟨k, hk⟩).right) : ∃ step head tail, (scan stream schedule)[k]? = some step ∧ step.window = schedule.windows.get ⟨k, hk⟩ ∧ step.after = head :: tail ∧ Active step.window head ∧ ∀ i, Active step.window i → stream.value i ≤ stream.value head := by obtain ⟨step, hstep, hwindow, hvalid⟩ := scan_valid_at stream schedule hk have hne_step : step.window.left < step.window.right := by simpa [hwindow] using hne obtain ⟨head, tail, hafter, hactive, hmax⟩ := hvalid.head_argmax hne_step exact ⟨step, head, tail, hstep, hwindow, hafter, hactive, hmax⟩
PredicateSchedule 10 core · 17 supporting This module turns entry and stay predicates on an arbitrary sparse list of raw keys into bounded half-open position windows. ★ active_schedule_iff
Compiling monotone raw-key predicates to position windows
This module turns entry and stay predicates on an arbitrary sparse list of raw keys into bounded half-open position windows. The hypotheses say exactly that entry sets are prefixes, stay sets are suffixes, entry can only expand along the step list, and stay can only shrink. No order or density assumption is imposed on the raw key type itself.
structure PredicateWindowSchedule reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A sparse raw-key list and an ordered step list determine a predicate window specification whose entry predicate, stay predicate, entry-prefix law, stay-suffix law, entry monotonicity across steps, and stay antitonicity across steps describe a monotone active window.
Definition (Lean source)
parameters
fields
entry :
κ → ι → Prop
stay :
κ → ι → Prop
entry_prefix :
∀ (s : κ) {i j : ℕ} (hi : i < keys.length) (hj : j < keys.length)
if
i ≤ j
and
entry s (keys.get ⟨j, hj⟩)
then
entry s (keys.get ⟨i, hi⟩)
stay_suffix :
∀ (s : κ) {i j : ℕ} (hi : i < keys.length) (hj : j < keys.length)
if
i ≤ j
and
stay s (keys.get ⟨i, hi⟩)
then
stay s (keys.get ⟨j, hj⟩)
entry_step_mono :
steps.Pairwise (fun s t => ∀ x ∈ keys, entry s x → entry t x)
stay_step_anti :
steps.Pairwise (fun s t => ∀ x ∈ keys, stay t x → stay s x)
def entryTest reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque.PredicateWindowSchedule
A predicate schedule, a step, and a raw key determine the Boolean entry test used by the list operations. It decides the entry predicate classically, so it is a noncomputable specification rather than executable code.
Definition (Lean source)
parameters
def
given by
by classical exact decide (P.entry s x)
def expiredTest reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque.PredicateWindowSchedule
A predicate schedule, a step, and a raw key determine the Boolean test that the key has expired, true exactly when the key does not stay at that step. It decides the stay predicate classically, so it is noncomputable.
Definition (Lean source)
parameters
def
given by
by classical exact decide (¬ P.stay s x)
def entered reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque.PredicateWindowSchedule
A predicate schedule and a step determine the raw prefix that has entered by that step.
Definition (Lean source)
parameters
def
given by
by exact keys.takeWhile (P.entryTest s)
def rightEndpoint reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque.PredicateWindowSchedule
A predicate schedule and a step determine the right position endpoint, namely the length of the entered raw-key prefix.
Definition (Lean source)
parameters
def
rightEndpoint P s :
ℕ
given by
(P.entered s).length
def expiredPrefix reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque.PredicateWindowSchedule
A predicate schedule and a step determine the expired prefix of entered keys, namely the initial segment that no longer satisfies the stay predicate.
Definition (Lean source)
parameters
def
given by
by exact (keys.take (P.rightEndpoint s)).takeWhile (P.expiredTest s)
def leftEndpoint reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque.PredicateWindowSchedule
A predicate schedule and a step determine the left position endpoint, namely the length of the expired prefix among entered keys.
Definition (Lean source)
parameters
def
leftEndpoint P s :
ℕ
given by
(P.expiredPrefix s).length
def windowAt reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque.PredicateWindowSchedule
A predicate schedule and a step determine a bounded half-open position window, including when the raw-key list or the active window is empty.
Definition (Lean source)
parameters
def
given by
{ left := P.leftEndpoint s right := P.rightEndpoint s left_le_right := P.leftEndpoint_le_rightEndpoint s right_le_length := P.rightEndpoint_le_length s }
def schedule reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque.PredicateWindowSchedule
A predicate schedule compiles to the monotone bounded-window schedule over key positions.
Definition (Lean source)
parameters
def
schedule P :
Schedule keys.length
given by
by classical refine { windows := steps.map P.windowAt, left_mono := ?_, right_mono := ?_ } · rw [List.pairwise_map] exact (P.entry_step_mono.and P.stay_step_anti).imp (fun h => P.leftEndpoint_mono_of_predicates h.1 h.2) · rw [List.pairwise_map] exact P.entry_step_mono.imp (fun h => P.rightEndpoint_mono_of_entry h)
theorem active_schedule_iff reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque.PredicateWindowSchedule
A predicate schedule, a valid step position, and an in-bounds key position characterize activity in the compiled scheduled window by the raw predicates.
Formal statement
hypotheses
ι :
Type u_1
κ :
Type u_2
P :
PredicateWindowSchedule keys steps
k i :
ℕ
hk :
k < steps.length
hi :
i < keys.length
Proof (Lean source)
theorem active_schedule_iff (P : PredicateWindowSchedule keys steps) {k i : ℕ}
(hk : k < steps.length) (hi : i < keys.length) :
Active (P.schedule.windows.get ⟨k, by simpa [schedule, Schedule.steps] using hk⟩) i ↔
P.entry (steps.get ⟨k, hk⟩) (keys.get ⟨i, hi⟩) ∧
P.stay (steps.get ⟨k, hk⟩) (keys.get ⟨i, hi⟩) := by
rw [P.schedule_window_get hk]
exact P.active_windowAt_iff (steps.get ⟨k, hk⟩) hi
17 supporting declarations (lemmas, instances)
-
rightEndpoint_le_lengththeorem — A predicate schedule has every right endpoint bounded by the raw-key count.hypothesesconclusionP.rightEndpoint s ≤ keys.lengthProof (Lean source)
theorem rightEndpoint_le_length (P : PredicateWindowSchedule keys steps) (s : κ) : P.rightEndpoint s ≤ keys.length := by exact (List.takeWhile_prefix _).length_le -
leftEndpoint_le_rightEndpointtheorem — A predicate schedule has every left endpoint bounded by its right endpoint.hypothesesconclusionP.leftEndpoint s ≤ P.rightEndpoint sProof (Lean source)
theorem leftEndpoint_le_rightEndpoint (P : PredicateWindowSchedule keys steps) (s : κ) : P.leftEndpoint s ≤ P.rightEndpoint s := by change ((keys.take (P.rightEndpoint s)).takeWhile (P.expiredTest s)).length ≤ P.rightEndpoint s calc _ ≤ (keys.take (P.rightEndpoint s)).length := (List.takeWhile_prefix _).length_le _ = P.rightEndpoint s := by simp [List.length_take, Nat.min_eq_left (P.rightEndpoint_le_length s)] -
take_rightEndpoint_eq_enteredtheorem — A predicate schedule has its right prefix exactly equal to the takeWhile entry segment.hypothesesconclusionkeys.take (P.rightEndpoint s) = P.entered sProof (Lean source)
theorem take_rightEndpoint_eq_entered (P : PredicateWindowSchedule keys steps) (s : κ) : keys.take (P.rightEndpoint s) = P.entered s := by change keys.take (keys.takeWhile (P.entryTest s)).length = keys.takeWhile (P.entryTest s) calc _ = (keys.takeWhile (P.entryTest s) ++ keys.dropWhile (P.entryTest s)).take (keys.takeWhile (P.entryTest s)).length := by rw [List.takeWhile_append_dropWhile] _ = _ := List.take_left -
take_leftEndpoint_eq_expiredPrefixtheorem — A predicate schedule has its left prefix exactly equal to the takeWhile segment of entered keys that fail the stay predicate.hypothesesconclusion(keys.take (P.rightEndpoint s)).take (P.leftEndpoint s) = P.expiredPrefix sProof (Lean source)
theorem take_leftEndpoint_eq_expiredPrefix (P : PredicateWindowSchedule keys steps) (s : κ) : (keys.take (P.rightEndpoint s)).take (P.leftEndpoint s) = P.expiredPrefix s := by change (keys.take (P.rightEndpoint s)).take (P.expiredPrefix s).length = P.expiredPrefix s rw [← List.takeWhile_append_dropWhile (p := P.expiredTest s) (l := keys.take (P.rightEndpoint s))] exact List.take_left -
drop_leftEndpoint_eq_dropWhiletheorem — A predicate schedule has the keys between its endpoints exactly equal to dropping the non-staying prefix from the entered prefix.hypothesesProof (Lean source)
theorem drop_leftEndpoint_eq_dropWhile (P : PredicateWindowSchedule keys steps) (s : κ) : (keys.take (P.rightEndpoint s)).drop (P.leftEndpoint s) = (keys.take (P.rightEndpoint s)).dropWhile (P.expiredTest s) := by let l := keys.take (P.rightEndpoint s) change l.drop (l.takeWhile (P.expiredTest s)).length = l.dropWhile (P.expiredTest s) calc _ = (l.takeWhile (P.expiredTest s) ++ l.dropWhile (P.expiredTest s)).drop (l.takeWhile (P.expiredTest s)).length := by rw [List.takeWhile_append_dropWhile] _ = _ := List.drop_left -
active_windowAt_ifftheorem — A predicate schedule, a step, and an in-bounds position satisfy the exact equivalence between position activity and the raw entry-and-stay predicates.hypothesesι :sharedType u_1κ :sharedType u_2P :PredicateWindowSchedule keys stepss :κi :ℕhi :i < keys.lengthconclusionActive (P.windowAt s) i ↔ P.entry s (keys.get ⟨i, hi⟩) ∧ P.stay s (keys.get ⟨i, hi⟩)Proof (Lean source)
theorem active_windowAt_iff (P : PredicateWindowSchedule keys steps) (s : κ) {i : ℕ} (hi : i < keys.length) : Active (P.windowAt s) i ↔ P.entry s (keys.get ⟨i, hi⟩) ∧ P.stay s (keys.get ⟨i, hi⟩) := by constructor · rintro ⟨hli, hir⟩ refine ⟨(P.lt_rightEndpoint_iff_entry s hi).mp hir, ?_⟩ by_contra hstay exact (Nat.not_lt_of_ge hli) ((P.lt_leftEndpoint_iff_not_stay s hir).mpr hstay) · rintro ⟨hentry, hstay⟩ have hir := (P.lt_rightEndpoint_iff_entry s hi).mpr hentry refine ⟨Nat.le_of_not_gt ?_, hir⟩ intro hil exact ((P.lt_leftEndpoint_iff_not_stay s hir).mp hil) hstay -
rightEndpoint_mono_of_entrytheorem — Predicate inclusion from an earlier step to a later step makes right endpoints nondecreasing.hypothesesι :sharedType u_1κ :sharedType u_2P :PredicateWindowSchedule keys stepss t :κhentry :∀ x ∈ keysifP.entry s xthenP.entry t xconclusionP.rightEndpoint s ≤ P.rightEndpoint tProof (Lean source)
theorem rightEndpoint_mono_of_entry (P : PredicateWindowSchedule keys steps) {s t : κ} (hentry : ∀ x ∈ keys, P.entry s x → P.entry t x) : P.rightEndpoint s ≤ P.rightEndpoint t := by by_contra h have hlt : P.rightEndpoint t < P.rightEndpoint s := Nat.lt_of_not_ge h have hi : P.rightEndpoint t < keys.length := lt_of_lt_of_le hlt (P.rightEndpoint_le_length s) have hs := (P.lt_rightEndpoint_iff_entry s hi).mp hlt have ht := hentry _ (List.get_mem keys ⟨P.rightEndpoint t, hi⟩) hs exact (Nat.lt_irrefl _) ((P.lt_rightEndpoint_iff_entry t hi).mpr ht) -
leftEndpoint_mono_of_predicatestheorem — Expanding entry and shrinking stay from one step to another make left endpoints nondecreasing.hypothesesι :sharedType u_1κ :sharedType u_2P :PredicateWindowSchedule keys stepss t :κhentry :∀ x ∈ keysifP.entry s xthenP.entry t xhstay :∀ x ∈ keysifP.stay t xthenP.stay s xconclusionP.leftEndpoint s ≤ P.leftEndpoint tProof (Lean source)
theorem leftEndpoint_mono_of_predicates (P : PredicateWindowSchedule keys steps) {s t : κ} (hentry : ∀ x ∈ keys, P.entry s x → P.entry t x) (hstay : ∀ x ∈ keys, P.stay t x → P.stay s x) : P.leftEndpoint s ≤ P.leftEndpoint t := by by_contra h have hlt : P.leftEndpoint t < P.leftEndpoint s := Nat.lt_of_not_ge h have hright := P.rightEndpoint_mono_of_entry hentry have hirS : P.leftEndpoint t < P.rightEndpoint s := lt_of_lt_of_le hlt (P.leftEndpoint_le_rightEndpoint s) have hirT : P.leftEndpoint t < P.rightEndpoint t := lt_of_lt_of_le hirS hright have hi : P.leftEndpoint t < keys.length := lt_of_lt_of_le hirT (P.rightEndpoint_le_length t) have hnotStayS := (P.lt_leftEndpoint_iff_not_stay s hirS).mp hlt have hstayT : P.stay t (keys.get ⟨P.leftEndpoint t, hi⟩) := by by_contra hn exact (Nat.lt_irrefl _) ((P.lt_leftEndpoint_iff_not_stay t hirT).mpr hn) exact hnotStayS (hstay _ (List.get_mem keys ⟨P.leftEndpoint t, hi⟩) hstayT) -
newlyEntering_eq_drop_enteredtheorem — A predicate schedule, an earlier step, a later step, and entry inclusion have newly entered raw keys exactly equal to the later entered prefix after dropping the earlier right endpoint.hypothesesι :sharedType u_1κ :sharedType u_2P :PredicateWindowSchedule keys stepss t :κhentry :∀ x ∈ keysifP.entry s xthenP.entry t xProof (Lean source)
theorem newlyEntering_eq_drop_entered (P : PredicateWindowSchedule keys steps) (s t : κ) (hentry : ∀ x ∈ keys, P.entry s x → P.entry t x) : (keys.drop (P.rightEndpoint s)).takeWhile (P.entryTest t) = (P.entered t).drop (P.rightEndpoint s) := by exact takeWhile_drop_eq_drop_takeWhile (P.entryTest t) keys (P.rightEndpoint s) (P.rightEndpoint_mono_of_entry hentry) -
rightEndpoint_eq_add_newlyEnteringtheorem — A predicate schedule, an earlier step, a later step, and entry inclusion have later right endpoint equal to the earlier endpoint plus the exact takeWhile entering-segment length.hypothesesι :sharedType u_1κ :sharedType u_2P :PredicateWindowSchedule keys stepss t :κhentry :∀ x ∈ keysifP.entry s xthenP.entry t xProof (Lean source)
theorem rightEndpoint_eq_add_newlyEntering (P : PredicateWindowSchedule keys steps) (s t : κ) (hentry : ∀ x ∈ keys, P.entry s x → P.entry t x) : P.rightEndpoint t = P.rightEndpoint s + ((keys.drop (P.rightEndpoint s)).takeWhile (P.entryTest t)).length := by rw [P.newlyEntering_eq_drop_entered s t hentry, List.length_drop] exact (Nat.add_sub_of_le (P.rightEndpoint_mono_of_entry hentry)).symm -
newlyExpired_eq_takeWhiletheorem — A predicate schedule, an earlier step, a later step, entry expansion, and stay shrinkage have the keys crossing the left endpoint exactly equal to the takeWhile non-staying segment.hypothesesι :sharedType u_1κ :sharedType u_2P :PredicateWindowSchedule keys stepss t :κhentry :∀ x ∈ keysifP.entry s xthenP.entry t xhstay :∀ x ∈ keysifP.stay t xthenP.stay s xProof (Lean source)
theorem newlyExpired_eq_takeWhile (P : PredicateWindowSchedule keys steps) (s t : κ) (hentry : ∀ x ∈ keys, P.entry s x → P.entry t x) (hstay : ∀ x ∈ keys, P.stay t x → P.stay s x) : ((keys.take (P.rightEndpoint t)).drop (P.leftEndpoint s)).take (P.leftEndpoint t - P.leftEndpoint s) = ((keys.take (P.rightEndpoint t)).drop (P.leftEndpoint s)).takeWhile (P.expiredTest t) := by have hmono := P.leftEndpoint_mono_of_predicates hentry hstay let l := keys.take (P.rightEndpoint t) change (l.drop (P.leftEndpoint s)).take (P.leftEndpoint t - P.leftEndpoint s) = (l.drop (P.leftEndpoint s)).takeWhile (P.expiredTest t) calc _ = (l.take (P.leftEndpoint s + (P.leftEndpoint t - P.leftEndpoint s))).drop (P.leftEndpoint s) := List.take_drop _ = (l.take (P.leftEndpoint t)).drop (P.leftEndpoint s) := by rw [Nat.add_sub_of_le hmono] _ = (P.expiredPrefix t).drop (P.leftEndpoint s) := by rw [P.take_leftEndpoint_eq_expiredPrefix t] _ = _ := by symm exact takeWhile_drop_eq_drop_takeWhile (P.expiredTest t) l (P.leftEndpoint s) hmono -
leftEndpoint_eq_add_newlyExpiredtheorem — A predicate schedule, an earlier step, a later step, entry expansion, and stay shrinkage have later left endpoint equal to the earlier endpoint plus the exact takeWhile expiration-segment length.hypothesesι :sharedType u_1κ :sharedType u_2P :PredicateWindowSchedule keys stepss t :κhentry :∀ x ∈ keysifP.entry s xthenP.entry t xhstay :∀ x ∈ keysifP.stay t xthenP.stay s xProof (Lean source)
theorem leftEndpoint_eq_add_newlyExpired (P : PredicateWindowSchedule keys steps) (s t : κ) (hentry : ∀ x ∈ keys, P.entry s x → P.entry t x) (hstay : ∀ x ∈ keys, P.stay t x → P.stay s x) : P.leftEndpoint t = P.leftEndpoint s + (((keys.take (P.rightEndpoint t)).drop (P.leftEndpoint s)).takeWhile (P.expiredTest t)).length := by have hmono := P.leftEndpoint_mono_of_predicates hentry hstay have heq := congrArg length (P.newlyExpired_eq_takeWhile s t hentry hstay) have hbound := P.leftEndpoint_le_rightEndpoint t simp only [List.length_take, List.length_drop] at heq rw [Nat.min_eq_left (P.rightEndpoint_le_length t)] at heq rw [Nat.min_eq_left (Nat.sub_le_sub_right hbound (P.leftEndpoint s))] at heq omega -
schedule_stepstheorem — A predicate schedule compiles to one position window for each raw step.hypothesesconclusionP.schedule.steps = steps.lengthProof (Lean source)
theorem schedule_steps (P : PredicateWindowSchedule keys steps) : P.schedule.steps = steps.length := by simp [schedule, Schedule.steps] -
schedule_window_gettheorem — A predicate schedule and a valid step-list position compile the window at that position to the endpoints of the corresponding raw step.hypothesesι :sharedType u_1κ :sharedType u_2P :PredicateWindowSchedule keys stepsk :ℕhk :k < steps.lengthconclusionP.schedule.windows.get ⟨k, by simpa [schedule, Schedule.steps] using hk⟩= P.windowAt (steps.get ⟨k, hk⟩)Proof (Lean source)
theorem schedule_window_get (P : PredicateWindowSchedule keys steps) {k : ℕ} (hk : k < steps.length) : P.schedule.windows.get ⟨k, by simpa [schedule, Schedule.steps] using hk⟩ = P.windowAt (steps.get ⟨k, hk⟩) := by simp [schedule, List.get_eq_getElem] -
rightEndpoint_le_of_step_lttheorem — A predicate schedule, two valid step positions, and their strict order ensure the earlier compiled right endpoint is no larger.hypothesesι :sharedType u_1κ :sharedType u_2P :PredicateWindowSchedule keys stepsi j :ℕhi :i < steps.lengthhj :j < steps.lengthhij :i < jconclusionP.rightEndpoint (steps.get ⟨i, hi⟩) ≤ P.rightEndpoint (steps.get ⟨j, hj⟩)Proof (Lean source)
theorem rightEndpoint_le_of_step_lt (P : PredicateWindowSchedule keys steps) {i j : ℕ} (hi : i < steps.length) (hj : j < steps.length) (hij : i < j) : P.rightEndpoint (steps.get ⟨i, hi⟩) ≤ P.rightEndpoint (steps.get ⟨j, hj⟩) := by apply P.rightEndpoint_mono_of_entry exact P.entry_step_mono.rel_get_of_lt hij -
leftEndpoint_le_of_step_lttheorem — A predicate schedule, two valid step positions, and their strict order ensure the earlier compiled left endpoint is no larger.hypothesesι :sharedType u_1κ :sharedType u_2P :PredicateWindowSchedule keys stepsi j :ℕhi :i < steps.lengthhj :j < steps.lengthhij :i < jconclusionP.leftEndpoint (steps.get ⟨i, hi⟩) ≤ P.leftEndpoint (steps.get ⟨j, hj⟩)Proof (Lean source)
theorem leftEndpoint_le_of_step_lt (P : PredicateWindowSchedule keys steps) {i j : ℕ} (hi : i < steps.length) (hj : j < steps.length) (hij : i < j) : P.leftEndpoint (steps.get ⟨i, hi⟩) ≤ P.leftEndpoint (steps.get ⟨j, hj⟩) := by apply P.leftEndpoint_mono_of_predicates · exact P.entry_step_mono.rel_get_of_lt hij · exact P.stay_step_anti.rel_get_of_lt hij -
windowAt_emptytheorem — A predicate schedule over an empty raw-key list has both endpoints equal to zero at every step.hypothesesProof (Lean source)
theorem windowAt_empty (P : PredicateWindowSchedule ([] : List ι) steps) (s : κ) : (P.windowAt s).left = 0 ∧ (P.windowAt s).right = 0 := by simp [windowAt, leftEndpoint, rightEndpoint, expiredPrefix, entered]
Accounting 7 core · 11 supporting Exact event lists make the amortized proof explicit. ★ scanCost_le
Trace accounting and linear resource bounds
Exact event lists make the amortized proof explicit. Each pushed stream index is unique, every pop is charged to a prior unique push, the final deque contains the unpopped pushes, and therefore all deque mutations are linear in stream length. Pointwise storage is bounded by window width.
def TracePushed reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A stream and a scan trace determine the aggregate push log.
def TraceFrontPopped reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A stream and a scan trace determine the aggregate front-pop log.
def TraceBackPopped reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A stream and a scan trace determine the aggregate back-pop log.
def dequeOperations reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A stream and a scan trace determine the total number of deque mutations.
Definition (Lean source)
parameters
def
dequeOperations stream trace :
ℕ
given by
(TracePushed stream trace).length
+ (TraceFrontPopped stream trace).length
+ (TraceBackPopped stream trace).length
def scanCost reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A stream and a monotone window schedule determine the scan cost, including one bookkeeping unit per window.
Definition (Lean source)
parameters
def
scanCost stream schedule :
ℕ
given by
schedule.steps + dequeOperations stream (scan stream schedule)
def peakStored reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A stream and a scan trace determine the peak stored deque size.
theorem scanCost_le reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A stream and a monotone window schedule ensure that scan cost is at most twice stream length plus the number of scheduled windows.
Formal statement
Proof (Lean source)
theorem scanCost_le (stream : Stream α) (schedule : Schedule stream.length) :
scanCost stream schedule ≤ 2 * stream.length + schedule.steps := by
have h := dequeOperations_le_two_mul_length stream schedule
unfold scanCost
omega
11 supporting declarations (lemmas, instances)
-
scan_push_count_le_onetheorem — A stream, a monotone window schedule, and an index ensure that the index is pushed at most once in the aggregate scan log.hypothesesconclusionProof (Lean source)
theorem scan_push_count_le_one (stream : Stream α) (schedule : Schedule stream.length) (i : ℕ) : (TracePushed stream (scan stream schedule)).count i ≤ 1 := by apply (List.nodup_iff_count_le_one.mp ?_) i unfold scan apply scanFrom_pushed_nodup stream 0 initialDeque schedule.windows · intro w hw exact zero_le _ · exact schedule.right_mono -
scan_front_pop_count_le_onetheorem — A stream, a monotone window schedule, and an index ensure that the index is front-popped at most once in the aggregate scan log.hypothesesconclusionProof (Lean source)
theorem scan_front_pop_count_le_one (stream : Stream α) (schedule : Schedule stream.length) (i : ℕ) : (TraceFrontPopped stream (scan stream schedule)).count i ≤ 1 := by have hp := scan_push_count_le_one stream schedule i have hc := scan_count_conservation stream schedule i omega -
scan_back_pop_count_le_onetheorem — A stream, a monotone window schedule, and an index ensure that the index is back-popped at most once in the aggregate scan log.hypothesesconclusionProof (Lean source)
theorem scan_back_pop_count_le_one (stream : Stream α) (schedule : Schedule stream.length) (i : ℕ) : (TraceBackPopped stream (scan stream schedule)).count i ≤ 1 := by have hp := scan_push_count_le_one stream schedule i have hc := scan_count_conservation stream schedule i omega -
scan_pop_logs_disjointtheorem — A stream and a monotone window schedule ensure that no index appears in both front-pop and back-pop logs.hypothesesconclusionDisjoint (TraceFrontPopped stream (scan stream schedule)) (TraceBackPopped stream (scan stream schedule))Proof (Lean source)
theorem scan_pop_logs_disjoint (stream : Stream α) (schedule : Schedule stream.length) : Disjoint (TraceFrontPopped stream (scan stream schedule)) (TraceBackPopped stream (scan stream schedule)) := by rw [List.disjoint_iff_ne] intro i hi j hj hij subst j have hfi : 0 < (TraceFrontPopped stream (scan stream schedule)).count i := List.count_pos_iff.mpr hi have hbi : 0 < (TraceBackPopped stream (scan stream schedule)).count i := List.count_pos_iff.mpr hj have hp := scan_push_count_le_one stream schedule i have hc := scan_count_conservation stream schedule i omega -
scan_popped_was_pushedtheorem — A stream, a monotone window schedule, and an index recorded as a front or back pop ensure that the index was previously pushed.hypothesesα :sharedType u_1stream :Stream αschedule :Schedule stream.lengthi :ℕhi :i ∈ TraceFrontPopped stream (scan stream schedule) ∨ i ∈ TraceBackPopped stream (scan stream schedule)conclusioni ∈ TracePushed stream (scan stream schedule)Proof (Lean source)
theorem scan_popped_was_pushed (stream : Stream α) (schedule : Schedule stream.length) {i : ℕ} (hi : i ∈ TraceFrontPopped stream (scan stream schedule) ∨ i ∈ TraceBackPopped stream (scan stream schedule)) : i ∈ TracePushed stream (scan stream schedule) := by apply List.count_pos_iff.mp have hc := scan_count_conservation stream schedule i rcases hi with hi | hi · have : 0 < (TraceFrontPopped stream (scan stream schedule)).count i := List.count_pos_iff.mpr hi omega · have : 0 < (TraceBackPopped stream (scan stream schedule)).count i := List.count_pos_iff.mpr hi omega -
scan_total_pops_le_pushestheorem — A stream and a monotone window schedule ensure that total front and back pops are no more numerous than total pushes.hypothesesconclusionProof (Lean source)
theorem scan_total_pops_le_pushes (stream : Stream α) (schedule : Schedule stream.length) : (TraceFrontPopped stream (scan stream schedule)).length + (TraceBackPopped stream (scan stream schedule)).length ≤ (TracePushed stream (scan stream schedule)).length := by let popped := TraceFrontPopped stream (scan stream schedule) ++ TraceBackPopped stream (scan stream schedule) have hnodup : popped.Nodup := by rw [List.nodup_iff_count_le_one] intro i have hp := scan_push_count_le_one stream schedule i have hc := scan_count_conservation stream schedule i simp only [popped, List.count_append] omega have hsubset : popped ⊆ TracePushed stream (scan stream schedule) := by intro i hi apply scan_popped_was_pushed stream schedule simpa [popped] using hi have hlen := hnodup.length_le_of_subset hsubset simpa [popped] using hlen -
scan_total_pushes_le_lengththeorem — A stream and a monotone window schedule ensure that total pushes are at most the stream length.hypothesesconclusionProof (Lean source)
theorem scan_total_pushes_le_length (stream : Stream α) (schedule : Schedule stream.length) : (TracePushed stream (scan stream schedule)).length ≤ stream.length := by have hnodup : (TracePushed stream (scan stream schedule)).Nodup := by unfold scan apply scanFrom_pushed_nodup stream 0 initialDeque schedule.windows · intro w hw exact Nat.zero_le _ · exact schedule.right_mono have hsubset : TracePushed stream (scan stream schedule) ⊆ List.range stream.length := by intro i hi rw [List.mem_range] exact mem_scanFrom_pushed_lt_length stream 0 initialDeque schedule.windows hi simpa using hnodup.length_le_of_subset hsubset -
dequeOperations_le_two_mul_lengththeorem — A stream and a monotone window schedule ensure that total deque mutations are at most twice the stream length.hypothesesconclusiondequeOperations stream (scan stream schedule) ≤ 2 * stream.lengthProof (Lean source)
theorem dequeOperations_le_two_mul_length (stream : Stream α) (schedule : Schedule stream.length) : dequeOperations stream (scan stream schedule) ≤ 2 * stream.length := by have hpops := scan_total_pops_le_pushes stream schedule have hpush := scan_total_pushes_le_length stream schedule unfold dequeOperations omega -
length_le_windowWidththeorem — A valid bounded-window deque has stored length at most its window width.hypothesesconclusionq.length ≤ window.right - window.leftProof (Lean source)
theorem Valid.length_le_windowWidth {stream : Stream α} {window : Window stream.length} {q : Deque} (hq : Valid stream window q) : q.length ≤ window.right - window.left := by have hn : q.Nodup := ValidAt.nodup hq rw [← List.toFinset_card_of_nodup hn, ← Window.card_indexFinset window] apply Finset.card_le_card intro i hi rw [Window.mem_indexFinset_iff] exact (hq.active i (by simpa using hi)).1 -
scan_memory_le_windowWidththeorem — A stream, a monotone window schedule, and a valid schedule position ensure that the corresponding scan state stores no more indices than its window width.hypothesesα :sharedType u_1stream :Stream αschedule :Schedule stream.lengthk :ℕhk :k < schedule.stepsProof (Lean source)
theorem scan_memory_le_windowWidth (stream : Stream α) (schedule : Schedule stream.length) {k : ℕ} (hk : k < schedule.steps) : ∃ step, (scan stream schedule)[k]? = some step ∧ step.after.length ≤ (schedule.windows.get ⟨k, hk⟩).right - (schedule.windows.get ⟨k, hk⟩).left := by obtain ⟨step, hstep, hwindow, hvalid⟩ := scan_valid_at stream schedule hk refine ⟨step, hstep, ?_⟩ have hlen := Valid.length_le_windowWidth hvalid simpa [hwindow] using hlen -
peakStored_le_lengththeorem — A stream and a monotone window schedule ensure that peak deque storage is at most the stream length.hypothesesconclusionpeakStored stream (scan stream schedule) ≤ stream.lengthProof (Lean source)
theorem peakStored_le_length (stream : Stream α) (schedule : Schedule stream.length) : peakStored stream (scan stream schedule) ≤ stream.length := by unfold peakStored apply foldl_max_le_of_forall _ _ _ (zero_le _) intro n hn simp only [List.mem_map] at hn obtain ⟨step, hstep, rfl⟩ := hn obtain ⟨k, hk, hget⟩ := List.mem_iff_getElem.mp hstep have hk' : k < schedule.steps := by simpa [length_scan stream schedule] using hk obtain ⟨found, hfound, hwindow, hvalid⟩ := scan_valid_at stream schedule hk' have heq : found = step := by apply Option.some.inj rw [← hfound, List.getElem?_eq_getElem hk, hget] subst found have hwidth := Valid.length_le_windowWidth hvalid have hright := step.window.right_le_length omega
PredicateRawScan 16 core · 4 supporting This module gives the raw-key view of a compiled predicate-window scan (a noncomputable specification, since entry and stay are arbitrary predicates decided classically). ★ scan_predicateSchedule_state_eq
Raw-key execution and representation equivalence
This module gives the raw-key view of a compiled predicate-window scan (a noncomputable
specification, since entry and stay are arbitrary predicates decided classically). Pending keys
advance by takeWhile on entry, expired material is removed by dropWhile on stay, and surviving
new keys use the same rightmost-stable monotone back pruning as the position implementation. The
main theorem identifies every mapped position-level trace with this raw-key trace.
def keyedStream reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A raw-key list, a raw-key score, and an out-of-bounds fallback score determine the total position stream used by the generic deque. The fallback is never observed at a valid position.
def positionsToKeys reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A raw-key list and a list of natural positions determine the raw keys obtained by safe lookup of every in-bounds position.
def rawPruneBack reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A raw score, a raw deque, and a new key determine the deque prefix after deleting its suffix of scores no larger than the new score.
Definition (Lean source)
def rawPrunedBack reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A raw score, a raw deque, and a new key determine the keys removed from the back by the deterministic rightmost-stable tie policy.
Definition (Lean source)
def rawPush reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A raw score, a raw deque, and a new key determine one rightmost-stable monotone push; equal old scores are removed in favor of the new key.
Definition (Lean source)
structure RawPushBatch reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A raw-key type determines a batch record with the final key deque, the pushed keys, and the keys removed from the back.
def rawPushAll reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A raw score, together with an initial raw deque and a list of input keys, determines the recorded batch of rightmost-stable pushes, given by leaving an empty input list unchanged and pushing the first key before recursing on the remainder.
Definition (Lean source)
parameters
def
given by
clause 1
| q, [] => { state := q, pushed := [], backPopped := [] }
clause 2
| q, x :: xs
=> let removed := rawPrunedBack score q x let rest := rawPushAll score (rawPush score q x) xs { state := rest.state pushed := x :: rest.pushed backPopped := removed ++ rest.backPopped }
structure RawState reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A raw-key type determines a predicate-scan state with the unentered suffix and the current raw-key deque.
structure RawDequeTrace reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A raw-key type determines a deque-update trace with the deque before updating, the deque after expiration, the final deque, the pushed keys, the front-popped keys, and the back-popped keys.
structure RawStepTrace reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A raw-key type and a step type determine a predicate-scan step record that extends a deque update with the current step, the pending suffix before updating, the pending suffix afterward, and the complete entered prefix before expiration filtering.
Definition (Lean source)
parameters
ι κ :
Type*
extends :
def dequeTrace reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque.RawStepTrace
A raw predicate step trace determines its exact generic-shaped deque trace.
Definition (Lean source)
parameters
def
given by
trace.toRawDequeTrace
def rawUpdate reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque.PredicateWindowSchedule
A predicate schedule, a raw score, a step, and a raw state determine the next recorded raw-key update. It advances entry by takeWhile, removes the non-staying prefixes by dropWhile, and pushes precisely the surviving new suffix.
Definition (Lean source)
parameters
ι :
Type u_1
κ :
Type u_2
α :
Type u_3
P :
PredicateWindowSchedule keys steps
score :
ι → α
s :
κ
state :
RawState ι
def
given by
by let advanced := state.pending.takeWhile (P.entryTest s) let pending := state.pending.dropWhile (P.entryTest s) let afterExpiration := state.deque.dropWhile (P.expiredTest s) let frontPopped := state.deque.takeWhile (P.expiredTest s) let survivingNew := advanced.dropWhile (P.expiredTest s) let batch := rawPushAll score afterExpiration survivingNew exact { step := s beforePending := state.pending pending := pending advanced := advanced before := state.deque afterExpiration := afterExpiration after := batch.state pushed := batch.pushed frontPopped := frontPopped backPopped := batch.backPopped }
def rawScanFrom reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque.PredicateWindowSchedule
A predicate schedule and a raw score determine the raw trace obtained by folding over a supplied suffix of steps from a supplied state.
Definition (Lean source)
parameters
ι :
Type u_1
κ :
Type u_2
α :
Type u_3
P :
PredicateWindowSchedule keys steps
score :
ι → α
def
def rawScan reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque.PredicateWindowSchedule
A predicate schedule and a raw score determine the complete raw-key scan from all keys pending and an empty deque.
Definition (Lean source)
parameters
ι :
Type u_1
κ :
Type u_2
α :
Type u_3
P :
PredicateWindowSchedule keys steps
score :
ι → α
def
given by
P.rawScanFrom score { pending := keys, deque := [] } steps
def mapStepTrace reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A raw-key list maps one generic position-level step to the exact raw-key deque trace by safe lookup in every list-valued field.
Definition (Lean source)
parameters
def
given by
{ before := positionsToKeys keys trace.before afterExpiration := positionsToKeys keys trace.afterExpiration after := positionsToKeys keys trace.after pushed := positionsToKeys keys trace.pushed frontPopped := positionsToKeys keys trace.frontPopped backPopped := positionsToKeys keys trace.backPopped }
theorem scan_predicateSchedule_state_eq reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A predicate schedule, a raw-key score, and a fallback score have the generic position scan mapped through raw-key lookup exactly equal to the corresponding raw-key predicate scan, including every deque state and push/pop log.
Formal statement
hypotheses
ι :
Type u_1
κ :
Type u_2
α :
Type u_3
P :
PredicateWindowSchedule keys steps
score :
ι → α
fallback :
α
conclusion
= (P.rawScan score).map RawStepTrace.dequeTrace
Proof (Lean source)
theorem scan_predicateSchedule_state_eq [LinearOrder α]
(P : PredicateWindowSchedule keys steps) (score : ι → α) (fallback : α) :
(scan (keyedStream keys score fallback) P.schedule).map (mapStepTrace keys) =
(P.rawScan score).map RawStepTrace.dequeTrace := by
have hpair : steps.Pairwise
(fun s t => P.rightEndpoint s ≤ P.rightEndpoint t) :=
P.entry_step_mono.imp (fun h => P.rightEndpoint_mono_of_entry h)
have hbridge := scanFrom_bridge P score fallback steps hpair 0 []
(by simp) (by simp)
change (scanFrom (keyedStream keys score fallback) 0 initialDeque
(steps.map P.windowAt)).map (mapStepTrace keys) =
(P.rawScanFrom score { pending := keys, deque := [] } steps).map
RawStepTrace.dequeTrace
simpa [initialDeque, positionsToKeys] using hbridge
4 supporting declarations (lemmas, instances)
-
rawPush_getLast?_eqtheorem — One raw rightmost-stable push has the newly pushed key as its final element, including when all old entries tie with it.hypothesesProof (Lean source)
theorem rawPush_getLast?_eq [LinearOrder α] (score : ι → α) (q : List ι) (x : ι) : (rawPush score q x).getLast? = some x := by simp [rawPush] -
rawPrunedBack_score_letheorem — A key removed by rightmost-stable back pruning has score no larger than the newly pushed key, so equal-score ties deterministically favor the newer occurrence.hypothesesconclusionscore y ≤ score xProof (Lean source)
theorem rawPrunedBack_score_le [LinearOrder α] (score : ι → α) (q : List ι) (x y : ι) (hy : y ∈ rawPrunedBack score q x) : score y ≤ score x := by have h := List.mem_rtakeWhile_imp hy simpa [rawPrunedBack] using h -
length_rawScantheorem — A predicate schedule and a raw score produce one raw trace entry per step.hypothesesι :sharedType u_1κ :sharedType u_2α :sharedType u_3P :PredicateWindowSchedule keys stepsscore :ι → αconclusion(P.rawScan score).length = steps.lengthProof (Lean source)
theorem PredicateWindowSchedule.length_rawScan [LinearOrder α] (P : PredicateWindowSchedule keys steps) (score : ι → α) : (P.rawScan score).length = steps.length := by have hlength : ∀ (state : RawState ι) (ss : List κ), (P.rawScanFrom score state ss).length = ss.length := by intro state ss induction ss generalizing state with | nil => rfl | cons s ss ih => simp only [rawScanFrom, List.length_cons] rw [ih] exact hlength { pending := keys, deque := [] } steps -
scan_predicateSchedule_after_eqtheorem — A predicate schedule, a raw score, a valid step position, and a fallback score have the generic deque after that step mapped through key lookup equal to the raw predicate-scan deque.hypothesesι :sharedType u_1κ :sharedType u_2α :sharedType u_3P :PredicateWindowSchedule keys stepsscore :ι → αfallback :αk :ℕhk :k < steps.lengthconclusion∃ generic raw,conclusion 1(scan (keyedStream keys score fallback) P.schedule)[k]? = some genericconclusion 2(P.rawScan score)[k]? = some rawconclusion 3positionsToKeys keys generic.after = raw.afterProof (Lean source)
theorem scan_predicateSchedule_after_eq [LinearOrder α] (P : PredicateWindowSchedule keys steps) (score : ι → α) (fallback : α) {k : ℕ} (hk : k < steps.length) : ∃ generic raw, (scan (keyedStream keys score fallback) P.schedule)[k]? = some generic ∧ (P.rawScan score)[k]? = some raw ∧ positionsToKeys keys generic.after = raw.after := by let genericTrace := scan (keyedStream keys score fallback) P.schedule let rawTrace := P.rawScan score have hGenericLength : genericTrace.length = steps.length := by rw [show genericTrace.length = P.schedule.steps by exact length_scan (keyedStream keys score fallback) P.schedule] exact P.schedule_steps have hRawLength : rawTrace.length = steps.length := by exact P.length_rawScan score have hgk : k < genericTrace.length := by simpa [hGenericLength] using hk have hrk : k < rawTrace.length := by simpa [hRawLength] using hk let generic := genericTrace.get ⟨k, hgk⟩ let raw := rawTrace.get ⟨k, hrk⟩ refine ⟨generic, raw, ?_, ?_, ?_⟩ · exact List.getElem?_eq_getElem hgk · exact List.getElem?_eq_getElem hrk · have heq := congrArg (fun xs => xs[k]?) (scan_predicateSchedule_state_eq P score fallback) change (genericTrace.map (mapStepTrace keys))[k]? = (rawTrace.map RawStepTrace.dequeTrace)[k]? at heq simp only [List.getElem?_map, List.getElem?_eq_getElem hgk, List.getElem?_eq_getElem hrk, Option.map_some, Option.some.injEq] at heq exact congrArg RawDequeTrace.after heq
Passes 4 core · 2 supporting This module packages a constant number of independent schedules over the same finite stream. ★ totalCost_le
Fixed finite families of monotone-window passes
This module packages a constant number of independent schedules over the same finite stream. It exports per-pass correctness and the sum of the linear per-pass cost bounds, which is the interface needed by algorithms that run a fixed collection of monotone scans.
structure FixedPasses reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A stream and a finite pass count have a family of monotone-window schedules, one for each pass.
def totalCost reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque.FixedPasses
A fixed family of passes determines the sum of its individual scan costs.
Definition (Lean source)
def totalSteps reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque.FixedPasses
A fixed family of passes determines its total number of scheduled windows.
Definition (Lean source)
theorem totalCost_le reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque.FixedPasses
A fixed family of passes ensures that its total cost is at most twice the pass count times stream length plus its total scheduled-window count.
Formal statement
hypotheses
conclusion
family.totalCost ≤ 2 * passes * stream.length + family.totalSteps
Proof (Lean source)
theorem FixedPasses.totalCost_le {stream : Stream α} {passes : ℕ}
(family : FixedPasses stream passes) :
family.totalCost ≤ 2 * passes * stream.length + family.totalSteps := by
unfold FixedPasses.totalCost FixedPasses.totalSteps
calc
∑ p, scanCost stream (family.schedule p) ≤
∑ p, (2 * stream.length + (family.schedule p).steps) := by
classical
induction (Finset.univ : Finset (Fin passes)) using Finset.induction_on with
| empty => simp
| @insert p s hp ih =>
simp only [Finset.sum_insert hp]
exact Nat.add_le_add (scanCost_le stream (family.schedule p)) ih
_ = 2 * passes * stream.length + ∑ p, (family.schedule p).steps := by
simp [Finset.sum_add_distrib, Nat.mul_comm, Nat.mul_left_comm]
2 supporting declarations (lemmas, instances)
-
head_value_eq_windowMaxtheorem — A fixed family of passes, a selected pass, a valid position in that pass, and a nonempty window there ensure that the scan head is an active argmax with the finite-window maximum value.hypothesespasses :ℕfamily :FixedPasses stream passesp :Fin passesk :ℕhk :k < (family.schedule p).stepshne :((family.schedule p).windows.get ⟨k, hk⟩).left < ((family.schedule p).windows.get ⟨k, hk⟩).rightconclusion∃ step head tail,Proof (Lean source)
theorem FixedPasses.head_value_eq_windowMax {stream : Stream α} {passes : ℕ} (family : FixedPasses stream passes) (p : Fin passes) {k : ℕ} (hk : k < (family.schedule p).steps) (hne : ((family.schedule p).windows.get ⟨k, hk⟩).left < ((family.schedule p).windows.get ⟨k, hk⟩).right) : ∃ step head tail, (scan stream (family.schedule p))[k]? = some step ∧ step.window = (family.schedule p).windows.get ⟨k, hk⟩ ∧ step.after = head :: tail ∧ Active step.window head ∧ stream.value head = windowMax stream ((family.schedule p).windows.get ⟨k, hk⟩) hne ∧ ∀ i, Active step.window i → stream.value i ≤ stream.value head := by exact scan_head_value_eq_windowMax stream (family.schedule p) hk hne -
memory_le_windowWidththeorem — A fixed family of passes, a selected pass, and a valid position in that pass ensure that the corresponding state stores no more than its window width.hypothesespasses :ℕfamily :FixedPasses stream passesp :Fin passesk :ℕhk :k < (family.schedule p).stepsProof (Lean source)
theorem FixedPasses.memory_le_windowWidth {stream : Stream α} {passes : ℕ} (family : FixedPasses stream passes) (p : Fin passes) {k : ℕ} (hk : k < (family.schedule p).steps) : ∃ step, (scan stream (family.schedule p))[k]? = some step ∧ step.after.length ≤ ((family.schedule p).windows.get ⟨k, hk⟩).right - ((family.schedule p).windows.get ⟨k, hk⟩).left := by exact scan_memory_le_windowWidth stream (family.schedule p) hk
PredicateAccounting 9 core · 6 supporting This module transfers the generic monotone-window deque's head-argmax, amortized operation count, and peak-storage results to predicate scans on sparse raw keys. ★ rawScan_head_argmax
Correctness and resource bounds for compiled raw-key scans
This module transfers the generic monotone-window deque's head-argmax, amortized operation count, and peak-storage results to predicate scans on sparse raw keys. It also packages a fixed finite family of such scans, providing the constant-number-of-passes interface used by consumers.
def rawTracePushed reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A raw predicate-scan trace determines the aggregate list of pushed raw keys.
Definition (Lean source)
parameters
def
given by
trace.flatMap (fun step => step.pushed)
def rawTraceFrontPopped reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A raw predicate-scan trace determines the aggregate list of front-popped raw keys.
Definition (Lean source)
parameters
def
given by
trace.flatMap (fun step => step.frontPopped)
def rawTraceBackPopped reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A raw predicate-scan trace determines the aggregate list of back-popped raw keys.
Definition (Lean source)
parameters
def
given by
trace.flatMap (fun step => step.backPopped)
def rawDequeOperations reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A raw predicate-scan trace determines its exact number of deque mutations.
Definition (Lean source)
parameters
def
rawDequeOperations trace :
ℕ
given by
(rawTracePushed trace).length
+ (rawTraceFrontPopped trace).length
+ (rawTraceBackPopped trace).length
def rawScanCost reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque.PredicateWindowSchedule
A predicate schedule and a raw score determine the raw scan cost, including one bookkeeping unit per step.
Definition (Lean source)
parameters
ι :
Type u_1
κ :
Type u_2
α :
Type u_3
P :
PredicateWindowSchedule keys steps
score :
ι → α
def
rawScanCost P score :
ℕ
given by
steps.length + rawDequeOperations (P.rawScan score)
def rawPeakStored reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A raw predicate-scan trace determines the largest raw deque length reached.
Definition (Lean source)
parameters
def
rawPeakStored trace :
ℕ
given by
(trace.map (fun step => step.after.length)).foldl max 0
theorem rawScan_head_argmax reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A predicate schedule, a raw score, a fallback score, a valid step position, and a nonempty raw predicate window ensure the raw deque head is an active score maximizer, with equal maxima resolved at the greatest key position.
Formal statement
hypotheses
ι :
Type u_1
κ :
Type u_2
α :
Type u_3
P :
PredicateWindowSchedule keys steps
score :
ι → α
fallback :
α
k :
ℕ
hk :
k < steps.length
hne :
∃ i : Fin keys.length,
P.entry (steps.get ⟨k, hk⟩) (keys.get i) ∧ P.stay (steps.get ⟨k, hk⟩) (keys.get i)
conclusion
(P.rawScan score)[k]? = some trace
trace.step = steps.get ⟨k, hk⟩
trace.after = head :: tail
head = keys.get headPos
P.entry (steps.get ⟨k, hk⟩) head
P.stay (steps.get ⟨k, hk⟩) head
conclusion 1
i :
Fin keys.length
P.entry (steps.get ⟨k, hk⟩) (keys.get i)
P.stay (steps.get ⟨k, hk⟩) (keys.get i)
score (keys.get i) ≤ score head
conclusion 2
i :
Fin keys.length
P.entry (steps.get ⟨k, hk⟩) (keys.get i)
P.stay (steps.get ⟨k, hk⟩) (keys.get i)
score (keys.get i) = score head
i.1 ≤ headPos.1
Proof (Lean source)
theorem rawScan_head_argmax [LinearOrder α]
(P : PredicateWindowSchedule keys steps) (score : ι → α) (fallback : α)
{k : ℕ} (hk : k < steps.length)
(hne : ∃ i : Fin keys.length,
P.entry (steps.get ⟨k, hk⟩) (keys.get i) ∧
P.stay (steps.get ⟨k, hk⟩) (keys.get i)) :
∃ (trace : RawStepTrace ι κ) (head : ι) (tail : List ι)
(headPos : Fin keys.length),
(P.rawScan score)[k]? = some trace ∧
trace.step = steps.get ⟨k, hk⟩ ∧
trace.after = head :: tail ∧
head = keys.get headPos ∧
P.entry (steps.get ⟨k, hk⟩) head ∧
P.stay (steps.get ⟨k, hk⟩) head ∧
(∀ i : Fin keys.length,
P.entry (steps.get ⟨k, hk⟩) (keys.get i) →
P.stay (steps.get ⟨k, hk⟩) (keys.get i) →
score (keys.get i) ≤ score head) ∧
(∀ i : Fin keys.length,
P.entry (steps.get ⟨k, hk⟩) (keys.get i) →
P.stay (steps.get ⟨k, hk⟩) (keys.get i) →
score (keys.get i) = score head → i.1 ≤ headPos.1) := by
let stream := keyedStream keys score fallback
have hks : k < P.schedule.steps := by simpa [P.schedule_steps] using hk
have hwindowNonempty :
(P.schedule.windows.get ⟨k, hks⟩).left <
(P.schedule.windows.get ⟨k, hks⟩).right := by
obtain ⟨i, hentry, hstay⟩ := hne
have hactive := (P.active_schedule_iff hk i.isLt).mpr ⟨hentry, hstay⟩
exact lt_of_le_of_lt hactive.1 hactive.2
obtain ⟨generic, headIndex, posTail, hgeneric, hwindow, hposAfter,
hheadActive, hmax⟩ :=
scan_head_argmax stream P.schedule hks hwindowNonempty
obtain ⟨validTrace, hvalidTrace, hvalidWindow, hvalid⟩ :=
scan_valid_at stream P.schedule hks
have hvg : validTrace = generic :=
Option.some.inj (hvalidTrace.symm.trans hgeneric)
subst validTrace
rw [hwindow] at hvalid
rw [hwindow] at hheadActive hmax
obtain ⟨bridgeGeneric, raw, hbridgeGeneric, hraw, hmapAfter⟩ :=
scan_predicateSchedule_after_eq P score fallback hk
have hbg : bridgeGeneric = generic :=
Option.some.inj (hbridgeGeneric.symm.trans hgeneric)
subst bridgeGeneric
have hheadBound : headIndex < keys.length := by
exact lt_of_lt_of_le hheadActive.2
(P.schedule.windows.get ⟨k, hks⟩).right_le_length
let headPos : Fin keys.length := ⟨headIndex, hheadBound⟩
let rawTail := positionsToKeys keys posTail
have hrawAfter : raw.after = keys.get headPos :: rawTail := by
rw [← hmapAfter, hposAfter]
simp [positionsToKeys, headPos, rawTail, List.getElem?_eq_getElem hheadBound]
obtain ⟨rawAt, hrawAt, hrawStep⟩ :=
rawScanFrom_get_step P score { pending := keys, deque := [] } steps hk
have hrawEq : rawAt = raw := by
exact Option.some.inj (hrawAt.symm.trans hraw)
subst rawAt
have hheadPred :
P.entry (steps.get ⟨k, hk⟩) (keys.get headPos) ∧
P.stay (steps.get ⟨k, hk⟩) (keys.get headPos) := by
exact (P.active_schedule_iff hk hheadBound).mp hheadActive
have hstreamValue (i : Fin keys.length) : stream.value i.1 = score (keys.get i) := by
simp [stream, keyedStream]
have hretainedEqHead : ∀ j ∈ generic.after,
stream.value j = stream.value headIndex → j = headIndex := by
intro j hj heq
rw [hposAfter] at hj
rcases List.mem_cons.mp hj with rfl | hj
· rfl
· have hdec := hvalid.value_decreasing
rw [hposAfter] at hdec
have hlt := (List.pairwise_cons.mp hdec).1 j hj
exfalso
exact (ne_of_lt hlt) heq
refine ⟨raw, keys.get headPos, rawTail, headPos, hraw, hrawStep,
hrawAfter, rfl, hheadPred.1, hheadPred.2, ?_, ?_⟩
· intro i hentry hstay
have hactive := (P.active_schedule_iff hk i.isLt).mpr ⟨hentry, hstay⟩
have hv := hmax i.1 hactive
calc
score (keys.get i) = stream.value i.1 := (hstreamValue i).symm
_ ≤ stream.value headIndex := hv
_ = score (keys.get headPos) := hstreamValue headPos
· intro i hentry hstay heq
have hactive := (P.active_schedule_iff hk i.isLt).mpr ⟨hentry, hstay⟩
have hvalueEq : stream.value i.1 = stream.value headIndex := by
calc
stream.value i.1 = score (keys.get i) := hstreamValue i
_ = score (keys.get headPos) := heq
_ = stream.value headIndex := (hstreamValue headPos).symm
by_cases hiq : i.1 ∈ generic.after
· have := hretainedEqHead i.1 hiq hvalueEq
simpa [headPos] using Nat.le_of_eq this
· obtain ⟨j, hjq, hij, hvalue⟩ :=
hvalid.dominates_omitted i.1 hactive i.isLt hiq
have hjactive := (hvalid.active j hjq).1
have hjle := hmax j hjactive
have hjEq : stream.value j = stream.value headIndex := by
exact le_antisymm hjle (by simpa [hvalueEq] using hvalue)
have hjHead := hretainedEqHead j hjq hjEq
subst j
simpa [headPos] using le_of_lt hij
structure PredicatePasses reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque
A raw-key list, a step list, and a finite pass count determine a pass family with one predicate-window schedule per pass.
Definition (Lean source)
parameters
fields
pass :
Fin passes → PredicateWindowSchedule keys steps
def totalRawCost reviewed
⚑ flagged
Causalean.Mathlib.Algorithms.MonotoneWindowDeque.PredicatePasses
A fixed predicate-pass family and a raw score determine the sum of the raw costs of all passes.
Definition (Lean source)
parameters
ι :
Type u_1
κ :
Type u_2
α :
Type u_3
passes :
ℕ
family :
PredicatePasses keys steps passes
score :
ι → α
def
totalRawCost family score :
ℕ
given by
∑ p, (family.pass p).rawScanCost score
6 supporting declarations (lemmas, instances)
-
rawScanCost_eq_scanCosttheorem — A predicate schedule, a raw score, and a fallback score have raw operation cost exactly equal to the generic compiled position-scan cost.hypothesesι :sharedType u_1κ :sharedType u_2α :sharedType u_3P :PredicateWindowSchedule keys stepsscore :ι → αfallback :αconclusionP.rawScanCost score = scanCost (keyedStream keys score fallback) P.scheduleProof (Lean source)
theorem rawScanCost_eq_scanCost [LinearOrder α] (P : PredicateWindowSchedule keys steps) (score : ι → α) (fallback : α) : P.rawScanCost score = scanCost (keyedStream keys score fallback) P.schedule := by let stream := keyedStream keys score fallback let generic := scan stream P.schedule let raw := P.rawScan score have hmap : generic.map (mapStepTrace keys) = raw.map RawStepTrace.dequeTrace := scan_predicateSchedule_state_eq P score fallback have hfields : ∀ trace ∈ generic, (∀ i ∈ trace.pushed, i < keys.length) ∧ (∀ i ∈ trace.frontPopped, i < keys.length) ∧ (∀ i ∈ trace.backPopped, i < keys.length) := by intro trace htrace have h := scan_fields_bound stream P.schedule trace htrace exact ⟨h.2.2.2.1, h.2.2.2.2.1, h.2.2.2.2.2⟩ have hpushed := positionsToKeys_flatMap_length_eq keys generic StepTrace.pushed (fun trace htrace => (hfields trace htrace).1) have hfront := positionsToKeys_flatMap_length_eq keys generic StepTrace.frontPopped (fun trace htrace => (hfields trace htrace).2.1) have hback := positionsToKeys_flatMap_length_eq keys generic StepTrace.backPopped (fun trace htrace => (hfields trace htrace).2.2) have hoperations := congrArg (fun ts : List (RawDequeTrace ι) => (ts.flatMap RawDequeTrace.pushed).length + (ts.flatMap RawDequeTrace.frontPopped).length + (ts.flatMap RawDequeTrace.backPopped).length) hmap simp only [List.flatMap_map, mapStepTrace, RawStepTrace.dequeTrace] at hoperations rw [hpushed, hfront, hback] at hoperations have hop : dequeOperations stream generic = rawDequeOperations raw := by simpa [dequeOperations, TracePushed, TraceFrontPopped, TraceBackPopped, rawDequeOperations, rawTracePushed, rawTraceFrontPopped, rawTraceBackPopped] using hoperations unfold PredicateWindowSchedule.rawScanCost scanCost have hs : P.schedule.steps = steps.length := P.schedule_steps change steps.length + rawDequeOperations raw = P.schedule.steps + dequeOperations stream generic omega -
rawPeakStored_eq_peakStoredtheorem — A predicate schedule, a raw score, and a fallback score have raw peak storage exactly equal to generic compiled position-scan peak storage.hypothesesι :sharedType u_1κ :sharedType u_2α :sharedType u_3P :PredicateWindowSchedule keys stepsscore :ι → αfallback :αconclusionrawPeakStored (P.rawScan score)Proof (Lean source)
theorem rawPeakStored_eq_peakStored [LinearOrder α] (P : PredicateWindowSchedule keys steps) (score : ι → α) (fallback : α) : rawPeakStored (P.rawScan score) = peakStored (keyedStream keys score fallback) (scan (keyedStream keys score fallback) P.schedule) := by let stream := keyedStream keys score fallback let generic := scan stream P.schedule let raw := P.rawScan score have hmap : generic.map (mapStepTrace keys) = raw.map RawStepTrace.dequeTrace := scan_predicateSchedule_state_eq P score fallback have hlength : ∀ trace ∈ generic, (positionsToKeys keys trace.after).length = trace.after.length := by intro trace htrace exact positionsToKeys_length_eq keys trace.after (scan_fields_bound stream P.schedule trace htrace).2.2.1 have hafter := congrArg (fun ts : List (RawDequeTrace ι) => (ts.map (fun trace => trace.after.length)).foldl max 0) hmap simp only [List.map_map] at hafter change (generic.map (fun trace => (positionsToKeys keys trace.after).length)).foldl max 0 = (raw.map (fun trace => trace.after.length)).foldl max 0 at hafter have hmapped : generic.map (fun trace => (positionsToKeys keys trace.after).length) = generic.map (fun trace => trace.after.length) := by apply List.map_congr_left intro trace htrace exact hlength trace htrace rw [hmapped] at hafter simpa [rawPeakStored, peakStored, generic, raw, stream] using hafter.symm -
rawScanCost_letheorem — A predicate schedule, a raw score, and a fallback score ensure raw scan cost is at most twice the number of sparse keys plus the number of steps.hypothesesι :sharedType u_1κ :sharedType u_2α :sharedType u_3P :PredicateWindowSchedule keys stepsscore :ι → αfallback :αconclusionP.rawScanCost score ≤ 2 * keys.length + steps.lengthProof (Lean source)
theorem rawScanCost_le [LinearOrder α] (P : PredicateWindowSchedule keys steps) (score : ι → α) (fallback : α) : P.rawScanCost score ≤ 2 * keys.length + steps.length := by rw [rawScanCost_eq_scanCost P score fallback] simpa [keyedStream, P.schedule_steps] using scanCost_le (keyedStream keys score fallback) P.schedule -
rawPeakStored_le_lengththeorem — A predicate schedule, a raw score, and a fallback score ensure raw peak deque storage is at most the number of sparse keys.hypothesesι :sharedType u_1κ :sharedType u_2α :sharedType u_3P :PredicateWindowSchedule keys stepsscore :ι → αfallback :αconclusionrawPeakStored (P.rawScan score) ≤ keys.lengthProof (Lean source)
theorem rawPeakStored_le_length [LinearOrder α] (P : PredicateWindowSchedule keys steps) (score : ι → α) (fallback : α) : rawPeakStored (P.rawScan score) ≤ keys.length := by rw [rawPeakStored_eq_peakStored P score fallback] simpa [keyedStream] using peakStored_le_length (keyedStream keys score fallback) P.schedule -
rawScan_memory_le_windowWidththeorem — A predicate schedule, a raw score, a fallback score, and a valid step position ensure the raw deque stored there is no wider than its compiled window.hypothesesι :sharedType u_1κ :sharedType u_2α :sharedType u_3P :PredicateWindowSchedule keys stepsscore :ι → αfallback :αk :ℕhk :k < steps.lengthProof (Lean source)
theorem rawScan_memory_le_windowWidth [LinearOrder α] (P : PredicateWindowSchedule keys steps) (score : ι → α) (fallback : α) {k : ℕ} (hk : k < steps.length) : ∃ trace, (P.rawScan score)[k]? = some trace ∧ trace.after.length ≤ P.rightEndpoint (steps.get ⟨k, hk⟩) - P.leftEndpoint (steps.get ⟨k, hk⟩) := by have hks : k < P.schedule.steps := by simpa [P.schedule_steps] using hk obtain ⟨generic, raw, hgeneric, hraw, hafter⟩ := scan_predicateSchedule_after_eq P score fallback hk obtain ⟨found, hfound, hlen⟩ := scan_memory_le_windowWidth (keyedStream keys score fallback) P.schedule hks have hfoundEq : found = generic := by exact Option.some.inj (hfound.symm.trans hgeneric) subst found refine ⟨raw, hraw, ?_⟩ have hgenericMem : generic ∈ scan (keyedStream keys score fallback) P.schedule := by rcases List.getElem?_eq_some_iff.mp hgeneric with ⟨hkg, heq⟩ exact List.mem_iff_getElem.mpr ⟨k, hkg, heq⟩ have hbound := (scan_fields_bound (keyedStream keys score fallback) P.schedule generic hgenericMem).2.2.1 have hmapLength := positionsToKeys_length_eq keys generic.after hbound rw [← hafter, hmapLength] have hwindow := P.schedule_window_get hk have hget : P.schedule.windows.get ⟨k, hks⟩ = P.windowAt (steps.get ⟨k, hk⟩) := by convert hwindow using 1 calc generic.after.length ≤ (P.schedule.windows.get ⟨k, hks⟩).right - (P.schedule.windows.get ⟨k, hks⟩).left := hlen _ = P.rightEndpoint (steps.get ⟨k, hk⟩) - P.leftEndpoint (steps.get ⟨k, hk⟩) := by rw [hget] rfl -
totalRawCost_letheorem — A fixed predicate-pass family, a raw score, and a fallback score ensure total raw cost is at most twice pass count times key count plus pass count times step count.hypothesesι :sharedType u_1κ :sharedType u_2α :sharedType u_3passes :ℕfamily :PredicatePasses keys steps passesscore :ι → αfallback :αconclusionfamily.totalRawCost score ≤ 2 * passes * keys.length + passes * steps.lengthProof (Lean source)
theorem PredicatePasses.totalRawCost_le [LinearOrder α] {passes : ℕ} (family : PredicatePasses keys steps passes) (score : ι → α) (fallback : α) : family.totalRawCost score ≤ 2 * passes * keys.length + passes * steps.length := by unfold PredicatePasses.totalRawCost calc ∑ p, (family.pass p).rawScanCost score ≤ ∑ _p : Fin passes, (2 * keys.length + steps.length) := by apply Finset.sum_le_sum intro p hp exact rawScanCost_le (family.pass p) score fallback _ = 2 * passes * keys.length + passes * steps.length := by simp [Nat.mul_add, Nat.mul_left_comm, Nat.mul_comm]