The contracts of the Sturm step

The steps of the remainder chain Ratpoints.Sturm.chain as plain functions, by well-founded recursion where the model has a loop, the predicate of a remainder chain, and the contract of the chain as a @[spec] theorem proved with vcgen, the program logic of Lean core, with loop invariants that are named definitions; the contracts of the evaluation of a row at a dyadic number (Ratpoints.Sturm.evalSign: the sign of the value of the Horner rule in integers), of the signs and the count of sign changes of the chain there (Ratpoints.Sturm.signsAt) and at ±∞ (Ratpoints.Sturm.countsAtInfinity); the loop of the intersection with the caller's intervals (Ratpoints.Sturm.intersect) as a recursion on the two lists (Ratpoints.Sturm.intersectList); and the failure of the Sturm step (Ratpoints.Sturm.computeSturm) exactly when the chain fails.

Main definitions

• Ratpoints.Sturm.dropZeros, Ratpoints.Sturm.reduceOnce, Ratpoints.Sturm.fullReduce: the zero leading coefficients of a remainder dropped, one reduction step followed by that drop, and the reduction of a remainder until its degree is below that of the divisor, #[] when it becomes zero.
• Ratpoints.Sturm.content, Ratpoints.Sturm.normalize: the gcd of the coefficients of a remainder, and the remainder negated and divided by it.
• Ratpoints.Sturm.IsChain: a remainder chain of a polynomial and its derivative.
• Ratpoints.Sturm.IsChainResult: the result of the chain as its contract states it, a chain whose last row is constant, or none when a chain reduces to zero.
• Ratpoints.Sturm.hornerValue: the value of a row at n / 2 ^ e times 2 ^ (e deg), by the Horner rule of Ratpoints.Sturm.evalSign.
• Ratpoints.Sturm.signCount: the sign changes that Ratpoints.Sturm.signsAt counts, zeros skipped.
• Ratpoints.Sturm.signAtTop, Ratpoints.Sturm.signAtBot: the signs of the rows at ±∞.
• Ratpoints.Sturm.intersectList: the intersection of two lists of intervals by the steps of Ratpoints.Sturm.intersect.

Main statements

• Ratpoints.Sturm.chain_spec: the loops of Ratpoints.Sturm.chain end, and its result satisfies Ratpoints.Sturm.IsChainResult; Ratpoints.Sturm.isChainResult_run_chain states this without the program logic.
• Ratpoints.Sturm.IsChain.size_le: a chain of a polynomial of degree d has at most d + 1 rows.
• Ratpoints.Sturm.evalSign_spec, Ratpoints.Sturm.signsAt_spec, Ratpoints.Sturm.countsAtInfinity_spec, Ratpoints.Sturm.intersect_spec: the contracts of the evaluation, the signs at a midpoint, the counts at ±∞ and the intersection, with the plain statements Ratpoints.Sturm.run_evalSign, Ratpoints.Sturm.run_signsAt, Ratpoints.Sturm.run_countsAtInfinity and Ratpoints.Sturm.toList_run_intersect.
• Ratpoints.Sturm.run_computeSturm_eq_none_iff: the Sturm step fails exactly when the chain does.

Implementation notes

The file uses Lean core and Std only, as Ratpoints.Proof.Words does; the lemmas on arrays, lists, ranges and integers that are not about the model are in Ratpoints.Proof.Containers, those on longs in Ratpoints.Proof.Bits. The plain statements let the files with Mathlib use the contracts without the program logic; the values of the doubles of the intervals are in Ratpoints.Proof.Bisection.

The steps of the chain

@[irreducible]

def Ratpoints.Sturm.dropZeros (t : Array Int) : Array Int

The array t with its zero entries on top dropped, the zero leading coefficients of a remainder: the loop of Ratpoints.Sturm.chain after a reduction step.

Equations

• Ratpoints.Sturm.dropZeros t = if (t.back? == some 0) = true then Ratpoints.Sturm.dropZeros t.pop else t

theorem Ratpoints.Sturm.dropZeros_of_beq {t : Array Int} (h : (t.back? == some 0) = true) : dropZeros t = dropZeros t.pop

theorem Ratpoints.Sturm.dropZeros_of_not_beq {t : Array Int} (h : ¬(t.back? == some 0) = true) : dropZeros t = t

theorem Ratpoints.Sturm.size_dropZeros_le (t : Array Int) : (dropZeros t).size ≤ t.size

theorem Ratpoints.Sturm.back!_dropZeros_ne_zero {t : Array Int} (h : (dropZeros t).size ≠ 0) : (dropZeros t).back! ≠ 0

theorem Ratpoints.Sturm.getElem!_dropZeros (t : Array Int) (i : Nat) : (dropZeros t)[i]! = t[i]!

theorem Ratpoints.Sturm.size_reduce (s t : Array Int) : (reduce s t).size = t.size - 1 + 1

theorem Ratpoints.Sturm.exists_getElem!_reduce {s t : Array Int} (hle : s.size ≤ t.size) (hs : s.back! ≠ 0) : ∃ (u : Int), ∃ (v : Int), 0 < u ∧ u * t.back! = v * s.back! ∧ ∀ (n : Nat), (reduce s t)[n]! = u * t[n]! - v * if t.size - s.size ≤ n then s[n - (t.size - s.size)]! else 0

The entries of the reduction of t by s, deg t ≥ deg s: u t - v X^(deg t - deg s) s with u > 0 and u lc t = v lc s, so that the leading entry cancels.

theorem Ratpoints.Sturm.back!_reduce {s t : Array Int} (hle : s.size ≤ t.size) (hs : s.back! ≠ 0) : (reduce s t).back! = 0

