Exact stable-filter lookup with explicit dependent-index normalization
verified
First derive that the number of strictly smaller boundaries is at most the chosen ordinal, then induct on the sorted list to recover the complete selected record. Equal-boundary and smaller-boundary heads are handled separately. Duplicate payloads are admitted. Supporting layout lemma only; no causal/native/cost/novelty claim. The first submitted proof passed local Lean4.35 but failed the pinned checker due to simplification leaving inconsistent implicit decidability arguments. This revision normalizes dependent indices before filtering rewrites; the immutable statement is unchanged.
Lean proof and verification output
by
intro α
have earlier_count_le (b : List (α × Nat))
(hs : b.Pairwise (fun x y => x.2 ≤ y.2))
(j : Nat) (hj : j < b.length) :
(b.filter fun r => r.2 < b[j].2).length ≤ j := by
induction b generalizing j with
| nil => simp at hj
| cons r rs ih =>
have ht := hs.of_cons
have hrel := (List.pairwise_cons.mp hs).1
cases j with
| zero =>
change ((r :: rs).filter fun x => x.2 < r.2).length ≤ 0
have hf : (rs.filter fun x => x.2 < r.2) = [] := by
apply List.filter_eq_nil_iff.mpr
intro x hx
have hh := hrel x hx
simp only [decide_eq_true_eq]
omega
simp only [List.filter_cons, Nat.lt_irrefl, decide_false, Bool.false_eq_true, ↓reduceIte, hf, List.length_nil, Nat.le_refl]
| succ j =>
have hj' : j < rs.length := by simp only [List.length_cons] at hj; omega
have hh := ih ht j hj'
change ((r :: rs).filter fun x => x.2 < rs[j].2).length ≤ j + 1
simp only [List.filter_cons]
split
· change (rs.filter fun x => x.2 < rs[j].2).length + 1 ≤ j + 1
omega
· change (rs.filter fun x => x.2 < rs[j].2).length ≤ j + 1
omega
have gap_getElem (b : List (α × Nat))
(hs : b.Pairwise (fun x y => x.2 ≤ y.2))
(j : Nat) (hj : j < b.length) :
(b.filter fun r => r.2 == b[j].2)[j - (b.filter fun r => r.2 < b[j].2).length]? = some b[j] := by
induction b generalizing j with
| nil => simp at hj
| cons r rs ih =>
have ht := hs.of_cons
have hrel := (List.pairwise_cons.mp hs).1
cases j with
| zero =>
change ((r :: rs).filter fun x => x.2 == r.2)[0 - ((r :: rs).filter fun x => x.2 < r.2).length]? = some r
simp only [List.filter_cons, beq_self_eq_true, ↓reduceIte, Nat.zero_sub, List.getElem?_cons_zero]
| succ j =>
have hj' : j < rs.length := by simp only [List.length_cons] at hj; omega
have hr := hrel rs[j] (List.getElem_mem hj')
have hh := ih ht j hj'
have hc := earlier_count_le rs ht j hj'
change ((r :: rs).filter fun x => x.2 == rs[j].2)[j + 1 - ((r :: rs).filter fun x => x.2 < rs[j].2).length]? = some rs[j]
by_cases he : r.2 = rs[j].2
· simp only [List.filter_cons, he, beq_self_eq_true, ↓reduceIte,
Nat.lt_irrefl, decide_false, Bool.false_eq_true, ↓reduceIte]
have hi : j + 1 - (rs.filter fun x => x.2 < rs[j].2).length =
(j - (rs.filter fun x => x.2 < rs[j].2).length) + 1 := by omega
rw [hi, List.getElem?_cons_succ]
exact hh
· have hl : r.2 < rs[j].2 := by omega
simp only [List.filter_cons, show (r.2 == rs[j].2) = false by
simp [he],
↓reduceIte, Bool.false_eq_true, ↓reduceIte, hl, decide_true, List.length_cons]
simpa only [Nat.succ_sub_succ_eq_sub] using hh
intro b j hs hj
exact gap_getElem b hs j hjPreview only · 0.00 MiB. Download the full file below.
Checked against statement 185ca46ebc2f.
Independent checker: not_run. What this means
'_private.0.OA_target' depends on axioms: [propext, Classical.choice, Quot.sound] OA_target : OA_statement
Axioms: propext, Classical.choice, Quot.sound