Document présentant la preuve.
Théorie Isabelle de cette preuve :
section ‹ Introduction ›
text ‹
This Isabelle theory presents a proof of the equivalence of the \emph{natural} definition
of the Greatest Common Divisor for integers (as a common divisor that is greater than all
other common divisors),
and the definition on rings (as a common divisor that is divided by all other common divisors).
We finally show the equivalence between our definitions of the GCD using predicates, and the
functional definition in Isabelle, which relies on Euclid's algorithm.
›
theory IntGCD
imports Main
begin
section ‹ Common divisors ›
text ‹
We define a predicate for characterizing common divisors of two integers, and prove some
theorems that will be needed for proving properties of the GCD.
›
definition common_div :: ‹int ⇒ int ⇒ int ⇒ bool›
where
‹common_div a b p ≡ p dvd a ∧ p dvd b›
lemma common_div_comm:
‹common_div a b p = common_div b a p›
using common_div_def by blast
text ‹
Two integers have 0 as common divisor only if one of them is 0:
›
lemma cdiv_0: ‹common_div a b 0 ⟷ a = 0 ∧ b = 0›
using common_div_def by simp
text ‹
Common divisors are not changed by absolute values:
›
theorem common_div_abs:
‹common_div a b d = common_div ¦a¦ ¦b¦ d›
using common_div_def by simp
text ‹
The common divisors of \(a\) and \(b\) are the common divisors of \(a-b\) and \(b\).
This theorem is the basis of the proof of the equivalence of the two definitions of the GCD.
›
lemma common_div_ab_dir:
assumes ‹common_div a b p›
shows ‹common_div (a - b) b p›
proof -
from assms and dvd_def
obtain ka where ‹a = p * ka› unfolding common_div_def by blast
moreover from assms and dvd_def
obtain kb where ‹b = p * kb› unfolding common_div_def by blast
ultimately have ‹a - b = (ka - kb) * p› by algebra
hence ‹p dvd (a - b)› by simp
moreover from assms have ‹p dvd b› using common_div_def by simp
ultimately show ?thesis using common_div_def by simp
qed
lemma common_div_ab_rev:
assumes ‹common_div (a - b) b p›
shows ‹common_div a b p›
proof -
from assms and dvd_def
obtain ka where ‹(a - b) = p * ka› unfolding common_div_def by blast
moreover from assms and dvd_def
obtain kb where ‹b = p * kb› unfolding common_div_def by blast
ultimately have ‹a = (ka + kb) * p› by algebra
hence ‹p dvd a› by simp
moreover from assms have ‹p dvd b› using common_div_def by simp
ultimately show ?thesis using common_div_def by simp
qed
theorem common_div_ab:‹common_div a b p = common_div (a - b) b p›
using common_div_ab_dir and common_div_ab_rev by blast
theorem common_div_ba:‹common_div a b p = common_div a (b - a) p›
using common_div_ab and common_div_comm by simp
section ‹ Greatest common divisor, defined on order ›
text ‹
Here we define the greatest common divisor using the order on integers.
We define a predicate for identifying upper bounds of all common divisors:
›
definition no_greater_div :: ‹int ⇒ int ⇒ int ⇒ bool›
where
‹no_greater_div a b g ≡ ∀p. common_div a b p ⟶ p ≤ g›
text ‹
Such an upper bound is always strictly positive:
›
lemma greater_div_pos: ‹no_greater_div a b g ⟹ g > 0›
proof -
assume h:‹no_greater_div a b g›
have ‹1 dvd a› by simp
moreover have ‹1 dvd b› by simp
ultimately have ‹common_div a b 1› using common_div_def by simp
with h have ‹g ≥ 1› using no_greater_div_def by simp
thus ?thesis by simp
qed
theorem greater_div_abs:
‹no_greater_div a b g = no_greater_div ¦a¦ ¦b¦ g›
proof
assume h:‹no_greater_div a b g›
{
fix p assume ‹common_div ¦a¦ ¦b¦ p›
with common_div_abs have ‹common_div a b p› by simp
with h have ‹p ≤ g› using no_greater_div_def by simp
}
thus ‹no_greater_div ¦a¦ ¦b¦ g› using no_greater_div_def by simp
next
assume h:‹no_greater_div ¦a¦ ¦b¦ g›
{
fix p assume ‹common_div a b p›
with common_div_abs have ‹common_div ¦a¦ ¦b¦ p› by simp
with h have ‹p ≤ g› using no_greater_div_def by simp
}
thus ‹no_greater_div a b g› using no_greater_div_def by simp
qed
text ‹
The GCD is a common divisor which is an upper bound of the common divisors:
›
definition is_gcd :: ‹int ⇒ int ⇒ int ⇒ bool›
where
‹is_gcd a b g ≡ common_div a b g ∧ no_greater_div a b g›
text ‹
We now derive properties of the GCD from properties of divisors.
›
lemma gcd_comm: ‹is_gcd a b g = is_gcd b a g›
using is_gcd_def and common_div_def and no_greater_div_def by auto
lemma gcd_pos: ‹is_gcd a b g ⟹ g > 0›
using is_gcd_def and greater_div_pos by blast
lemma gcd_neq_zero:
assumes ‹is_gcd a b g›
shows ‹g ≠ 0›
using gcd_pos[OF assms] by simp
lemma gcd_a0:
assumes ‹a ≠ 0›
shows ‹is_gcd a 0 ¦a¦›
proof -
from dvd_imp_le_int[OF assms] have ‹∀p. p dvd a ∧ p dvd 0 ⟶ ¦p¦ ≤ ¦a¦›
by simp
hence ‹no_greater_div a 0 ¦a¦› unfolding no_greater_div_def and common_div_def
by auto
thus ?thesis using abs_div is_gcd_def common_div_def by simp
qed
lemma gcd_0b:
assumes ‹b ≠ 0›
shows ‹is_gcd 0 b ¦b¦›
using assms and gcd_a0 and gcd_comm by auto
lemma gcd_self:
assumes ‹a ≠ 0›
shows ‹is_gcd a a ¦a¦›
proof -
from dvd_imp_le_int[OF assms] have ‹∀p. p dvd a ∧ p dvd a ⟶ ¦p¦ ≤ ¦a¦›
by simp
hence ‹no_greater_div a a ¦a¦› unfolding no_greater_div_def and common_div_def
by auto
moreover from abs_div have ‹common_div a a ¦a¦› using common_div_def by simp
ultimately show ?thesis using is_gcd_def by simp
qed
lemma gcd_abs:
‹is_gcd a b g = is_gcd ¦a¦ ¦b¦ g›
using is_gcd_def and common_div_abs and greater_div_abs by simp
theorem gcd_ab:‹is_gcd a b g = is_gcd (a - b) b g›
using is_gcd_def no_greater_div_def common_div_ab by simp
theorem gcd_ba:‹is_gcd a b g = is_gcd a (b - a) g›
using gcd_ab and gcd_comm by simp
text ‹
With the definition of the GCD based on the order on integers, the GCD is unique.
›
lemma gcd_unique:
assumes ‹is_gcd a b g›
and ‹is_gcd a b g'›
shows ‹g = g'›
proof -
from assms(1) have ‹∀p. common_div a b p ⟶ p ≤ g›
using is_gcd_def and no_greater_div_def by simp
moreover from assms(2) have ‹common_div a b g'›
using is_gcd_def by simp
ultimately have 1:‹g' ≤ g› by simp
from assms(2) have ‹∀p. common_div a b p ⟶ p ≤ g'›
using is_gcd_def and no_greater_div_def by simp
moreover from assms(1) have ‹common_div a b g› using is_gcd_def by simp
ultimately have 2:‹g ≤ g'› by simp
from 1 and 2 show ?thesis by simp
qed
section ‹ Greatest common divisor, ring definition ›
text ‹
We now define the greatest common divisor as one which is divided by all other common divisors.
We keep the positive one, so that this definition match the previous one.
›
definition is_gcd_div :: ‹int ⇒ int ⇒ int ⇒ bool›
where
‹is_gcd_div a b g ≡ (g > 0) ∧ common_div a b g
∧ (∀p. common_div a b p ⟶ p dvd g)›
text ‹
With this definition, the GCD cannot be null. Although the GCD of 0 and 0 is 0 using the ring
definition of the GCD, this makes no sense with regard to the definition based on the order on
integers: any integer is a common divisor of 0 and 0, so there is no greatest one.
›
lemma gcd_div_neq_zero:‹is_gcd_div a b g ⟹ g ≠ 0›
using is_gcd_div_def by simp
section ‹ Proof of the equivalence of the two definitions ›
text ‹
We can now show that both definitions of the GCD are equivalent.
Showing that being the GCD with the ring definition implies being the GCD
with the order definition is straightforward:
›
lemma gcd_div_inf:
assumes ‹is_gcd_div a b g›
shows ‹is_gcd a b g›
proof -
from assms have 1:‹common_div a b g› using is_gcd_div_def by simp
from assms have 2:‹∀p. common_div a b p ⟶ p dvd g›
using is_gcd_div_def by simp
from assms have 3:‹g > 0› using is_gcd_div_def by simp
have ‹∀p. common_div a b p ⟶ p ≤ g›
proof -
{
fix p assume h:‹common_div a b p›
with 2 have dp:‹p dvd g› by simp
from 3 have ‹¦g¦ = g› and ‹g ≠ 0› by simp+
with zdvd_imp_le[OF dp] have ‹p ≤ g› by simp
}
thus ?thesis by auto
qed
thus ?thesis using 1 and is_gcd_def and no_greater_div_def by simp
qed
text ‹
The other way is more difficult. We use induction on natural numbers with an upper bound on
the sum of the absolute values, and use the fact that @{prop ‹is_gcd (a - b) b g = is_gcd a b g›}
›
lemma cdiv_div_gcd:
‹(¦a¦ + ¦b¦ > 0) ∧ (nat (¦a¦ + ¦b¦) ≤ Suc n) ∧ is_gcd ¦a¦ ¦b¦ g
⟹ (∀p. common_div ¦a¦ ¦b¦ p ⟶ p dvd g)›
proof (induction n arbitrary: a b)
case 0
hence pos:‹¦a¦ + ¦b¦ > 0›
and leq1:‹¦a¦ + ¦b¦ ≤ 1›
and gcd:‹is_gcd ¦a¦ ¦b¦ g› by auto
show ?case
proof (cases ‹a = 0›)
case True (* a = 0 *)
with leq1 and pos have ‹¦b¦ = 1› by simp
moreover with this have ‹g = 1›
using gcd_0b[of ‹¦b¦›] and `a = 0` and gcd and gcd_unique by simp
ultimately show ?thesis using common_div_def by simp
next
case False (* a ≠ 0 *)
with leq1 have ‹¦a¦ = 1› and ‹b = 0› by auto
moreover with this have ‹g = 1›
using gcd_a0[of ‹¦a¦›] and `¬a = 0` and gcd and gcd_unique by simp
ultimately show ?thesis using common_div_def by simp
qed
next
case (Suc k)
from Suc.prems have
1:‹nat (¦a¦ + ¦b¦) ≤ Suc (Suc k)› and
2:‹is_gcd ¦a¦ ¦b¦ g› and 3:‹¦a¦ + ¦b¦ > 0› by auto
show ?case
proof (cases ‹nat (¦a¦ + ¦b¦) ≤ Suc k›)
case True
thus ?thesis using Suc.IH and 2 and 3 by simp
next
case False
with 1 have ab:‹nat (¦a¦ + ¦b¦) = Suc (Suc k)› by simp
show ?thesis
proof (cases ‹¦a¦ ≥ ¦b¦›)
case True (* ¦a¦ ≥ ¦b¦ *)
show ?thesis
proof (cases ‹¦b¦ = 0›)
case True (* ¦b¦ = 0 *)
with ab have ‹¦a¦ ≠ 0› by simp
with `¦b¦ = 0` and 2 and gcd_a0[of ‹¦a¦›] and gcd_unique
have ‹g = ¦a¦› by simp
thus ?thesis using common_div_def by simp
next
case False (* ¦b¦ ≠ 0 *)
with ab have ‹nat (¦a¦ - ¦b¦ + ¦b¦) ≤ Suc k›
using `¦a¦ ≥ ¦b¦` by simp
moreover from 2 and gcd_ab have ‹is_gcd (¦a¦ - ¦b¦) ¦b¦ g›
by simp
moreover from `¦b¦ ≠ 0` and `¦a¦ ≥ ¦b¦` have ‹¦a¦ + ¦b¦ - ¦b¦ > 0›
by simp
ultimately show ?thesis
using Suc.IH[of ‹¦a¦ - ¦b¦› ‹¦b¦›] and `¦a¦ ≥ ¦b¦` and common_div_ab
by simp
qed
next
case False (* ¦a¦ < ¦b¦ *)
show ?thesis
proof (cases ‹¦a¦ = 0›)
case True
with ab have ‹¦b¦ ≠ 0› by simp
with True and 2 and gcd_0b[of ‹¦b¦›] and gcd_unique
have ‹g = ¦b¦› by simp
thus ?thesis using common_div_def by simp
next
case False
with ab have ‹nat (¦a¦ + ¦b¦ - ¦a¦) ≤ Suc k›
using `¬ ¦a¦ ≥ ¦b¦` by simp
moreover from 2 and `¬ ¦a¦ ≥ ¦b¦` and gcd_ba
have ‹is_gcd ¦a¦ (¦b¦ - ¦a¦) g› by simp
moreover from `¦a¦ ≠ 0` and `¬ ¦a¦ ≥ ¦b¦`
have ‹¦a¦ + ¦b¦ - ¦a¦ > 0› by simp
ultimately show ?thesis
using Suc.IH[of ‹¦a¦› ‹¦b¦ - ¦a¦›] and `¬ ¦a¦ ≥ ¦b¦`
and common_div_ba by simp
qed
qed
qed
qed
text ‹
We can now remove the condition used to make the induction on \(n\):
›
lemma common_div_gcd:
assumes ‹a ≠ 0 ∨ b ≠ 0›
and ‹is_gcd ¦a¦ ¦b¦ g›
shows ‹(∀p. common_div ¦a¦ ¦b¦ p ⟶ p dvd g)›
proof -
from assms(1) have 1:‹¦a¦ + ¦b¦ > 0› by auto
have ‹nat (¦a¦ + ¦b¦) ≤ Suc (nat (¦a¦ + ¦b¦))› by simp
with assms and 1 have
‹(¦a¦ + ¦b¦ > 0) ∧ (nat (¦a¦ + ¦b¦) ≤ Suc (nat (¦a¦ + ¦b¦))) ∧ is_gcd ¦a¦ ¦b¦ g›
by blast
from cdiv_div_gcd[OF this] show ?thesis .
qed
text ‹
Therefore, we have the equivalence of the two definitions when \(a\) and \(b\) are not both null:
›
lemma gcd_inf_div:
assumes ‹is_gcd a b g›
and ‹a ≠ 0 ∨ b ≠ 0›
shows ‹is_gcd_div a b g›
proof -
from assms(1) have ‹is_gcd ¦a¦ ¦b¦ g› using gcd_abs by simp
with assms(2) and common_div_gcd
have ‹(∀p. common_div ¦a¦ ¦b¦ p ⟶ p dvd g)› by simp
hence ‹(∀p. common_div a b p ⟶ p dvd g)› using common_div_abs by simp
moreover from assms(1) have ‹common_div a b g› using is_gcd_def by simp
moreover from assms(1) have ‹g > 0› using gcd_pos by simp
ultimately show ?thesis using is_gcd_div_def by simp
qed
theorem gcd_inf_div_eq:
assumes ‹a ≠ 0 ∨ b ≠ 0›
shows ‹is_gcd a b g = is_gcd_div a b g›
using assms and gcd_div_inf and gcd_inf_div by blast
text ‹
The condition on the simultaneous nullity of \(a\) and \(b\) comes from the fact that
there is no GCD of 0 and 0 with the definiton based on the order on integers:
›
lemma any_common_div_0:‹common_div 0 0 d›
proof -
have ‹d dvd 0› by simp
thus ?thesis using common_div_def by simp
qed
theorem ‹¬(∃g. no_greater_div 0 0 g)›
proof
assume ‹∃g. no_greater_div 0 0 g›
from this obtain g where ngd:‹no_greater_div 0 0 g› by blast
from any_common_div_0[of ‹g+1›] have ‹common_div 0 0 (g+1)› .
with ngd have ‹g+1 ≤ g› using no_greater_div_def by blast
thus False by simp
qed
text ‹
Finally, we prove that our definition of the GCD matches the definition
of the \(\mathop{gcd}\) function in Isabelle.
›
lemma gcdfunc_imp_gcd_div:
assumes ‹a ≠ 0 ∨ b ≠ 0›
and ‹g = gcd a b›
shows ‹is_gcd_div a b g›
using assms common_div_def is_gcd_div_def by auto
theorem gcd_func_is_gcd_div:
assumes ‹a ≠ 0 ∨ b ≠ 0›
shows ‹(g = gcd a b) = is_gcd_div a b g›
proof
assume ‹is_gcd_div a b g›
hence h:‹is_gcd a b g› using gcd_inf_div_eq[OF assms] by simp
let ?g' = ‹gcd a b›
from assms and gcdfunc_imp_gcd_div have ‹is_gcd_div a b ?g'› by simp
hence ‹is_gcd a b ?g'› using gcd_inf_div_eq[OF assms] by simp
from gcd_unique[OF this h] show ‹g = ?g'› ..
qed (simp add: gcdfunc_imp_gcd_div[OF assms])
end