Core proof of the raw-predicate insertion destination identity
verified
First Stop and pre-Stop Clear/Start searches satisfy direct head/tail recurrences. Extending the selected destination to arbitrary saved positions permits induction on the raw rows. Each native-shaped rank/key branch is proved to be a Stop, Clear, Start or Skip using its actual numeric inequalities; no action-classification assumption is used. Instantiating the saved state to none proves the initialized target. All rank/getter data are quantified, including unreachable histories. This proves the list query law, not an efficient implementation, native refinement or novelty.
Lean proof and verification output
by
intro Row leftRank rightRank actor sequence
let keyBefore : Row → Row → Bool := fun incoming other => decide (actor incoming < actor other ∨ (actor incoming = actor other ∧ sequence incoming < sequence other))
let literalScan : Row → List Row → Nat → Bool → Nat → Nat := fun incoming rows => List.foldr (fun other tail position scanning back =>
if (leftRank other) = (leftRank incoming) then
if (rightRank other) = (rightRank incoming) then
if keyBefore incoming other then
if scanning then back else position
else tail (position + 1) false back
else if (rightRank other) < (rightRank incoming) then
tail (position + 1) true
(if scanning then back else position)
else tail (position + 1) false back
else if (leftRank other) < (leftRank incoming) then
if scanning then back else position
else tail (position + 1) scanning back) (fun position scanning back => if scanning then back else position) rows
let stopPredicate : Row → Row → Bool := fun incoming other => decide ((leftRank other) < (leftRank incoming)) ||
(decide ((leftRank other) = (leftRank incoming) ∧
(rightRank other) = (rightRank incoming)) && keyBefore incoming other)
let clearPredicate : Row → Row → Bool := fun incoming other => decide ((leftRank other) = (leftRank incoming) ∧
(rightRank incoming) ≤ (rightRank other))
let startPredicate : Row → Row → Bool := fun incoming other => decide ((leftRank other) = (leftRank incoming) ∧
(rightRank other) < (rightRank incoming))
let firstStop : Row → List Row → Nat := fun incoming rows => (((rows.zipIdx).find? (fun pair => stopPredicate incoming pair.1)).map
Prod.snd).getD rows.length
let lastClearBeforeStop : Row → List Row → Option Nat := fun incoming rows => ((((rows.take (firstStop incoming rows)).zipIdx).reverse.find?
(fun pair => clearPredicate incoming pair.1)).map Prod.snd)
let firstStartAfterClear : Row → List Row → Option Nat := fun incoming rows =>
((((rows.take (firstStop incoming rows)).zipIdx).drop (((lastClearBeforeStop incoming rows).map Nat.succ).getD 0)).find? (fun pair => startPredicate incoming pair.1)).map Prod.snd
let selectedDestination : Row → List Row → Nat → Nat := fun incoming rows position => position + (firstStartAfterClear incoming rows).getD (firstStop incoming rows)
change ∀ (incoming : Row) (rows : List Row) (position : Nat),
literalScan incoming rows position false position = selectedDestination incoming rows position
have firstStop_cons (incoming other : Row) (rows : List Row) :
firstStop incoming (other :: rows) =
if stopPredicate incoming other then 0 else firstStop incoming rows + 1 := by
unfold firstStop
cases hs : stopPredicate incoming other <;>
simp [List.zipIdx_succ, List.find?_map,
Option.map_map, Function.comp_def, hs]
cases h : rows.zipIdx.find? (fun pair => stopPredicate incoming pair.1) <;>
simp [Option.getD]
have active_cons (incoming other : Row) (rows : List Row)
(hs : stopPredicate incoming other = false) :
(other :: rows).take (firstStop incoming (other :: rows)) =
other :: rows.take (firstStop incoming rows) := by
rw [firstStop_cons]
simp [hs]
have clear_cons (incoming other : Row) (rows : List Row)
(hs : stopPredicate incoming other = false) :
lastClearBeforeStop incoming (other :: rows) =
((lastClearBeforeStop incoming rows).map (· + 1)).or
(if clearPredicate incoming other then some 0 else none) := by
simp only [lastClearBeforeStop, active_cons incoming other rows hs,
List.zipIdx_cons', List.reverse_cons, ← List.map_reverse,
List.find?_append]
cases hc : clearPredicate incoming other <;>
simp [-List.map_reverse, List.find?_map, Option.map_map,
Function.comp_def, Prod.map, hc]
cases h : (rows.take (firstStop incoming rows)).zipIdx.reverse.fPreview only · 0.01 MiB. Download the full file below.
Checked against statement 71a28134bc10.
Independent checker: error. What this means
'_private.0.OA_target' depends on axioms: [propext, Quot.sound] OA_target : OA_statement
Axioms: propext, Quot.sound