def Ratpoints.Sturm.reduceOnce (s t : Array Int) : Array Int

One reduction of t by s with the leading entry, which cancels, dropped, and then the zeros on top: one pass of the reduction loop of Ratpoints.Sturm.chain.

Equations

• Ratpoints.Sturm.reduceOnce s t = Ratpoints.Sturm.dropZeros (Ratpoints.Sturm.reduce s t).pop

theorem Ratpoints.Sturm.exists_getElem!_reduceOnce {s t : Array Int} (hle : s.size ≤ t.size) (hs : s.back! ≠ 0) : ∃ (u : Int), ∃ (v : Int), 0 < u ∧ ∀ (n : Nat), (reduceOnce s t)[n]! = u * t[n]! - v * if t.size - s.size ≤ n then s[n - (t.size - s.size)]! else 0

theorem Ratpoints.Sturm.size_reduceOnce_lt {s t : Array Int} (h : (reduceOnce s t).size ≠ 0) : (reduceOnce s t).size < t.size

@[irreducible]

def Ratpoints.Sturm.fullReduce (s t : Array Int) : Array Int

The reduction loop of Ratpoints.Sturm.chain: t reduced by s until its size is below that of s, and #[] when a reduction leaves nothing, where the chain returns none.

Equations

• Ratpoints.Sturm.fullReduce s t = if s.size ≤ t.size then if (Ratpoints.Sturm.reduceOnce s t).size = 0 then #[] else Ratpoints.Sturm.fullReduce s (Ratpoints.Sturm.reduceOnce s t) else t

theorem Ratpoints.Sturm.fullReduce_of_lt {s t : Array Int} (h : t.size < s.size) : fullReduce s t = t

theorem Ratpoints.Sturm.fullReduce_of_size_eq_zero {s t : Array Int} (hle : s.size ≤ t.size) (h : (reduceOnce s t).size = 0) : fullReduce s t = #[]

theorem Ratpoints.Sturm.fullReduce_of_size_ne_zero {s t : Array Int} (hle : s.size ≤ t.size) (h : (reduceOnce s t).size ≠ 0) : fullReduce s t = fullReduce s (reduceOnce s t)

def Ratpoints.Sturm.content (t : Array Int) : Nat

The gcd of the entries of t, the loop of Ratpoints.Sturm.chain over the coefficients of a remainder, there with a break once the gcd is 1.

Equations

• Ratpoints.Sturm.content t = Array.foldl (fun (g : Nat) (a : Int) => g.gcd a.natAbs) 0 t

def Ratpoints.Sturm.normalize (t : Array Int) : Array Int

The array t negated and divided by the gcd of its entries: the change of sign and the division of a remainder by the gcd of its coefficients in Ratpoints.Sturm.chain.

Equations

• Ratpoints.Sturm.normalize t = Array.map (fun (x : Int) => x / ↑(Ratpoints.Sturm.content (Array.map Neg.neg t))) (Array.map Neg.neg t)

theorem Ratpoints.Sturm.natCast_content_dvd_getElem! (t : Array Int) (i : Nat) : ↑(content t) ∣ t[i]!

theorem Ratpoints.Sturm.size_normalize (t : Array Int) : (normalize t).size = t.size

theorem Ratpoints.Sturm.mul_getElem!_normalize (t : Array Int) (i : Nat) : ↑(content (Array.map Neg.neg t)) * (normalize t)[i]! = -t[i]!

theorem Ratpoints.Sturm.content_map_neg_ne_zero {t : Array Int} (h : (normalize t).back! ≠ 0) : content (Array.map Neg.neg t) ≠ 0

theorem Ratpoints.Sturm.back!_normalize_ne_zero {t : Array Int} (h : t.back! ≠ 0) : (normalize t).back! ≠ 0

Remainder chains

structure Ratpoints.Sturm.IsChain (c : List Int) (d : Nat) (ch : Array (Array Int)) : Prop

The rows ch are a remainder chain of the polynomial f of degree d with the coefficients c₀, …, c_d, the entries of c, as Ratpoints.Sturm.chain computes it.

• two_le_size : 2 ≤ ch.size

  The chain has f and f' at least.

• getElem!_zero : ch[0]! = Array.map (fun (x : Nat) => c.getD x 0) (Array.range (d + 1))

  The first row is f, the coefficients c₀, …, c_d.

• getElem!_one : ch[1]! = Array.map (fun (n : Nat) => (↑n + 1) * c.getD (n + 1) 0) (Array.range d)

  The second row is f', the coefficients (n + 1) c_(n+1) for n < d.

• getElem!_add_two (k : Nat) (hk : k + 2 < ch.size) : ch[k + 2]! = normalize (fullReduce ch[k + 1]! ch[k]!)

  Each further row is the full reduction of the row two before by the row before, negated and divided by the gcd of its entries.

• back!_ne_zero (k : Nat) (hk : k < ch.size) : ch[k]!.back! ≠ 0

  Every row has a nonzero last entry, its leading coefficient.

• size_lt (k : Nat) (hk : k + 2 < ch.size) : ch[k + 2]!.size < ch[k + 1]!.size

  The sizes decrease strictly from f' on.

def Ratpoints.Sturm.IsChainResult (c : List Int) (d : Nat) : Option (Array (Array Int)) → Prop

The result of Ratpoints.Sturm.chain as its contract states it: some ch for a chain ch whose last row is constant; none when there is a chain whose last row is not constant and reduces the row before it to zero, which Ratpoints.Sturm.fullReduce gives as #[].

Equations

