# Diviseurs

Definition divides n m := exists p, m = n*p.
Infix "|" := divides (at level 80).

un exemple concret

Lemma divides_11_165: divides 11 165.
Proof.
exists 15. easy.
Qed.

trois cas génériques

Lemma divides_1_n: forall n, 1|n.
Proof.
intros n.
exists n.
ring.
Qed.

Lemma divides_n_n: forall n, n|n.
Proof.
intros n.
exists 1.
ring.
Qed.

Lemma divides_n_0: forall n, n|0.
Proof.
intros n.
exists 0.
ring.
Qed.

lemmes généraux

Lemma divides_transitive: forall n m p, n|p -> p|m -> n|m.
Proof.
intros n m p.
intros Hnp Hpm.
destruct Hnp as [i Hi].
destruct Hpm as [j Hj].
exists (i*j).
rewrite Hj, Hi. ring.
Qed.

Lemma divides_mult_l: forall n m p, n|m -> n|m*p.
Proof. intros n m p [i Hi]. rewrite Hi. exists (i*p). ring. Qed.

Lemma divides_mult_r: forall n m p, n|m -> n|p*m.
Proof. intros n m p. rewrite Zmult_comm. apply divides_mult_l. Qed.

Lemma divides_plus: forall n m p, n|m -> n|p -> n|m+p.
Proof. intros n m p [i ->] [j ->]. exists (i+j). ring. Qed.

Lemma divides_minus: forall n m p, n|m -> n|p -> n|m-p.
Proof. intros n m p [i ->] [j ->]. exists (i-j). ring. Qed.

# PGCD

Définition: x est un pgcd de a et b si c'est un diviseur commun de a et b, et s'il divise tout diviseur commun de a et b

Definition is_pgcd a b x := x|a /\ x|b /\ forall y, y|a -> y|b -> y|x.

un exemple concret

Lemma is_pgcd_27_36_9: is_pgcd 27 36 9.
Proof.
split. exists 3; reflexivity.
split. exists 4; reflexivity.
intros y [i Hi] [j Hj].
change 9 with (36-27). rewrite Hi, Hj.
auto using divides_minus, divides_mult_l, divides_n_n.
Qed.

trois cas génériques

Lemma is_pgcd_0: forall a, is_pgcd a 0 a.
Proof.
intros a.
split. apply divides_n_n.
split. apply divides_n_0.
intros b [i ->] _. apply divides_mult_l, divides_n_n.
Qed.

Lemma is_pgcd_1: forall a, is_pgcd a 1 1.
Proof.
intros a.
split. apply divides_1_n.
split. apply divides_1_n.
easy.
Qed.

Lemma is_pgcd_idem: forall a, is_pgcd a a a.
Proof.
intros a.
split. apply divides_n_n.
split. apply divides_n_n.
easy.
Qed.

# Algorithme d'Euclide étendu

Pour calculer le pgcd et les coefficients de Bézout (cf. wikipedia):
• on calcule une suite de triplets (r{i},u{i},v{i}) par une récurrence de rang 2:
• r{i+1} = r{i-1} mod r{i}
• u{i+1} = u{i-1} - (r{i-1} ÷ r{i}) * u{i}
• v{i+1} = v{i-1} - (r{i-1} ÷ r{i}) * v{i}
• on part de
• r{0} = a, u{0} = 1, v{0} = 0
• r{1} = b, u{1} = 0, v{1} = 1
• on s'arrête quand r{i} = 0: on a alors pgcd(a,b) = r{i-1} = a*u{i-1} + b*v{i-1}
Dans la fonction suivante,
• r,u,v sont les termes de rang {i-1};
• r',u',v' sont les termes de rang {i}.
On s'arrête si r'=0; sinon, on calcule la division euclidienne de r par r':
• q = r ÷ r'
• t = r mod r'
et continue en décalant les indices et en utilisant le schéma de récurrence indiqué ci-dessus.
Function Euclid (r u v r' u' v': Z) {measure Zabs_nat r'}: Z*Z*Z :=
if Zeq_bool r' 0 then (r,u,v) else
let (q,t) := Zdiv_eucl r r' in
Euclid r' u' v' t (u-q*u') (v-q*v').

la preuve suivante correspond à la terminaison de l'algorithme: la valeur absolue du reste (r') décroit strictement
Proof.
intros r _ _ r' _ _ Hr' q t Hqt.
apply Zeq_bool_neq in Hr'.
apply (Z_div_mod_full r r') in Hr'. rewrite Hqt in Hr'. clear Hqt.
apply proj2, Remainder_equiv in Hr' as [H _].
rewrite <-(Zabs_nat_Zabs t), <-(Zabs_nat_Zabs r').
apply Zabs_nat_lt. auto using Zabs_pos.
Defined.

le pgcd s'obtient en démarrant l'algorithme avec les bonnes valeurs

Definition pgcd a b := let '(p,_,_) := Euclid a 1 0 b 0 1 in p.

on peut vérifier que cette fonction retourne les bons résultats sur quelques exemples

Compute pgcd 27 36.
Compute pgcd 36 555.
Compute pgcd (2*3*5*7*11*13*17) 103.

# Preuve de correction de l'algorithme étendu

Lemma Euclid_spec: forall a b r u v r' u' v',

on démontre un invariant sur les termes de la suite
r = a*u + b*v ->
r' = a*u' + b*v' ->
spec3
(fun r'' u'' v'' => r'' = a*u''+b*v'' /\ r'' | r' /\ r'' | r)
(Euclid r u v r' u' v').
Proof.
intros a b r u v r' u' v'.
functional induction (Euclid r u v r' u' v')
as [?????? H|?????? H q t Hdiv IH]; intros Hr Hr'.
apply Zeq_bool_eq in H. split.
split. apply Hr.
split. rewrite H. apply divides_n_0.
apply divides_n_n.

apply Zeq_bool_neq, (Z_div_mod_full r r') in H.
rewrite Hdiv in H. clear Hdiv. destruct H as [Ht _].
case IH; clear IH.
assumption.
apply Zplus_minus_eq in Ht. rewrite Ht, Hr, Hr'. ring.
intros r'' u'' v'' [IH1 [IH2 IH3]]. split.
rewrite Ht. auto using divides_plus, divides_mult_l.
Qed.

On en déduit que la fonction pgcd renvoie bien le pgcd

Theorem pgcd_spec: forall a b, is_pgcd a b (pgcd a b).
Proof.
intros a b. unfold pgcd. case (Euclid_spec a b). ring. ring.
intros r u v [-> [Hra Hrb]].
unfold is_pgcd. auto using divides_plus, divides_mult_l.
Qed.

# Théorème de Bachet-Bézout

Theorem Bachet_Bezout: forall a b, exists u, exists v, a*u+b*v = pgcd a b.
Proof.
intros a b. unfold pgcd. case (Euclid_spec a b). ring. ring.
intros r u v [-> _]. exists u, v. easy.
Qed.

# Théorème de Gauss

Theorem Gauss: forall a b c, pgcd a b = 1 -> a|b*c -> a|c.
Proof.
intros a b c H [i Hi].
destruct (Bachet_Bezout a b) as (u&v&H'). rewrite H in H'.
exists (u*c+v*i).
transitivity (c*(a*u+b*v)).
rewrite H'. ring.
transitivity (c*a*u+b*c*v).
ring.
rewrite Hi. ring.
Qed.