def HexArith.natDivMod (a b : Nat) : Nat × Nat

Quotient/remainder pairing used by extGcd.

Lean 4.30's stdlib exposes Nat.div and Nat.mod, but not a public fused Nat.divMod; keep the pairing local so the Euclidean step can switch to a fused primitive once one is available.

Equations

• HexArith.natDivMod a b = (a / b, a % b)

@[irreducible]

def 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 HexArith.Int.extGcd for integer inputs and HexArith.UInt64.extGcd for UInt64 inputs.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HexArith.extGcd_fst (a b : Nat) : (extGcd a b).fst = a.gcd b

The gcd component returned by the pure Nat extended-GCD algorithm is Lean's Nat.gcd.

@[simp]

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

The coefficient components returned by the pure Nat extended-GCD algorithm form a Bezout certificate for the inputs.

@[simp]

theorem HexArith.extGcd_bezout_proj (a b : Nat) : (extGcd a b).snd.fst * ↑a + (extGcd a b).snd.snd * ↑b = ↑(extGcd a b).fst

Bezout certificate for the pure Nat extGcd, stated on the returned triple's projections: the cofactors s = (extGcd a b).2.1 and t = (extGcd a b).2.2 satisfy s * a + t * b = (extGcd a b).1 after coercing a and b to Int. The _proj form keeps the right-hand side as the routine's own returned gcd component; see extGcd_bezout_gcd for the variant phrased against Nat.gcd a b.

@[simp]

theorem HexArith.extGcd_bezout_gcd (a b : Nat) : (extGcd a b).snd.fst * ↑a + (extGcd a b).snd.snd * ↑b = ↑(a.gcd b)

Bezout certificate for the pure Nat extGcd with the gcd resolved to Nat.gcd a b: the returned cofactors satisfy s * a + t * b = Nat.gcd a b over Int. Same identity as extGcd_bezout_proj, with the right-hand side rewritten through extGcd_fst.

@[simp]

theorem HexArith.extGcd_spec (a b : Nat) : match 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.

@[irreducible]

def Hex.pureIntExtGcd.go (old_r r old_s s old_t t : Int) : Nat × Int × Int

Pure Lean reference implementation of extended GCD over integers.

This runs the Euclidean algorithm directly on Int, carrying Bezout coefficients through the usual quotient/remainder updates.

Equations

• One or more equations did not get rendered due to their size.
• Hex.pureIntExtGcd.go old_r 0 old_s s old_t t = if old_r < 0 then (old_r.natAbs, -old_s, -old_t) else (old_r.natAbs, old_s, old_t)

def Hex.pureIntExtGcd (a b : Int) : Nat × Int × Int

Pure Lean integer extended GCD.

Hex.pureIntExtGcd is the proof reference and portable fallback for HexArith.Int.extGcd; callers that want the project public integer API should use HexArith.Int.extGcd instead.

Equations

• Hex.pureIntExtGcd a b = Hex.pureIntExtGcd.go a b 1 0 0 1

@[simp]

theorem Hex.pureIntExtGcd_fst (a b : Int) : (pureIntExtGcd a b).fst = a.gcd b

The gcd component returned by the pure integer reference implementation is Lean's Int.gcd.

@[simp]

theorem Hex.pureIntExtGcd_bezout (a b : Int) : match pureIntExtGcd a b with | (g, s, t) => s * a + t * b = ↑g

The coefficient components returned by the pure integer reference implementation form a Bezout certificate for the inputs.

@[simp]

theorem Hex.pureIntExtGcd_bezout_proj (a b : Int) : (pureIntExtGcd a b).snd.fst * a + (pureIntExtGcd a b).snd.snd * b = ↑(pureIntExtGcd a b).fst

Bezout certificate for the pure integer reference pureIntExtGcd, stated on the returned triple's projections: the cofactors (pureIntExtGcd a b).2.1 and (pureIntExtGcd a b).2.2 satisfy s * a + t * b = (pureIntExtGcd a b).1. Inputs are already Int, so no coercion is involved.

@[simp]

theorem Hex.pureIntExtGcd_spec (a b : Int) : match pureIntExtGcd a b with | (g, s, t) => g = a.gcd b ∧ s * a + t * b = ↑g

Combined correctness theorem for the pure integer reference implementation.

Use this when a proof needs both the gcd projection and the Bezout certificate without unfolding the recursive reference implementation.

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

Public extended GCD on integers.

The logical definition retains the signed Euclidean algorithm. A proved compiler rewrite uses Nat.extendedGcd on nonnegative inputs, preserving this definition's exact coefficients; negative inputs use the signed algorithm.

Equations

• HexArith.Int.extGcd a b = Hex.pureIntExtGcd a b

@[simp]

theorem HexArith.Int.extGcd_fst (a b : Int) : (extGcd a b).fst = a.gcd b

