Gauss

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.

This page has been generated by coqdoc