Primes

Petits exemples sur les nombres premiers

Définition: un nombre p est premier s'il est plus grand que 1 et s'il n'est divisible par aucun nombre strictement compris entre 1 et p

Definition prime p := p >1 /\ forall n, 1<n <p -> p mod n > 0.

exemples de nombres premiers

Lemma prime_2: prime 2.
Proof.
split. easy.
intros n H. in_seq H.

1<n<2 est impossible

Qed.

Lemma prime_3: prime 3.
Proof.
split. easy.
intros n H. in_seq H.

1<n<3 implique n=2

  rewrite H. compute. easy.
Qed.

Lemma prime_5: prime 5.
Proof.
  split. easy.
  intros n H. in_seq H.
   rewrite H. easy.

n=2

rewrite H. easy.

n=3

rewrite H. easy.

n=4

Qed.

exemples de nombres non premiers

Lemma prime_6: prime 6.
Proof.
  split. easy.
  intros n H. in_seq H; rewrite H.
  Fail easy.

6 mod 2 = 0

  compute.
Abort.

Lemma not_prime_6: ~ prime 6.
Proof.
  intros [_ H].
  specialize (H 2).
  discriminate H.
  easy.
Qed.

pour des nombres plus grands, il faut utiliser des "tacticielles"

Lemma prime_7: prime 7.
Proof.
split. easy.
intros n H.

le point virgule permet d'enchaîner les séquences de preuve

in_seq H; rewrite H; easy.
Qed.

on peut faire un raccourci pour la séquence entière de tactiques:

Ltac prove_prime :=
split; [easy | intros n H; in_seq H; rewrite H; try easy ].

Lemma prime_61: prime 61.
Proof.
prove_prime.
Qed.

évidement la tactique échoue sur les nombres non premiers

Lemma prime_20: prime 20.
Proof.
prove_prime.
Abort.

This page has been generated by coqdoc