Mulders-Storjohann Correctness Termination Measure Helpers

Measure-decrease and fuel-bound lemmas for Mulders-Storjohann reduction.

def CompPoly.PolynomialMatrix.shiftedRowMeasure {F : Type u_1} [Field F] [BEq F] (row : PolynomialRow F) (shift : Array ℕ) : ℕ

def CompPoly.PolynomialMatrix.shiftedMatrixMeasure {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) : ℕ

theorem CompPoly.PolynomialMatrix.cancelShiftedLeadingTerm_shiftedRowMeasure_lt {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {target reducer : PolynomialRow F} {shift : Array ℕ} {t r : ShiftedLeadingTerm F} (ht : rowShiftedLeadingTerm? target shift = some t) (hr : rowShiftedLeadingTerm? reducer shift = some r) (hpos : t.position = r.position) (hle : r.shiftedDegree ≤ t.shiftedDegree) (hsize : Array.size reducer = Array.size target) : shiftedRowMeasure (cancelShiftedLeadingTerm target reducer shift) shift < shiftedRowMeasure target shift

theorem CompPoly.PolynomialMatrix.foldRange_add_eq_of_pointwise (n : ℕ) {f g : ℕ → ℕ} (heq : ∀ k < n, f k = g k) : List.foldl (fun (acc k : ℕ) => acc + f k) 0 (List.range n) = List.foldl (fun (acc k : ℕ) => acc + g k) 0 (List.range n)

theorem CompPoly.PolynomialMatrix.foldRange_add_lt_of_pointwise_lt (n : ℕ) {f g : ℕ → ℕ} {idx : ℕ} (hidx : idx < n) (hlt : f idx < g idx) (heq : ∀ k < n, k ≠ idx → f k = g k) : List.foldl (fun (acc k : ℕ) => acc + f k) 0 (List.range n) < List.foldl (fun (acc k : ℕ) => acc + g k) 0 (List.range n)

theorem CompPoly.PolynomialMatrix.shiftedMatrixMeasure_replaceRow_lt {F : Type u_1} [Field F] [BEq F] {M : PolynomialMatrix F} {shift : Array ℕ} {idx : ℕ} {newRow : PolynomialRow F} (hidx : idx < Array.size M) (hlt : shiftedRowMeasure newRow shift < shiftedRowMeasure (Array.getD M idx #[]) shift) : (M.replaceRow idx newRow).shiftedMatrixMeasure shift < M.shiftedMatrixMeasure shift

theorem CompPoly.PolynomialMatrix.muldersStorjohannStep_shiftedMatrixMeasure_lt {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {M : PolynomialMatrix F} {shift : Array ℕ} {i j : ℕ} (hM : M.WellFormed) (hconf : M.shiftedLeadingConflict? shift = some (i, j)) : (M.muldersStorjohannStep shift i j).shiftedMatrixMeasure shift < M.shiftedMatrixMeasure shift

def CompPoly.PolynomialMatrix.matrixShiftedDegreeStep? {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) (acc : Option ℕ) (i : ℕ) : Option ℕ

def CompPoly.PolynomialMatrix.matrixShiftedDegreeSpec? {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) : Option ℕ

theorem CompPoly.PolynomialMatrix.matrixShiftedDegreeStep?_eq {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) : M.matrixShiftedDegreeStep? shift = fun (acc : Option ℕ) (i : ℕ) => match rowShiftedDegree? (Array.getD M i #[]) shift with | none => acc | some d => maxOption acc d

theorem CompPoly.PolynomialMatrix.matrixShiftedDegree?_eq_spec {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) : M.matrixShiftedDegree? shift = M.matrixShiftedDegreeSpec? shift

theorem CompPoly.PolynomialMatrix.matrixShiftedDegreeSpecFold_acc_le {F : Type u_1} [Field F] [BEq F] {M : PolynomialMatrix F} {shift : Array ℕ} (xs : List ℕ) {acc : Option ℕ} {a D : ℕ} (hacc : acc = some a) (hfold : List.foldl (M.matrixShiftedDegreeStep? shift) acc xs = some D) : a ≤ D

theorem CompPoly.PolynomialMatrix.matrixShiftedDegreeSpecFold_row_le {F : Type u_1} [Field F] [BEq F] {M : PolynomialMatrix F} {shift : Array ℕ} (xs : List ℕ) {acc : Option ℕ} {D i rowDeg : ℕ} (hfold : List.foldl (M.matrixShiftedDegreeStep? shift) acc xs = some D) (hi : i ∈ xs) (hdeg : rowShiftedDegree? (Array.getD M i #[]) shift = some rowDeg) : rowDeg ≤ D

theorem CompPoly.PolynomialMatrix.matrixShiftedDegreeSpec?_row_le {F : Type u_1} [Field F] [BEq F] {M : PolynomialMatrix F} {shift : Array ℕ} {D i rowDeg : ℕ} (hmat : M.matrixShiftedDegreeSpec? shift = some D) (hi : i < Array.size M) (hdeg : rowShiftedDegree? (Array.getD M i #[]) shift = some rowDeg) : rowDeg ≤ D

theorem CompPoly.PolynomialMatrix.matrixShiftedDegree?_row_le {F : Type u_1} [Field F] [BEq F] {M : PolynomialMatrix F} {shift : Array ℕ} {D i rowDeg : ℕ} (hmat : M.matrixShiftedDegree? shift = some D) (hi : i < Array.size M) (hdeg : rowShiftedDegree? (Array.getD M i #[]) shift = some rowDeg) : rowDeg ≤ D

theorem CompPoly.PolynomialMatrix.matrixShiftedDegreeSpecFold_some_of_acc_some {F : Type u_1} [Field F] [BEq F] {M : PolynomialMatrix F} {shift : Array ℕ} (xs : List ℕ) {acc : Option ℕ} {a : ℕ} (hacc : acc = some a) : ∃ (D : ℕ), List.foldl (M.matrixShiftedDegreeStep? shift) acc xs = some D

theorem CompPoly.PolynomialMatrix.matrixShiftedDegreeSpecFold_exists_some_of_row {F : Type u_1} [Field F] [BEq F] {M : PolynomialMatrix F} {shift : Array ℕ} (xs : List ℕ) {i rowDeg : ℕ} (hi : i ∈ xs) (hdeg : rowShiftedDegree? (Array.getD M i #[]) shift = some rowDeg) : ∃ (D : ℕ), List.foldl (M.matrixShiftedDegreeStep? shift) none xs = some D

theorem CompPoly.PolynomialMatrix.matrixShiftedDegree?_row_le_getD {F : Type u_1} [Field F] [BEq F] {M : PolynomialMatrix F} {shift : Array ℕ} {i rowDeg : ℕ} (hi : i < Array.size M) (hdeg : rowShiftedDegree? (Array.getD M i #[]) shift = some rowDeg) : rowDeg ≤ (M.matrixShiftedDegree? shift).getD 0

theorem CompPoly.PolynomialMatrix.shiftedRowMeasure_le_of_degree_bound {F : Type u_1} [Field F] [BEq F] {row : PolynomialRow F} {shift : Array ℕ} {d : ℕ} (hbound : ∀ (rowDeg : ℕ), rowShiftedDegree? row shift = some rowDeg → rowDeg ≤ d) : shiftedRowMeasure row shift ≤ (d + 1) * (Array.size row + 1)

theorem CompPoly.PolynomialMatrix.shiftedMatrixMeasure_range_le_of_degree_bound {F : Type u_1} [Field F] [BEq F] {M : PolynomialMatrix F} {shift : Array ℕ} {d : ℕ} (hM : M.WellFormed) (hbound : ∀ (i rowDeg : ℕ), i < Array.size M → rowShiftedDegree? (Array.getD M i #[]) shift = some rowDeg → rowDeg ≤ d) (n : ℕ) : n ≤ Array.size M → List.foldl (fun (acc i : ℕ) => acc + shiftedRowMeasure (Array.getD M i #[]) shift) 0 (List.range n) ≤ n * ((d + 1) * (M.MatrixWidth + 1))

theorem CompPoly.PolynomialMatrix.shiftedMatrixMeasure_le_of_degree_bound {F : Type u_1} [Field F] [BEq F] {M : PolynomialMatrix F} {shift : Array ℕ} {d : ℕ} (hM : M.WellFormed) (hbound : ∀ (i rowDeg : ℕ), i < Array.size M → rowShiftedDegree? (Array.getD M i #[]) shift = some rowDeg → rowDeg ≤ d) : M.shiftedMatrixMeasure shift ≤ Array.size M * ((d + 1) * (M.MatrixWidth + 1))

theorem CompPoly.PolynomialMatrix.shiftedMatrixMeasure_lt_muldersStorjohannFuel {F : Type u_1} [Field F] [BEq F] {M : PolynomialMatrix F} {shift : Array ℕ} (hM : M.WellFormed) : M.shiftedMatrixMeasure shift < M.muldersStorjohannFuel shift