1.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.

The result (g, s, t) satisfies g = Nat.gcd a b and s * a + t * b = g after coercing the inputs to Int. Use the GMP-backed HexArith.Int.extGcd entry point for integer inputs and HexArith.UInt64.extGcd for UInt64 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 HexArith.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.