Conversation
This PR adds `Nat.extendedGcd` to compute the greatest common divisor of two natural numbers together with signed Bézout coefficients, and provides correctness lemmas for using those coefficients in proofs. Return the gcd and both coefficients in a single `Nat.ExtendedGcdResult`, with named fields `gcd`, `coeffA`, and `coeffB`. Compute all three values in one tail-recursive Euclidean pass using arbitrary-precision `Nat` and `Int` arithmetic. Prove `extendedGcd_gcd`, `extendedGcd_bezout`, divisibility, and the zero-input and equal-input simplification lemmas. Use mathlib's initialization and zero-input conventions: `extendedGcd 0 b = ⟨b, 0, 1⟩`, including at `(0, 0)`, and `extendedGcd a 0 = ⟨a, 1, 0⟩` for `a ≠ 0`. Specify no coefficient minimality or symmetry. This is the standalone public API follow-up to [the review discussion on leanprover#15077](leanprover#15077 (comment)). Keep the UInt64 inverse integration out of this PR; it can use this API in a subsequent change. Leave mathlib's existing `xgcd`, `gcdA`, and `gcdB` names untouched. Add regression coverage for kernel and compiled evaluation, signed coefficient examples, zero inputs, a curated cross-product of arbitrary-precision inputs, long Fibonacci-driven Euclidean chains, and use of the public lemmas.
github-actions
Bot
added
the
toolchain-available
This PR accelerates compiled extended greatest-common-divisor computations while preserving the Lean definition’s exact coefficient choices. Borrow bignum inputs, use read-only stack views for scalar inputs, and move heap-sized outputs into Lean objects. Handle zero, equal, and 16-bit inputs directly, and provide an arbitrary-precision native fallback when GMP is disabled. Add exact extern/reference comparisons and compiled-caller coverage for coefficient ties, scalar and signed-integer boundaries, heap-sized outputs, long Euclidean chains, and retained operands.
Keep the existing copying allocation and result-conversion paths. Limit the extended-GCD extern to borrowed inputs, stack views, and fast paths; allocate its outputs without changing other arithmetic operations.
|
Do you have numbers and a use case showing that having the |
|
I measured the extern against the exact Lean body (
A concrete use case is modular inversion, as in mathlib’s |
This PR simplifies runtime support for Nat.extendedGcd by reusing its Lean implementation for small and exceptional inputs and for builds without GMP. Replace handwritten Euclidean loops with an exported Lean fallback, use ordinary mpz conversions for the GMP call, and test the fallback ownership convention with retained operands.
I've reduced the new C code from about 70 lines to 30, with ~1% slowdowns on large GMP workloads and larger losses on small inputs and some no-GMP cases. |
2 participants
This PR adds
Nat.extendedGcd, returning a gcd and signed Bézout coefficients together with correctness and simplification lemmas.Use a tail-recursive Lean definition and a GMP-backed extern with borrowed inputs and small-input fast paths. Preserve exact coefficient agreement, including zero and equal inputs, and provide a native fallback without GMP. Add
test_externand compiled-caller coverage for arbitrary-precision inputs, coefficient ties, allocation boundaries, and long Euclidean chains. Keep shared bignum allocation changes in #15162.Follow up on the review discussion on #15077; leave UInt64 inverse integration and mathlib's existing APIs unchanged.
🤖 prepared with codex