Core Lean proof of the exact shared-left neighbor rule
capacity
Proves the exact distinct-priority list target. Ordered find helpers characterize minimal/maximal matching positions. A larger priority to the right cannot share the earlier position's nearest-left parent. Case analysis on the nearest right and left neighbors establishes either the next group member or the left-parent boundary. No native correspondence, efficiency or novelty claim. Separate local specification fixed by an adversarial evaluator; self-contained port also requires pinned validation.
Lean proof and verification output
by
let priorityAt : List Nat → Nat → Nat := fun a i => (a[i]?).getD 0
let nearestLeft : List Nat → Nat → Option Nat := fun a i => (List.range i).reverse.find? (fun j => decide (priorityAt a j < priorityAt a i))
let nearestRight : List Nat → Nat → Option Nat := fun a i => (List.range a.length).find? (fun j => decide (i < j ∧ priorityAt a j < priorityAt a i))
let nextSameLeft : List Nat → Nat → Option Nat := fun a i => (List.range a.length).find? (fun j => decide (i < j ∧ nearestLeft a j = nearestLeft a i))
let groupRight : List Nat → Nat → Option Nat := fun a i => match nextSameLeft a i with | some j => some j | none => (nearestLeft a i).bind (nearestRight a)
have find_min_spec (p : Nat → Bool) (xs : List Nat)
(hs : xs.Pairwise (· ≤ ·)) (b : Nat) :
xs.find? p = some b ↔ b ∈ xs ∧ p b = true ∧ ∀ a ∈ xs, a < b → p a = false := by
induction xs with
| nil => simp
| cons x xs ih =>
have htail := hs.of_cons
have hrel := (List.pairwise_cons.mp hs).1
by_cases hx : p x = true
· simp only [List.find?_cons_of_pos hx, Option.some.injEq]
constructor
· intro he; subst b
refine ⟨List.mem_cons_self, hx, ?_⟩
intro a ha hab
rcases List.mem_cons.mp ha with rfl | ha
· omega
· have := hrel a ha; omega
· rintro ⟨hb, hp, hn⟩
rcases List.mem_cons.mp hb with rfl | hb
· rfl
· have he := hrel b hb
by_cases hxb : x = b
· exact hxb
· have := hn x List.mem_cons_self (by omega)
simp [hx] at this
· have hf : p x = false := by cases h : p x <;> simp_all
rw [List.find?_cons_of_neg (by simpa using hx), ih htail]
constructor
· rintro ⟨hb,hp,hn⟩
refine ⟨List.mem_cons_of_mem x hb,hp,?_⟩
intro a ha hab
rcases List.mem_cons.mp ha with rfl | ha
· exact hf
· exact hn a ha hab
· rintro ⟨hb,hp,hn⟩
have hb' : b ∈ xs := by
rcases List.mem_cons.mp hb with rfl | hb
· simp [hf] at hp
· exact hb
exact ⟨hb',hp,fun a ha hab => hn a (List.mem_cons_of_mem x ha) hab⟩
have find_max_spec (p : Nat → Bool) (xs : List Nat)
(hs : xs.Pairwise (fun x y => y ≤ x)) (b : Nat) :
xs.find? p = some b ↔ b ∈ xs ∧ p b = true ∧ ∀ a ∈ xs, b < a → p a = false := by
induction xs with
| nil => simp
| cons x xs ih =>
have htail := hs.of_cons
have hrel := (List.pairwise_cons.mp hs).1
by_cases hx : p x = true
· simp only [List.find?_cons_of_pos hx, Option.some.injEq]
constructor
· intro he; subst b
refine ⟨List.mem_cons_self, hx, ?_⟩
intro a ha hab
rcases List.mem_cons.mp ha with rfl | ha
· omega
· have := hrel a ha; omega
· rintro ⟨hb, hp, hn⟩
rcases List.mem_cons.mp hb with rfl | hb
· rfl
· have he := hrel b hb
by_cases hxb : x = b
· exact hxb
· have := hn x List.mem_cons_self (by omega)
simp [hx] at this
· have hf : p x = false := by cases h : p x <;> simp_all
rw [List.find?_cons_of_neg (by simpa using hx), ih htail]
constructor
· rintro ⟨hb,hp,hn⟩
refine ⟨List.mem_cons_of_mem x hb,hp,?_⟩
intro a ha hab
rcases List.mem_cons.mp ha with rfl | ha
· exact hf
· exact hn a ha hab
· rintro ⟨hb,hp,hn⟩
have hb' : b ∈ xs := by
rcases List.mem_cons.mp hb with rfl | hb
· simp [hf] at hp
· exact hb
exact ⟨hb',hp,fun a ha hab => hn a (List.mem_cons_of_mem x ha) hab⟩
have range_sorted (n : Nat) : (List.range n).Pairwise (· ≤ ·) := by
rw [List.pairwise_iff_getElem]
intro i j hi hj hij
simp only [List.length_range] at hi hj
simp [List.getElem_range, Nat.le_of_lt hij]
have left_some (a : List Nat)Preview only · 0.01 MiB. Download the full file below.
This submission is not a completed checked proof.
runtime: Maximum call stack size exceeded
Axioms: none