diff options
Diffstat (limited to 'theories/ZArith')
| -rw-r--r-- | theories/ZArith/BinInt.v | 12 | ||||
| -rw-r--r-- | theories/ZArith/Int.v | 421 | ||||
| -rw-r--r-- | theories/ZArith/Zcompare.v | 2 | ||||
| -rw-r--r-- | theories/ZArith/Znumtheory.v | 454 |
4 files changed, 863 insertions, 26 deletions
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 02cf5f2d..fda521de 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -6,10 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: BinInt.v 6295 2004-11-12 16:40:39Z gregoire $ i*) +(*i $Id: BinInt.v 8883 2006-05-31 21:56:37Z letouzey $ i*) (***********************************************************) -(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) +(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) (***********************************************************) Require Export BinPos. @@ -703,6 +703,12 @@ Qed. (**********************************************************************) (** Properties of multiplication on binary integer numbers *) +Theorem Zpos_mult_morphism : + forall p q:positive, Zpos (p*q) = Zpos p * Zpos q. +Proof. +auto. +Qed. + (** One is neutral for multiplication *) Theorem Zmult_1_l : forall n:Z, Zpos 1 * n = n. @@ -935,6 +941,8 @@ Proof. intros; symmetry in |- *; apply Zmult_succ_l. Qed. + + (** Misc redundant properties *) Lemma Z_eq_mult : forall n m:Z, m = Z0 -> m * n = Z0. diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v new file mode 100644 index 00000000..cb51b9d2 --- /dev/null +++ b/theories/ZArith/Int.v @@ -0,0 +1,421 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(* Finite sets library. + * Authors: Pierre Letouzey and Jean-Christophe Filliâtre + * Institution: LRI, CNRS UMR 8623 - Université Paris Sud + * 91405 Orsay, France *) + +(* $Id: Int.v 8933 2006-06-09 14:08:38Z herbelin $ *) + +(** * An axiomatization of integers. *) + +(** We define a signature for an integer datatype based on [Z]. + The goal is to allow a switch after extraction to ocaml's + [big_int] or even [int] when finiteness isn't a problem + (typically : when mesuring the height of an AVL tree). +*) + +Require Import ZArith. +Require Import ROmega. +Delimit Scope Int_scope with I. + +Module Type Int. + + Open Scope Int_scope. + + Parameter int : Set. + + Parameter i2z : int -> Z. + Arguments Scope i2z [ Int_scope ]. + + Parameter _0 : int. + Parameter _1 : int. + Parameter _2 : int. + Parameter _3 : int. + Parameter plus : int -> int -> int. + Parameter opp : int -> int. + Parameter minus : int -> int -> int. + Parameter mult : int -> int -> int. + Parameter max : int -> int -> int. + + Notation "0" := _0 : Int_scope. + Notation "1" := _1 : Int_scope. + Notation "2" := _2 : Int_scope. + Notation "3" := _3 : Int_scope. + Infix "+" := plus : Int_scope. + Infix "-" := minus : Int_scope. + Infix "*" := mult : Int_scope. + Notation "- x" := (opp x) : Int_scope. + +(** For logical relations, we can rely on their counterparts in Z, + since they don't appear after extraction. Moreover, using tactics + like omega is easier this way. *) + + Notation "x == y" := (i2z x = i2z y) + (at level 70, y at next level, no associativity) : Int_scope. + Notation "x <= y" := (Zle (i2z x) (i2z y)): Int_scope. + Notation "x < y" := (Zlt (i2z x) (i2z y)) : Int_scope. + Notation "x >= y" := (Zge (i2z x) (i2z y)) : Int_scope. + Notation "x > y" := (Zgt (i2z x) (i2z y)): Int_scope. + Notation "x <= y <= z" := (x <= y /\ y <= z) : Int_scope. + Notation "x <= y < z" := (x <= y /\ y < z) : Int_scope. + Notation "x < y < z" := (x < y /\ y < z) : Int_scope. + Notation "x < y <= z" := (x < y /\ y <= z) : Int_scope. + + (** Some decidability fonctions (informative). *) + + Axiom gt_le_dec : forall x y: int, {x > y} + {x <= y}. + Axiom ge_lt_dec : forall x y : int, {x >= y} + {x < y}. + Axiom eq_dec : forall x y : int, { x == y } + {~ x==y }. + + (** Specifications *) + + (** First, we ask [i2z] to be injective. Said otherwise, our ad-hoc equality + [==] and the generic [=] are in fact equivalent. We define [==] + nonetheless since the translation to [Z] for using automatic tactic is easier. *) + + Axiom i2z_eq : forall n p : int, n == p -> n = p. + + (** Then, we express the specifications of the above parameters using their + Z counterparts. *) + + Open Scope Z_scope. + Axiom i2z_0 : i2z _0 = 0. + Axiom i2z_1 : i2z _1 = 1. + Axiom i2z_2 : i2z _2 = 2. + Axiom i2z_3 : i2z _3 = 3. + Axiom i2z_plus : forall n p, i2z (n + p) = i2z n + i2z p. + Axiom i2z_opp : forall n, i2z (-n) = -i2z n. + Axiom i2z_minus : forall n p, i2z (n - p) = i2z n - i2z p. + Axiom i2z_mult : forall n p, i2z (n * p) = i2z n * i2z p. + Axiom i2z_max : forall n p, i2z (max n p) = Zmax (i2z n) (i2z p). + +End Int. + +Module MoreInt (I:Int). + Import I. + + Open Scope Int_scope. + + (** A magic (but costly) tactic that goes from [int] back to the [Z] + friendly world ... *) + + Hint Rewrite -> + i2z_0 i2z_1 i2z_2 i2z_3 i2z_plus i2z_opp i2z_minus i2z_mult i2z_max : i2z. + + Ltac i2z := match goal with + | H : (eq (A:=int) ?a ?b) |- _ => + generalize (f_equal i2z H); + try autorewrite with i2z; clear H; intro H; i2z + | |- (eq (A:=int) ?a ?b) => apply (i2z_eq a b); try autorewrite with i2z; i2z + | H : _ |- _ => progress autorewrite with i2z in H; i2z + | _ => try autorewrite with i2z + end. + + (** A reflexive version of the [i2z] tactic *) + + (** this [i2z_refl] is actually weaker than [i2z]. For instance, if a + [i2z] is buried deep inside a subterm, [i2z_refl] may miss it. + See also the limitation about [Set] or [Type] part below. + Anyhow, [i2z_refl] is enough for applying [romega]. *) + + Ltac i2z_gen := match goal with + | |- (eq (A:=int) ?a ?b) => apply (i2z_eq a b); i2z_gen + | H : (eq (A:=int) ?a ?b) |- _ => + generalize (f_equal i2z H); clear H; i2z_gen + | H : (eq (A:=Z) ?a ?b) |- _ => generalize H; clear H; i2z_gen + | H : (Zlt ?a ?b) |- _ => generalize H; clear H; i2z_gen + | H : (Zle ?a ?b) |- _ => generalize H; clear H; i2z_gen + | H : (Zgt ?a ?b) |- _ => generalize H; clear H; i2z_gen + | H : (Zge ?a ?b) |- _ => generalize H; clear H; i2z_gen + | H : _ -> ?X |- _ => + (* A [Set] or [Type] part cannot be dealt with easily + using the [ExprP] datatype. So we forget it, leaving + a goal that can be weaker than the original. *) + match type of X with + | Type => clear H; i2z_gen + | Prop => generalize H; clear H; i2z_gen + end + | H : _ <-> _ |- _ => generalize H; clear H; i2z_gen + | H : _ /\ _ |- _ => generalize H; clear H; i2z_gen + | H : _ \/ _ |- _ => generalize H; clear H; i2z_gen + | H : ~ _ |- _ => generalize H; clear H; i2z_gen + | _ => idtac + end. + + Inductive ExprI : Set := + | EI0 : ExprI + | EI1 : ExprI + | EI2 : ExprI + | EI3 : ExprI + | EIplus : ExprI -> ExprI -> ExprI + | EIopp : ExprI -> ExprI + | EIminus : ExprI -> ExprI -> ExprI + | EImult : ExprI -> ExprI -> ExprI + | EImax : ExprI -> ExprI -> ExprI + | EIraw : int -> ExprI. + + Inductive ExprZ : Set := + | EZplus : ExprZ -> ExprZ -> ExprZ + | EZopp : ExprZ -> ExprZ + | EZminus : ExprZ -> ExprZ -> ExprZ + | EZmult : ExprZ -> ExprZ -> ExprZ + | EZmax : ExprZ -> ExprZ -> ExprZ + | EZofI : ExprI -> ExprZ + | EZraw : Z -> ExprZ. + + Inductive ExprP : Type := + | EPeq : ExprZ -> ExprZ -> ExprP + | EPlt : ExprZ -> ExprZ -> ExprP + | EPle : ExprZ -> ExprZ -> ExprP + | EPgt : ExprZ -> ExprZ -> ExprP + | EPge : ExprZ -> ExprZ -> ExprP + | EPimpl : ExprP -> ExprP -> ExprP + | EPequiv : ExprP -> ExprP -> ExprP + | EPand : ExprP -> ExprP -> ExprP + | EPor : ExprP -> ExprP -> ExprP + | EPneg : ExprP -> ExprP + | EPraw : Prop -> ExprP. + + (** [int] to [ExprI] *) + + Ltac i2ei trm := + match constr:trm with + | 0 => constr:EI0 + | 1 => constr:EI1 + | 2 => constr:EI2 + | 3 => constr:EI3 + | ?x + ?y => let ex := i2ei x with ey := i2ei y in constr:(EIplus ex ey) + | ?x - ?y => let ex := i2ei x with ey := i2ei y in constr:(EIminus ex ey) + | ?x * ?y => let ex := i2ei x with ey := i2ei y in constr:(EImult ex ey) + | max ?x ?y => let ex := i2ei x with ey := i2ei y in constr:(EImax ex ey) + | - ?x => let ex := i2ei x in constr:(EIopp ex) + | ?x => constr:(EIraw x) + end + + (** [Z] to [ExprZ] *) + + with z2ez trm := + match constr:trm with + | (?x+?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZplus ex ey) + | (?x-?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZminus ex ey) + | (?x*?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZmult ex ey) + | (Zmax ?x ?y) => let ex := z2ez x with ey := z2ez y in constr:(EZmax ex ey) + | (-?x)%Z => let ex := z2ez x in constr:(EZopp ex) + | i2z ?x => let ex := i2ei x in constr:(EZofI ex) + | ?x => constr:(EZraw x) + end. + + (** [Prop] to [ExprP] *) + + Ltac p2ep trm := + match constr:trm with + | (?x <-> ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPequiv ex ey) + | (?x -> ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPimpl ex ey) + | (?x /\ ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPand ex ey) + | (?x \/ ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPor ex ey) + | (~ ?x) => let ex := p2ep x in constr:(EPneg ex) + | (eq (A:=Z) ?x ?y) => let ex := z2ez x with ey := z2ez y in constr:(EPeq ex ey) + | (?x<?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPlt ex ey) + | (?x<=?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPle ex ey) + | (?x>?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPgt ex ey) + | (?x>=?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EPge ex ey) + | ?x => constr:(EPraw x) + end. + + (** [ExprI] to [int] *) + + Fixpoint ei2i (e:ExprI) : int := + match e with + | EI0 => 0 + | EI1 => 1 + | EI2 => 2 + | EI3 => 3 + | EIplus e1 e2 => (ei2i e1)+(ei2i e2) + | EIminus e1 e2 => (ei2i e1)-(ei2i e2) + | EImult e1 e2 => (ei2i e1)*(ei2i e2) + | EImax e1 e2 => max (ei2i e1) (ei2i e2) + | EIopp e => -(ei2i e) + | EIraw i => i + end. + + (** [ExprZ] to [Z] *) + + Fixpoint ez2z (e:ExprZ) : Z := + match e with + | EZplus e1 e2 => ((ez2z e1)+(ez2z e2))%Z + | EZminus e1 e2 => ((ez2z e1)-(ez2z e2))%Z + | EZmult e1 e2 => ((ez2z e1)*(ez2z e2))%Z + | EZmax e1 e2 => Zmax (ez2z e1) (ez2z e2) + | EZopp e => (-(ez2z e))%Z + | EZofI e => i2z (ei2i e) + | EZraw z => z + end. + + (** [ExprP] to [Prop] *) + + Fixpoint ep2p (e:ExprP) : Prop := + match e with + | EPeq e1 e2 => (ez2z e1) = (ez2z e2) + | EPlt e1 e2 => ((ez2z e1)<(ez2z e2))%Z + | EPle e1 e2 => ((ez2z e1)<=(ez2z e2))%Z + | EPgt e1 e2 => ((ez2z e1)>(ez2z e2))%Z + | EPge e1 e2 => ((ez2z e1)>=(ez2z e2))%Z + | EPimpl e1 e2 => (ep2p e1) -> (ep2p e2) + | EPequiv e1 e2 => (ep2p e1) <-> (ep2p e2) + | EPand e1 e2 => (ep2p e1) /\ (ep2p e2) + | EPor e1 e2 => (ep2p e1) \/ (ep2p e2) + | EPneg e => ~ (ep2p e) + | EPraw p => p + end. + + (** [ExprI] (supposed under a [i2z]) to a simplified [ExprZ] *) + + Fixpoint norm_ei (e:ExprI) : ExprZ := + match e with + | EI0 => EZraw (0%Z) + | EI1 => EZraw (1%Z) + | EI2 => EZraw (2%Z) + | EI3 => EZraw (3%Z) + | EIplus e1 e2 => EZplus (norm_ei e1) (norm_ei e2) + | EIminus e1 e2 => EZminus (norm_ei e1) (norm_ei e2) + | EImult e1 e2 => EZmult (norm_ei e1) (norm_ei e2) + | EImax e1 e2 => EZmax (norm_ei e1) (norm_ei e2) + | EIopp e => EZopp (norm_ei e) + | EIraw i => EZofI (EIraw i) + end. + + (** [ExprZ] to a simplified [ExprZ] *) + + Fixpoint norm_ez (e:ExprZ) : ExprZ := + match e with + | EZplus e1 e2 => EZplus (norm_ez e1) (norm_ez e2) + | EZminus e1 e2 => EZminus (norm_ez e1) (norm_ez e2) + | EZmult e1 e2 => EZmult (norm_ez e1) (norm_ez e2) + | EZmax e1 e2 => EZmax (norm_ez e1) (norm_ez e2) + | EZopp e => EZopp (norm_ez e) + | EZofI e => norm_ei e + | EZraw z => EZraw z + end. + + (** [ExprP] to a simplified [ExprP] *) + + Fixpoint norm_ep (e:ExprP) : ExprP := + match e with + | EPeq e1 e2 => EPeq (norm_ez e1) (norm_ez e2) + | EPlt e1 e2 => EPlt (norm_ez e1) (norm_ez e2) + | EPle e1 e2 => EPle (norm_ez e1) (norm_ez e2) + | EPgt e1 e2 => EPgt (norm_ez e1) (norm_ez e2) + | EPge e1 e2 => EPge (norm_ez e1) (norm_ez e2) + | EPimpl e1 e2 => EPimpl (norm_ep e1) (norm_ep e2) + | EPequiv e1 e2 => EPequiv (norm_ep e1) (norm_ep e2) + | EPand e1 e2 => EPand (norm_ep e1) (norm_ep e2) + | EPor e1 e2 => EPor (norm_ep e1) (norm_ep e2) + | EPneg e => EPneg (norm_ep e) + | EPraw p => EPraw p + end. + + Lemma norm_ei_correct : forall e:ExprI, ez2z (norm_ei e) = i2z (ei2i e). + Proof. + induction e; simpl; intros; i2z; auto; try congruence. + Qed. + + Lemma norm_ez_correct : forall e:ExprZ, ez2z (norm_ez e) = ez2z e. + Proof. + induction e; simpl; intros; i2z; auto; try congruence; apply norm_ei_correct. + Qed. + + Lemma norm_ep_correct : + forall e:ExprP, ep2p (norm_ep e) <-> ep2p e. + Proof. + induction e; simpl; repeat (rewrite norm_ez_correct); intuition. + Qed. + + Lemma norm_ep_correct2 : + forall e:ExprP, ep2p (norm_ep e) -> ep2p e. + Proof. + intros; destruct (norm_ep_correct e); auto. + Qed. + + Ltac i2z_refl := + i2z_gen; + match goal with |- ?t => + let e := p2ep t + in + (change (ep2p e); + apply norm_ep_correct2; + simpl) + end. + + Ltac iauto := i2z_refl; auto. + Ltac iomega := i2z_refl; intros; romega. + + Open Scope Z_scope. + + Lemma max_spec : forall (x y:Z), + x >= y /\ Zmax x y = x \/ + x < y /\ Zmax x y = y. + Proof. + intros; unfold Zmax, Zlt, Zge. + destruct (Zcompare x y); [ left | right | left ]; split; auto; discriminate. + Qed. + + Ltac omega_max_genspec x y := + generalize (max_spec x y); + let z := fresh "z" in let Hz := fresh "Hz" in + (set (z:=Zmax x y); clearbody z). + + Ltac omega_max_loop := + match goal with + (* hack: we don't want [i2z (height ...)] to be reduced by romega later... *) + | |- context [ i2z (?f ?x) ] => + let i := fresh "i2z" in (set (i:=i2z (f x)); clearbody i); omega_max_loop + | |- context [ Zmax ?x ?y ] => omega_max_genspec x y; omega_max_loop + | _ => intros + end. + + Ltac omega_max := i2z_refl; omega_max_loop; try romega. + + Ltac false_omega := i2z_refl; intros; romega. + Ltac false_omega_max := elimtype False; omega_max. + + Open Scope Int_scope. +End MoreInt. + + +(** It's always nice to know that our [Int] interface is realizable :-) *) + +Module Z_as_Int <: Int. + Open Scope Z_scope. + Definition int := Z. + Definition _0 := 0. + Definition _1 := 1. + Definition _2 := 2. + Definition _3 := 3. + Definition plus := Zplus. + Definition opp := Zopp. + Definition minus := Zminus. + Definition mult := Zmult. + Definition max := Zmax. + Definition gt_le_dec := Z_gt_le_dec. + Definition ge_lt_dec := Z_ge_lt_dec. + Definition eq_dec := Z_eq_dec. + Definition i2z : int -> Z := fun n => n. + Lemma i2z_eq : forall n p, i2z n=i2z p -> n = p. Proof. auto. Qed. + Lemma i2z_0 : i2z _0 = 0. Proof. auto. Qed. + Lemma i2z_1 : i2z _1 = 1. Proof. auto. Qed. + Lemma i2z_2 : i2z _2 = 2. Proof. auto. Qed. + Lemma i2z_3 : i2z _3 = 3. Proof. auto. Qed. + Lemma i2z_plus : forall n p, i2z (n + p) = i2z n + i2z p. Proof. auto. Qed. + Lemma i2z_opp : forall n, i2z (- n) = - i2z n. Proof. auto. Qed. + Lemma i2z_minus : forall n p, i2z (n - p) = i2z n - i2z p. Proof. auto. Qed. + Lemma i2z_mult : forall n p, i2z (n * p) = i2z n * i2z p. Proof. auto. Qed. + Lemma i2z_max : forall n p, i2z (max n p) = Zmax (i2z n) (i2z p). Proof. auto. Qed. +End Z_as_Int. + diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v index 714abfc4..4003c338 100644 --- a/theories/ZArith/Zcompare.v +++ b/theories/ZArith/Zcompare.v @@ -383,7 +383,7 @@ Qed. (** Reverting [x ?= y] to trichotomy *) Lemma rename : - forall (A:Set) (P:A -> Prop) (x:A), (forall y:A, x = y -> P y) -> P x. + forall (A:Type) (P:A -> Prop) (x:A), (forall y:A, x = y -> P y) -> P x. Proof. auto with arith. Qed. diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v index a1963446..b74f7585 100644 --- a/theories/ZArith/Znumtheory.v +++ b/theories/ZArith/Znumtheory.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Znumtheory.v 6984 2005-05-02 10:50:15Z herbelin $ i*) +(*i $Id: Znumtheory.v 8853 2006-05-23 18:17:38Z herbelin $ i*) Require Import ZArith_base. Require Import ZArithRing. @@ -367,11 +367,391 @@ rewrite H6; rewrite H7; ring. ring. Qed. +Lemma Zis_gcd_0_abs : forall b, + Zis_gcd 0 b (Zabs b) /\ Zabs b >= 0 /\ 0 = Zabs b * 0 /\ b = Zabs b * Zsgn b. +Proof. +intro b. +elim (Z_le_lt_eq_dec _ _ (Zabs_pos b)). +intros H0; split. +apply Zabs_ind. +intros; apply Zis_gcd_sym; apply Zis_gcd_0; auto. +intros; apply Zis_gcd_opp; apply Zis_gcd_0; auto. +repeat split; auto with zarith. +symmetry; apply Zabs_Zsgn. + +intros H0; rewrite <- H0. +rewrite <- (Zabs_Zsgn b); rewrite <- H0; simpl in |- *. +split; [ apply Zis_gcd_0 | idtac ]; auto with zarith. +Qed. + + (** We could obtain a [Zgcd] function via [euclid]. But we propose - here a more direct version of a [Zgcd], with better extraction - (no bezout coeffs). *) + here a more direct version of a [Zgcd], that can compute within Coq. + For that, we use an explicit measure in [nat], and we proved later + that using [2(d+1)] is enough, where [d] is the number of binary digits + of the first argument. *) + +Fixpoint Zgcdn (n:nat) : Z -> Z -> Z := fun a b => + match n with + | O => 1 (* arbitrary, since n should be big enough *) + | S n => match a with + | Z0 => Zabs b + | Zpos _ => Zgcdn n (Zmod b a) a + | Zneg a => Zgcdn n (Zmod b (Zpos a)) (Zpos a) + end + end. + +(* For technical reason, we don't use [Ndigit.Psize] but this + ad-hoc version: [Psize p = S (Psiz p)]. *) + +Fixpoint Psiz (p:positive) : nat := + match p with + | xH => O + | xI p => S (Psiz p) + | xO p => S (Psiz p) + end. + +Definition Zgcd_bound (a:Z) := match a with + | Z0 => S O + | Zpos p => let n := Psiz p in S (S (n+n)) + | Zneg p => let n := Psiz p in S (S (n+n)) +end. + +Definition Zgcd a b := Zgcdn (Zgcd_bound a) a b. + +(** A first obvious fact : [Zgcd a b] is positive. *) + +Lemma Zgcdn_is_pos : forall n a b, + 0 <= Zgcdn n a b. +Proof. +induction n. +simpl; auto with zarith. +destruct a; simpl; intros; auto with zarith; auto. +Qed. + +Lemma Zgcd_is_pos : forall a b, 0 <= Zgcd a b. +Proof. +intros; unfold Zgcd; apply Zgcdn_is_pos; auto. +Qed. + +(** We now prove that Zgcd is indeed a gcd. *) + +(** 1) We prove a weaker & easier bound. *) + +Lemma Zgcdn_linear_bound : forall n a b, + Zabs a < Z_of_nat n -> Zis_gcd a b (Zgcdn n a b). +Proof. +induction n. +simpl; intros. +elimtype False; generalize (Zabs_pos a); omega. +destruct a; intros; simpl; + [ generalize (Zis_gcd_0_abs b); intuition | | ]; + unfold Zmod; + generalize (Z_div_mod b (Zpos p) (refl_equal Gt)); + destruct (Zdiv_eucl b (Zpos p)) as (q,r); + intros (H0,H1); + rewrite inj_S in H; simpl Zabs in H; + assert (H2: Zabs r < Z_of_nat n) by (rewrite Zabs_eq; auto with zarith); + assert (IH:=IHn r (Zpos p) H2); clear IHn; + simpl in IH |- *; + rewrite H0. + apply Zis_gcd_for_euclid2; auto. + apply Zis_gcd_minus; apply Zis_gcd_sym. + apply Zis_gcd_for_euclid2; auto. +Qed. + +(** 2) For Euclid's algorithm, the worst-case situation corresponds + to Fibonacci numbers. Let's define them: *) + +Fixpoint fibonacci (n:nat) : Z := + match n with + | O => 1 + | S O => 1 + | S (S n as p) => fibonacci p + fibonacci n + end. + +Lemma fibonacci_pos : forall n, 0 <= fibonacci n. +Proof. +cut (forall N n, (n<N)%nat -> 0<=fibonacci n). +eauto. +induction N. +inversion 1. +intros. +destruct n. +simpl; auto with zarith. +destruct n. +simpl; auto with zarith. +change (0 <= fibonacci (S n) + fibonacci n). +generalize (IHN n) (IHN (S n)); omega. +Qed. + +Lemma fibonacci_incr : + forall n m, (n<=m)%nat -> fibonacci n <= fibonacci m. +Proof. +induction 1. +auto with zarith. +apply Zle_trans with (fibonacci m); auto. +clear. +destruct m. +simpl; auto with zarith. +change (fibonacci (S m) <= fibonacci (S m)+fibonacci m). +generalize (fibonacci_pos m); omega. +Qed. + +(** 3) We prove that fibonacci numbers are indeed worst-case: + for a given number [n], if we reach a conclusion about [gcd(a,b)] in + exactly [n+1] loops, then [fibonacci (n+1)<=a /\ fibonacci(n+2)<=b] *) + +Lemma Zgcdn_worst_is_fibonacci : forall n a b, + 0 < a < b -> + Zis_gcd a b (Zgcdn (S n) a b) -> + Zgcdn n a b <> Zgcdn (S n) a b -> + fibonacci (S n) <= a /\ + fibonacci (S (S n)) <= b. +Proof. +induction n. +simpl; intros. +destruct a; omega. +intros. +destruct a; [simpl in *; omega| | destruct H; discriminate]. +revert H1; revert H0. +set (m:=S n) in *; (assert (m=S n) by auto); clearbody m. +pattern m at 2; rewrite H0. +simpl Zgcdn. +unfold Zmod; generalize (Z_div_mod b (Zpos p) (refl_equal Gt)). +destruct (Zdiv_eucl b (Zpos p)) as (q,r). +intros (H1,H2). +destruct H2. +destruct (Zle_lt_or_eq _ _ H2). +generalize (IHn _ _ (conj H4 H3)). +intros H5 H6 H7. +replace (fibonacci (S (S m))) with (fibonacci (S m) + fibonacci m) by auto. +assert (r = Zpos p * (-q) + b) by (rewrite H1; ring). +destruct H5; auto. +pattern r at 1; rewrite H8. +apply Zis_gcd_sym. +apply Zis_gcd_for_euclid2; auto. +apply Zis_gcd_sym; auto. +split; auto. +rewrite H1. +apply Zplus_le_compat; auto. +apply Zle_trans with (Zpos p * 1); auto. +ring (Zpos p * 1); auto. +apply Zmult_le_compat_l. +destruct q. +omega. +assert (0 < Zpos p0) by (compute; auto). +omega. +assert (Zpos p * Zneg p0 < 0) by (compute; auto). +omega. +compute; intros; discriminate. +(* r=0 *) +subst r. +simpl; rewrite H0. +intros. +simpl in H4. +simpl in H5. +destruct n. +simpl in H5. +simpl. +omega. +simpl in H5. +elim H5; auto. +Qed. + +(** 3b) We reformulate the previous result in a more positive way. *) + +Lemma Zgcdn_ok_before_fibonacci : forall n a b, + 0 < a < b -> a < fibonacci (S n) -> + Zis_gcd a b (Zgcdn n a b). +Proof. +destruct a; [ destruct 1; elimtype False; omega | | destruct 1; discriminate]. +cut (forall k n b, + k = (S (nat_of_P p) - n)%nat -> + 0 < Zpos p < b -> Zpos p < fibonacci (S n) -> + Zis_gcd (Zpos p) b (Zgcdn n (Zpos p) b)). +destruct 2; eauto. +clear n; induction k. +intros. +assert (nat_of_P p < n)%nat by omega. +apply Zgcdn_linear_bound. +simpl. +generalize (inj_le _ _ H2). +rewrite inj_S. +rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; auto. +omega. +intros. +generalize (Zgcdn_worst_is_fibonacci n (Zpos p) b H0); intros. +assert (Zis_gcd (Zpos p) b (Zgcdn (S n) (Zpos p) b)). + apply IHk; auto. + omega. + replace (fibonacci (S (S n))) with (fibonacci (S n)+fibonacci n) by auto. + generalize (fibonacci_pos n); omega. +replace (Zgcdn n (Zpos p) b) with (Zgcdn (S n) (Zpos p) b); auto. +generalize (H2 H3); clear H2 H3; omega. +Qed. + +(** 4) The proposed bound leads to a fibonacci number that is big enough. *) + +Lemma Zgcd_bound_fibonacci : + forall a, 0 < a -> a < fibonacci (Zgcd_bound a). +Proof. +destruct a; [omega| | intro H; discriminate]. +intros _. +induction p. +simpl Zgcd_bound in *. +rewrite Zpos_xI. +rewrite plus_comm; simpl plus. +set (n:=S (Psiz p+Psiz p)) in *. +change (2*Zpos p+1 < + fibonacci (S n) + fibonacci n + fibonacci (S n)). +generalize (fibonacci_pos n). +omega. +simpl Zgcd_bound in *. +rewrite Zpos_xO. +rewrite plus_comm; simpl plus. +set (n:= S (Psiz p +Psiz p)) in *. +change (2*Zpos p < + fibonacci (S n) + fibonacci n + fibonacci (S n)). +generalize (fibonacci_pos n). +omega. +simpl; auto with zarith. +Qed. -Definition Zgcd_pos : +(* 5) the end: we glue everything together and take care of + situations not corresponding to [0<a<b]. *) + +Lemma Zgcd_is_gcd : + forall a b, Zis_gcd a b (Zgcd a b). +Proof. +unfold Zgcd; destruct a; intros. +simpl; generalize (Zis_gcd_0_abs b); intuition. +(*Zpos*) +generalize (Zgcd_bound_fibonacci (Zpos p)). +simpl Zgcd_bound. +set (n:=S (Psiz p+Psiz p)); (assert (n=S (Psiz p+Psiz p)) by auto); clearbody n. +simpl Zgcdn. +unfold Zmod. +generalize (Z_div_mod b (Zpos p) (refl_equal Gt)). +destruct (Zdiv_eucl b (Zpos p)) as (q,r). +intros (H1,H2) H3. +rewrite H1. +apply Zis_gcd_for_euclid2. +destruct H2. +destruct (Zle_lt_or_eq _ _ H0). +apply Zgcdn_ok_before_fibonacci; auto; omega. +subst r n; simpl. +apply Zis_gcd_sym; apply Zis_gcd_0. +(*Zneg*) +generalize (Zgcd_bound_fibonacci (Zpos p)). +simpl Zgcd_bound. +set (n:=S (Psiz p+Psiz p)); (assert (n=S (Psiz p+Psiz p)) by auto); clearbody n. +simpl Zgcdn. +unfold Zmod. +generalize (Z_div_mod b (Zpos p) (refl_equal Gt)). +destruct (Zdiv_eucl b (Zpos p)) as (q,r). +intros (H1,H2) H3. +rewrite H1. +apply Zis_gcd_minus. +apply Zis_gcd_sym. +apply Zis_gcd_for_euclid2. +destruct H2. +destruct (Zle_lt_or_eq _ _ H0). +apply Zgcdn_ok_before_fibonacci; auto; omega. +subst r n; simpl. +apply Zis_gcd_sym; apply Zis_gcd_0. +Qed. + +(** A generalized gcd: it additionnally keeps track of the divisors. *) + +Fixpoint Zggcdn (n:nat) : Z -> Z -> (Z*(Z*Z)) := fun a b => + match n with + | O => (1,(a,b)) (*(Zabs b,(0,Zsgn b))*) + | S n => match a with + | Z0 => (Zabs b,(0,Zsgn b)) + | Zpos _ => + let (q,r) := Zdiv_eucl b a in (* b = q*a+r *) + let (g,p) := Zggcdn n r a in + let (rr,aa) := p in (* r = g *rr /\ a = g * aa *) + (g,(aa,q*aa+rr)) + | Zneg a => + let (q,r) := Zdiv_eucl b (Zpos a) in (* b = q*(-a)+r *) + let (g,p) := Zggcdn n r (Zpos a) in + let (rr,aa) := p in (* r = g*rr /\ (-a) = g * aa *) + (g,(-aa,q*aa+rr)) + end + end. + +Definition Zggcd a b : Z * (Z * Z) := Zggcdn (Zgcd_bound a) a b. + +(** The first component of [Zggcd] is [Zgcd] *) + +Lemma Zggcdn_gcdn : forall n a b, + fst (Zggcdn n a b) = Zgcdn n a b. +Proof. +induction n; simpl; auto. +destruct a; unfold Zmod; simpl; intros; auto; + destruct (Zdiv_eucl b (Zpos p)) as (q,r); + rewrite <- IHn; + destruct (Zggcdn n r (Zpos p)) as (g,(rr,aa)); simpl; auto. +Qed. + +Lemma Zggcd_gcd : forall a b, fst (Zggcd a b) = Zgcd a b. +Proof. +intros; unfold Zggcd, Zgcd; apply Zggcdn_gcdn; auto. +Qed. + +(** [Zggcd] always returns divisors that are coherent with its + first output. *) + +Lemma Zggcdn_correct_divisors : forall n a b, + let (g,p) := Zggcdn n a b in + let (aa,bb):=p in + a=g*aa /\ b=g*bb. +Proof. +induction n. +simpl. +split; [destruct a|destruct b]; auto. +intros. +simpl. +destruct a. +rewrite Zmult_comm; simpl. +split; auto. +symmetry; apply Zabs_Zsgn. +generalize (Z_div_mod b (Zpos p)); +destruct (Zdiv_eucl b (Zpos p)) as (q,r). +generalize (IHn r (Zpos p)); +destruct (Zggcdn n r (Zpos p)) as (g,(rr,aa)). +intuition. +destruct H0. +compute; auto. +rewrite H; rewrite H1; rewrite H2; ring. +generalize (Z_div_mod b (Zpos p)); +destruct (Zdiv_eucl b (Zpos p)) as (q,r). +destruct 1. +compute; auto. +generalize (IHn r (Zpos p)); +destruct (Zggcdn n r (Zpos p)) as (g,(rr,aa)). +intuition. +destruct H0. +replace (Zneg p) with (-Zpos p) by compute; auto. +rewrite H4; ring. +rewrite H; rewrite H4; rewrite H0; ring. +Qed. + +Lemma Zggcd_correct_divisors : forall a b, + let (g,p) := Zggcd a b in + let (aa,bb):=p in + a=g*aa /\ b=g*bb. +Proof. +unfold Zggcd; intros; apply Zggcdn_correct_divisors; auto. +Qed. + +(** Due to the use of an explicit measure, the extraction of [Zgcd] + isn't optimal. We propose here another version [Zgcd_spec] that + doesn't suffer from this problem (but doesn't compute in Coq). *) + +Definition Zgcd_spec_pos : forall a:Z, 0 <= a -> forall b:Z, {g : Z | 0 <= a -> Zis_gcd a b g /\ g >= 0}. Proof. @@ -382,16 +762,7 @@ apply try assumption. intro x; case x. intros _ _ b; exists (Zabs b). - elim (Z_le_lt_eq_dec _ _ (Zabs_pos b)). - intros H0; split. - apply Zabs_ind. - intros; apply Zis_gcd_sym; apply Zis_gcd_0; auto. - intros; apply Zis_gcd_opp; apply Zis_gcd_0; auto. - auto with zarith. - - intros H0; rewrite <- H0. - rewrite <- (Zabs_Zsgn b); rewrite <- H0; simpl in |- *. - split; [ apply Zis_gcd_0 | idtac ]; auto with zarith. +generalize (Zis_gcd_0_abs b); intuition. intros p Hrec _ b. generalize (Z_div_mod b (Zpos p)). @@ -414,21 +785,58 @@ Proof. intros a; case (Z_gt_le_dec 0 a). intros; assert (0 <= - a). omega. -elim (Zgcd_pos (- a) H b); intros g Hgkl. +elim (Zgcd_spec_pos (- a) H b); intros g Hgkl. exists g. intuition. -intros Ha b; elim (Zgcd_pos a Ha b); intros g; exists g; intuition. +intros Ha b; elim (Zgcd_spec_pos a Ha b); intros g; exists g; intuition. Defined. -Definition Zgcd (a b:Z) := let (g, _) := Zgcd_spec a b in g. +(** A last version aimed at extraction that also returns the divisors. *) -Lemma Zgcd_is_pos : forall a b:Z, Zgcd a b >= 0. -intros a b; unfold Zgcd in |- *; case (Zgcd_spec a b); tauto. -Qed. +Definition Zggcd_spec_pos : + forall a:Z, + 0 <= a -> forall b:Z, {p : Z*(Z*Z) | let (g,p):=p in let (aa,bb):=p in + 0 <= a -> Zis_gcd a b g /\ g >= 0 /\ a=g*aa /\ b=g*bb}. +Proof. +intros a Ha. +pattern a; apply Zlt_0_rec; try assumption. +intro x; case x. +intros _ _ b; exists (Zabs b,(0,Zsgn b)). +intros _; apply Zis_gcd_0_abs. + +intros p Hrec _ b. +generalize (Z_div_mod b (Zpos p)). +case (Zdiv_eucl b (Zpos p)); intros q r Hqr. +elim Hqr; clear Hqr; intros; auto with zarith. +destruct (Hrec r H0 (Zpos p)) as ((g,(rr,pp)),Hgkl). +destruct H0. +destruct (Hgkl H0) as (H3,(H4,(H5,H6))). +exists (g,(pp,pp*q+rr)); intros. +split; auto. +rewrite H. +apply Zis_gcd_for_euclid2; auto. +repeat split; auto. +rewrite H; rewrite H6; rewrite H5; ring. -Lemma Zgcd_is_gcd : forall a b:Z, Zis_gcd a b (Zgcd a b). -intros a b; unfold Zgcd in |- *; case (Zgcd_spec a b); tauto. -Qed. +intros p _ H b. +elim H; auto. +Defined. + +Definition Zggcd_spec : + forall a b:Z, {p : Z*(Z*Z) | let (g,p):=p in let (aa,bb):=p in + Zis_gcd a b g /\ g >= 0 /\ a=g*aa /\ b=g*bb}. +Proof. +intros a; case (Z_gt_le_dec 0 a). +intros; assert (0 <= - a). +omega. +destruct (Zggcd_spec_pos (- a) H b) as ((g,(aa,bb)),Hgkl). +exists (g,(-aa,bb)). +intuition. +rewrite <- Zopp_mult_distr_r. +rewrite <- H2; auto with zarith. +intros Ha b; elim (Zggcd_spec_pos a Ha b); intros p; exists p. + repeat destruct p; intuition. +Defined. (** * Relative primality *) |