Commit dfce1fb3 authored by MARCHE Claude's avatar MARCHE Claude

One more lemma in number.Coprime, finished example gcd.mlw

parent 91427594
...@@ -56,6 +56,8 @@ module BinaryGcd ...@@ -56,6 +56,8 @@ module BinaryGcd
lemma odd1: forall n: int. 0 <= n -> not (even n) <-> n = 2 * div n 2 + 1 lemma odd1: forall n: int. 0 <= n -> not (even n) <-> n = 2 * div n 2 + 1
lemma div_nonneg: forall n: int. 0 <= n -> 0 <= div n 2 lemma div_nonneg: forall n: int. 0 <= n -> 0 <= div n 2
use number.Coprime
lemma gcd_even_even: forall u v: int. 0 <= v -> 0 <= u -> lemma gcd_even_even: forall u v: int. 0 <= v -> 0 <= u ->
gcd (2 * u) (2 * v) = 2 * gcd u v gcd (2 * u) (2 * v) = 2 * gcd u v
lemma gcd_even_odd: forall u v: int. 0 <= v -> 0 <= u -> lemma gcd_even_odd: forall u v: int. 0 <= v -> 0 <= u ->
...@@ -64,9 +66,11 @@ module BinaryGcd ...@@ -64,9 +66,11 @@ module BinaryGcd
even u -> odd v -> gcd u v = gcd (div u 2) v even u -> odd v -> gcd u v = gcd (div u 2) v
lemma odd_odd_div2: forall u v: int. 0 <= v -> 0 <= u -> lemma odd_odd_div2: forall u v: int. 0 <= v -> 0 <= u ->
div ((2*u+1) - (2*v+1)) 2 = u - v div ((2*u+1) - (2*v+1)) 2 = u - v
lemma gcd_odd_odd: forall u v: int. 0 <= v -> 0 <= u -> lemma gcd_odd_odd_aux: forall u v: int. 0 <= v <= u ->
gcd (2 * u + 1) (2 * v + 1) = gcd ((2*u+1) - 1*(2*v+1)) (2 * v + 1)
lemma gcd_odd_odd: forall u v: int. 0 <= v <= u ->
gcd (2 * u + 1) (2 * v + 1) = gcd (u - v) (2 * v + 1) gcd (2 * u + 1) (2 * v + 1) = gcd (u - v) (2 * v + 1)
lemma gcd_odd_odd2: forall u v: int. 0 <= v -> 0 <= u -> lemma gcd_odd_odd2: forall u v: int. 0 <= v <= u ->
odd u -> odd v -> gcd u v = gcd (div (u - v) 2) v odd u -> odd v -> gcd u v = gcd (div (u - v) 2) v
let rec binary_gcd (u v: int) : int let rec binary_gcd (u v: int) : int
......
(* This file is generated by Why3's Coq 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.
Require number.Coprime.
(* Why3 assumption *)
Definition unit := unit.
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
(* Why3 assumption *)
Definition lt_nat (x:Z) (y:Z): Prop := (0%Z <= y)%Z /\ (x < y)%Z.
(* Why3 assumption *)
Inductive lex: (Z* Z)%type -> (Z* Z)%type -> Prop :=
| Lex_1 : forall (x1:Z) (x2:Z) (y1:Z) (y2:Z), (lt_nat x1 x2) -> (lex (x1,
y1) (x2, y2))
| Lex_2 : forall (x:Z) (y1:Z) (y2:Z), (lt_nat y1 y2) -> (lex (x, y1) (x,
y2)).
Axiom even1 : forall (n:Z), (0%Z <= n)%Z -> ((number.Parity.even n) <->
(n = (2%Z * (ZArith.BinInt.Z.quot n 2%Z))%Z)).
Axiom odd1 : forall (n:Z), (0%Z <= n)%Z -> ((~ (number.Parity.even n)) <->
(n = ((2%Z * (ZArith.BinInt.Z.quot n 2%Z))%Z + 1%Z)%Z)).
Axiom div_nonneg : forall (n:Z), (0%Z <= n)%Z ->
(0%Z <= (ZArith.BinInt.Z.quot n 2%Z))%Z.
Axiom gcd_even_even : forall (u:Z) (v:Z), (0%Z <= v)%Z -> ((0%Z <= u)%Z ->
((number.Gcd.gcd (2%Z * u)%Z (2%Z * v)%Z) = (2%Z * (number.Gcd.gcd u
v))%Z)).
(* Why3 goal *)
Theorem gcd_even_odd : forall (u:Z) (v:Z), (0%Z <= v)%Z -> ((0%Z <= u)%Z ->
((number.Gcd.gcd (2%Z * u)%Z ((2%Z * v)%Z + 1%Z)%Z) = (number.Gcd.gcd u
((2%Z * v)%Z + 1%Z)%Z))).
(* Why3 intros u v h1 h2. *)
intros u v h1 h2.
rewrite Gcd.Comm.
rewrite number.Coprime.gcd_coprime.
now rewrite Gcd.Comm.
unfold Coprime.coprime.
rewrite <- Gcd.Gcd_computer_mod; auto with zarith.
rewrite ComputerDivision.Mod_mult; auto with zarith.
Qed.
This diff is collapsed.
...@@ -67,3 +67,21 @@ apply Znumtheory.prime_mult; auto. ...@@ -67,3 +67,21 @@ apply Znumtheory.prime_mult; auto.
now rewrite <- Prime.prime_is_Zprime. now rewrite <- Prime.prime_is_Zprime.
Qed. Qed.
(* Why3 goal *)
Lemma gcd_coprime : forall (a:Z) (b:Z) (c:Z), (coprime a b) ->
((number.Gcd.gcd a (b * c)%Z) = (number.Gcd.gcd a c)).
intros a b c h1.
apply Z.gcd_unique.
- apply Z.gcd_nonneg.
- apply Gcd.gcd_def1.
- apply Divisibility.divides_multl.
apply Gcd.gcd_def2.
- intros q h2 h3.
apply Gcd.gcd_def3.
trivial.
apply Gauss with b; split; auto.
rewrite coprime_is_Zrel_prime.
rewrite coprime_is_Zrel_prime in h1.
now apply Znumtheory.rel_prime_div with (2:=h2).
Qed.
...@@ -118,7 +118,6 @@ theory Gcd ...@@ -118,7 +118,6 @@ theory Gcd
clone algebra.AC with type t = int, function op = gcd, clone algebra.AC with type t = int, function op = gcd,
lemma Comm.Comm, lemma Assoc lemma Comm.Comm, lemma Assoc
(*** FIXME: Alt-Ergo proves gcd_0_pos even without gcd_unique *)
lemma gcd_0_pos: forall a: int. 0 <= a -> gcd a 0 = a lemma gcd_0_pos: forall a: int. 0 <= a -> gcd a 0 = a
lemma gcd_0_neg: forall a: int. a < 0 -> gcd a 0 = -a lemma gcd_0_neg: forall a: int. a < 0 -> gcd a 0 = -a
...@@ -196,5 +195,7 @@ theory Coprime ...@@ -196,5 +195,7 @@ theory Coprime
forall p a b:int. forall p a b:int.
prime p /\ divides p (a*b) -> divides p a \/ divides p b prime p /\ divides p (a*b) -> divides p a \/ divides p b
lemma gcd_coprime:
forall a b c. coprime a b -> gcd a (b*c) = gcd a c
end end
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment