gcd_props — Mathlib

English

Let d,w,x,y,z,a',b' be defined by gcdD, gcdW, gcdX, gcdY, gcdZ, gcdA', gcdB' for a,b in PNat. Then w z = succ(x y); a = a' d; b = b' d; z a' = succ(x b'); w b' = succ(y a'); and z a, x b, etc. satisfy the usual Bezout relations.

Русский

Пусть d,w,x,y,z,a',b' заданы как gcdD, gcdW, gcdX, gcdY, gcdZ, gcdA', gcdB' для a,b в PNat. Тогда выполняются: w z = succ(x y); a = a' d; b = b' d; z a' = succ(x b'); w b' = succ(y a'); а также остальные отношения типа Bezout.

LaTeX

$$$w z = \operatorname{succPNat}(x y) \land a = a' d \land b = b' d \land z a' = \operatorname{succPNat}(x b') \land w b' = \operatorname{succPNat}(y a') \land (z a : \mathbb{N}) = x b + d \land (w b : \mathbb{N}) = y a + d$$$

Lean4

theorem gcd_props :
    let d := gcdD a b
    let w := gcdW a b
    let x := gcdX a b
    let y := gcdY a b
    let z := gcdZ a b
    let a' := gcdA' a b
    let b' := gcdB' a b
    w * z = succPNat (x * y) ∧
      a = a' * d ∧
        b = b' * d ∧
          z * a' = succPNat (x * b') ∧ w * b' = succPNat (y * a') ∧ (z * a : ℕ) = x * b + d ∧ (w * b : ℕ) = y * a + d :=
  by
  intro d w x y z a' b'
  let u := XgcdType.start a b
  let ur := u.reduce
  have hb : d = ur.b := u.reduce_isReduced'
  have ha' : (a' : ℕ) = w + x := gcdA'_coe a b
  have hb' : (b' : ℕ) = y + z := gcdB'_coe a b
  have hdet : w * z = succPNat (x * y) := u.reduce_isSpecial' rfl
  constructor
  · exact hdet
  have hdet' : (w * z : ℕ) = x * y + 1 := by rw [← mul_coe, hdet, succPNat_coe]
  let hv : Prod.mk (w * d + x * ur.b : ℕ) (y * d + z * ur.b : ℕ) = ⟨a, b⟩ := u.reduce_v.trans (XgcdType.start_v a b)
  rw [← hb, ← add_mul, ← add_mul, ← ha', ← hb'] at hv
  have ha'' : (a : ℕ) = a' * d := (congr_arg Prod.fst hv).symm
  have hb'' : (b : ℕ) = b' * d := (congr_arg Prod.snd hv).symm
  constructor
  · exact eq ha''
  constructor
  · exact eq hb''
  have hza' : (z * a' : ℕ) = x * b' + 1 :=
    by
    rw [ha', hb', mul_add, mul_add, mul_comm (z : ℕ), hdet']
    ring
  have hwb' : (w * b' : ℕ) = y * a' + 1 :=
    by
    rw [ha', hb', mul_add, mul_add, hdet']
    ring
  constructor
  · apply eq
    rw [succPNat_coe, Nat.succ_eq_add_one, mul_coe, hza']
  constructor
  · apply eq
    rw [succPNat_coe, Nat.succ_eq_add_one, mul_coe, hwb']
  grind

Похожие утверждения