• Ratpoints.Sturm.IsChainResult c d none = ∃ (ch : Array (Array Int)), Ratpoints.Sturm.IsChain c d ch ∧ 2 ≤ ch.back!.size ∧ Ratpoints.Sturm.fullReduce ch.back! ch[ch.size - 2]! = #[]
• Ratpoints.Sturm.IsChainResult c d (some ch) = (Ratpoints.Sturm.IsChain c d ch ∧ ch.back!.size = 1)

theorem Ratpoints.Sturm.isChain_pair {c : List Int} {d : Nat} (hd : 1 ≤ d) (hc : c.getD d 0 ≠ 0) : IsChain c d #[Array.map (fun (x : Nat) => c.getD x 0) (Array.range (d + 1)), Array.map (fun (n : Nat) => (↑n + 1) * c.getD (n + 1) 0) (Array.range d)]

theorem Ratpoints.Sturm.IsChain.push {c : List Int} {d : Nat} {ch : Array (Array Int)} {t : Array Int} (h : IsChain c d ch) (ht : fullReduce ch.back! ch[ch.size - 2]! = t) (ht0 : t.back! ≠ 0) (hlt : t.size < ch.back!.size) : IsChain c d (ch.push (normalize t))

theorem Ratpoints.Sturm.IsChain.size_getElem!_add_one_add_le {c : List Int} {d : Nat} {ch : Array (Array Int)} (h : IsChain c d ch) {k : Nat} (hk : k + 1 < ch.size) : ch[k + 1]!.size + k ≤ d

The row k + 1 of a chain has at most d - k entries: the sizes drop by one at least from f' on.

theorem Ratpoints.Sturm.IsChain.size_le {c : List Int} {d : Nat} {ch : Array (Array Int)} (h : IsChain c d ch) : ch.size ≤ d + 1

A chain has at most d + 1 rows, the rows of the table of the C code.

The invariants

def Ratpoints.Sturm.ChainLoopInvariant (c : List Int) (d : Nat) (pref suff : List Nat) (ch : Array (Array Int)) : Prop

The rows while the loop of Ratpoints.Sturm.chain over k runs, after the indices pref, with the indices suff still to come: a chain (Ratpoints.Sturm.IsChain), whose last row is constant once no index is left; while indices are left, one row for each index done after f and f', the last one not constant, its size and the number of rows adding up to at most d + 2.

Equations

• One or more equations did not get rendered due to their size.

def Ratpoints.Sturm.ChainInvariant (c : List Int) (d : Nat) (pref suff : List Nat) (x : Option (Option (Array (Array Int))) × Array (Array Int)) : Prop

The invariant of the loop of Ratpoints.Sturm.chain over k, on the pair of the value of an early return and the rows: no return yet and Ratpoints.Sturm.ChainLoopInvariant, or the return of none, which ends the loop, with the result none of the contract.

Equations

• Ratpoints.Sturm.ChainInvariant c d pref suff x = (x.fst = none ∧ Ratpoints.Sturm.ChainLoopInvariant c d pref suff x.snd ∨ suff = [] ∧ x.fst = some none ∧ Ratpoints.Sturm.IsChainResult c d none)

def Ratpoints.Sturm.ReduceInvariant (s t₀ : Array Int) (exit : Bool) (x : Option (Option (Array (Array Int))) × Array Int) : Prop

The invariant of the reduction loop of Ratpoints.Sturm.chain of t₀ by s, on the pair of the value of an early return and the remainder: no return, the same full reduction as t₀, a nonzero last entry, and at the exit a size below that of s; or, at the exit, the return of none, when the full reduction of t₀ leaves nothing.

Equations

• One or more equations did not get rendered due to their size.

def Ratpoints.Sturm.DropZerosInvariant (t₀ : Array Int) (exit : Bool) (t : Array Int) : Prop

The invariant of the loop of Ratpoints.Sturm.chain that drops the zeros on top of t₀: the same result of Ratpoints.Sturm.dropZeros, and no zero on top at the exit.

Equations

• Ratpoints.Sturm.DropZerosInvariant t₀ exit t = (Ratpoints.Sturm.dropZeros t = Ratpoints.Sturm.dropZeros t₀ ∧ (exit = true → ¬(t.back? == some 0) = true))

def Ratpoints.Sturm.ContentInvariant (pref : List Int) (g : Nat) : Prop

The invariant of the loop of Ratpoints.Sturm.chain over the entries of a remainder: the gcd of the entries pref done, the break at 1 included.

Equations

• Ratpoints.Sturm.ContentInvariant pref g = (g = List.foldl (fun (g : Nat) (a : Int) => g.gcd a.natAbs) 0 pref)

The verification conditions, one lemma each in the shape vcgen states it

