Email Gateway (Sep 30 2022 at 09:04): Email Gateway (Sep 30 2022 at 09:04):From: Stepan Holub <holub@karlin.mff.cuni.cz>
Hello,
is the following stronger version of GCD.bezout_nat of a general interest?
(Sub-question: is my use of arg_min combined with id a standard solution?)
lemma bezout_nat':
assumes "(a :: nat) ≠ 0"
shows "∃x y. a * x = b * y + c * gcd a b ∧ y < a"
proof-
let ?P = "(λ y. ∃ x. a * x = b * y + c * gcd a b)"
define ymin where "ymin = arg_min id ?P"
from bezout_nat[OF ‹a ≠ 0›]
obtain x' y' where "a * x' = b * y' + gcd a b"
by blast
hence eq': "a * (c*x') = b * (c*y') + c * gcd a b"
by algebra
with arg_min_natI[of ?P _ id, folded ymin_def]
obtain x where eq: "a * x = b * ymin + c * gcd a b"
by blast
have "ymin < a"
proof (rule ccontr)
assume "¬ ymin < a"
hence "a * (x - b) = b * (ymin - a) + c * gcd a b"
using eq by (simp add: diff_mult_distrib2 mult.commute)
with arg_min_nat_le[of ?P "ymin - a" id, folded ymin_def, unfolded
id_apply]
have "ymin ≤ ymin - a"
by blast
thus False
using ‹¬ ymin < a› ‹a ≠ 0›
by force
qed
then show ?thesis
using eq by blast
qed
Stepan
Email Gateway (Sep 30 2022 at 09:12):From: Manuel Eberl <manuel@pruvisto.org>
Looks sufficiently interesting to me, yes. I can put it into the
distribution later.
Using arg_min with id is a standard solution, but for "nat" you can also
use "Inf" or "Least". Not sure which is more convenient.
Incidentally, our "arg_min"/"arg_max" library is still somewhat
incomplete and could definitely use further development…
Manuel
Last updated: Apr 20 2024 at 08:16 UTC