Email Gateway (Nov 21 2022 at 12:19): Email Gateway (Nov 21 2022 at 12:19):From: Stepan Holub <holubstep@gmail.com>
Hello,
for some reason, I need to characterize all solutions of the Bezout-like
equation
ax + by = c
in nat. That is, no subtraction, no negative numbers.
Here, is the report on the outcome, in case it is of a general interest,
or in case it duplicates some existing work.
It can be seen as na extension of bezw from GCD.thy, in particular, of
‹Versions of Bezout for ‹nat›, by Amine Chaieb.›
We define a division of /c/ by /a/ modulo /b/ constructively as follows
definition div_mod
where "div_mod c a b =
(let b' = b div gcd a b;
a' = a div gcd a b;
c' = c div gcd a b
in
nat (int c' * fst (bezw a' b') mod int b')
)
"
Its desired property, if the necessary condition is satisfied, is
captured by the introduction rule:
lemma div_modI: assumes "gcd a b dvd c"
shows "a * div_mod c a b mod b = c mod b"
sorry
and its minimality:
lemma div_mod_min: assumes "a * x mod b = c mod b"
shows "a * div_mod c a b mod b = c mod b" and
"div_mod c a b ≤ x"
sorry
For non-zero b, the value satisfies the following bound:
lemma div_mod_bound: assumes "b ≠ 0" shows "div_mod c a b < b div gcd a b"
sorry
For b = 0 we get the standard division:
lemma div_mod_zero: assumes "b = 0" shows "div_mod c a b = c div a"
sorry
and division by zero is zero, as usual,
lemma div_mod_zero': assumes "a = 0" shows "div_mod c a b = 0"
Back to the original motivation, we now have the following
characterization of solvability:
lemma bezout_nat_solution_test: "(∃ x y. ax + by = (c:: nat)) ⟷ (gcd a
b) dvd c ∧ a * div_mod c a b ≤ c"
sorry
A solution can be easily obtained
fun solve_bezout_nat :: "nat ⇒ nat ⇒ nat ⇒ nat * nat"
where "solve_bezout_nat a b c = (div_mod c a b, (c - a*div_mod c a
b) div b)"
with verification:
lemma solve_bezout_nat_correct: assumes "(gcd a b) dvd c" and "a *
div_mod c a b ≤ c"
shows "a * fst (solve_bezout_nat a b c) + b * snd (solve_bezout_nat a
b c) = c"
(is "a * ?x + b * ?y = c")
sorry
Best regards
Stepan
Last updated: Jan 04 2025 at 20:18 UTC