7.3. Extended GCD🔗

The extended Euclidean algorithm returns a triple (g, s, t) with g = gcd a b and the Bezout certificate s · a + t · b = g. The pure Nat version is the reference implementation; an Int variant routes through GMP's mpz_gcdext via @[extern], and a UInt64 variant takes machine-word inputs. All three share the same name in their respective namespaces.

def

HexArith.extGcd (a b : Nat) : Nat × Int × Int
HexArith.extGcd (a b : Nat) :
  Nat × Int × Int

Pure natural-number extended GCD.

HexArith.extGcd a b returns (g, s, t) with g = Nat.gcd a b and s * a + t * b = g after coercing the inputs to Int. Use HexArith.Int.extGcd for the GMP-backed integer API and HexArith.UInt64.extGcd for machine-word inputs.

The combined correctness theorem packages both halves of the specification (the gcd projection and the Bezout identity) for callers that destructure the returned triple.

theorem

HexArith.extGcd_spec (a b : Nat) :
  match HexArith.extGcd a b with
  | (g, s, t) => g = a.gcd b ∧ s * ↑a + t * ↑b = ↑g
HexArith.extGcd_spec (a b : Nat) :
  match HexArith.extGcd a b with
  | (g, s, t) =>
    g = a.gcd b ∧ s * ↑a + t * ↑b = ↑g

Combined correctness theorem for extGcd.

Use this when a caller needs both the gcd projection and the Bezout certificate after destructuring the returned triple.

The Int variant runs the same recurrence over Int, with the GMP mpz_gcdext extern as its trusted runtime replacement.

def

HexArith.Int.extGcd (a b : Int) : Nat × Int × Int
HexArith.Int.extGcd (a b : Int) :
  Nat × Int × Int

Public extended GCD on integers.

Trusted runtime contract: the lean_hex_mpz_gcdext attachment may replace this pure Lean reference with a GMP-backed implementation that returns the same (g, s, t) triple, where g = Int.gcd a b and s * a + t * b = g.

theorem

HexArith.Int.extGcd_spec (a b : Int) :
  match HexArith.Int.extGcd a b with
  | (g, s, t) => g = a.gcd b ∧ s * a + t * b = ↑g
HexArith.Int.extGcd_spec (a b : Int) :
  match HexArith.Int.extGcd a b with
  | (g, s, t) =>
    g = a.gcd b ∧ s * a + t * b = ↑g

Combined correctness theorem for the GMP-backed integer extended GCD surface.

The executable may run through the mpz_gcdext extern, while this theorem characterises the same public triple used by proofs.

The UInt64 variant interprets its word inputs by their natural values, returning the gcd as a word and the Bezout coefficients as signed integers.

def

HexArith.UInt64.extGcd (a b : UInt64) : UInt64 × Int × Int
HexArith.UInt64.extGcd (a b : UInt64) :
  UInt64 × Int × Int

Extended GCD on machine words.

The input words are interpreted by their natural representatives. The gcd is returned as a UInt64, while the Bezout coefficients remain signed integers so the certificate can be stated over Int.ofNat a.toNat and Int.ofNat b.toNat.

theorem

HexArith.UInt64.extGcd_spec (a b : UInt64) :
  match HexArith.UInt64.extGcd a b with
  | (g, s, t) =>
    g.toNat = a.toNat.gcd b.toNat ∧
      s * Int.ofNat a.toNat + t * Int.ofNat b.toNat = Int.ofNat g.toNat
HexArith.UInt64.extGcd_spec
  (a b : UInt64) :
  match HexArith.UInt64.extGcd a b with
  | (g, s, t) =>
    g.toNat = a.toNat.gcd b.toNat ∧
      s * Int.ofNat a.toNat +
          t * Int.ofNat b.toNat =
        Int.ofNat g.toNat

Combined correctness theorem for the UInt64 extended-GCD API.

The gcd component is stored as a word, so the gcd equality is stated after toNat; the Bezout certificate is stated over the natural representatives of the input words.