theorem Ratpoints.Sturm.chainInvariant_nil {c : List Int} {d : Nat} (h : 1 ≤ d ∧ c.getD d 0 ≠ 0) : ChainInvariant c d [] (ForIn.toList [2:d + 1]) (none, #[Array.map (fun (x : Nat) => c.getD x 0) (Array.range (d + 1)), Array.map (fun (n : Nat) => (↑n + 1) * c.getD (n + 1) 0) (Array.range d)])

theorem Ratpoints.Sturm.ChainInvariant.isChainResult {c : List Int} {d : Nat} {pref suff : List Nat} {y : Option (Option (Array (Array Int)))} {ch : Array (Array Int)} {a : Option (Array (Array Int))} (h : ChainInvariant c d pref suff (y, ch)) (hy : y = some a) : IsChainResult c d a

theorem Ratpoints.Sturm.ChainInvariant.isChainResult_some {c : List Int} {d : Nat} {pref : List Nat} {y : Option (Option (Array (Array Int)))} {ch : Array (Array Int)} (h : ChainInvariant c d pref [] (y, ch)) (hy : y = none) : IsChainResult c d (some ch)

theorem Ratpoints.Sturm.ChainInvariant.chainLoopInvariant {c : List Int} {d : Nat} {pref : List Nat} {cur : Nat} {suff : List Nat} {y : Option (Option (Array (Array Int)))} {ch : Array (Array Int)} (h : ChainInvariant c d pref (cur :: suff) (y, ch)) : y = none ∧ ChainLoopInvariant c d pref (cur :: suff) ch

theorem Ratpoints.Sturm.ChainLoopInvariant.size_eq {c : List Int} {d : Nat} {pref : List Nat} {cur : Nat} {suff : List Nat} {ch : Array (Array Int)} (hl : ForIn.toList [2:d + 1] = pref ++ cur :: suff) (h : ChainLoopInvariant c d pref (cur :: suff) ch) : ch.size = cur

At the index cur, the chain has cur rows: the reduction is of the row cur - 2 by the row cur - 1, the last one.

theorem Ratpoints.Sturm.ChainInvariant.reduceInvariant {c : List Int} {d : Nat} {pref : List Nat} {cur : Nat} {suff : List Nat} {y : Option (Option (Array (Array Int)))} {ch : Array (Array Int)} (hl : ForIn.toList [2:d + 1] = pref ++ cur :: suff) (h : ChainInvariant c d pref (cur :: suff) (y, ch)) : ReduceInvariant ch[cur - 1]! ch[cur - 2]! false (none, ch[cur - 2]!)

theorem Ratpoints.Sturm.ChainInvariant.of_reduceInvariant_some {c : List Int} {d : Nat} {pref : List Nat} {cur : Nat} {suff : List Nat} {y z : Option (Option (Array (Array Int)))} {ch : Array (Array Int)} {t : Array Int} {a : Option (Array (Array Int))} (hl : ForIn.toList [2:d + 1] = pref ++ cur :: suff) (h : ChainInvariant c d pref (cur :: suff) (y, ch)) (ht : ReduceInvariant ch[cur - 1]! ch[cur - 2]! true (z, t)) (hz : z = some a) : ChainInvariant c d (ForIn.toList [2:d + 1]) [] (some a, ch)

theorem Ratpoints.Sturm.ChainLoopInvariant.push {c : List Int} {d : Nat} {pref : List Nat} {cur : Nat} {suff : List Nat} {ch : Array (Array Int)} {t : Array Int} (hl : ForIn.toList [2:d + 1] = pref ++ cur :: suff) (h : ChainLoopInvariant c d pref (cur :: suff) ch) (ht : fullReduce ch[cur - 1]! ch[cur - 2]! = t) (ht0 : t.back! ≠ 0) (hlt : t.size < ch[cur - 1]!.size) : IsChain c d (ch.push (normalize t)) ∧ (¬(normalize t).size = 1 → ChainLoopInvariant c d (pref ++ [cur]) suff (ch.push (normalize t)))

The step of the loop over k: the normalized full reduction t pushed onto the chain.

theorem Ratpoints.Sturm.ChainInvariant.push_normalize {c : List Int} {d : Nat} {pref : List Nat} {cur : Nat} {suff : List Nat} {y : Option (Option (Array (Array Int)))} {ch : Array (Array Int)} {t : Array Int} (hl : ForIn.toList [2:d + 1] = pref ++ cur :: suff) (h : ChainInvariant c d pref (cur :: suff) (y, ch)) (ht : ReduceInvariant ch[cur - 1]! ch[cur - 2]! true (none, t)) : ((normalize t).size = 1 → ChainInvariant c d (ForIn.toList [2:d + 1]) [] (none, ch.push (normalize t))) ∧ (¬(normalize t).size = 1 → ChainInvariant c d (pref ++ [cur]) suff (none, ch.push (normalize t)))

theorem Ratpoints.Sturm.contentInvariant_nil : ContentInvariant [] 0

theorem Ratpoints.Sturm.ContentInvariant.append {pref : List Int} {g : Nat} (h : ContentInvariant pref g) (cur : Int) : ContentInvariant (pref ++ [cur]) (g.gcd cur.natAbs)

theorem Ratpoints.Sturm.ContentInvariant.of_gcd_eq_one {xs pref suff : List Int} {cur : Int} {g : Nat} (hl : xs = pref ++ cur :: suff) (h : ContentInvariant pref g) (hg : g.gcd cur.natAbs = 1) : ContentInvariant xs (g.gcd cur.natAbs)

theorem Ratpoints.Sturm.ContentInvariant.normalize_eq {t : Array Int} {g : Nat} (h : ContentInvariant (ForIn.toList (Array.map Neg.neg t)) g) : normalize t = Array.map (fun (x : Int) => x / ↑g) (Array.map Neg.neg t)

theorem Ratpoints.Sturm.ContentInvariant.normalize_eq_map_neg {t : Array Int} {g : Nat} (h : ContentInvariant (ForIn.toList (Array.map Neg.neg t)) g) (h1 : ¬¬g = 1) : normalize t = Array.map Neg.neg t

theorem Ratpoints.Sturm.ChainInvariant.push_of_size_eq_one {c : List Int} {d : Nat} {pref : List Nat} {cur : Nat} {suff : List Nat} {y z : Option (Option (Array (Array Int)))} {ch : Array (Array Int)} {t r : Array Int} (hl : ForIn.toList [2:d + 1] = pref ++ cur :: suff) (h : ChainInvariant c d pref (cur :: suff) (y, ch)) (ht : ReduceInvariant ch[cur - 1]! ch[cur - 2]! true (z, t)) (hz : z = none) (hr : normalize t = r) (h1 : r.size = 1) : ChainInvariant c d (ForIn.toList [2:d + 1]) [] (none, ch.push r)

theorem Ratpoints.Sturm.ChainInvariant.push_of_size_ne_one {c : List Int} {d : Nat} {pref : List Nat} {cur : Nat} {suff : List Nat} {y z : Option (Option (Array (Array Int)))} {ch : Array (Array Int)} {t r : Array Int} (hl : ForIn.toList [2:d + 1] = pref ++ cur :: suff) (h : ChainInvariant c d pref (cur :: suff) (y, ch)) (ht : ReduceInvariant ch[cur - 1]! ch[cur - 2]! true (z, t)) (hz : z = none) (hr : normalize t = r) (h1 : ¬r.size = 1) : ChainInvariant c d (pref ++ [cur]) suff (none, ch.push r)

theorem Ratpoints.Sturm.dropZerosInvariant_self (t : Array Int) : DropZerosInvariant t false t

theorem Ratpoints.Sturm.DropZerosInvariant.pop {t₀ t : Array Int} {mb : Nat} (h : t.size = mb ∧ DropZerosInvariant t₀ false t) (hb : (t.back? == some 0) = true) : t.pop.size < mb ∧ DropZerosInvariant t₀ false t.pop

theorem Ratpoints.Sturm.DropZerosInvariant.exit {t₀ t : Array Int} {mb : Nat} (h : t.size = mb ∧ DropZerosInvariant t₀ false t) (hb : ¬(t.back? == some 0) = true) : DropZerosInvariant t₀ true t

theorem Ratpoints.Sturm.DropZerosInvariant.eq_reduceOnce {s t t' : Array Int} (h : DropZerosInvariant (reduce s t).pop true t') : t' = reduceOnce s t

theorem Ratpoints.Sturm.ReduceInvariant.of_size_eq_zero {s t₀ t t' : Array Int} {y : Option (Option (Array (Array Int)))} {mb : Nat} (h : t.size = mb ∧ ReduceInvariant s t₀ false (y, t)) (hle : s.size ≤ t.size) (hd : DropZerosInvariant (reduce s t).pop true t') (h0 : t'.size = 0) : ReduceInvariant s t₀ true (some none, t')

theorem Ratpoints.Sturm.ReduceInvariant.of_size_ne_zero {s t₀ t t' : Array Int} {y : Option (Option (Array (Array Int)))} {mb : Nat} (h : t.size = mb ∧ ReduceInvariant s t₀ false (y, t)) (hle : s.size ≤ t.size) (hd : DropZerosInvariant (reduce s t).pop true t') (h0 : ¬t'.size = 0) : t'.size < mb ∧ ReduceInvariant s t₀ false (none, t')

theorem Ratpoints.Sturm.ReduceInvariant.exit {s t₀ t : Array Int} {y : Option (Option (Array (Array Int)))} {mb : Nat} (h : t.size = mb ∧ ReduceInvariant s t₀ false (y, t)) (hlt : ¬s.size ≤ t.size) : ReduceInvariant s t₀ true (none, t)

theorem Ratpoints.Sturm.chain_spec (c : List Int) (d : Nat) : ⦃ 1 ≤ d ∧ c.getD d 0 ≠ 0 ⦄ chain c d ⦃ IsChainResult c d ⦄

The loop over k ends by its range, the reduction loop by the size of the remainder, which drops with every pass, and the loop that drops the zeros on top by the size as well.

theorem Ratpoints.Sturm.isChainResult_run_chain {c : List Int} {d : Nat} (hd : 1 ≤ d) (hc : c.getD d 0 ≠ 0) : IsChainResult c d (chain c d).run

Ratpoints.Sturm.chain_spec as a plain statement, which the files with Mathlib use without the program logic.

The signs of the chain

def Ratpoints.Sturm.hornerValue (row : Array Int) (num : Int) (e : Nat) : Nat → Int

The value of the polynomial with the coefficients row, constant term first, at num / 2 ^ e, times 2 ^ (e deg), deg the size of row less one, as the Horner rule of Ratpoints.Sturm.evalSign computes it in integers, after j of its steps: from the leading coefficient, w ↦ w num + c_(deg - j - 1) 2 ^ (e (j + 1)) at the step j.

Equations

• Ratpoints.Sturm.hornerValue row num e 0 = row[row.size - 1]!
• Ratpoints.Sturm.hornerValue row num e j.succ = Ratpoints.Sturm.hornerValue row num e j * num + row[row.size - 2 - j]! * 2 ^ (e * (j + 1))

def Ratpoints.Sturm.EvalSignInvariant (row : Array Int) (num denexp : Int64) (pref : List Nat) (x : Int × Int64) : Prop

The invariant of the loop of Ratpoints.Sturm.evalSign after the steps pref: the value of the Horner rule after as many steps, and the exponent of the next step.

Equations

• Ratpoints.Sturm.EvalSignInvariant row num denexp pref x = (x.fst = Ratpoints.Sturm.hornerValue row num.toInt denexp.toInt.toNat pref.length ∧ x.snd.toInt = denexp.toInt * (↑pref.length + 1))

theorem Ratpoints.Sturm.evalSignInvariant_nil (row : Array Int) (num denexp : Int64) : EvalSignInvariant row num denexp [] (row[row.size - 1]!, denexp)

theorem Ratpoints.Sturm.EvalSignInvariant.sign_eq {row : Array Int} {num denexp : Int64} {w : Int} {e : Int64} (h : EvalSignInvariant row num denexp (ForIn.toList [:row.size - 1]) (w, e)) : w.sign = (hornerValue row num.toInt denexp.toInt.toNat (row.size - 1)).sign

theorem Ratpoints.Sturm.EvalSignInvariant.push {row : Array Int} {num denexp : Int64} {pref suff : List Nat} {cur : Nat} (hd : 0 ≤ denexp.toInt ∧ denexp.toInt * ↑row.size < 2 ^ 63) (hl : ForIn.toList [:row.size - 1] = pref ++ cur :: suff) {w : Int} {e : Int64} (h : EvalSignInvariant row num denexp pref (w, e)) : EvalSignInvariant row num denexp (pref ++ [cur]) (w * num.toInt + row[row.size - 1 - 1 - cur]! * 2 ^ e.toInt.toNat, e + denexp)

A step of the loop of Ratpoints.Sturm.evalSign; the exponents denexp (j + 1) stay below 2 ^ 63.

def Ratpoints.Sturm.signCount : Int → List Int → Nat

The number of sign changes that the loop of Ratpoints.Sturm.signsAt counts in the signs l after the sign s: a sign -s counts and becomes the sign compared, another sign that is not 0 becomes the sign compared, and a 0 is skipped. For a sign s ≠ 0 this is the number of sign changes of s followed by l, the zeros skipped.

Equations

• Ratpoints.Sturm.signCount x✝ [] = 0
• Ratpoints.Sturm.signCount x✝ (t :: ts) = if t = -x✝ then Ratpoints.Sturm.signCount t ts + 1 else if t ≠ 0 then Ratpoints.Sturm.signCount t ts else Ratpoints.Sturm.signCount x✝ ts

def Ratpoints.Sturm.SignsAtInvariant (σ : Nat → Int) (total : Nat) (suff : List Nat) (x : Nat × Int) : Prop

The invariant of the loop of Ratpoints.Sturm.signsAt with the indices suff still to come: the count so far and the count of the signs σ n still to come after the sign compared add up to total.

Equations

• Ratpoints.Sturm.SignsAtInvariant σ total suff x = (x.fst + Ratpoints.Sturm.signCount x.snd (List.map σ suff) = total)

theorem Ratpoints.Sturm.signsAtInvariant_init (σ : Nat → Int) (c : Nat) (s : Int) (l : List Nat) : SignsAtInvariant σ (c + signCount s (List.map σ l)) l (c, s)

theorem Ratpoints.Sturm.SignsAtInvariant.of_cons {σ : Nat → Int} {total cur : Nat} {suff : List Nat} {cmid : Nat} {s : Int} (h : SignsAtInvariant σ total (cur :: suff) (cmid, s)) : SignsAtInvariant σ total suff (if σ cur = -s then cmid + 1 else cmid, if σ cur = -s then σ cur else if σ cur ≠ 0 then σ cur else s)

theorem Ratpoints.Sturm.SignsAtInvariant.of_cons_neg {σ : Nat → Int} {total cur : Nat} {suff : List Nat} {cmid : Nat} {s s2 : Int} (h : SignsAtInvariant σ total (cur :: suff) (cmid, s)) (h2 : s2 = σ cur) (hn : s2 = -s) : SignsAtInvariant σ total suff (cmid + 1, s2)

theorem Ratpoints.Sturm.SignsAtInvariant.of_cons_ne {σ : Nat → Int} {total cur : Nat} {suff : List Nat} {cmid : Nat} {s s2 : Int} (h : SignsAtInvariant σ total (cur :: suff) (cmid, s)) (h2 : s2 = σ cur) (hn : ¬s2 = -s) (h0 : ¬s2 = 0) : SignsAtInvariant σ total suff (cmid, s2)

theorem Ratpoints.Sturm.SignsAtInvariant.of_cons_zero {σ : Nat → Int} {total cur : Nat} {suff : List Nat} {cmid : Nat} {s s2 : Int} (h : SignsAtInvariant σ total (cur :: suff) (cmid, s)) (h2 : s2 = σ cur) (hn : ¬s2 = -s) (h0 : ¬¬s2 = 0) : SignsAtInvariant σ total suff (cmid, s)

theorem Ratpoints.Sturm.SignsAtInvariant.eq {σ : Nat → Int} {s0 s1 r0 r1 b : Int} {k cmid : Nat} (h0 : s0 = r0) (h1 : s1 = r1) (h : SignsAtInvariant σ ((if s0 * s1 = -1 then 1 else 0) + signCount (if s1 = 0 then s0 else s1) (List.map σ (ForIn.toList [2:k + 1]))) [] (cmid, b)) : (s0, s1, cmid) = (r0, r1, (if r0 * r1 = -1 then 1 else 0) + signCount (if r1 = 0 then r0 else r1) (List.map σ (List.range' 2 (k - 1))))

def Ratpoints.Sturm.signAtTop (rows : Array (Array Int)) (n : Nat) : Int

The sign of the leading coefficient of the row n of the chain rows, the sign of the row at +∞.

Equations

• Ratpoints.Sturm.signAtTop rows n = rows[n]![rows[n]!.size - 1]!.sign

def Ratpoints.Sturm.signAtBot (rows : Array (Array Int)) (n : Nat) : Int

The sign of the row n of the chain rows at -∞: that of its leading coefficient, negated for odd degree.

Equations

• Ratpoints.Sturm.signAtBot rows n = if (rows[n]!.size - 1) % 2 = 1 then -Ratpoints.Sturm.signAtTop rows n else Ratpoints.Sturm.signAtTop rows n

def Ratpoints.Sturm.CountsInvariant (rows : Array (Array Int)) (pref : List Nat) (x : Nat × Nat) : Prop

The invariant of the loop of Ratpoints.Sturm.countsAtInfinity after the indices pref: the numbers of the indices n among them where the signs of the rows n and n + 1 differ at +∞ and at -∞.

Equations

• One or more equations did not get rendered due to their size.

theorem Ratpoints.Sturm.countsInvariant_nil (rows : Array (Array Int)) : CountsInvariant rows [] (0, 0)

theorem Ratpoints.Sturm.CountsInvariant.push {rows : Array (Array Int)} {pref : List Nat} {cur c1 c2 : Nat} (h : CountsInvariant rows pref (c1, c2)) {a b : Nat} (ha : a = if signAtTop rows cur = signAtTop rows (cur + 1) then c1 else c1 + 1) (hb : b = if signAtBot rows cur = signAtBot rows (cur + 1) then c2 else c2 + 1) : CountsInvariant rows (pref ++ [cur]) (a, b)

theorem Ratpoints.Sturm.CountsInvariant.range {rows : Array (Array Int)} {k : Nat} {x : Nat × Nat} (h : CountsInvariant rows (ForIn.toList [:k]) x) : CountsInvariant rows (List.range k) x

theorem Ratpoints.Sturm.evalSign_spec (row : Array Int) (num denexp : Int64) : ⦃ 0 ≤ denexp.toInt ∧ denexp.toInt * ↑row.size < 2 ^ 63 ⦄ evalSign row num denexp ⦃ fun (s : Int) => s = (hornerValue row num.toInt denexp.toInt.toNat (row.size - 1)).sign ⦄

The exponents denexp (j + 1) of the Horner rule stay below 2 ^ 63, so that the long e does not overflow.

theorem Ratpoints.Sturm.run_evalSign {row : Array Int} (num : Int64) {denexp : Int64} (h0 : 0 ≤ denexp.toInt) (h : denexp.toInt * ↑row.size < 2 ^ 63) : (evalSign row num denexp).run = (hornerValue row num.toInt denexp.toInt.toNat (row.size - 1)).sign

Ratpoints.Sturm.evalSign_spec as a plain statement.

theorem Ratpoints.Sturm.signsAt_spec (rows : Array (Array Int)) (k : Nat) (nm dem : Int64) : ⦃ True ⦄ signsAt rows k nm dem ⦃ fun (r : Int × Int × Nat) => r = ((evalSign rows[0]! nm dem).run, (evalSign rows[1]! nm dem).run, (if (evalSign rows[0]! nm dem).run * (evalSign rows[1]! nm dem).run = -1 then 1 else 0) + signCount (if (evalSign rows[1]! nm dem).run = 0 then (evalSign rows[0]! nm dem).run else (evalSign rows[1]! nm dem).run) (List.map (fun (n : Nat) => (evalSign rows[n]! nm dem).run) (List.range' 2 (k - 1)))) ⦄

theorem Ratpoints.Sturm.run_signsAt (rows : Array (Array Int)) (k : Nat) (nm dem : Int64) : (signsAt rows k nm dem).run = ((evalSign rows[0]! nm dem).run, (evalSign rows[1]! nm dem).run, (if (evalSign rows[0]! nm dem).run * (evalSign rows[1]! nm dem).run = -1 then 1 else 0) + signCount (if (evalSign rows[1]! nm dem).run = 0 then (evalSign rows[0]! nm dem).run else (evalSign rows[1]! nm dem).run) (List.map (fun (n : Nat) => (evalSign rows[n]! nm dem).run) (List.range' 2 (k - 1))))

Ratpoints.Sturm.signsAt_spec as a plain statement: the signs σ 0 and σ 1 of f and f' at the midpoint, and the number of sign changes of σ 0, …, σ k, the signs of the rows of the chain there, the zeros skipped (Ratpoints.Sturm.signCount).

theorem Ratpoints.Sturm.countsAtInfinity_spec (rows : Array (Array Int)) (k : Nat) : ⦃ True ⦄ countsAtInfinity rows k ⦃ fun (r : Nat × Nat) => CountsInvariant rows (List.range k) r ⦄

theorem Ratpoints.Sturm.run_countsAtInfinity (rows : Array (Array Int)) (k : Nat) : (countsAtInfinity rows k).run = (List.countP (fun (n : Nat) => signAtTop rows n != signAtTop rows (n + 1)) (List.range k), List.countP (fun (n : Nat) => signAtBot rows n != signAtBot rows (n + 1)) (List.range k))

Ratpoints.Sturm.countsAtInfinity_spec as a plain statement: the numbers of the indices n < k where the signs of the rows n and n + 1 of the chain differ at +∞ and at -∞, the numbers of sign changes of a chain whose rows have nonzero leading coefficients.

The intersection with the caller's intervals

@[irreducible]

def Ratpoints.Sturm.intersectList : List (Double × Double) → List (Double × Double) → List (Double × Double)

The intersection of the intervals loc with the intervals ivs, by the steps of Ratpoints.Sturm.intersect (Ratpoints.Sturm.meet) as a recursion on the two lists: the interval that a step notes, followed by the intersection of the rest, without the interval of loc or of ivs that ends first.

Equations

• One or more equations did not get rendered due to their size.
• Ratpoints.Sturm.intersectList [] x✝ = []
• Ratpoints.Sturm.intersectList (head :: tail) [] = []

theorem Ratpoints.Sturm.intersectList_cons_cons (a b : Double × Double) (as bs : List (Double × Double)) : intersectList (a :: as) (b :: bs) = (meet a b).fst.toList ++ if (meet a b).snd = true then intersectList as (b :: bs) else intersectList (a :: as) bs

@[simp]

theorem Ratpoints.Sturm.intersectList_nil_left (bs : List (Double × Double)) : intersectList [] bs = []

@[simp]

theorem Ratpoints.Sturm.intersectList_nil_right (as : List (Double × Double)) : intersectList as [] = []

def Ratpoints.Sturm.IntersectInvariant (loc ivs : Array (Double × Double)) (exit : Bool) (x : Nat × Nat × Array (Double × Double)) : Prop

The invariant of the loop of Ratpoints.Sturm.intersect on the cursors n1, n2 and the intervals noted: they followed by the intersection of the rest of the lists are the intersection of the lists, and at the exit the rest of one of the lists is empty.

Equations

• One or more equations did not get rendered due to their size.

theorem Ratpoints.Sturm.intersectInvariant_zero (loc ivs : Array (Double × Double)) : IntersectInvariant loc ivs false (0, 0, #[])

theorem Ratpoints.Sturm.IntersectInvariant.exit {loc ivs : Array (Double × Double)} {n1 n2 : Nat} {out : Array (Double × Double)} (h : IntersectInvariant loc ivs false (n1, n2, out)) (hx : ¬(n1 < loc.size ∧ n2 < ivs.size)) : IntersectInvariant loc ivs true (n1, n2, out)

theorem Ratpoints.Sturm.IntersectInvariant.eq {loc ivs : Array (Double × Double)} {n1 n2 : Nat} {out : Array (Double × Double)} (h : IntersectInvariant loc ivs true (n1, n2, out)) : out.toList = intersectList loc.toList ivs.toList

theorem Ratpoints.Sturm.IntersectInvariant.next {loc ivs : Array (Double × Double)} {n1 n2 : Nat} {out : Array (Double × Double)} (h : IntersectInvariant loc ivs false (n1, n2, out)) (hx : n1 < loc.size ∧ n2 < ivs.size) : IntersectInvariant loc ivs false (if (meet loc[n1]! ivs[n2]!).snd = true then n1 + 1 else n1, if (meet loc[n1]! ivs[n2]!).snd = true then n2 else n2 + 1, match (meet loc[n1]! ivs[n2]!).fst with | some v => out.push v | none => out)

theorem Ratpoints.Sturm.IntersectInvariant.push_left {loc ivs : Array (Double × Double)} {n1 n2 : Nat} {out : Array (Double × Double)} (h : IntersectInvariant loc ivs false (n1, n2, out)) (hx : n1 < loc.size ∧ n2 < ivs.size) {v : Double × Double} (hm : (meet loc[n1]! ivs[n2]!).fst = some v) (hs : (meet loc[n1]! ivs[n2]!).snd = true) : IntersectInvariant loc ivs false (n1 + 1, n2, out.push v)

theorem Ratpoints.Sturm.IntersectInvariant.push_right {loc ivs : Array (Double × Double)} {n1 n2 : Nat} {out : Array (Double × Double)} (h : IntersectInvariant loc ivs false (n1, n2, out)) (hx : n1 < loc.size ∧ n2 < ivs.size) {v : Double × Double} (hm : (meet loc[n1]! ivs[n2]!).fst = some v) (hs : ¬(meet loc[n1]! ivs[n2]!).snd = true) : IntersectInvariant loc ivs false (n1, n2 + 1, out.push v)

theorem Ratpoints.Sturm.IntersectInvariant.skip_left {loc ivs : Array (Double × Double)} {n1 n2 : Nat} {out : Array (Double × Double)} (h : IntersectInvariant loc ivs false (n1, n2, out)) (hx : n1 < loc.size ∧ n2 < ivs.size) {o : Option (Double × Double)} (ho : ∀ (v : Double × Double), o = some v → False) (hm : (meet loc[n1]! ivs[n2]!).fst = o) (hs : (meet loc[n1]! ivs[n2]!).snd = true) : IntersectInvariant loc ivs false (n1 + 1, n2, out)

theorem Ratpoints.Sturm.IntersectInvariant.skip_right {loc ivs : Array (Double × Double)} {n1 n2 : Nat} {out : Array (Double × Double)} (h : IntersectInvariant loc ivs false (n1, n2, out)) (hx : n1 < loc.size ∧ n2 < ivs.size) {o : Option (Double × Double)} (ho : ∀ (v : Double × Double), o = some v → False) (hm : (meet loc[n1]! ivs[n2]!).fst = o) (hs : ¬(meet loc[n1]! ivs[n2]!).snd = true) : IntersectInvariant loc ivs false (n1, n2 + 1, out)

theorem Ratpoints.Sturm.intersect_spec (loc ivs : Array (Double × Double)) : ⦃ True ⦄ intersect loc ivs ⦃ fun (out : Array (Double × Double)) => out.toList = intersectList loc.toList ivs.toList ⦄

The loop ends since every pass moves one of the cursors.

theorem Ratpoints.Sturm.toList_run_intersect (loc ivs : Array (Double × Double)) : (intersect loc ivs).run.toList = intersectList loc.toList ivs.toList

Ratpoints.Sturm.intersect_spec as a plain statement.

The Sturm step

theorem Ratpoints.Sturm.run_computeSturm_eq_none_iff (c : List Int) (d iter : Nat) (ivlist : Array (Double × Double)) : (computeSturm c d iter ivlist).run = none ↔ (chain c d).run = none

The Sturm step fails exactly when the remainder chain does: after the chain, the counts at infinity, the bisection and the intersection always give intervals.