9.7. Key correctness theorems🔗

The Euclidean operators are pinned down by a small set of laws. The quotient-remainder identity reconstructs the dividend, and the remainder has strictly smaller degree than a positive-degree divisor. Together these are the defining properties of Euclidean division. They are stated under the DivModLaws hypothesis bundling the per-field proof obligations, which HexPolyFp discharges for the concrete prime fields.

theorem

Hex.DensePoly.divMod_spec.{u} {R : Type u} [Zero R] [DecidableEq R]
  [One R] [Add R] [Sub R] [Mul R] [Div R] [Hex.DensePoly.DivModLaws R]
  (p q : Hex.DensePoly R) :
  have qr := p.divMod q;
  qr.1 * q + qr.2 = p
Hex.DensePoly.divMod_spec.{u} {R : Type u}
  [Zero R] [DecidableEq R] [One R] [Add R]
  [Sub R] [Mul R] [Div R]
  [Hex.DensePoly.DivModLaws R]
  (p q : Hex.DensePoly R) :
  have qr := p.divMod q;
  qr.1 * q + qr.2 = p

Euclidean division spec: the field-style quotient and remainder reconstruct the dividend.

theorem

Hex.DensePoly.div_mul_add_mod.{u} {R : Type u} [Zero R] [DecidableEq R]
  [One R] [Add R] [Sub R] [Mul R] [Div R] [Hex.DensePoly.DivModLaws R]
  (p q : Hex.DensePoly R) : p / q * q + p % q = p
Hex.DensePoly.div_mul_add_mod.{u}
  {R : Type u} [Zero R] [DecidableEq R]
  [One R] [Add R] [Sub R] [Mul R] [Div R]
  [Hex.DensePoly.DivModLaws R]
  (p q : Hex.DensePoly R) :
  p / q * q + p % q = p

Euclidean division identity: (p / q) * q + (p % q) = p.

theorem

Hex.DensePoly.mod_degree_lt_of_pos_degree.{u} {R : Type u} [Zero R]
  [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R]
  [Hex.DensePoly.DivModLaws R] (p q : Hex.DensePoly R) :
  0 < q.degree?.getD 0 → (p % q).degree?.getD 0 < q.degree?.getD 0
Hex.DensePoly.mod_degree_lt_of_pos_degree.{u}
  {R : Type u} [Zero R] [DecidableEq R]
  [One R] [Add R] [Sub R] [Mul R] [Div R]
  [Hex.DensePoly.DivModLaws R]
  (p q : Hex.DensePoly R) :
  0 < q.degree?.getD 0 →
    (p % q).degree?.getD 0 <
      q.degree?.getD 0

The computed remainder has degree below a positive-degree divisor.

A polynomial of smaller degree is its own remainder, and a divisor divides its dividend exactly when the remainder is zero.

theorem

Hex.DensePoly.mod_eq_self_of_degree_lt.{u} {R : Type u} [Zero R]
  [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R]
  (p q : Hex.DensePoly R) :
  p.degree?.getD 0 < q.degree?.getD 0 → p % q = p
Hex.DensePoly.mod_eq_self_of_degree_lt.{u}
  {R : Type u} [Zero R] [DecidableEq R]
  [One R] [Add R] [Sub R] [Mul R] [Div R]
  (p q : Hex.DensePoly R) :
  p.degree?.getD 0 < q.degree?.getD 0 →
    p % q = p

A polynomial whose degree is already below the divisor is its own remainder.

theorem

Hex.DensePoly.mod_eq_zero_of_dvd.{u} {R : Type u} [Zero R]
  [DecidableEq R] [One R] [Add R] [Sub R] [Mul R] [Div R]
  [Hex.DensePoly.DivModLaws R] (p q : Hex.DensePoly R) :
  q ∣ p → p % q = 0
Hex.DensePoly.mod_eq_zero_of_dvd.{u}
  {R : Type u} [Zero R] [DecidableEq R]
  [One R] [Add R] [Sub R] [Mul R] [Div R]
  [Hex.DensePoly.DivModLaws R]
  (p q : Hex.DensePoly R) :
  q ∣ p → p % q = 0

If q ∣ p, then p % q = 0.

The gcd divides both arguments and is divisible by every common divisor (its universal property), and the extended coefficients satisfy the Bezout identity. These are bundled under the GcdLaws hypothesis, again discharged downstream.

theorem

Hex.DensePoly.gcd_dvd_left.{u} {R : Type u} [Zero R] [DecidableEq R]
  [One R] [Add R] [Sub R] [Mul R] [Div R] [Hex.DensePoly.GcdLaws R]
  (p q : Hex.DensePoly R) : p.gcd q ∣ p
Hex.DensePoly.gcd_dvd_left.{u}
  {R : Type u} [Zero R] [DecidableEq R]
  [One R] [Add R] [Sub R] [Mul R] [Div R]
  [Hex.DensePoly.GcdLaws R]
  (p q : Hex.DensePoly R) : p.gcd q ∣ p

The polynomial gcd divides the left argument.

theorem

Hex.DensePoly.gcd_dvd_right.{u} {R : Type u} [Zero R] [DecidableEq R]
  [One R] [Add R] [Sub R] [Mul R] [Div R] [Hex.DensePoly.GcdLaws R]
  (p q : Hex.DensePoly R) : p.gcd q ∣ q
Hex.DensePoly.gcd_dvd_right.{u}
  {R : Type u} [Zero R] [DecidableEq R]
  [One R] [Add R] [Sub R] [Mul R] [Div R]
  [Hex.DensePoly.GcdLaws R]
  (p q : Hex.DensePoly R) : p.gcd q ∣ q

The polynomial gcd divides the right argument.

theorem

Hex.DensePoly.dvd_gcd.{u} {R : Type u} [Zero R] [DecidableEq R] [One R]
  [Add R] [Sub R] [Mul R] [Div R] [Hex.DensePoly.GcdLaws R]
  (d p q : Hex.DensePoly R) : d ∣ p → d ∣ q → d ∣ p.gcd q
Hex.DensePoly.dvd_gcd.{u} {R : Type u}
  [Zero R] [DecidableEq R] [One R] [Add R]
  [Sub R] [Mul R] [Div R]
  [Hex.DensePoly.GcdLaws R]
  (d p q : Hex.DensePoly R) :
  d ∣ p → d ∣ q → d ∣ p.gcd q

Every common divisor of p and q divides gcd p q.

theorem

Hex.DensePoly.xgcd_bezout.{u} {R : Type u} [Zero R] [DecidableEq R]
  [One R] [Add R] [Sub R] [Mul R] [Div R] [Hex.DensePoly.GcdLaws R]
  (p q : Hex.DensePoly R) :
  have r := p.xgcd q;
  r.left * p + r.right * q = r.gcd
Hex.DensePoly.xgcd_bezout.{u} {R : Type u}
  [Zero R] [DecidableEq R] [One R] [Add R]
  [Sub R] [Mul R] [Div R]
  [Hex.DensePoly.GcdLaws R]
  (p q : Hex.DensePoly R) :
  have r := p.xgcd q;
  r.left * p + r.right * q = r.gcd

Bezout identity: the extended-gcd coefficients reconstruct the gcd as left * p + right * q.