The gcd component returned by the public integer extended-GCD API is Lean's Int.gcd.

@[simp]

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

The coefficient components returned by the public integer extended-GCD API form a Bezout certificate for the inputs.

@[simp]

theorem HexArith.Int.extGcd_bezout_proj (a b : Int) : (extGcd a b).snd.fst * a + (extGcd a b).snd.snd * b = ↑(extGcd a b).fst

Projection form of the integer Bezout certificate: the coefficient components, addressed directly as (extGcd a b).2.1 and (extGcd a b).2.2, combine to the returned gcd component (extGcd a b).1. Lets callers rewrite a Bezout identity without first destructuring the (g, s, t) triple.

@[simp]

theorem HexArith.Int.extGcd_bezout_gcd (a b : Int) : (extGcd a b).snd.fst * a + (extGcd a b).snd.snd * b = ↑(a.gcd b)

Bezout certificate stated against Int.gcd a b directly: the coefficient projections combine to the canonical gcd rather than the returned (extGcd a b).1 component. Lets callers rewrite a Bezout identity straight to Int.gcd, skipping the intermediate extGcd_fst step.

@[simp]

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

Combined correctness theorem for the public integer extended GCD.

The proved compiler rewrite uses the GMP-backed natural-number primitive on nonnegative inputs, while preserving the same public triple used by proofs.

@[simp]

theorem HexArith.Int.extGcd_fst_ofNat (a b : Nat) : (extGcd (Int.ofNat a) (Int.ofNat b)).fst = a.gcd b

The integer extended-GCD API agrees with Nat.gcd on nonnegative inputs.

@[simp]

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

Combined correctness theorem for the integer extended-GCD API specialised to nonnegative inputs.

theorem HexArith.Int.extGcd_zero_left_s_ofNat (p : Nat) (hp : 0 < p) : (extGcd 0 (Int.ofNat p)).snd.fst = 0

For a positive natural modulus, the Bezout coefficient of the zero input in Int.extGcd 0 p is zero.

def HexArith.Int.extGcdImpl (a b : Int) : Nat × Int × Int

Runtime implementation using the natural primitive on nonnegative inputs. Reversing the inputs and coefficients preserves the signed reference's exact zero, equal-input, and coefficient conventions.

Equations

• HexArith.Int.extGcdImpl (Int.ofNat a_2) (Int.ofNat b_2) = ((b_2.extendedGcd a_2).gcd, (b_2.extendedGcd a_2).coeffB, (b_2.extendedGcd a_2).coeffA)
• HexArith.Int.extGcdImpl a b = Hex.pureIntExtGcd a b

@[csimp]

theorem HexArith.Int.extGcd_eq_extGcdImpl : extGcd = extGcdImpl

The native natural-number route returns exactly the signed reference's triple, rather than merely another valid Bezout certificate.

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

Equations

• HexArith.UInt64.extGcd a b = match HexArith.Int.extGcd (Int.ofNat a.toNat) (Int.ofNat b.toNat) with | (g, s, t) => (UInt64.ofNat g, s, t)

@[simp]

theorem HexArith.UInt64.extGcd_fst (a b : UInt64) : (extGcd a b).fst.toNat = a.toNat.gcd b.toNat

The gcd component returned by the UInt64 extended-GCD API represents the gcd of the natural values of the input words.

@[simp]

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

The coefficient components returned by the UInt64 extended-GCD API form a Bezout certificate for the natural values of the input words.

@[simp]

theorem HexArith.UInt64.extGcd_bezout_proj (a b : UInt64) : (extGcd a b).snd.fst * Int.ofNat a.toNat + (extGcd a b).snd.snd * Int.ofNat b.toNat = Int.ofNat (extGcd a b).fst.toNat

Bezout certificate for the UInt64 extGcd, stated on the returned triple's projections: the cofactors satisfy s * a.toNat + t * b.toNat = (extGcd a b).1.toNat, with each word coerced to Int via Int.ofNat ·.toNat. The _proj form keeps the right-hand side as the routine's own returned gcd word; see extGcd_bezout_gcd for the variant phrased against Nat.gcd a.toNat b.toNat.

@[simp]

theorem HexArith.UInt64.extGcd_bezout_gcd (a b : UInt64) : (extGcd a b).snd.fst * Int.ofNat a.toNat + (extGcd a b).snd.snd * Int.ofNat b.toNat = Int.ofNat (a.toNat.gcd b.toNat)

Bezout certificate for the UInt64 extGcd with the gcd resolved to Nat.gcd a.toNat b.toNat: the returned cofactors satisfy s * a.toNat + t * b.toNat = Nat.gcd a.toNat b.toNat, coerced to Int via Int.ofNat ·.toNat. Same identity as extGcd_bezout_proj, with the right-hand side rewritten through extGcd_fst.

@[simp]

theorem HexArith.UInt64.extGcd_spec (a b : UInt64) : match 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.