Coprime.v 1.8 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below    *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
Require int.ComputerDivision.
Require number.Parity.
Require number.Divisibility.
Require number.Gcd.
Require number.Prime.

(* Why3 assumption *)
Definition coprime (a:Z) (b:Z): Prop := ((number.Gcd.gcd a b) = 1%Z).

Lemma coprime_is_Zrel_prime :
  forall a b, coprime a b <-> Znumtheory.rel_prime a b.
intros.
unfold coprime.
unfold Znumtheory.rel_prime.
split; intro h.
rewrite <- h; apply Znumtheory.Zgcd_is_gcd.
apply Znumtheory.Zis_gcd_gcd; auto with zarith.
Qed.

(* Why3 goal *)
Lemma prime_coprime : forall (p:Z), (number.Prime.prime p) <->
  ((2%Z <= p)%Z /\ forall (n:Z), ((1%Z <= n)%Z /\ (n < p)%Z) -> (coprime n
  p)).
intros p.
(*
Znumtheory.prime_intro:
  forall p : int,
  (1 < p)%Z ->
  (forall n : int, (1 <= n < p)%Z -> Znumtheory.rel_prime n p) ->
  Znumtheory.prime p
*)
rewrite Prime.prime_is_Zprime.
split.
intro h; inversion h; clear h.
split; auto with zarith.
intros n h.
rewrite coprime_is_Zrel_prime.
apply H0; auto.
intros (h1,h2).
constructor; auto with zarith.
intros n h.
rewrite <- coprime_is_Zrel_prime.
apply h2; auto.
Qed.

(* Why3 goal *)
Lemma Gauss : forall (a:Z) (b:Z) (c:Z), ((number.Divisibility.divides a
  (b * c)%Z) /\ (coprime a b)) -> (number.Divisibility.divides a c).
intros a b c (h1,h2).
apply Znumtheory.Gauss with b; auto.
rewrite <- coprime_is_Zrel_prime; auto.
Qed.

(* Why3 goal *)
Lemma Euclid : forall (p:Z) (a:Z) (b:Z), ((number.Prime.prime p) /\
  (number.Divisibility.divides p (a * b)%Z)) -> ((number.Divisibility.divides
  p a) \/ (number.Divisibility.divides p b)).
intros p a b (h1,h2).
apply Znumtheory.prime_mult; auto.
now rewrite <- Prime.prime_is_Zprime.
Qed.
69