Documentation

CompPoly.LinearAlgebra.PolynomialMatrix.MuldersStorjohannCorrectness.Conflict

Mulders-Storjohann Correctness Shifted Leading Conflict Helpers #

Bounds and validity lemmas for shifted-leading-position conflict detection.

theorem CompPoly.PolynomialMatrix.index_lt_of_rowShiftedDegree?_getElem?_eq_some {F : Type u_1} [Field F] [BEq F] {M : PolynomialMatrix F} {shift : Array ℕ} {i d : ℕ} (hdeg : rowShiftedDegree? (M[i]?.getD #[]) shift = some d) :

i < Array.size M

def CompPoly.PolynomialMatrix.ConflictBounds {F : Type u_1} [Field F] (M : PolynomialMatrix F) :

Option (ℕ × ℕ) → Prop

Instances For

theorem CompPoly.PolynomialMatrix.shiftedLeadingConflictInRowFold_bounds {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) (i : ℕ) (xs : List ℕ) (found : Option (ℕ × ℕ)) (hxs : ∀ j ∈ xs, i < j ∧ j < Array.size M) (hfound : M.ConflictBounds found) :

M.ConflictBounds (List.foldl (fun (found : Option (ℕ × ℕ)) (j : ℕ) => match found with | some val => found | none => match rowShiftedLeadingPosition? (Array.getD M i #[]) shift, rowShiftedLeadingPosition? (Array.getD M j #[]) shift with | some pi, some pj => if (pi == pj) = true then some (i, j) else none | x, x_1 => none) found xs)

theorem CompPoly.PolynomialMatrix.shiftedLeadingConflictInRow?_bounds {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) {i : ℕ} {found : Option (ℕ × ℕ)} (hi : i < Array.size M) (hfound : M.ConflictBounds found) :

M.ConflictBounds (M.shiftedLeadingConflictInRow? shift i found)

theorem CompPoly.PolynomialMatrix.shiftedLeadingConflictFromFold_bounds {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) (xs : List ℕ) (found : Option (ℕ × ℕ)) (hxs : ∀ i ∈ xs, i < Array.size M) (hfound : M.ConflictBounds found) :

M.ConflictBounds (List.foldl (fun (found : Option (ℕ × ℕ)) (i : ℕ) => M.shiftedLeadingConflictInRow? shift i found) found xs)

theorem CompPoly.PolynomialMatrix.shiftedLeadingConflictFrom?_bounds {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) {found : Option (ℕ × ℕ)} (hfound : M.ConflictBounds found) :

M.ConflictBounds (M.shiftedLeadingConflictFrom? shift found)

theorem CompPoly.PolynomialMatrix.shiftedLeadingConflict?_some_bounds {F : Type u_1} [Field F] [BEq F] {M : PolynomialMatrix F} {shift : Array ℕ} {i j : ℕ} (hconf : M.shiftedLeadingConflict? shift = some (i, j)) :

i < Array.size M ∧ j < Array.size M ∧ i < j

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

Option (ℕ × ℕ) → Prop

Instances For

theorem CompPoly.PolynomialMatrix.shiftedLeadingConflictInRowStep?_valid {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) (i : ℕ) {found : Option (ℕ × ℕ)} (j : ℕ) (hfound : M.ConflictValid shift found) :

M.ConflictValid shift (M.shiftedLeadingConflictInRowStep? shift i found j)

theorem CompPoly.PolynomialMatrix.shiftedLeadingConflictInRowFold_valid {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) (i : ℕ) (xs : List ℕ) {found : Option (ℕ × ℕ)} (hfound : M.ConflictValid shift found) :

M.ConflictValid shift (List.foldl (M.shiftedLeadingConflictInRowStep? shift i) found xs)

theorem CompPoly.PolynomialMatrix.shiftedLeadingConflictInRow?_valid {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) (i : ℕ) {found : Option (ℕ × ℕ)} (hfound : M.ConflictValid shift found) :

M.ConflictValid shift (M.shiftedLeadingConflictInRow? shift i found)

theorem CompPoly.PolynomialMatrix.shiftedLeadingConflictFromFold_valid {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) (xs : List ℕ) {found : Option (ℕ × ℕ)} (hfound : M.ConflictValid shift found) :

M.ConflictValid shift (List.foldl (M.shiftedLeadingConflictFromStep? shift) found xs)

theorem CompPoly.PolynomialMatrix.shiftedLeadingConflictFrom?_valid {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) {found : Option (ℕ × ℕ)} (hfound : M.ConflictValid shift found) :

M.ConflictValid shift (M.shiftedLeadingConflictFrom? shift found)

theorem CompPoly.PolynomialMatrix.shiftedLeadingConflict?_some_valid {F : Type u_1} [Field F] [BEq F] {M : PolynomialMatrix F} {shift : Array ℕ} {i j : ℕ} (hconf : M.shiftedLeadingConflict? shift = some (i, j)) :

∃ (p : ℕ), rowShiftedLeadingPosition? (Array.getD M i #[]) shift = some p ∧ rowShiftedLeadingPosition? (Array.getD M j #[]) shift = some p

theorem CompPoly.PolynomialMatrix.shiftedLeadingConflictInRowFold_some {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) (i : ℕ) (xs : List ℕ) (pair : ℕ × ℕ) :

List.foldl (M.shiftedLeadingConflictInRowStep? shift i) (some pair) xs = some pair

theorem CompPoly.PolynomialMatrix.shiftedLeadingConflictInRow?_some {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) (i : ℕ) (pair : ℕ × ℕ) :

M.shiftedLeadingConflictInRow? shift i (some pair) = some pair

theorem CompPoly.PolynomialMatrix.shiftedLeadingConflictFromFold_some {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) (xs : List ℕ) (pair : ℕ × ℕ) :

List.foldl (M.shiftedLeadingConflictFromStep? shift) (some pair) xs = some pair

theorem CompPoly.PolynomialMatrix.shiftedLeadingConflictFrom?_some {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) (pair : ℕ × ℕ) :

M.shiftedLeadingConflictFrom? shift (some pair) = some pair

theorem CompPoly.PolynomialMatrix.shiftedLeadingConflictInRowFold_none_no_conflict {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) (i : ℕ) (xs : List ℕ) (hfold : List.foldl (M.shiftedLeadingConflictInRowStep? shift i) none xs = none) {j p : ℕ} (hj : j ∈ xs) (hposI : rowShiftedLeadingPosition? (Array.getD M i #[]) shift = some p) (hposJ : rowShiftedLeadingPosition? (Array.getD M j #[]) shift = some p) :

theorem CompPoly.PolynomialMatrix.shiftedLeadingConflictInRow?_none_no_conflict {F : Type u_1} [Field F] [BEq F] {M : PolynomialMatrix F} {shift : Array ℕ} {i j p : ℕ} (hfold : M.shiftedLeadingConflictInRow? shift i none = none) (hij : i < j) (hj : j < Array.size M) (hposI : rowShiftedLeadingPosition? (Array.getD M i #[]) shift = some p) (hposJ : rowShiftedLeadingPosition? (Array.getD M j #[]) shift = some p) :

theorem CompPoly.PolynomialMatrix.shiftedLeadingConflictFromFold_none_inner_none {F : Type u_1} [Field F] [BEq F] (M : PolynomialMatrix F) (shift : Array ℕ) (xs : List ℕ) (hfold : List.foldl (M.shiftedLeadingConflictFromStep? shift) none xs = none) {i : ℕ} (hi : i ∈ xs) :

M.shiftedLeadingConflictInRow? shift i none = none

theorem CompPoly.PolynomialMatrix.shiftedLeadingConflict?_none_no_conflict {F : Type u_1} [Field F] [BEq F] {M : PolynomialMatrix F} {shift : Array ℕ} {i j p : ℕ} (hconf : M.shiftedLeadingConflict? shift = none) (hi : i < Array.size M) (hj : j < Array.size M) (hij : i < j) (hposI : rowShiftedLeadingPosition? (Array.getD M i #[]) shift = some p) (hposJ : rowShiftedLeadingPosition? (Array.getD M j #[]) shift = some p) :

theorem CompPoly.PolynomialMatrix.shiftedLeadingConflict?_none_weakPopov {F : Type u_1} [Field F] [BEq F] {M : PolynomialMatrix F} {shift : Array ℕ} (hconf : M.shiftedLeadingConflict? shift = none) :

M.ShiftedWeakPopov shift