diff options
Diffstat (limited to 'theories/ZArith')
33 files changed, 1298 insertions, 1137 deletions
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 1ff88604..d976b01c 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -6,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: BinInt.v 11015 2008-05-28 20:06:42Z herbelin $ i*) +(*i $Id$ i*) (***********************************************************) (** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) @@ -225,6 +226,11 @@ Qed. (** ** Properties of opposite on binary integer numbers *) +Theorem Zopp_0 : Zopp Z0 = Z0. +Proof. + reflexivity. +Qed. + Theorem Zopp_neg : forall p:positive, - Zneg p = Zpos p. Proof. reflexivity. @@ -336,8 +342,8 @@ Proof. rewrite nat_of_P_gt_Gt_compare_complement_morphism; [ discriminate | rewrite nat_of_P_plus_morphism; rewrite (Pcompare_Eq_eq y z E0); - elim (ZL4 x); intros k E2; rewrite E2; - simpl in |- *; unfold gt, lt in |- *; + elim (ZL4 x); intros k E2; rewrite E2; + simpl in |- *; unfold gt, lt in |- *; apply le_n_S; apply le_plus_r ] | assumption ] | absurd ((x + y ?= z)%positive Eq = Lt); @@ -345,8 +351,8 @@ Proof. rewrite nat_of_P_gt_Gt_compare_complement_morphism; [ discriminate | rewrite nat_of_P_plus_morphism; rewrite (Pcompare_Eq_eq y z E0); - elim (ZL4 x); intros k E2; rewrite E2; - simpl in |- *; unfold gt, lt in |- *; + elim (ZL4 x); intros k E2; rewrite E2; + simpl in |- *; unfold gt, lt in |- *; apply le_n_S; apply le_plus_r ] | assumption ] | rewrite (Pcompare_Eq_eq y z E0); @@ -377,7 +383,7 @@ Proof. [ intros i H5; elim H5; intros H6 H7; elim H7; intros H8 H9; elim (Pminus_mask_Gt z (x + y)); [ intros j H10; elim H10; intros H11 H12; elim H12; - intros H13 H14; unfold Pminus in |- *; + intros H13 H14; unfold Pminus in |- *; rewrite H6; rewrite H11; cut (i = j); [ intros E; rewrite E; auto with arith | apply (Pplus_reg_l (x + y)); rewrite H13; @@ -388,7 +394,7 @@ Proof. | apply nat_of_P_lt_Lt_compare_complement_morphism; apply plus_lt_reg_l with (p := nat_of_P y); do 2 rewrite <- nat_of_P_plus_morphism; - apply nat_of_P_lt_Lt_compare_morphism; + apply nat_of_P_lt_Lt_compare_morphism; rewrite H3; rewrite Pplus_comm; assumption ] | apply ZC2; assumption ] | elim (Pminus_mask_Gt z y); @@ -399,22 +405,22 @@ Proof. unfold Pminus in |- *; rewrite H1; rewrite H6; cut ((x ?= k)%positive Eq = Gt); [ intros H10; elim (Pminus_mask_Gt x k H10); intros j H11; - elim H11; intros H12 H13; elim H13; - intros H14 H15; rewrite H10; rewrite H12; + elim H11; intros H12 H13; elim H13; + intros H14 H15; rewrite H10; rewrite H12; cut (i = j); [ intros H16; rewrite H16; auto with arith | apply (Pplus_reg_l (z + k)); rewrite <- (Pplus_assoc z k j); rewrite H14; rewrite (Pplus_comm z k); rewrite <- Pplus_assoc; rewrite H8; rewrite (Pplus_comm x y); rewrite Pplus_assoc; - rewrite (Pplus_comm k y); rewrite H3; + rewrite (Pplus_comm k y); rewrite H3; trivial with arith ] | apply nat_of_P_gt_Gt_compare_complement_morphism; unfold lt, gt in |- *; apply plus_lt_reg_l with (p := nat_of_P y); do 2 rewrite <- nat_of_P_plus_morphism; - apply nat_of_P_lt_Lt_compare_morphism; - rewrite H3; rewrite Pplus_comm; apply ZC1; + apply nat_of_P_lt_Lt_compare_morphism; + rewrite H3; rewrite Pplus_comm; apply ZC1; assumption ] | assumption ] | apply ZC2; assumption ] @@ -437,14 +443,14 @@ Proof. | assumption ] | elim Pminus_mask_Gt with (1 := E0); intros k H1; (* Case 9 *) - elim Pminus_mask_Gt with (1 := E1); intros i H2; - elim H1; intros H3 H4; elim H4; intros H5 H6; - elim H2; intros H7 H8; elim H8; intros H9 H10; + elim Pminus_mask_Gt with (1 := E1); intros i H2; + elim H1; intros H3 H4; elim H4; intros H5 H6; + elim H2; intros H7 H8; elim H8; intros H9 H10; unfold Pminus in |- *; rewrite H3; rewrite H7; cut ((x + k)%positive = i); [ intros E; rewrite E; auto with arith | apply (Pplus_reg_l z); rewrite (Pplus_comm x k); rewrite Pplus_assoc; - rewrite H5; rewrite H9; rewrite Pplus_comm; + rewrite H5; rewrite H9; rewrite Pplus_comm; trivial with arith ] ] ]. Qed. @@ -460,7 +466,7 @@ Proof. rewrite Zplus_comm; rewrite <- weak_assoc; rewrite (Zplus_comm (- Zpos p1)); rewrite (Zplus_comm (Zpos p0 + - Zpos p1)); rewrite (weak_assoc p); - rewrite weak_assoc; rewrite (Zplus_comm (Zpos p0)); + rewrite weak_assoc; rewrite (Zplus_comm (Zpos p0)); trivial with arith | rewrite Zplus_comm; rewrite (Zplus_comm (Zpos p0) (Zpos p)); rewrite <- weak_assoc; rewrite Zplus_comm; rewrite (Zplus_comm (Zpos p0)); @@ -503,7 +509,7 @@ Qed. Lemma Zplus_succ_l : forall n m:Z, Zsucc n + m = Zsucc (n + m). Proof. intros x y; unfold Zsucc in |- *; rewrite (Zplus_comm (x + y)); - rewrite Zplus_assoc; rewrite (Zplus_comm (Zpos 1)); + rewrite Zplus_assoc; rewrite (Zplus_comm (Zpos 1)); trivial with arith. Qed. @@ -706,7 +712,7 @@ Lemma Zplus_minus_eq : forall n m p:Z, n = m + p -> p = n - m. Proof. intros n m p H; unfold Zminus in |- *; apply (Zplus_reg_l m); rewrite (Zplus_comm m (n + - m)); rewrite <- Zplus_assoc; - rewrite Zplus_opp_l; rewrite Zplus_0_r; rewrite H; + rewrite Zplus_opp_l; rewrite Zplus_0_r; rewrite H; trivial with arith. Qed. @@ -747,7 +753,7 @@ Proof. reflexivity. Qed. -Lemma Zpos_minus_morphism : forall a b:positive, Pcompare a b Eq = Lt -> +Lemma Zpos_minus_morphism : forall a b:positive, Pcompare a b Eq = Lt -> Zpos (b-a) = Zpos b - Zpos a. Proof. intros. @@ -773,7 +779,7 @@ Qed. (**********************************************************************) (** * Properties of multiplication on binary integer numbers *) -Theorem Zpos_mult_morphism : +Theorem Zpos_mult_morphism : forall p q:positive, Zpos (p*q) = Zpos p * Zpos q. Proof. auto. @@ -862,7 +868,7 @@ Lemma Zmult_1_inversion_l : Proof. intros x y; destruct x as [| p| p]; intro; [ discriminate | left | right ]; (destruct y as [| q| q]; try discriminate; simpl in H; injection H; clear H; - intro H; rewrite Pmult_1_inversion_l with (1 := H); + intro H; rewrite Pmult_1_inversion_l with (1 := H); reflexivity). Qed. @@ -873,7 +879,7 @@ Proof. reflexivity. Qed. -Lemma Zdouble_plus_one_mult : forall z, +Lemma Zdouble_plus_one_mult : forall z, Zdouble_plus_one z = (Zpos 2) * z + (Zpos 1). Proof. destruct z; simpl; auto with zarith. @@ -927,13 +933,13 @@ Proof. [ intros E; rewrite E; rewrite Pmult_minus_distr_l; [ trivial with arith | apply ZC2; assumption ] | apply nat_of_P_lt_Lt_compare_complement_morphism; - do 2 rewrite nat_of_P_mult_morphism; elim (ZL4 x); + do 2 rewrite nat_of_P_mult_morphism; elim (ZL4 x); intros h H1; rewrite H1; apply mult_S_lt_compat_l; exact (nat_of_P_lt_Lt_compare_morphism z y E0) ] | cut ((x * z ?= x * y)%positive Eq = Gt); [ intros E; rewrite E; rewrite Pmult_minus_distr_l; auto with arith | apply nat_of_P_gt_Gt_compare_complement_morphism; unfold gt in |- *; - do 2 rewrite nat_of_P_mult_morphism; elim (ZL4 x); + do 2 rewrite nat_of_P_mult_morphism; elim (ZL4 x); intros h H1; rewrite H1; apply mult_S_lt_compat_l; exact (nat_of_P_gt_Gt_compare_morphism z y E0) ] ]). Qed. @@ -963,7 +969,7 @@ Proof. apply Zmult_plus_distr_l. Qed. - + Lemma Zmult_minus_distr_l : forall n m p:Z, p * (n - m) = p * n - p * m. Proof. intros x y z; rewrite (Zmult_comm z (x - y)). @@ -1007,7 +1013,7 @@ Qed. Lemma Zmult_succ_r : forall n m:Z, n * Zsucc m = n * m + n. Proof. intros n m; unfold Zsucc in |- *; rewrite Zmult_plus_distr_r; - rewrite (Zmult_comm n (Zpos 1)); rewrite Zmult_1_l; + rewrite (Zmult_comm n (Zpos 1)); rewrite Zmult_1_l; trivial with arith. Qed. @@ -1146,7 +1152,7 @@ Definition Zabs_N (z:Z) := | Zneg p => Npos p end. -Definition Z_of_N (x:N) := +Definition Z_of_N (x:N) := match x with | N0 => Z0 | Npos p => Zpos p diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index fcb44d6f..30c08fdc 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -6,23 +6,17 @@ (* * 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$ *) -(* $Id: Int.v 10739 2008-04-01 14:45:20Z herbelin $ *) +(** * An light axiomatization of integers (used in FSetAVL). *) -(** 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). +(** 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. +Require Import ZArith. Delimit Scope Int_scope with I. @@ -31,33 +25,33 @@ Delimit Scope Int_scope with I. Module Type Int. Open Scope Int_scope. - - Parameter int : Set. - + + Parameter int : Set. + Parameter i2z : int -> Z. Arguments Scope i2z [ Int_scope ]. - - Parameter _0 : int. - Parameter _1 : int. - Parameter _2 : int. + + Parameter _0 : int. + Parameter _1 : int. + Parameter _2 : int. Parameter _3 : int. - Parameter plus : int -> int -> int. + Parameter plus : int -> int -> int. Parameter opp : int -> int. - Parameter minus : int -> int -> int. + Parameter minus : int -> int -> int. Parameter mult : int -> int -> int. - Parameter max : int -> int -> int. - + Parameter max : int -> int -> int. + Notation "0" := _0 : Int_scope. - Notation "1" := _1 : Int_scope. - Notation "2" := _2 : 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 + (** 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) @@ -70,22 +64,22 @@ Module Type Int. 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 [==] + (** 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 + 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. @@ -99,25 +93,25 @@ Module Type Int. 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. +End Int. (** * Facts and tactics using [Int] *) Module MoreInt (I:Int). Import I. - + Open Scope Int_scope. - (** A magic (but costly) tactic that goes from [int] back to the [Z] + (** A magic (but costly) tactic that goes from [int] back to the [Z] friendly world ... *) - Hint Rewrite -> + 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); + 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 @@ -126,39 +120,39 @@ Module MoreInt (I:Int). (** 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. + (** 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 + + Ltac i2z_gen := match goal with | |- (eq (A:=int) ?a ?b) => apply (i2z_eq a b); i2z_gen - | H : (eq (A:=int) ?a ?b) |- _ => + | 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 |- _ => + | H : (eq (A:=Z) ?a ?b) |- _ => revert H; i2z_gen + | H : (Zlt ?a ?b) |- _ => revert H; i2z_gen + | H : (Zle ?a ?b) |- _ => revert H; i2z_gen + | H : (Zgt ?a ?b) |- _ => revert H; i2z_gen + | H : (Zge ?a ?b) |- _ => revert H; i2z_gen + | H : _ -> ?X |- _ => (* A [Set] or [Type] part cannot be dealt with easily - using the [ExprP] datatype. So we forget it, leaving + using the [ExprP] datatype. So we forget it, leaving a goal that can be weaker than the original. *) - match type of X with + match type of X with | Type => clear H; i2z_gen - | Prop => generalize H; clear H; i2z_gen + | Prop => revert 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 + | H : _ <-> _ |- _ => revert H; i2z_gen + | H : _ /\ _ |- _ => revert H; i2z_gen + | H : _ \/ _ |- _ => revert H; i2z_gen + | H : ~ _ |- _ => revert H; i2z_gen | _ => idtac end. - Inductive ExprI : Set := + Inductive ExprI : Set := | EI0 : ExprI | EI1 : ExprI - | EI2 : ExprI + | EI2 : ExprI | EI3 : ExprI | EIplus : ExprI -> ExprI -> ExprI | EIopp : ExprI -> ExprI @@ -167,7 +161,7 @@ Module MoreInt (I:Int). | EImax : ExprI -> ExprI -> ExprI | EIraw : int -> ExprI. - Inductive ExprZ : Set := + Inductive ExprZ : Set := | EZplus : ExprZ -> ExprZ -> ExprZ | EZopp : ExprZ -> ExprZ | EZminus : ExprZ -> ExprZ -> ExprZ @@ -176,12 +170,12 @@ Module MoreInt (I:Int). | 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 + 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 @@ -191,8 +185,8 @@ Module MoreInt (I:Int). (** [int] to [ExprI] *) - Ltac i2ei trm := - match constr:trm with + Ltac i2ei trm := + match constr:trm with | 0 => constr:EI0 | 1 => constr:EI1 | 2 => constr:EI2 @@ -207,8 +201,8 @@ Module MoreInt (I:Int). (** [Z] to [ExprZ] *) - with z2ez trm := - match constr:trm with + 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) @@ -219,7 +213,7 @@ Module MoreInt (I:Int). 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) @@ -229,11 +223,11 @@ Module MoreInt (I:Int). | (~ ?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:(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. + end. (** [ExprI] to [int] *) @@ -242,19 +236,19 @@ Module MoreInt (I:Int). | EI0 => 0 | EI1 => 1 | EI2 => 2 - | EI3 => 3 + | 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. + | EIraw i => i + end. (** [ExprZ] to [Z] *) - Fixpoint ez2z (e:ExprZ) : Z := - match e with + 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 @@ -266,8 +260,8 @@ Module MoreInt (I:Int). (** [ExprP] to [Prop] *) - Fixpoint ep2p (e:ExprP) : Prop := - match e with + 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 @@ -282,25 +276,25 @@ Module MoreInt (I:Int). end. (** [ExprI] (supposed under a [i2z]) to a simplified [ExprZ] *) - - Fixpoint norm_ei (e:ExprI) : ExprZ := - match e with + + 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) + | 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) + | EIraw i => EZofI (EIraw i) end. (** [ExprZ] to a simplified [ExprZ] *) - Fixpoint norm_ez (e:ExprZ) : ExprZ := - match e with + 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) @@ -311,9 +305,9 @@ Module MoreInt (I:Int). end. (** [ExprP] to a simplified [ExprP] *) - - Fixpoint norm_ep (e:ExprP) : ExprP := - match e with + + 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) @@ -328,38 +322,36 @@ Module MoreInt (I:Int). end. Lemma norm_ei_correct : forall e:ExprI, ez2z (norm_ei e) = i2z (ei2i e). - Proof. + 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. + Qed. - Lemma norm_ep_correct : + 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 : + 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 := + Ltac i2z_refl := i2z_gen; - match goal with |- ?t => - let e := p2ep t in + match goal with |- ?t => + let e := p2ep t in change (ep2p e); apply norm_ep_correct2; simpl end. - (* i2z_refl can be replaced below by (simpl in *; i2z). + (* i2z_refl can be replaced below by (simpl in *; i2z). The reflexive version improves compilation of AVL files by about 15% *) - - Ltac omega_max := i2z_refl; romega with Z. End MoreInt. @@ -381,7 +373,7 @@ Module Z_as_Int <: Int. Definition minus := Zminus. Definition mult := Zmult. Definition max := Zmax. - Definition gt_le_dec := Z_gt_le_dec. + 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. diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v index 1d7948a5..46f64c88 100644 --- a/theories/ZArith/Wf_Z.v +++ b/theories/ZArith/Wf_Z.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Wf_Z.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id$ i*) Require Import BinInt. Require Import Zcompare. @@ -40,7 +40,7 @@ Proof. intro x; destruct x; intros; [ exists 0%nat; auto with arith | specialize (ZL4 p); intros Hp; elim Hp; intros; exists (S x); intros; - simpl in |- *; specialize (nat_of_P_o_P_of_succ_nat_eq_succ x); + simpl in |- *; specialize (nat_of_P_o_P_of_succ_nat_eq_succ x); intro Hx0; rewrite <- H0 in Hx0; apply f_equal with (f := Zpos); apply nat_of_P_inj; auto with arith | absurd (0 <= Zneg p); @@ -120,13 +120,13 @@ Proof. | assumption ]. Qed. -Section Efficient_Rec. +Section Efficient_Rec. - (** [natlike_rec2] is the same as [natlike_rec], but with a different proof, designed + (** [natlike_rec2] is the same as [natlike_rec], but with a different proof, designed to give a better extracted term. *) Let R (a b:Z) := 0 <= a /\ a < b. - + Let R_wf : well_founded R. Proof. set diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v index 66e0bda8..5747afc9 100644 --- a/theories/ZArith/ZArith.v +++ b/theories/ZArith/ZArith.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ZArith.v 9210 2006-10-05 10:12:15Z barras $ i*) +(*i $Id$ i*) (** Library for manipulating integers based on binary encoding *) diff --git a/theories/ZArith/ZArith_base.v b/theories/ZArith/ZArith_base.v index 20fd6b5f..cd866c37 100644 --- a/theories/ZArith/ZArith_base.v +++ b/theories/ZArith/ZArith_base.v @@ -6,10 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ZArith_base.v 8032 2006-02-12 21:20:48Z herbelin $ *) +(* $Id$ *) (** Library for manipulating integers based on binary encoding. - These are the basic modules, required by [Omega] and [Ring] for instance. + These are the basic modules, required by [Omega] and [Ring] for instance. The full library is [ZArith]. *) Require Export BinPos. @@ -18,9 +18,9 @@ Require Export BinInt. Require Export Zcompare. Require Export Zorder. Require Export Zeven. +Require Export Zminmax. Require Export Zmin. Require Export Zmax. -Require Export Zminmax. Require Export Zabs. Require Export Znat. Require Export auxiliary. diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v index b831afee..6e69350d 100644 --- a/theories/ZArith/ZArith_dec.v +++ b/theories/ZArith/ZArith_dec.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ZArith_dec.v 9759 2007-04-12 17:46:54Z notin $ i*) +(*i $Id$ i*) Require Import Sumbool. @@ -15,35 +15,39 @@ Require Import Zorder. Require Import Zcompare. Open Local Scope Z_scope. +(* begin hide *) +(* Trivial, to deprecate? *) Lemma Dcompare_inf : forall r:comparison, {r = Eq} + {r = Lt} + {r = Gt}. Proof. - simple induction r; auto with arith. + induction r; auto. +Defined. +(* end hide *) + +Lemma Zcompare_rect : + forall (P:Type) (n m:Z), + ((n ?= m) = Eq -> P) -> ((n ?= m) = Lt -> P) -> ((n ?= m) = Gt -> P) -> P. +Proof. + intros * H1 H2 H3. + destruct (n ?= m); auto. Defined. Lemma Zcompare_rec : forall (P:Set) (n m:Z), ((n ?= m) = Eq -> P) -> ((n ?= m) = Lt -> P) -> ((n ?= m) = Gt -> P) -> P. Proof. - intros P x y H1 H2 H3. - elim (Dcompare_inf (x ?= y)). - intro H. elim H; auto with arith. auto with arith. + intro; apply Zcompare_rect. Defined. Section decidability. Variables x y : Z. - + (** * Decidability of equality on binary integers *) Definition Z_eq_dec : {x = y} + {x <> y}. Proof. - apply Zcompare_rec with (n := x) (m := y). - intro. left. elim (Zcompare_Eq_iff_eq x y); auto with arith. - intro H3. right. elim (Zcompare_Eq_iff_eq x y). intros H1 H2. unfold not in |- *. intro H4. - rewrite (H2 H4) in H3. discriminate H3. - intro H3. right. elim (Zcompare_Eq_iff_eq x y). intros H1 H2. unfold not in |- *. intro H4. - rewrite (H2 H4) in H3. discriminate H3. - Defined. + decide equality; apply positive_eq_dec. + Defined. (** * Decidability of order on binary integers *) @@ -64,7 +68,7 @@ Section decidability. left. rewrite H. discriminate. right. tauto. Defined. - + Definition Z_gt_dec : {x > y} + {~ x > y}. Proof. unfold Zgt in |- *. @@ -214,13 +218,16 @@ Proof. [ right; assumption | left; apply (not_Zeq_inf _ _ H) ]. Defined. - - -Definition Z_zerop : forall x:Z, {x = 0} + {x <> 0}. +(* begin hide *) +(* To deprecate ? *) +Corollary Z_zerop : forall x:Z, {x = 0} + {x <> 0}. Proof. exact (fun x:Z => Z_eq_dec x 0). Defined. -Definition Z_notzerop (x:Z) := sumbool_not _ _ (Z_zerop x). +Corollary Z_notzerop : forall (x:Z), {x <> 0} + {x = 0}. +Proof (fun x => sumbool_not _ _ (Z_zerop x)). -Definition Z_noteq_dec (x y:Z) := sumbool_not _ _ (Z_eq_dec x y). +Corollary Z_noteq_dec : forall (x y:Z), {x <> y} + {x = y}. +Proof (fun x y => sumbool_not _ _ (Z_eq_dec x y)). +(* end hide *) diff --git a/theories/ZArith/ZOdiv.v b/theories/ZArith/ZOdiv.v index 03e061f2..28b664aa 100644 --- a/theories/ZArith/ZOdiv.v +++ b/theories/ZArith/ZOdiv.v @@ -13,19 +13,19 @@ Require Zdiv. Open Scope Z_scope. -(** This file provides results about the Round-Toward-Zero Euclidean +(** This file provides results about the Round-Toward-Zero Euclidean division [ZOdiv_eucl], whose projections are [ZOdiv] and [ZOmod]. - Definition of this division can be found in file [ZOdiv_def]. + Definition of this division can be found in file [ZOdiv_def]. - This division and the one defined in Zdiv agree only on positive - numbers. Otherwise, Zdiv performs Round-Toward-Bottom. + This division and the one defined in Zdiv agree only on positive + numbers. Otherwise, Zdiv performs Round-Toward-Bottom. - The current approach is compatible with the division of usual - programming languages such as Ocaml. In addition, it has nicer + The current approach is compatible with the division of usual + programming languages such as Ocaml. In addition, it has nicer properties with respect to opposite and other usual operations. *) -(** Since ZOdiv and Zdiv are not meant to be used concurrently, +(** Since ZOdiv and Zdiv are not meant to be used concurrently, we reuse the same notation. *) Infix "/" := ZOdiv : Z_scope. @@ -36,7 +36,7 @@ Infix "mod" := Nmod (at level 40, no associativity) : N_scope. (** Auxiliary results on the ad-hoc comparison [NPgeb]. *) -Lemma NPgeb_Zge : forall (n:N)(p:positive), +Lemma NPgeb_Zge : forall (n:N)(p:positive), NPgeb n p = true -> Z_of_N n >= Zpos p. Proof. destruct n as [|n]; simpl; intros. @@ -44,7 +44,7 @@ Proof. red; simpl; destruct Pcompare; now auto. Qed. -Lemma NPgeb_Zlt : forall (n:N)(p:positive), +Lemma NPgeb_Zlt : forall (n:N)(p:positive), NPgeb n p = false -> Z_of_N n < Zpos p. Proof. destruct n as [|n]; simpl; intros. @@ -54,7 +54,7 @@ Qed. (** * Relation between division on N and on Z. *) -Lemma Ndiv_Z0div : forall a b:N, +Lemma Ndiv_Z0div : forall a b:N, Z_of_N (a/b) = (Z_of_N a / Z_of_N b). Proof. intros. @@ -62,7 +62,7 @@ Proof. unfold Ndiv, ZOdiv; simpl; destruct Pdiv_eucl; auto. Qed. -Lemma Nmod_Z0mod : forall a b:N, +Lemma Nmod_Z0mod : forall a b:N, Z_of_N (a mod b) = (Z_of_N a) mod (Z_of_N b). Proof. intros. @@ -72,11 +72,11 @@ Qed. (** * Characterization of this euclidean division. *) -(** First, the usual equation [a=q*b+r]. Notice that [a mod 0] +(** First, the usual equation [a=q*b+r]. Notice that [a mod 0] has been chosen to be [a], so this equation holds even for [b=0]. *) -Theorem N_div_mod_eq : forall a b, +Theorem N_div_mod_eq : forall a b, a = (b * (Ndiv a b) + (Nmod a b))%N. Proof. intros; generalize (Ndiv_eucl_correct a b). @@ -84,7 +84,7 @@ Proof. intro H; rewrite H; rewrite Nmult_comm; auto. Qed. -Theorem ZO_div_mod_eq : forall a b, +Theorem ZO_div_mod_eq : forall a b, a = b * (ZOdiv a b) + (ZOmod a b). Proof. intros; generalize (ZOdiv_eucl_correct a b). @@ -94,8 +94,8 @@ Qed. (** Then, the inequalities constraining the remainder. *) -Theorem Pdiv_eucl_remainder : forall a b:positive, - Z_of_N (snd (Pdiv_eucl a b)) < Zpos b. +Theorem Pdiv_eucl_remainder : forall a b:positive, + Z_of_N (snd (Pdiv_eucl a b)) < Zpos b. Proof. induction a; cbv beta iota delta [Pdiv_eucl]; fold Pdiv_eucl; cbv zeta. intros b; generalize (IHa b); case Pdiv_eucl. @@ -111,7 +111,7 @@ Proof. destruct b; simpl; romega with *. Qed. -Theorem Nmod_lt : forall (a b:N), b<>0%N -> +Theorem Nmod_lt : forall (a b:N), b<>0%N -> (a mod b < b)%N. Proof. destruct b as [ |b]; intro H; try solve [elim H;auto]. @@ -122,20 +122,20 @@ Qed. (** The remainder is bounded by the divisor, in term of absolute values *) -Theorem ZOmod_lt : forall a b:Z, b<>0 -> +Theorem ZOmod_lt : forall a b:Z, b<>0 -> Zabs (a mod b) < Zabs b. Proof. - destruct b as [ |b|b]; intro H; try solve [elim H;auto]; - destruct a as [ |a|a]; try solve [compute;auto]; unfold ZOmod, ZOdiv_eucl; - generalize (Pdiv_eucl_remainder a b); destruct Pdiv_eucl; simpl; + destruct b as [ |b|b]; intro H; try solve [elim H;auto]; + destruct a as [ |a|a]; try solve [compute;auto]; unfold ZOmod, ZOdiv_eucl; + generalize (Pdiv_eucl_remainder a b); destruct Pdiv_eucl; simpl; try rewrite Zabs_Zopp; rewrite Zabs_eq; auto; apply Z_of_N_le_0. Qed. -(** The sign of the remainder is the one of [a]. Due to the possible +(** The sign of the remainder is the one of [a]. Due to the possible nullity of [a], a general result is to be stated in the following form: -*) +*) -Theorem ZOmod_sgn : forall a b:Z, +Theorem ZOmod_sgn : forall a b:Z, 0 <= Zsgn (a mod b) * Zsgn a. Proof. destruct b as [ |b|b]; destruct a as [ |a|a]; simpl; auto with zarith; @@ -150,16 +150,16 @@ Proof. destruct z; simpl; intuition auto with zarith. Qed. -Theorem ZOmod_sgn2 : forall a b:Z, +Theorem ZOmod_sgn2 : forall a b:Z, 0 <= (a mod b) * a. Proof. intros; rewrite <-Zsgn_pos_iff, Zsgn_Zmult; apply ZOmod_sgn. -Qed. +Qed. -(** Reformulation of [ZOdiv_lt] and [ZOmod_sgn] in 2 +(** Reformulation of [ZOdiv_lt] and [ZOmod_sgn] in 2 then 4 particular cases. *) -Theorem ZOmod_lt_pos : forall a b:Z, 0<=a -> b<>0 -> +Theorem ZOmod_lt_pos : forall a b:Z, 0<=a -> b<>0 -> 0 <= a mod b < Zabs b. Proof. intros. @@ -171,7 +171,7 @@ Proof. generalize (ZOmod_lt a b H0); romega with *. Qed. -Theorem ZOmod_lt_neg : forall a b:Z, a<=0 -> b<>0 -> +Theorem ZOmod_lt_neg : forall a b:Z, a<=0 -> b<>0 -> -Zabs b < a mod b <= 0. Proof. intros. @@ -209,49 +209,49 @@ Qed. Theorem ZOdiv_opp_l : forall a b:Z, (-a)/b = -(a/b). Proof. - destruct a; destruct b; simpl; auto; + destruct a; destruct b; simpl; auto; unfold ZOdiv, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith. Qed. Theorem ZOdiv_opp_r : forall a b:Z, a/(-b) = -(a/b). Proof. - destruct a; destruct b; simpl; auto; + destruct a; destruct b; simpl; auto; unfold ZOdiv, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith. Qed. Theorem ZOmod_opp_l : forall a b:Z, (-a) mod b = -(a mod b). Proof. - destruct a; destruct b; simpl; auto; + destruct a; destruct b; simpl; auto; unfold ZOmod, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith. Qed. Theorem ZOmod_opp_r : forall a b:Z, a mod (-b) = a mod b. Proof. - destruct a; destruct b; simpl; auto; + destruct a; destruct b; simpl; auto; unfold ZOmod, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith. Qed. Theorem ZOdiv_opp_opp : forall a b:Z, (-a)/(-b) = a/b. Proof. - destruct a; destruct b; simpl; auto; + destruct a; destruct b; simpl; auto; unfold ZOdiv, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith. Qed. Theorem ZOmod_opp_opp : forall a b:Z, (-a) mod (-b) = -(a mod b). Proof. - destruct a; destruct b; simpl; auto; + destruct a; destruct b; simpl; auto; unfold ZOmod, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith. Qed. (** * Unicity results *) -Definition Remainder a b r := +Definition Remainder a b r := (0 <= a /\ 0 <= r < Zabs b) \/ (a <= 0 /\ -Zabs b < r <= 0). -Definition Remainder_alt a b r := +Definition Remainder_alt a b r := Zabs r < Zabs b /\ 0 <= r * a. -Lemma Remainder_equiv : forall a b r, +Lemma Remainder_equiv : forall a b r, Remainder a b r <-> Remainder_alt a b r. Proof. unfold Remainder, Remainder_alt; intuition. @@ -259,12 +259,12 @@ Proof. romega with *. rewrite <-(Zmult_opp_opp). apply Zmult_le_0_compat; romega. - assert (0 <= Zsgn r * Zsgn a) by (rewrite <-Zsgn_Zmult, Zsgn_pos_iff; auto). + assert (0 <= Zsgn r * Zsgn a) by (rewrite <-Zsgn_Zmult, Zsgn_pos_iff; auto). destruct r; simpl Zsgn in *; romega with *. Qed. Theorem ZOdiv_mod_unique_full: - forall a b q r, Remainder a b r -> + forall a b q r, Remainder a b r -> a = b*q + r -> q = a/b /\ r = a mod b. Proof. destruct 1 as [(H,H0)|(H,H0)]; intros. @@ -281,30 +281,30 @@ Proof. romega with *. Qed. -Theorem ZOdiv_unique_full: - forall a b q r, Remainder a b r -> +Theorem ZOdiv_unique_full: + forall a b q r, Remainder a b r -> a = b*q + r -> q = a/b. Proof. intros; destruct (ZOdiv_mod_unique_full a b q r); auto. Qed. Theorem ZOdiv_unique: - forall a b q r, 0 <= a -> 0 <= r < b -> + forall a b q r, 0 <= a -> 0 <= r < b -> a = b*q + r -> q = a/b. Proof. intros; eapply ZOdiv_unique_full; eauto. red; romega with *. Qed. -Theorem ZOmod_unique_full: - forall a b q r, Remainder a b r -> +Theorem ZOmod_unique_full: + forall a b q r, Remainder a b r -> a = b*q + r -> r = a mod b. Proof. intros; destruct (ZOdiv_mod_unique_full a b q r); auto. Qed. Theorem ZOmod_unique: - forall a b q r, 0 <= a -> 0 <= r < b -> + forall a b q r, 0 <= a -> 0 <= r < b -> a = b*q + r -> r = a mod b. Proof. intros; eapply ZOmod_unique_full; eauto. @@ -345,7 +345,7 @@ Proof. rewrite Remainder_equiv; red; simpl; auto with zarith. Qed. -Hint Resolve ZOmod_0_l ZOmod_0_r ZOdiv_0_l ZOdiv_0_r ZOdiv_1_r ZOmod_1_r +Hint Resolve ZOmod_0_l ZOmod_0_r ZOdiv_0_l ZOdiv_0_r ZOdiv_1_r ZOmod_1_r : zarith. Lemma ZOdiv_1_l: forall a, 1 < a -> 1/a = 0. @@ -381,7 +381,7 @@ Qed. Lemma ZO_div_mult : forall a b:Z, b <> 0 -> (a*b)/b = a. Proof. - intros; symmetry; apply ZOdiv_unique_full with 0; auto with zarith; + intros; symmetry; apply ZOdiv_unique_full with 0; auto with zarith; [ red; romega with * | ring]. Qed. @@ -403,12 +403,12 @@ Proof. subst b; rewrite ZOdiv_0_r; auto. Qed. -(** As soon as the divisor is greater or equal than 2, +(** As soon as the divisor is greater or equal than 2, the division is strictly decreasing. *) Lemma ZO_div_lt : forall a b:Z, 0 < a -> 2 <= b -> a/b < a. Proof. - intros. + intros. assert (Hb : 0 < b) by romega. assert (H1 : 0 <= a/b) by (apply ZO_div_pos; auto with zarith). assert (H2 : 0 <= a mod b < b) by (apply ZOmod_lt_pos_pos; auto with zarith). @@ -441,7 +441,7 @@ Lemma ZO_div_monotone_pos : forall a b c:Z, 0<=c -> 0<=a<=b -> a/c <= b/c. Proof. intros. destruct H0. - destruct (Zle_lt_or_eq 0 c H); + destruct (Zle_lt_or_eq 0 c H); [ clear H | subst c; do 2 rewrite ZOdiv_0_r; auto]. generalize (ZO_div_mod_eq a c). generalize (ZOmod_lt_pos_pos a c H0 H2). @@ -452,7 +452,7 @@ Proof. intro. absurd (a - b >= 1). omega. - replace (a-b) with (c * (a/c-b/c) + a mod c - b mod c) by + replace (a-b) with (c * (a/c-b/c) + a mod c - b mod c) by (symmetry; pattern a at 1; rewrite H5; pattern b at 1; rewrite H3; ring). assert (c * (a / c - b / c) >= c * 1). apply Zmult_ge_compat_l. @@ -519,7 +519,7 @@ Proof. apply ZO_div_pos; auto with zarith. Qed. -(** The previous inequalities between [b*(a/b)] and [a] are exact +(** The previous inequalities between [b*(a/b)] and [a] are exact iff the modulo is zero. *) Lemma ZO_div_exact_full_1 : forall a b:Z, a = b*(a/b) -> a mod b = 0. @@ -535,7 +535,7 @@ Qed. (** A modulo cannot grow beyond its starting point. *) Theorem ZOmod_le: forall a b, 0 <= a -> 0 <= b -> a mod b <= a. -Proof. +Proof. intros a b H1 H2. destruct (Zle_lt_or_eq _ _ H2). case (Zle_or_lt b a); intros H3. @@ -546,17 +546,15 @@ Qed. (** Some additionnal inequalities about Zdiv. *) -Theorem ZOdiv_le_upper_bound: - forall a b q, 0 <= a -> 0 < b -> a <= q*b -> a/b <= q. +Theorem ZOdiv_le_upper_bound: + forall a b q, 0 < b -> a <= q*b -> a/b <= q. Proof. - intros a b q H1 H2 H3. - apply Zmult_le_reg_r with b; auto with zarith. - apply Zle_trans with (2 := H3). - pattern a at 2; rewrite (ZO_div_mod_eq a b); auto with zarith. - rewrite (Zmult_comm b); case (ZOmod_lt_pos_pos a b); auto with zarith. + intros. + rewrite <- (ZO_div_mult q b); auto with zarith. + apply ZO_div_monotone; auto with zarith. Qed. -Theorem ZOdiv_lt_upper_bound: +Theorem ZOdiv_lt_upper_bound: forall a b q, 0 <= a -> 0 < b -> a < q*b -> a/b < q. Proof. intros a b q H1 H2 H3. @@ -566,33 +564,29 @@ Proof. rewrite (Zmult_comm b); case (ZOmod_lt_pos_pos a b); auto with zarith. Qed. -Theorem ZOdiv_le_lower_bound: - forall a b q, 0 <= a -> 0 < b -> q*b <= a -> q <= a/b. +Theorem ZOdiv_le_lower_bound: + forall a b q, 0 < b -> q*b <= a -> q <= a/b. Proof. - intros a b q H1 H2 H3. - assert (q < a / b + 1); auto with zarith. - apply Zmult_lt_reg_r with b; auto with zarith. - apply Zle_lt_trans with (1 := H3). - pattern a at 1; rewrite (ZO_div_mod_eq a b); auto with zarith. - rewrite Zmult_plus_distr_l; rewrite (Zmult_comm b); case (ZOmod_lt_pos_pos a b); - auto with zarith. + intros. + rewrite <- (ZO_div_mult q b); auto with zarith. + apply ZO_div_monotone; auto with zarith. Qed. -Theorem ZOdiv_sgn: forall a b, +Theorem ZOdiv_sgn: forall a b, 0 <= Zsgn (a/b) * Zsgn a * Zsgn b. Proof. - destruct a as [ |a|a]; destruct b as [ |b|b]; simpl; auto with zarith; + destruct a as [ |a|a]; destruct b as [ |b|b]; simpl; auto with zarith; unfold ZOdiv; simpl; destruct Pdiv_eucl; simpl; destruct n; simpl; auto with zarith. Qed. (** * Relations between usual operations and Zmod and Zdiv *) -(** First, a result that used to be always valid with Zdiv, - but must be restricted here. +(** First, a result that used to be always valid with Zdiv, + but must be restricted here. For instance, now (9+(-5)*2) mod 2 = -1 <> 1 = 9 mod 2 *) -Lemma ZO_mod_plus : forall a b c:Z, - 0 <= (a+b*c) * a -> +Lemma ZO_mod_plus : forall a b c:Z, + 0 <= (a+b*c) * a -> (a + b * c) mod c = a mod c. Proof. intros; destruct (Z_eq_dec a 0) as [Ha|Ha]. @@ -611,8 +605,8 @@ Proof. generalize (ZO_div_mod_eq a c); romega. Qed. -Lemma ZO_div_plus : forall a b c:Z, - 0 <= (a+b*c) * a -> c<>0 -> +Lemma ZO_div_plus : forall a b c:Z, + 0 <= (a+b*c) * a -> c<>0 -> (a + b * c) / c = a / c + b. Proof. intros; destruct (Z_eq_dec a 0) as [Ha|Ha]. @@ -630,17 +624,17 @@ Proof. generalize (ZO_div_mod_eq a c); romega. Qed. -Theorem ZO_div_plus_l: forall a b c : Z, - 0 <= (a*b+c)*c -> b<>0 -> +Theorem ZO_div_plus_l: forall a b c : Z, + 0 <= (a*b+c)*c -> b<>0 -> b<>0 -> (a * b + c) / b = a + c / b. Proof. intros a b c; rewrite Zplus_comm; intros; rewrite ZO_div_plus; - try apply Zplus_comm; auto with zarith. + try apply Zplus_comm; auto with zarith. Qed. (** Cancellations. *) -Lemma ZOdiv_mult_cancel_r : forall a b c:Z, +Lemma ZOdiv_mult_cancel_r : forall a b c:Z, c<>0 -> (a*c)/(b*c) = a/b. Proof. intros a b c Hc. @@ -661,7 +655,7 @@ Proof. pattern a at 1; rewrite (ZO_div_mod_eq a b); ring. Qed. -Lemma ZOdiv_mult_cancel_l : forall a b c:Z, +Lemma ZOdiv_mult_cancel_l : forall a b c:Z, c<>0 -> (c*a)/(c*b) = a/b. Proof. intros. @@ -669,7 +663,7 @@ Proof. apply ZOdiv_mult_cancel_r; auto. Qed. -Lemma ZOmult_mod_distr_l: forall a b c, +Lemma ZOmult_mod_distr_l: forall a b c, (c*a) mod (c*b) = c * (a mod b). Proof. intros; destruct (Z_eq_dec c 0) as [Hc|Hc]. @@ -684,7 +678,7 @@ Proof. ring. Qed. -Lemma ZOmult_mod_distr_r: forall a b c, +Lemma ZOmult_mod_distr_r: forall a b c, (a*c) mod (b*c) = (a mod b) * c. Proof. intros; repeat rewrite (fun x => (Zmult_comm x c)). @@ -712,7 +706,7 @@ Proof. pattern a at 2 3; rewrite (ZO_div_mod_eq a n); auto with zarith. pattern b at 2 3; rewrite (ZO_div_mod_eq b n); auto with zarith. set (A:=a mod n); set (B:=b mod n); set (A':=a/n); set (B':=b/n). - replace (A*(n*A'+A)*(B*(n*B'+B))) with (((n*A' + A) * (n*B' + B))*(A*B)) + replace (A*(n*A'+A)*(B*(n*B'+B))) with (((n*A' + A) * (n*B' + B))*(A*B)) by ring. replace ((n*A' + A) * (n*B' + B)) with (A*B + (A'*B+B'*A+n*A'*B')*n) by ring. @@ -721,15 +715,15 @@ Proof. Qed. (** addition and modulo - - Generally speaking, unlike with Zdiv, we don't have - (a+b) mod n = (a mod n + b mod n) mod n - for any a and b. - For instance, take (8 + (-10)) mod 3 = -2 whereas + + Generally speaking, unlike with Zdiv, we don't have + (a+b) mod n = (a mod n + b mod n) mod n + for any a and b. + For instance, take (8 + (-10)) mod 3 = -2 whereas (8 mod 3 + (-10 mod 3)) mod 3 = 1. *) Theorem ZOplus_mod: forall a b n, - 0 <= a * b -> + 0 <= a * b -> (a + b) mod n = (a mod n + b mod n) mod n. Proof. assert (forall a b n, 0<a -> 0<b -> @@ -761,16 +755,16 @@ Proof. rewrite <-(Zopp_involutive a), <-(Zopp_involutive b). rewrite <- Zopp_plus_distr; rewrite ZOmod_opp_l. rewrite (ZOmod_opp_l (-a)),(ZOmod_opp_l (-b)). - match goal with |- _ = (-?x+-?y) mod n => + match goal with |- _ = (-?x+-?y) mod n => rewrite <-(Zopp_plus_distr x y), ZOmod_opp_l end. f_equal; apply H; auto with zarith. Qed. -Lemma ZOplus_mod_idemp_l: forall a b n, - 0 <= a * b -> +Lemma ZOplus_mod_idemp_l: forall a b n, + 0 <= a * b -> (a mod n + b) mod n = (a + b) mod n. Proof. - intros. + intros. rewrite ZOplus_mod. rewrite ZOmod_mod. symmetry. @@ -791,8 +785,8 @@ Proof. destruct b; simpl; auto with zarith. Qed. -Lemma ZOplus_mod_idemp_r: forall a b n, - 0 <= a*b -> +Lemma ZOplus_mod_idemp_r: forall a b n, + 0 <= a*b -> (b + a mod n) mod n = (b + a) mod n. Proof. intros. @@ -822,12 +816,12 @@ Proof. replace (b * (c * (a / b / c) + (a / b) mod c) + a mod b) with ((a / b / c)*(b * c) + (b * ((a / b) mod c) + a mod b)) by ring. assert (b*c<>0). - intro H2; - assert (H3: c <> 0) by auto with zarith; + intro H2; + assert (H3: c <> 0) by auto with zarith; rewrite (Zmult_integral_l _ _ H3 H2) in H0; auto with zarith. assert (0<=a/b) by (apply (ZO_div_pos a b); auto with zarith). assert (0<=a mod b < b) by (apply ZOmod_lt_pos_pos; auto with zarith). - assert (0<=(a/b) mod c < c) by + assert (0<=(a/b) mod c < c) by (apply ZOmod_lt_pos_pos; auto with zarith). rewrite ZO_div_plus_l; auto with zarith. rewrite (ZOdiv_small (b * ((a / b) mod c) + a mod b)). @@ -852,14 +846,14 @@ Proof. intros; destruct b as [ |b|b]. repeat rewrite ZOdiv_0_r; reflexivity. apply H0; auto with zarith. - change (Zneg b) with (-Zpos b); + change (Zneg b) with (-Zpos b); repeat (rewrite ZOdiv_opp_r || rewrite ZOdiv_opp_l || rewrite <- Zopp_mult_distr_l). f_equal; apply H0; auto with zarith. (* a b c general *) intros; destruct c as [ |c|c]. rewrite Zmult_0_r; repeat rewrite ZOdiv_0_r; reflexivity. apply H1; auto with zarith. - change (Zneg c) with (-Zpos c); + change (Zneg c) with (-Zpos c); rewrite <- Zopp_mult_distr_r; do 2 rewrite ZOdiv_opp_r. f_equal; apply H1; auto with zarith. Qed. @@ -870,11 +864,11 @@ Theorem ZOdiv_mult_le: forall a b c, 0<=a -> 0<=b -> 0<=c -> c*(a/b) <= (c*a)/b. Proof. intros a b c Ha Hb Hc. - destruct (Zle_lt_or_eq _ _ Ha); + destruct (Zle_lt_or_eq _ _ Ha); [ | subst; rewrite ZOdiv_0_l, Zmult_0_r, ZOdiv_0_l; auto]. - destruct (Zle_lt_or_eq _ _ Hb); + destruct (Zle_lt_or_eq _ _ Hb); [ | subst; rewrite ZOdiv_0_r, ZOdiv_0_r, Zmult_0_r; auto]. - destruct (Zle_lt_or_eq _ _ Hc); + destruct (Zle_lt_or_eq _ _ Hc); [ | subst; rewrite ZOdiv_0_l; auto]. case (ZOmod_lt_pos_pos a b); auto with zarith; intros Hu1 Hu2. case (ZOmod_lt_pos_pos c b); auto with zarith; intros Hv1 Hv2. @@ -890,14 +884,14 @@ Proof. apply (ZOmod_le ((c mod b) * (a mod b)) b); auto with zarith. apply Zmult_le_compat_r; auto with zarith. apply (ZOmod_le c b); auto. - pattern (c * a) at 1; rewrite (ZO_div_mod_eq (c * a) b); try ring; + pattern (c * a) at 1; rewrite (ZO_div_mod_eq (c * a) b); try ring; auto with zarith. pattern a at 1; rewrite (ZO_div_mod_eq a b); try ring; auto with zarith. Qed. (** ZOmod is related to divisibility (see more in Znumtheory) *) -Lemma ZOmod_divides : forall a b, +Lemma ZOmod_divides : forall a b, a mod b = 0 <-> exists c, a = b*c. Proof. split; intros. @@ -916,7 +910,7 @@ Qed. (** They agree at least on positive numbers: *) -Theorem ZOdiv_eucl_Zdiv_eucl_pos : forall a b:Z, 0 <= a -> 0 < b -> +Theorem ZOdiv_eucl_Zdiv_eucl_pos : forall a b:Z, 0 <= a -> 0 < b -> a/b = Zdiv.Zdiv a b /\ a mod b = Zdiv.Zmod a b. Proof. intros. @@ -927,7 +921,7 @@ Proof. symmetry; apply ZO_div_mod_eq; auto with *. Qed. -Theorem ZOdiv_Zdiv_pos : forall a b, 0 <= a -> 0 <= b -> +Theorem ZOdiv_Zdiv_pos : forall a b, 0 <= a -> 0 <= b -> a/b = Zdiv.Zdiv a b. Proof. intros a b Ha Hb. @@ -936,7 +930,7 @@ Proof. subst; rewrite ZOdiv_0_r, Zdiv.Zdiv_0_r; reflexivity. Qed. -Theorem ZOmod_Zmod_pos : forall a b, 0 <= a -> 0 < b -> +Theorem ZOmod_Zmod_pos : forall a b, 0 <= a -> 0 < b -> a mod b = Zdiv.Zmod a b. Proof. intros a b Ha Hb; generalize (ZOdiv_eucl_Zdiv_eucl_pos a b Ha Hb); @@ -945,9 +939,9 @@ Qed. (** Modulos are null at the same places *) -Theorem ZOmod_Zmod_zero : forall a b, b<>0 -> +Theorem ZOmod_Zmod_zero : forall a b, b<>0 -> (a mod b = 0 <-> Zdiv.Zmod a b = 0). Proof. intros. rewrite ZOmod_divides, Zdiv.Zmod_divides; intuition. -Qed. +Qed. diff --git a/theories/ZArith/ZOdiv_def.v b/theories/ZArith/ZOdiv_def.v index 2c84765e..88d573bb 100644 --- a/theories/ZArith/ZOdiv_def.v +++ b/theories/ZArith/ZOdiv_def.v @@ -17,9 +17,9 @@ Definition NPgeb (a:N)(b:positive) := | Npos na => match Pcompare na b Eq with Lt => false | _ => true end end. -Fixpoint Pdiv_eucl (a b:positive) {struct a} : N * N := +Fixpoint Pdiv_eucl (a b:positive) : N * N := match a with - | xH => + | xH => match b with xH => (1, 0)%N | _ => (0, 1)%N end | xO a' => let (q, r) := Pdiv_eucl a' b in @@ -33,21 +33,21 @@ Fixpoint Pdiv_eucl (a b:positive) {struct a} : N * N := else (2 * q, r')%N end. -Definition ZOdiv_eucl (a b:Z) : Z * Z := +Definition ZOdiv_eucl (a b:Z) : Z * Z := match a, b with | Z0, _ => (Z0, Z0) | _, Z0 => (Z0, a) - | Zpos na, Zpos nb => - let (nq, nr) := Pdiv_eucl na nb in + | Zpos na, Zpos nb => + let (nq, nr) := Pdiv_eucl na nb in (Z_of_N nq, Z_of_N nr) - | Zneg na, Zpos nb => - let (nq, nr) := Pdiv_eucl na nb in + | Zneg na, Zpos nb => + let (nq, nr) := Pdiv_eucl na nb in (Zopp (Z_of_N nq), Zopp (Z_of_N nr)) - | Zpos na, Zneg nb => - let (nq, nr) := Pdiv_eucl na nb in + | Zpos na, Zneg nb => + let (nq, nr) := Pdiv_eucl na nb in (Zopp (Z_of_N nq), Z_of_N nr) - | Zneg na, Zneg nb => - let (nq, nr) := Pdiv_eucl na nb in + | Zneg na, Zneg nb => + let (nq, nr) := Pdiv_eucl na nb in (Z_of_N nq, Zopp (Z_of_N nr)) end. @@ -55,7 +55,7 @@ Definition ZOdiv a b := fst (ZOdiv_eucl a b). Definition ZOmod a b := snd (ZOdiv_eucl a b). -Definition Ndiv_eucl (a b:N) : N * N := +Definition Ndiv_eucl (a b:N) : N * N := match a, b with | N0, _ => (N0, N0) | _, N0 => (N0, a) @@ -68,13 +68,13 @@ Definition Nmod a b := snd (Ndiv_eucl a b). (* Proofs of specifications for these euclidean divisions. *) -Theorem NPgeb_correct: forall (a:N)(b:positive), +Theorem NPgeb_correct: forall (a:N)(b:positive), if NPgeb a b then a = (Nminus a (Npos b) + Npos b)%N else True. Proof. destruct a; intros; simpl; auto. generalize (Pcompare_Eq_eq p b). case_eq (Pcompare p b Eq); intros; auto. - rewrite H0; auto. + rewrite H0; auto. now rewrite Pminus_mask_diag. destruct (Pminus_mask_Gt p b H) as [d [H2 [H3 _]]]. rewrite H2. rewrite <- H3. @@ -82,11 +82,11 @@ Proof. Qed. Hint Rewrite Z_of_N_plus Z_of_N_mult Z_of_N_minus Zmult_1_l Zmult_assoc - Zmult_plus_distr_l Zmult_plus_distr_r : zdiv. -Hint Rewrite <- Zplus_assoc : zdiv. + Zmult_plus_distr_l Zmult_plus_distr_r : zdiv. +Hint Rewrite <- Zplus_assoc : zdiv. Theorem Pdiv_eucl_correct: forall a b, - let (q,r) := Pdiv_eucl a b in + let (q,r) := Pdiv_eucl a b in Zpos a = Z_of_N q * Zpos b + Z_of_N r. Proof. induction a; cbv beta iota delta [Pdiv_eucl]; fold Pdiv_eucl; cbv zeta. diff --git a/theories/ZArith/ZOrderedType.v b/theories/ZArith/ZOrderedType.v new file mode 100644 index 00000000..570e2a4d --- /dev/null +++ b/theories/ZArith/ZOrderedType.v @@ -0,0 +1,60 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import BinInt Zcompare Zorder Zbool ZArith_dec + Equalities Orders OrdersTac. + +Local Open Scope Z_scope. + +(** * DecidableType structure for binary integers *) + +Module Z_as_UBE <: UsualBoolEq. + Definition t := Z. + Definition eq := @eq Z. + Definition eqb := Zeq_bool. + Definition eqb_eq x y := iff_sym (Zeq_is_eq_bool x y). +End Z_as_UBE. + +Module Z_as_DT <: UsualDecidableTypeFull := Make_UDTF Z_as_UBE. + +(** Note that the last module fulfills by subtyping many other + interfaces, such as [DecidableType] or [EqualityType]. *) + + +(** * OrderedType structure for binary integers *) + +Module Z_as_OT <: OrderedTypeFull. + Include Z_as_DT. + Definition lt := Zlt. + Definition le := Zle. + Definition compare := Zcompare. + + Instance lt_strorder : StrictOrder Zlt. + Proof. split; [ exact Zlt_irrefl | exact Zlt_trans ]. Qed. + + Instance lt_compat : Proper (Logic.eq==>Logic.eq==>iff) Zlt. + Proof. repeat red; intros; subst; auto. Qed. + + Definition le_lteq := Zle_lt_or_eq_iff. + Definition compare_spec := Zcompare_spec. + +End Z_as_OT. + +(** Note that [Z_as_OT] can also be seen as a [UsualOrderedType] + and a [OrderedType] (and also as a [DecidableType]). *) + + + +(** * An [order] tactic for integers *) + +Module ZOrder := OTF_to_OrderTac Z_as_OT. +Ltac z_order := ZOrder.order. + +(** Note that [z_order] is domain-agnostic: it will not prove + [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *) + diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v index c15493e3..36eb4110 100644 --- a/theories/ZArith/Zabs.v +++ b/theories/ZArith/Zabs.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -5,7 +6,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zabs.v 10302 2007-11-08 09:54:31Z letouzey $ i*) +(*i $Id$ i*) (** Binary Integers (Pierre Crégut (CNET, Lannion, France) *) @@ -77,9 +78,9 @@ Proof. (intros H2; rewrite H2); auto. Qed. -Lemma Zabs_spec : forall x:Z, - 0 <= x /\ Zabs x = x \/ - 0 > x /\ Zabs x = -x. +Lemma Zabs_spec : forall x:Z, + 0 <= x /\ Zabs x = x \/ + 0 > x /\ Zabs x = -x. Proof. intros; unfold Zabs, Zle, Zgt; destruct x; simpl; intuition discriminate. Qed. @@ -142,7 +143,7 @@ Lemma Zabs_nat_mult: forall n m:Z, Zabs_nat (n*m) = (Zabs_nat n * Zabs_nat m)%na Proof. intros; apply inj_eq_rev. rewrite inj_mult; repeat rewrite inj_Zabs_nat; apply Zabs_Zmult. -Qed. +Qed. Lemma Zabs_nat_Zsucc: forall p, 0 <= p -> Zabs_nat (Zsucc p) = S (Zabs_nat p). @@ -151,13 +152,13 @@ Proof. rewrite inj_S; repeat rewrite inj_Zabs_nat, Zabs_eq; auto with zarith. Qed. -Lemma Zabs_nat_Zplus: +Lemma Zabs_nat_Zplus: forall x y, 0<=x -> 0<=y -> Zabs_nat (x+y) = (Zabs_nat x + Zabs_nat y)%nat. Proof. intros; apply inj_eq_rev. rewrite inj_plus; repeat rewrite inj_Zabs_nat, Zabs_eq; auto with zarith. apply Zplus_le_0_compat; auto. -Qed. +Qed. Lemma Zabs_nat_Zminus: forall x y, 0 <= x <= y -> Zabs_nat (y - x) = (Zabs_nat y - Zabs_nat x)%nat. @@ -200,11 +201,11 @@ Qed. (** A characterization of the sign function: *) -Lemma Zsgn_spec : forall x:Z, - 0 < x /\ Zsgn x = 1 \/ - 0 = x /\ Zsgn x = 0 \/ +Lemma Zsgn_spec : forall x:Z, + 0 < x /\ Zsgn x = 1 \/ + 0 = x /\ Zsgn x = 0 \/ 0 > x /\ Zsgn x = -1. -Proof. +Proof. intros; unfold Zsgn, Zle, Zgt; destruct x; compute; intuition. Qed. diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v index 34771897..8cdd73cc 100644 --- a/theories/ZArith/Zbool.v +++ b/theories/ZArith/Zbool.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Zbool.v 12271 2009-08-11 10:29:45Z herbelin $ *) +(* $Id$ *) Require Import BinInt. Require Import Zeven. @@ -228,3 +228,8 @@ Proof. discriminate. Qed. +Lemma Zeq_bool_if : forall x y, if Zeq_bool x y then x=y else x<>y. +Proof. + intros. generalize (Zeq_bool_eq x y)(Zeq_bool_neq x y). + destruct Zeq_bool; auto. +Qed.
\ No newline at end of file diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v index 8244d4ce..3e611d54 100644 --- a/theories/ZArith/Zcompare.v +++ b/theories/ZArith/Zcompare.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -9,7 +10,7 @@ (*i $$ i*) (**********************************************************************) -(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) +(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) (**********************************************************************) Require Export BinPos. @@ -40,12 +41,12 @@ Proof. | destruct ((x' ?= y')%positive Eq); reflexivity || discriminate ] ]. Qed. -Ltac destr_zcompare := - match goal with |- context [Zcompare ?x ?y] => - let H := fresh "H" in +Ltac destr_zcompare := + match goal with |- context [Zcompare ?x ?y] => + let H := fresh "H" in case_eq (Zcompare x y); intro H; [generalize (Zcompare_Eq_eq _ _ H); clear H; intro H | - change (x<y)%Z in H | + change (x<y)%Z in H | change (x>y)%Z in H ] end. @@ -58,35 +59,48 @@ Qed. Lemma Zcompare_antisym : forall n m:Z, CompOpp (n ?= m) = (m ?= n). Proof. intros x y; destruct x; destruct y; simpl in |- *; - reflexivity || discriminate H || rewrite Pcompare_antisym; + reflexivity || discriminate H || rewrite Pcompare_antisym; reflexivity. Qed. Lemma Zcompare_Gt_Lt_antisym : forall n m:Z, (n ?= m) = Gt <-> (m ?= n) = Lt. Proof. - intros x y; split; intro H; - [ change Lt with (CompOpp Gt) in |- *; rewrite <- Zcompare_antisym; - rewrite H; reflexivity - | change Gt with (CompOpp Lt) in |- *; rewrite <- Zcompare_antisym; - rewrite H; reflexivity ]. + intros x y. + rewrite <- Zcompare_antisym. change Gt with (CompOpp Lt). + split. + auto using CompOpp_inj. + intros; f_equal; auto. Qed. +Lemma Zcompare_spec : forall n m, CompSpec eq Zlt n m (n ?= m). +Proof. + intros. + destruct (n?=m) as [ ]_eqn:H; constructor; auto. + apply Zcompare_Eq_eq; auto. + red; rewrite <- Zcompare_antisym, H; auto. +Qed. + + (** * Transitivity of comparison *) +Lemma Zcompare_Lt_trans : + forall n m p:Z, (n ?= m) = Lt -> (m ?= p) = Lt -> (n ?= p) = Lt. +Proof. + intros x y z; case x; case y; case z; simpl; + try discriminate; auto with arith. + intros; eapply Plt_trans; eauto. + intros p q r; rewrite 3 Pcompare_antisym; simpl. + intros; eapply Plt_trans; eauto. +Qed. + Lemma Zcompare_Gt_trans : forall n m p:Z, (n ?= m) = Gt -> (m ?= p) = Gt -> (n ?= p) = Gt. Proof. - intros x y z; case x; case y; case z; simpl in |- *; - try (intros; discriminate H || discriminate H0); auto with arith; - [ intros p q r H H0; apply nat_of_P_gt_Gt_compare_complement_morphism; - unfold gt in |- *; apply lt_trans with (m := nat_of_P q); - apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; - assumption - | intros p q r; do 3 rewrite <- ZC4; intros H H0; - apply nat_of_P_gt_Gt_compare_complement_morphism; - unfold gt in |- *; apply lt_trans with (m := nat_of_P q); - apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; - assumption ]. + intros n m p Hnm Hmp. + apply <- Zcompare_Gt_Lt_antisym. + apply -> Zcompare_Gt_Lt_antisym in Hnm. + apply -> Zcompare_Gt_Lt_antisym in Hmp. + eapply Zcompare_Lt_trans; eauto. Qed. (** * Comparison and opposite *) @@ -129,7 +143,7 @@ Proof. [ reflexivity | apply H | rewrite (Zcompare_opp x y); rewrite Zcompare_opp; - do 2 rewrite Zopp_plus_distr; rewrite Zopp_neg; + do 2 rewrite Zopp_plus_distr; rewrite Zopp_neg; apply H ]. Qed. @@ -145,7 +159,7 @@ Proof. rewrite nat_of_P_minus_morphism; [ unfold gt in |- *; apply ZL16 | assumption ] | intros p; ElimPcompare z p; intros E; auto with arith; - apply nat_of_P_gt_Gt_compare_complement_morphism; + apply nat_of_P_gt_Gt_compare_complement_morphism; unfold gt in |- *; apply ZL17 | intros p q; ElimPcompare q p; intros E; rewrite E; [ rewrite (Pcompare_Eq_eq q p E); apply Pcompare_refl @@ -170,7 +184,7 @@ Proof. [ apply lt_trans with (m := nat_of_P z); [ apply ZL16 | apply ZL17 ] | assumption ] | intros p q; ElimPcompare z q; intros E0; rewrite E0; ElimPcompare z p; - intros E1; rewrite E1; ElimPcompare q p; intros E2; + intros E1; rewrite E1; ElimPcompare q p; intros E2; rewrite E2; auto with arith; [ absurd ((q ?= p)%positive Eq = Lt); [ rewrite <- (Pcompare_Eq_eq z q E0); @@ -273,7 +287,7 @@ Proof. [ rewrite plus_comm; apply plus_lt_reg_l with (p := nat_of_P q); rewrite plus_assoc; rewrite le_plus_minus_r; [ rewrite (plus_comm (nat_of_P q)); apply plus_lt_compat_l; - apply nat_of_P_lt_Lt_compare_morphism; + apply nat_of_P_lt_Lt_compare_morphism; assumption | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; assumption ] @@ -289,7 +303,7 @@ Proof. [ rewrite plus_comm; apply plus_lt_reg_l with (p := nat_of_P p); rewrite plus_assoc; rewrite le_plus_minus_r; [ rewrite (plus_comm (nat_of_P p)); apply plus_lt_compat_l; - apply nat_of_P_lt_Lt_compare_morphism; + apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; assumption | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; assumption ] @@ -330,7 +344,7 @@ Qed. Lemma Zcompare_succ_Gt : forall n:Z, (Zsucc n ?= n) = Gt. Proof. intro x; unfold Zsucc in |- *; pattern x at 2 in |- *; - rewrite <- (Zplus_0_r x); rewrite Zcompare_plus_compat; + rewrite <- (Zplus_0_r x); rewrite Zcompare_plus_compat; reflexivity. Qed. @@ -351,7 +365,7 @@ Proof. apply nat_of_P_lt_Lt_compare_morphism; change ((Zpos h ?= 1) = Lt) in |- *; rewrite <- H2; rewrite <- (fun m n:Z => Zcompare_plus_compat m n y); - rewrite (Zplus_comm x); rewrite Zplus_assoc; + rewrite (Zplus_comm x); rewrite Zplus_assoc; rewrite Zplus_opp_r; simpl in |- *; exact H1 ] ] | intros H1; rewrite H1; discriminate ] | intros H; elim_compare x (y + 1); @@ -369,7 +383,7 @@ Proof. intros n m; unfold Zsucc in |- *; do 2 rewrite (fun t:Z => Zplus_comm t 1); rewrite Zcompare_plus_compat; auto with arith. Qed. - + (** * Multiplication and comparison *) Lemma Zcompare_mult_compat : @@ -394,7 +408,7 @@ Qed. Lemma rename : forall (A:Type) (P:A -> Prop) (x:A), (forall y:A, x = y -> P y) -> P x. Proof. - auto with arith. + auto with arith. Qed. Lemma Zcompare_elim : @@ -473,7 +487,7 @@ Lemma Zge_compare : | Gt => True end. Proof. - intros x y; unfold Zge in |- *; elim (x ?= y); auto with arith. + intros x y; unfold Zge in |- *; elim (x ?= y); auto with arith. Qed. Lemma Zgt_compare : diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v index c6ade934..08cc564d 100644 --- a/theories/ZArith/Zcomplements.v +++ b/theories/ZArith/Zcomplements.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zcomplements.v 10617 2008-03-04 18:07:16Z letouzey $ i*) +(*i $Id$ i*) Require Import ZArithRing. Require Import ZArith_base. @@ -19,26 +19,26 @@ Open Local Scope Z_scope. (** About parity *) Lemma two_or_two_plus_one : - forall n:Z, {y : Z | n = 2 * y} + {y : Z | n = 2 * y + 1}. + forall n:Z, {y : Z | n = 2 * y} + {y : Z | n = 2 * y + 1}. Proof. intro x; destruct x. left; split with 0; reflexivity. - + destruct p. right; split with (Zpos p); reflexivity. - + left; split with (Zpos p); reflexivity. - + right; split with 0; reflexivity. - + destruct p. right; split with (Zneg (1 + p)). rewrite BinInt.Zneg_xI. rewrite BinInt.Zneg_plus_distr. omega. - + left; split with (Zneg p); reflexivity. - + right; split with (-1); reflexivity. Qed. @@ -64,24 +64,24 @@ Proof. trivial. Qed. -Lemma floor_ok : forall p:positive, floor p <= Zpos p < 2 * floor p. +Lemma floor_ok : forall p:positive, floor p <= Zpos p < 2 * floor p. Proof. unfold floor in |- *. intro a; induction a as [p| p| ]. - + simpl in |- *. repeat rewrite BinInt.Zpos_xI. - rewrite (BinInt.Zpos_xO (xO (floor_pos p))). + rewrite (BinInt.Zpos_xO (xO (floor_pos p))). rewrite (BinInt.Zpos_xO (floor_pos p)). omega. - + simpl in |- *. repeat rewrite BinInt.Zpos_xI. rewrite (BinInt.Zpos_xO (xO (floor_pos p))). rewrite (BinInt.Zpos_xO (floor_pos p)). rewrite (BinInt.Zpos_xO p). omega. - + simpl in |- *; omega. Qed. @@ -128,7 +128,7 @@ Proof. elim (Zabs_dec m); intro eq; rewrite eq; trivial. Qed. -(** To do case analysis over the sign of [z] *) +(** To do case analysis over the sign of [z] *) Lemma Zcase_sign : forall (n:Z) (P:Prop), (n = 0 -> P) -> (n > 0 -> P) -> (n < 0 -> P) -> P. @@ -160,11 +160,11 @@ Qed. Require Import List. -Fixpoint Zlength_aux (acc:Z) (A:Type) (l:list A) {struct l} : Z := +Fixpoint Zlength_aux (acc:Z) (A:Type) (l:list A) : Z := match l with | nil => acc | _ :: l => Zlength_aux (Zsucc acc) A l - end. + end. Definition Zlength := Zlength_aux 0. Implicit Arguments Zlength [A]. @@ -177,7 +177,7 @@ Section Zlength_properties. Lemma Zlength_correct : forall l, Zlength l = Z_of_nat (length l). Proof. - assert (forall l (acc:Z), Zlength_aux acc A l = acc + Z_of_nat (length l)). + assert (forall l (acc:Z), Zlength_aux acc A l = acc + Z_of_nat (length l)). simple induction l. simpl in |- *; auto with zarith. intros; simpl (length (a :: l0)) in |- *; rewrite Znat.inj_S. @@ -202,7 +202,7 @@ Section Zlength_properties. case l; auto. intros x l'; simpl (length (x :: l')) in |- *. rewrite Znat.inj_S. - intros; elimtype False; generalize (Zle_0_nat (length l')); omega. + intros; exfalso; generalize (Zle_0_nat (length l')); omega. Qed. End Zlength_properties. diff --git a/theories/ZArith/Zbinary.v b/theories/ZArith/Zdigits.v index 08f08e12..0a6c9498 100644 --- a/theories/ZArith/Zbinary.v +++ b/theories/ZArith/Zdigits.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -6,9 +7,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zbinary.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id$ i*) -(** Bit vectors interpreted as integers. +(** Bit vectors interpreted as integers. Contribution by Jean Duprat (ENS Lyon). *) Require Import Bvector. @@ -16,27 +17,22 @@ Require Import ZArith. Require Export Zpower. Require Import Omega. -(** L'évaluation des vecteurs de booléens se font à la fois en binaire et - en complément à deux. Le nombre appartient à Z. - On utilise donc Omega pour faire les calculs dans Z. - De plus, on utilise les fonctions 2^n où n est un naturel, ici la longueur. - two_power_nat = [n:nat](POS (shift_nat n xH)) - : nat->Z - two_power_nat_S - : (n:nat)`(two_power_nat (S n)) = 2*(two_power_nat n)` - Z_lt_ge_dec - : (x,y:Z){`x < y`}+{`x >= y`} +(** The evaluation of boolean vector is done both in binary and + two's complement. The computed number belongs to Z. + We hence use Omega to perform computations in Z. + Moreover, we use functions [2^n] where [n] is a natural number + (here the vector length). *) Section VALUE_OF_BOOLEAN_VECTORS. -(** Les calculs sont effectués dans la convention positive usuelle. - Les valeurs correspondent soit à l'écriture binaire (nat), - soit au complément à deux (int). - On effectue le calcul suivant le schéma de Horner. - Le complément à deux n'a de sens que sur les vecteurs de taille - supérieure ou égale à un, le bit de signe étant évalué négativement. +(** Computations are done in the usual convention. + The values correspond either to the binary coding (nat) or + to the two's complement coding (int). + We perform the computation via Horner scheme. + The two's complement coding only makes sense on vectors whose + size is greater or equal to one (a sign bit should be present). *) Definition bit_value (b:bool) : Z := @@ -44,12 +40,12 @@ Section VALUE_OF_BOOLEAN_VECTORS. | true => 1%Z | false => 0%Z end. - + Lemma binary_value : forall n:nat, Bvector n -> Z. Proof. simple induction n; intros. exact 0%Z. - + inversion H0. exact (bit_value a + 2 * H H2)%Z. Defined. @@ -68,12 +64,12 @@ End VALUE_OF_BOOLEAN_VECTORS. Section ENCODING_VALUE. -(** On calcule la valeur binaire selon un schema de Horner. - Le calcul s'arrete à la longueur du vecteur sans vérification. - On definit une fonction Zmod2 calquee sur Zdiv2 mais donnant le quotient - de la division z=2q+r avec 0<=r<=1. - La valeur en complément à deux est calculée selon un schema de Horner - avec Zmod2, le paramètre est la taille moins un. +(** We compute the binary value via a Horner scheme. + Computation stops at the vector length without checks. + We define a function Zmod2 similar to Zdiv2 returning the + quotient of division z=2q+r with 0<=r<=1. + The two's complement value is also computed via a Horner scheme + with Zmod2, the parameter is the size minus one. *) Definition Zmod2 (z:Z) := @@ -98,19 +94,19 @@ Section ENCODING_VALUE. Proof. destruct z; simpl in |- *. trivial. - + destruct p; simpl in |- *; trivial. - + destruct p; simpl in |- *. destruct p as [p| p| ]; simpl in |- *. rewrite <- (Pdouble_minus_one_o_succ_eq_xI p); trivial. trivial. - + trivial. - + trivial. - + trivial. Qed. @@ -118,7 +114,7 @@ Section ENCODING_VALUE. Proof. simple induction n; intros. exact Bnil. - + exact (Bcons (Zeven.Zodd_bool H0) n0 (H (Zeven.Zdiv2 H0))). Defined. @@ -126,7 +122,7 @@ Section ENCODING_VALUE. Proof. simple induction n; intros. exact (Bcons (Zeven.Zodd_bool H) 0 Bnil). - + exact (Bcons (Zeven.Zodd_bool H0) (S n0) (H (Zmod2 H0))). Defined. @@ -134,9 +130,8 @@ End ENCODING_VALUE. Section Z_BRIC_A_BRAC. - (** Bibliotheque de lemmes utiles dans la section suivante. - Utilise largement ZArith. - Mériterait d'être récrite. + (** Some auxiliary lemmas used in the next section. Large use of ZArith. + Deserve to be properly rewritten. *) Lemma binary_value_Sn : @@ -206,10 +201,10 @@ Section Z_BRIC_A_BRAC. Proof. destruct z as [| p| p]. auto. - + destruct p; auto. simpl in |- *; intros; omega. - + intro H; elim H; trivial. Qed. @@ -221,11 +216,11 @@ Section Z_BRIC_A_BRAC. intros. cut (2 * Zeven.Zdiv2 z < 2 * two_power_nat n)%Z; intros. omega. - + rewrite <- two_power_nat_S. destruct (Zeven.Zeven_odd_dec z); intros. rewrite <- Zeven.Zeven_div2; auto. - + generalize (Zeven.Zodd_div2 z H z0); omega. Qed. @@ -236,7 +231,7 @@ Section Z_BRIC_A_BRAC. Proof. intros; auto. Qed. - + Lemma Zeven_bit_value : forall z:Z, Zeven.Zeven z -> bit_value (Zeven.Zodd_bool z) = 0%Z. Proof. @@ -244,7 +239,7 @@ Section Z_BRIC_A_BRAC. destruct p; tauto || (intro H; elim H). destruct p; tauto || (intro H; elim H). Qed. - + Lemma Zodd_bit_value : forall z:Z, Zeven.Zodd z -> bit_value (Zeven.Zodd_bool z) = 1%Z. Proof. @@ -253,7 +248,7 @@ Section Z_BRIC_A_BRAC. destruct p; tauto || (intros; elim H). destruct p; tauto || (intros; elim H). Qed. - + Lemma Zge_minus_two_power_nat_S : forall (n:nat) (z:Z), (z >= - two_power_nat (S n))%Z -> (Zmod2 z >= - two_power_nat n)%Z. @@ -265,7 +260,7 @@ Section Z_BRIC_A_BRAC. rewrite (Zodd_bit_value z H); intros; omega. Qed. - + Lemma Zlt_two_power_nat_S : forall (n:nat) (z:Z), (z < two_power_nat (S n))%Z -> (Zmod2 z < two_power_nat n)%Z. @@ -282,8 +277,8 @@ End Z_BRIC_A_BRAC. Section COHERENT_VALUE. -(** On vérifie que dans l'intervalle de définition les fonctions sont - réciproques l'une de l'autre. Elles utilisent les lemmes du bric-a-brac. +(** We check that the functions are reciprocal on the definition interval. + This uses earlier library lemmas. *) Lemma binary_to_Z_to_binary : @@ -291,26 +286,26 @@ Section COHERENT_VALUE. Proof. induction bv as [| a n bv IHbv]. auto. - + rewrite binary_value_Sn. rewrite Z_to_binary_Sn. rewrite IHbv; trivial. - + apply binary_value_pos. Qed. - + Lemma two_compl_to_Z_to_two_compl : forall (n:nat) (bv:Bvector n) (b:bool), Z_to_two_compl n (two_compl_value n (Bcons b n bv)) = Bcons b n bv. Proof. induction bv as [| a n bv IHbv]; intro b. destruct b; auto. - + rewrite two_compl_value_Sn. rewrite Z_to_two_compl_Sn. rewrite IHbv; trivial. Qed. - + Lemma Z_to_binary_to_Z : forall (n:nat) (z:Z), (z >= 0)%Z -> @@ -318,17 +313,17 @@ Section COHERENT_VALUE. Proof. induction n as [| n IHn]. unfold two_power_nat, shift_nat in |- *; simpl in |- *; intros; omega. - + intros; rewrite Z_to_binary_Sn_z. rewrite binary_value_Sn. rewrite IHn. apply Z_div2_value; auto. - + apply Pdiv2; trivial. - + apply Zdiv2_two_power_nat; trivial. Qed. - + Lemma Z_to_two_compl_to_Z : forall (n:nat) (z:Z), (z >= - two_power_nat n)%Z -> @@ -345,7 +340,7 @@ Section COHERENT_VALUE. generalize (Zmod2_twice z); omega. apply Zge_minus_two_power_nat_S; auto. - + apply Zlt_two_power_nat_S; auto. Qed. diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index 228a882a..f3e65697 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -6,13 +7,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zdiv.v 11477 2008-10-20 15:16:14Z letouzey $ i*) +(*i $Id$ i*) (* Contribution by Claude Marché and Xavier Urbain *) (** Euclidean Division - Defines first of function that allows Coq to normalize. + Defines first of function that allows Coq to normalize. Then only after proves the main required property. *) @@ -26,16 +27,15 @@ Open Local Scope Z_scope. (** * Definitions of Euclidian operations *) -(** Euclidean division of a positive by a integer +(** Euclidean division of a positive by a integer (that is supposed to be positive). Total function than returns an arbitrary value when divisor is not positive - + *) -Unboxed Fixpoint Zdiv_eucl_POS (a:positive) (b:Z) {struct a} : - Z * Z := +Unboxed Fixpoint Zdiv_eucl_POS (a:positive) (b:Z) : Z * Z := match a with | xH => if Zge_bool b 2 then (0, 1) else (1, 0) | xO a' => @@ -50,41 +50,41 @@ Unboxed Fixpoint Zdiv_eucl_POS (a:positive) (b:Z) {struct a} : (** Euclidean division of integers. - - Total function than returns (0,0) when dividing by 0. -*) - -(** + + Total function than returns (0,0) when dividing by 0. +*) + +(** The pseudo-code is: - + if b = 0 : (0,0) - + if b <> 0 and a = 0 : (0,0) - if b > 0 and a < 0 : let (q,r) = div_eucl_pos (-a) b in + if b > 0 and a < 0 : let (q,r) = div_eucl_pos (-a) b in if r = 0 then (-q,0) else (-(q+1),b-r) if b < 0 and a < 0 : let (q,r) = div_eucl (-a) (-b) in (q,-r) - if b < 0 and a > 0 : let (q,r) = div_eucl a (-b) in + if b < 0 and a > 0 : let (q,r) = div_eucl a (-b) in if r = 0 then (-q,0) else (-(q+1),b+r) - In other word, when b is non-zero, q is chosen to be the greatest integer - smaller or equal to a/b. And sgn(r)=sgn(b) and |r| < |b| (at least when - r is not null). + In other word, when b is non-zero, q is chosen to be the greatest integer + smaller or equal to a/b. And sgn(r)=sgn(b) and |r| < |b| (at least when + r is not null). *) (* Nota: At least two others conventions also exist for euclidean division. - They all satify the equation a=b*q+r, but differ on the choice of (q,r) + They all satify the equation a=b*q+r, but differ on the choice of (q,r) on negative numbers. * Ocaml uses Round-Toward-Zero division: (-a)/b = a/(-b) = -(a/b). Hence (-a) mod b = - (a mod b) a mod (-b) = a mod b - And: |r| < |b| and sgn(r) = sgn(a) (notice the a here instead of b). + And: |r| < |b| and sgn(r) = sgn(a) (notice the a here instead of b). - * Another solution is to always pick a non-negative remainder: + * Another solution is to always pick a non-negative remainder: a=b*q+r with 0 <= r < |b| *) @@ -113,7 +113,7 @@ Definition Zdiv_eucl (a b:Z) : Z * Z := Definition Zdiv (a b:Z) : Z := let (q, _) := Zdiv_eucl a b in q. -Definition Zmod (a b:Z) : Z := let (_, r) := Zdiv_eucl a b in r. +Definition Zmod (a b:Z) : Z := let (_, r) := Zdiv_eucl a b in r. (** Syntax *) @@ -122,7 +122,7 @@ Infix "mod" := Zmod (at level 40, no associativity) : Z_scope. (* Tests: -Eval compute in (Zdiv_eucl 7 3). +Eval compute in (Zdiv_eucl 7 3). Eval compute in (Zdiv_eucl (-7) 3). @@ -133,7 +133,7 @@ Eval compute in (Zdiv_eucl (-7) (-3)). *) -(** * Main division theorem *) +(** * Main division theorem *) (** First a lemma for two positive arguments *) @@ -170,7 +170,7 @@ Theorem Z_div_mod : Proof. intros a b; case a; case b; try (simpl in |- *; intros; omega). unfold Zdiv_eucl in |- *; intros; apply Z_div_mod_POS; trivial. - + intros; discriminate. intros. @@ -179,25 +179,25 @@ Proof. case (Zdiv_eucl_POS p0 (Zpos p)). intros z z0. case z0. - + intros [H1 H2]. split; trivial. change (Zneg p0) with (- Zpos p0); rewrite H1; ring. - + intros p1 [H1 H2]. split; trivial. change (Zneg p0) with (- Zpos p0); rewrite H1; ring. generalize (Zorder.Zgt_pos_0 p1); omega. - + intros p1 [H1 H2]. split; trivial. change (Zneg p0) with (- Zpos p0); rewrite H1; ring. generalize (Zorder.Zlt_neg_0 p1); omega. - + intros; discriminate. Qed. -(** For stating the fully general result, let's give a short name +(** For stating the fully general result, let's give a short name to the condition on the remainder. *) Definition Remainder r b := 0 <= r < b \/ b < r <= 0. @@ -206,7 +206,7 @@ Definition Remainder r b := 0 <= r < b \/ b < r <= 0. Definition Remainder_alt r b := Zabs r < Zabs b /\ Zsgn r <> - Zsgn b. -(* In the last formulation, [ Zsgn r <> - Zsgn b ] is less nice than saying +(* In the last formulation, [ Zsgn r <> - Zsgn b ] is less nice than saying [ Zsgn r = Zsgn b ], but at least it works even when [r] is null. *) Lemma Remainder_equiv : forall r b, Remainder r b <-> Remainder_alt r b. @@ -250,7 +250,7 @@ Proof. destruct Zdiv_eucl_POS as (q,r). destruct r as [|r|r]; change (Zneg b) with (-Zpos b). rewrite Zmult_opp_comm; omega with *. - rewrite <- Zmult_opp_comm, Zmult_plus_distr_r; + rewrite <- Zmult_opp_comm, Zmult_plus_distr_r; repeat rewrite Zmult_opp_comm; omega. rewrite Zmult_opp_comm; omega with *. Qed. @@ -331,14 +331,14 @@ elim (Zlt_not_le (Zabs (r2 - r1)) (Zabs b)). omega with *. replace (r2-r1) with (b*(q1-q2)) by (rewrite Zmult_minus_distr_l; omega). replace (Zabs b) with ((Zabs b)*1) by ring. -rewrite Zabs_Zmult. +rewrite Zabs_Zmult. apply Zmult_le_compat_l; auto with *. omega with *. Qed. Theorem Zdiv_mod_unique_2 : forall b q1 q2 r1 r2:Z, - Remainder r1 b -> Remainder r2 b -> + Remainder r1 b -> Remainder r2 b -> b*q1+r1 = b*q2+r2 -> q1=q2 /\ r1=r2. Proof. unfold Remainder. @@ -356,7 +356,7 @@ omega with *. Qed. Theorem Zdiv_unique_full: - forall a b q r, Remainder r b -> + forall a b q r, Remainder r b -> a = b*q + r -> q = a/b. Proof. intros. @@ -368,7 +368,7 @@ Proof. Qed. Theorem Zdiv_unique: - forall a b q r, 0 <= r < b -> + forall a b q r, 0 <= r < b -> a = b*q + r -> q = a/b. Proof. intros; eapply Zdiv_unique_full; eauto. @@ -425,7 +425,7 @@ Proof. intros; symmetry; apply Zdiv_unique with 0; auto with zarith. Qed. -Hint Resolve Zmod_0_l Zmod_0_r Zdiv_0_l Zdiv_0_r Zdiv_1_r Zmod_1_r +Hint Resolve Zmod_0_l Zmod_0_r Zdiv_0_l Zdiv_0_r Zdiv_1_r Zmod_1_r : zarith. Lemma Zdiv_1_l: forall a, 1 < a -> 1/a = 0. @@ -460,7 +460,7 @@ Qed. Lemma Z_div_mult_full : forall a b:Z, b <> 0 -> (a*b)/b = a. Proof. - intros; symmetry; apply Zdiv_unique_full with 0; auto with zarith; + intros; symmetry; apply Zdiv_unique_full with 0; auto with zarith; [ red; omega | ring]. Qed. @@ -485,7 +485,7 @@ Proof. intros; generalize (Z_div_pos a b H); auto with zarith. Qed. -(** As soon as the divisor is greater or equal than 2, +(** As soon as the divisor is greater or equal than 2, the division is strictly decreasing. *) Lemma Z_div_lt : forall a b:Z, b >= 2 -> a > 0 -> a/b < a. @@ -530,7 +530,7 @@ Proof. intro. absurd (b - a >= 1). omega. - replace (b-a) with (c * (b/c-a/c) + b mod c - a mod c) by + replace (b-a) with (c * (b/c-a/c) + b mod c - a mod c) by (symmetry; pattern a at 1; rewrite H2; pattern b at 1; rewrite H0; ring). assert (c * (b / c - a / c) >= c * 1). apply Zmult_ge_compat_l. @@ -580,7 +580,7 @@ Qed. (** A modulo cannot grow beyond its starting point. *) Theorem Zmod_le: forall a b, 0 < b -> 0 <= a -> a mod b <= a. -Proof. +Proof. intros a b H1 H2; case (Zle_or_lt b a); intros H3. case (Z_mod_lt a b); auto with zarith. rewrite Zmod_small; auto with zarith. @@ -588,45 +588,38 @@ Qed. (** Some additionnal inequalities about Zdiv. *) -Theorem Zdiv_le_upper_bound: - forall a b q, 0 <= a -> 0 < b -> a <= q*b -> a/b <= q. +Theorem Zdiv_lt_upper_bound: + forall a b q, 0 < b -> a < q*b -> a/b < q. Proof. - intros a b q H1 H2 H3. - apply Zmult_le_reg_r with b; auto with zarith. - apply Zle_trans with (2 := H3). + intros a b q H1 H2. + apply Zmult_lt_reg_r with b; auto with zarith. + apply Zle_lt_trans with (2 := H2). pattern a at 2; rewrite (Z_div_mod_eq a b); auto with zarith. rewrite (Zmult_comm b); case (Z_mod_lt a b); auto with zarith. Qed. -Theorem Zdiv_lt_upper_bound: - forall a b q, 0 <= a -> 0 < b -> a < q*b -> a/b < q. +Theorem Zdiv_le_upper_bound: + forall a b q, 0 < b -> a <= q*b -> a/b <= q. Proof. - intros a b q H1 H2 H3. - apply Zmult_lt_reg_r with b; auto with zarith. - apply Zle_lt_trans with (2 := H3). - pattern a at 2; rewrite (Z_div_mod_eq a b); auto with zarith. - rewrite (Zmult_comm b); case (Z_mod_lt a b); auto with zarith. + intros. + rewrite <- (Z_div_mult_full q b); auto with zarith. + apply Z_div_le; auto with zarith. Qed. -Theorem Zdiv_le_lower_bound: - forall a b q, 0 <= a -> 0 < b -> q*b <= a -> q <= a/b. +Theorem Zdiv_le_lower_bound: + forall a b q, 0 < b -> q*b <= a -> q <= a/b. Proof. - intros a b q H1 H2 H3. - assert (q < a / b + 1); auto with zarith. - apply Zmult_lt_reg_r with b; auto with zarith. - apply Zle_lt_trans with (1 := H3). - pattern a at 1; rewrite (Z_div_mod_eq a b); auto with zarith. - rewrite Zmult_plus_distr_l; rewrite (Zmult_comm b); case (Z_mod_lt a b); - auto with zarith. + intros. + rewrite <- (Z_div_mult_full q b); auto with zarith. + apply Z_div_le; auto with zarith. Qed. - (** A division of respect opposite monotonicity for the divisor *) Lemma Zdiv_le_compat_l: forall p q r, 0 <= p -> 0 < q < r -> p / r <= p / q. Proof. - intros p q r H H1. + intros p q r H H1. apply Zdiv_le_lower_bound; auto with zarith. rewrite Zmult_comm. pattern p at 2; rewrite (Z_div_mod_eq p r); auto with zarith. @@ -636,11 +629,11 @@ Proof. case (Z_mod_lt p r); auto with zarith. Qed. -Theorem Zdiv_sgn: forall a b, +Theorem Zdiv_sgn: forall a b, 0 <= Zsgn (a/b) * Zsgn a * Zsgn b. Proof. - destruct a as [ |a|a]; destruct b as [ |b|b]; simpl; auto with zarith; - generalize (Z_div_pos (Zpos a) (Zpos b)); unfold Zdiv, Zdiv_eucl; + destruct a as [ |a|a]; destruct b as [ |b|b]; simpl; auto with zarith; + generalize (Z_div_pos (Zpos a) (Zpos b)); unfold Zdiv, Zdiv_eucl; destruct Zdiv_eucl_POS as (q,r); destruct r; omega with *. Qed. @@ -668,12 +661,12 @@ Qed. Theorem Z_div_plus_full_l: forall a b c : Z, b <> 0 -> (a * b + c) / b = a + c / b. Proof. intros a b c H; rewrite Zplus_comm; rewrite Z_div_plus_full; - try apply Zplus_comm; auto with zarith. + try apply Zplus_comm; auto with zarith. Qed. (** [Zopp] and [Zdiv], [Zmod]. - Due to the choice of convention for our Euclidean division, - some of the relations about [Zopp] and divisions are rather complex. *) + Due to the choice of convention for our Euclidean division, + some of the relations about [Zopp] and divisions are rather complex. *) Lemma Zdiv_opp_opp : forall a b:Z, (-a)/(-b) = a/b. Proof. @@ -702,7 +695,7 @@ Proof. ring. Qed. -Lemma Z_mod_nz_opp_full : forall a b:Z, a mod b <> 0 -> +Lemma Z_mod_nz_opp_full : forall a b:Z, a mod b <> 0 -> (-a) mod b = b - (a mod b). Proof. intros. @@ -721,7 +714,7 @@ Proof. rewrite Z_mod_zero_opp_full; auto. Qed. -Lemma Z_mod_nz_opp_r : forall a b:Z, a mod b <> 0 -> +Lemma Z_mod_nz_opp_r : forall a b:Z, a mod b <> 0 -> a mod (-b) = (a mod b) - b. Proof. intros. @@ -740,7 +733,7 @@ Proof. rewrite H; ring. Qed. -Lemma Z_div_nz_opp_full : forall a b:Z, a mod b <> 0 -> +Lemma Z_div_nz_opp_full : forall a b:Z, a mod b <> 0 -> (-a)/b = -(a/b)-1. Proof. intros. @@ -758,7 +751,7 @@ Proof. rewrite Z_div_zero_opp_full; auto. Qed. -Lemma Z_div_nz_opp_r : forall a b:Z, a mod b <> 0 -> +Lemma Z_div_nz_opp_r : forall a b:Z, a mod b <> 0 -> a/(-b) = -(a/b)-1. Proof. intros. @@ -769,7 +762,7 @@ Qed. (** Cancellations. *) -Lemma Zdiv_mult_cancel_r : forall a b c:Z, +Lemma Zdiv_mult_cancel_r : forall a b c:Z, c <> 0 -> (a*c)/(b*c) = a/b. Proof. assert (X: forall a b c, b > 0 -> c > 0 -> (a*c) / (b*c) = a / b). @@ -781,17 +774,17 @@ assert (X: forall a b c, b > 0 -> c > 0 -> (a*c) / (b*c) = a / b). apply Zmult_lt_compat_r; auto with zarith. pattern a at 1; rewrite (Z_div_mod_eq a b Hb); ring. intros a b c Hc. -destruct (Z_dec b 0) as [Hb|Hb]. +destruct (Z_dec b 0) as [Hb|Hb]. destruct Hb as [Hb|Hb]; destruct (not_Zeq_inf _ _ Hc); auto with *. -rewrite <- (Zdiv_opp_opp a), <- (Zmult_opp_opp b), <-(Zmult_opp_opp a); +rewrite <- (Zdiv_opp_opp a), <- (Zmult_opp_opp b), <-(Zmult_opp_opp a); auto with *. -rewrite <- (Zdiv_opp_opp a), <- Zdiv_opp_opp, Zopp_mult_distr_l, +rewrite <- (Zdiv_opp_opp a), <- Zdiv_opp_opp, Zopp_mult_distr_l, Zopp_mult_distr_l; auto with *. rewrite <- Zdiv_opp_opp, Zopp_mult_distr_r, Zopp_mult_distr_r; auto with *. rewrite Hb; simpl; do 2 rewrite Zdiv_0_r; auto. Qed. -Lemma Zdiv_mult_cancel_l : forall a b c:Z, +Lemma Zdiv_mult_cancel_l : forall a b c:Z, c<>0 -> (c*a)/(c*b) = a/b. Proof. intros. @@ -799,7 +792,7 @@ Proof. apply Zdiv_mult_cancel_r; auto. Qed. -Lemma Zmult_mod_distr_l: forall a b c, +Lemma Zmult_mod_distr_l: forall a b c, (c*a) mod (c*b) = c * (a mod b). Proof. intros; destruct (Z_eq_dec c 0) as [Hc|Hc]. @@ -814,7 +807,7 @@ Proof. ring. Qed. -Lemma Zmult_mod_distr_r: forall a b c, +Lemma Zmult_mod_distr_r: forall a b c, (a*c) mod (b*c) = (a mod b) * c. Proof. intros; repeat rewrite (fun x => (Zmult_comm x c)). @@ -982,8 +975,8 @@ Proof. apply Zplus_le_compat;auto with zarith. destruct (Z_mod_lt (a/b) c);auto with zarith. replace (b * (c - 1) + (b - 1)) with (b*c-1);try ring;auto with zarith. - intro H1; - assert (H2: c <> 0) by auto with zarith; + intro H1; + assert (H2: c <> 0) by auto with zarith; rewrite (Zmult_integral_l _ _ H2 H1) in H; auto with zarith. Qed. @@ -996,7 +989,7 @@ Theorem Zdiv_mult_le: forall a b c, 0<=a -> 0<=b -> 0<=c -> c*(a/b) <= (c*a)/b. Proof. intros a b c H1 H2 H3. - destruct (Zle_lt_or_eq _ _ H2); + destruct (Zle_lt_or_eq _ _ H2); [ | subst; rewrite Zdiv_0_r, Zdiv_0_r, Zmult_0_r; auto]. case (Z_mod_lt a b); auto with zarith; intros Hu1 Hu2. case (Z_mod_lt c b); auto with zarith; intros Hv1 Hv2. @@ -1012,14 +1005,14 @@ Proof. apply (Zmod_le ((c mod b) * (a mod b)) b); auto with zarith. apply Zmult_le_compat_r; auto with zarith. apply (Zmod_le c b); auto. - pattern (c * a) at 1; rewrite (Z_div_mod_eq (c * a) b); try ring; + pattern (c * a) at 1; rewrite (Z_div_mod_eq (c * a) b); try ring; auto with zarith. pattern a at 1; rewrite (Z_div_mod_eq a b); try ring; auto with zarith. Qed. (** Zmod is related to divisibility (see more in Znumtheory) *) -Lemma Zmod_divides : forall a b, b<>0 -> +Lemma Zmod_divides : forall a b, b<>0 -> (a mod b = 0 <-> exists c, a = b*c). Proof. split; intros. @@ -1077,7 +1070,7 @@ Qed. (** * A direct way to compute Zmod *) -Fixpoint Zmod_POS (a : positive) (b : Z) {struct a} : Z := +Fixpoint Zmod_POS (a : positive) (b : Z) : Z := match a with | xI a' => let r := Zmod_POS a' b in @@ -1166,11 +1159,11 @@ Qed. Implicit Arguments Zdiv_eucl_extended. (** A third convention: Ocaml. - + See files ZOdiv_def.v and ZOdiv.v. - + Ocaml uses Round-Toward-Zero division: (-a)/b = a/(-b) = -(a/b). Hence (-a) mod b = - (a mod b) a mod (-b) = a mod b - And: |r| < |b| and sgn(r) = sgn(a) (notice the a here instead of b). + And: |r| < |b| and sgn(r) = sgn(a) (notice the a here instead of b). *) diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v index 4a402c61..09131043 100644 --- a/theories/ZArith/Zeven.v +++ b/theories/ZArith/Zeven.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zeven.v 10291 2007-11-06 02:18:53Z letouzey $ i*) +(*i $Id$ i*) Require Import BinInt. @@ -96,32 +96,32 @@ Qed. Lemma Zeven_Sn : forall n:Z, Zodd n -> Zeven (Zsucc n). Proof. intro z; destruct z; unfold Zsucc in |- *; - [ idtac | destruct p | destruct p ]; simpl in |- *; - trivial. + [ idtac | destruct p | destruct p ]; simpl in |- *; + trivial. unfold Pdouble_minus_one in |- *; case p; simpl in |- *; auto. Qed. Lemma Zodd_Sn : forall n:Z, Zeven n -> Zodd (Zsucc n). Proof. intro z; destruct z; unfold Zsucc in |- *; - [ idtac | destruct p | destruct p ]; simpl in |- *; - trivial. + [ idtac | destruct p | destruct p ]; simpl in |- *; + trivial. unfold Pdouble_minus_one in |- *; case p; simpl in |- *; auto. Qed. Lemma Zeven_pred : forall n:Z, Zodd n -> Zeven (Zpred n). Proof. intro z; destruct z; unfold Zpred in |- *; - [ idtac | destruct p | destruct p ]; simpl in |- *; - trivial. + [ idtac | destruct p | destruct p ]; simpl in |- *; + trivial. unfold Pdouble_minus_one in |- *; case p; simpl in |- *; auto. Qed. Lemma Zodd_pred : forall n:Z, Zeven n -> Zodd (Zpred n). Proof. intro z; destruct z; unfold Zpred in |- *; - [ idtac | destruct p | destruct p ]; simpl in |- *; - trivial. + [ idtac | destruct p | destruct p ]; simpl in |- *; + trivial. unfold Pdouble_minus_one in |- *; case p; simpl in |- *; auto. Qed. @@ -132,7 +132,7 @@ Hint Unfold Zeven Zodd: zarith. (** * Definition of [Zdiv2] and properties wrt [Zeven] and [Zodd] *) (** [Zdiv2] is defined on all [Z], but notice that for odd negative - integers it is not the euclidean quotient: in that case we have + integers it is not the euclidean quotient: in that case we have [n = 2*(n/2)-1] *) Definition Zdiv2 (z:Z) := @@ -200,7 +200,7 @@ Proof. intros x. elim (Z_modulo_2 x); intros [y Hy]; rewrite Zmult_comm in Hy; rewrite <- Zplus_diag_eq_mult_2 in Hy. - exists (y, y); split. + exists (y, y); split. assumption. left; reflexivity. exists (y, (y + 1)%Z); split. @@ -239,7 +239,7 @@ Proof. destruct p; simpl; auto. Qed. -Theorem Zeven_plus_Zodd: forall a b, +Theorem Zeven_plus_Zodd: forall a b, Zeven a -> Zodd b -> Zodd (a + b). Proof. intros a b H1 H2; case Zeven_ex with (1 := H1); intros x H3; try rewrite H3; auto. @@ -257,13 +257,13 @@ Proof. apply Zmult_plus_distr_r; auto. Qed. -Theorem Zodd_plus_Zeven: forall a b, +Theorem Zodd_plus_Zeven: forall a b, Zodd a -> Zeven b -> Zodd (a + b). Proof. intros a b H1 H2; rewrite Zplus_comm; apply Zeven_plus_Zodd; auto. Qed. -Theorem Zodd_plus_Zodd: forall a b, +Theorem Zodd_plus_Zodd: forall a b, Zodd a -> Zodd b -> Zeven (a + b). Proof. intros a b H1 H2; case Zodd_ex with (1 := H1); intros x H3; try rewrite H3; auto. @@ -276,7 +276,7 @@ Proof. repeat rewrite <- Zplus_assoc; auto. Qed. -Theorem Zeven_mult_Zeven_l: forall a b, +Theorem Zeven_mult_Zeven_l: forall a b, Zeven a -> Zeven (a * b). Proof. intros a b H1; case Zeven_ex with (1 := H1); intros x H3; try rewrite H3; auto. @@ -285,7 +285,7 @@ Proof. apply Zmult_assoc. Qed. -Theorem Zeven_mult_Zeven_r: forall a b, +Theorem Zeven_mult_Zeven_r: forall a b, Zeven b -> Zeven (a * b). Proof. intros a b H1; case Zeven_ex with (1 := H1); intros x H3; try rewrite H3; auto. @@ -296,10 +296,10 @@ Proof. rewrite (Zmult_comm 2 a); auto. Qed. -Hint Rewrite Zmult_plus_distr_r Zmult_plus_distr_l +Hint Rewrite Zmult_plus_distr_r Zmult_plus_distr_l Zplus_assoc Zmult_1_r Zmult_1_l : Zexpand. -Theorem Zodd_mult_Zodd: forall a b, +Theorem Zodd_mult_Zodd: forall a b, Zodd a -> Zodd b -> Zodd (a * b). Proof. intros a b H1 H2; case Zodd_ex with (1 := H1); intros x H3; try rewrite H3; auto. @@ -308,7 +308,7 @@ Proof. (* ring part *) autorewrite with Zexpand; f_equal. repeat rewrite <- Zplus_assoc; f_equal. - repeat rewrite <- Zmult_assoc; f_equal. + repeat rewrite <- Zmult_assoc; f_equal. repeat rewrite Zmult_assoc; f_equal; apply Zmult_comm. Qed. diff --git a/theories/ZArith/Zgcd_alt.v b/theories/ZArith/Zgcd_alt.v index 286dd710..447f6101 100644 --- a/theories/ZArith/Zgcd_alt.v +++ b/theories/ZArith/Zgcd_alt.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zgcd_alt.v 10997 2008-05-27 15:16:40Z letouzey $ i*) +(*i $Id$ i*) (** * Zgcd_alt : an alternate version of Zgcd, based on Euler's algorithm *) @@ -30,7 +30,7 @@ Open Scope Z_scope. (** In Coq, we need to control the number of iteration of modulo. For that, we use an explicit measure in [nat], and we prove later - that using [2*d] is enough, where [d] is the number of binary + that using [2*d] is enough, where [d] is the number of binary digits of the first argument. *) Fixpoint Zgcdn (n:nat) : Z -> Z -> Z := fun a b => @@ -43,17 +43,17 @@ Open Scope Z_scope. end end. - Definition Zgcd_bound (a:Z) := + Definition Zgcd_bound (a:Z) := match a with | Z0 => S O | Zpos p => let n := Psize p in (n+n)%nat | Zneg p => let n := Psize p in (n+n)%nat end. - + Definition Zgcd_alt a b := Zgcdn (Zgcd_bound a) a b. - + (** A first obvious fact : [Zgcd a b] is positive. *) - + Lemma Zgcdn_pos : forall n a b, 0 <= Zgcdn n a b. Proof. @@ -61,22 +61,22 @@ Open Scope Z_scope. simpl; auto with zarith. destruct a; simpl; intros; auto with zarith; auto. Qed. - + Lemma Zgcd_alt_pos : forall a b, 0 <= Zgcd_alt a b. Proof. intros; unfold Zgcd; apply Zgcdn_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. + exfalso; generalize (Zabs_pos a); omega. destruct a; intros; simpl; [ generalize (Zis_gcd_0_abs b); intuition | | ]; unfold Zmod; @@ -93,17 +93,17 @@ Open Scope Z_scope. 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). @@ -118,7 +118,7 @@ Open Scope Z_scope. 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. @@ -131,11 +131,11 @@ Open Scope Z_scope. 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) -> @@ -192,14 +192,14 @@ Open Scope Z_scope. 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]. + destruct a; [ destruct 1; exfalso; 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) -> @@ -224,44 +224,44 @@ Open Scope Z_scope. 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; [ | | compute; auto ]; + induction p; [ | | compute; auto ]; simpl Zgcd_bound in *; - rewrite plus_comm; simpl plus; + rewrite plus_comm; simpl plus; set (n:= (Psize p+Psize p)%nat) in *; simpl; assert (n <> O) by (unfold n; destruct p; simpl; auto). - + destruct n as [ |m]; [elim H; auto| ]. generalize (fibonacci_pos m); rewrite Zpos_xI; omega. destruct n as [ |m]; [elim H; auto| ]. generalize (fibonacci_pos m); rewrite Zpos_xO; omega. Qed. - + (* 5) the end: we glue everything together and take care of situations not corresponding to [0<a<b]. *) Lemma Zgcdn_is_gcd : - forall n a b, (Zgcd_bound a <= n)%nat -> + forall n a b, (Zgcd_bound a <= n)%nat -> Zis_gcd a b (Zgcdn n a b). Proof. destruct a; intros. simpl in H. - destruct n; [elimtype False; omega | ]. + destruct n; [exfalso; omega | ]. simpl; generalize (Zis_gcd_0_abs b); intuition. (*Zpos*) generalize (Zgcd_bound_fibonacci (Zpos p)). simpl Zgcd_bound in *. remember (Psize p+Psize p)%nat as m. assert (1 < m)%nat. - rewrite Heqm; destruct p; simpl; rewrite 1? plus_comm; + rewrite Heqm; destruct p; simpl; rewrite 1? plus_comm; auto with arith. destruct m as [ |m]; [inversion H0; auto| ]. destruct n as [ |n]; [inversion H; auto| ]. @@ -277,15 +277,15 @@ Open Scope Z_scope. apply Zgcdn_ok_before_fibonacci; auto. apply Zlt_le_trans with (fibonacci (S m)); [ omega | apply fibonacci_incr; auto]. subst r; simpl. - destruct m as [ |m]; [elimtype False; omega| ]. - destruct n as [ |n]; [elimtype False; omega| ]. + destruct m as [ |m]; [exfalso; omega| ]. + destruct n as [ |n]; [exfalso; omega| ]. simpl; apply Zis_gcd_sym; apply Zis_gcd_0. (*Zneg*) generalize (Zgcd_bound_fibonacci (Zpos p)). simpl Zgcd_bound in *. remember (Psize p+Psize p)%nat as m. assert (1 < m)%nat. - rewrite Heqm; destruct p; simpl; rewrite 1? plus_comm; + rewrite Heqm; destruct p; simpl; rewrite 1? plus_comm; auto with arith. destruct m as [ |m]; [inversion H0; auto| ]. destruct n as [ |n]; [inversion H; auto| ]. @@ -303,11 +303,11 @@ Open Scope Z_scope. apply Zgcdn_ok_before_fibonacci; auto. apply Zlt_le_trans with (fibonacci (S m)); [ omega | apply fibonacci_incr; auto]. subst r; simpl. - destruct m as [ |m]; [elimtype False; omega| ]. - destruct n as [ |n]; [elimtype False; omega| ]. + destruct m as [ |m]; [exfalso; omega| ]. + destruct n as [ |n]; [exfalso; omega| ]. simpl; apply Zis_gcd_sym; apply Zis_gcd_0. Qed. - + Lemma Zgcd_is_gcd : forall a b, Zis_gcd a b (Zgcd_alt a b). Proof. diff --git a/theories/ZArith/Zhints.v b/theories/ZArith/Zhints.v index b8f8ba30..5459e693 100644 --- a/theories/ZArith/Zhints.v +++ b/theories/ZArith/Zhints.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zhints.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id$ i*) (** This file centralizes the lemmas about [Z], classifying them according to the way they can be used in automatic search *) @@ -40,27 +40,27 @@ Require Import Wf_Z. (** No subgoal or smaller subgoals *) -Hint Resolve +Hint Resolve (** ** Reversible simplification lemmas (no loss of information) *) (** Should clearly be declared as hints *) - + (** Lemmas ending by eq *) Zsucc_eq_compat (* :(n,m:Z)`n = m`->`(Zs n) = (Zs m)` *) - + (** Lemmas ending by Zgt *) Zsucc_gt_compat (* :(n,m:Z)`m > n`->`(Zs m) > (Zs n)` *) Zgt_succ (* :(n:Z)`(Zs n) > n` *) Zorder.Zgt_pos_0 (* :(p:positive)`(POS p) > 0` *) Zplus_gt_compat_l (* :(n,m,p:Z)`n > m`->`p+n > p+m` *) Zplus_gt_compat_r (* :(n,m,p:Z)`n > m`->`n+p > m+p` *) - + (** Lemmas ending by Zlt *) Zlt_succ (* :(n:Z)`n < (Zs n)` *) Zsucc_lt_compat (* :(n,m:Z)`n < m`->`(Zs n) < (Zs m)` *) Zlt_pred (* :(n:Z)`(Zpred n) < n` *) Zplus_lt_compat_l (* :(n,m,p:Z)`n < m`->`p+n < p+m` *) Zplus_lt_compat_r (* :(n,m,p:Z)`n < m`->`n+p < m+p` *) - + (** Lemmas ending by Zle *) Zle_0_nat (* :(n:nat)`0 <= (inject_nat n)` *) Zorder.Zle_0_pos (* :(p:positive)`0 <= (POS p)` *) @@ -73,24 +73,24 @@ Hint Resolve Zplus_le_compat_l (* :(n,m,p:Z)`n <= m`->`p+n <= p+m` *) Zplus_le_compat_r (* :(a,b,c:Z)`a <= b`->`a+c <= b+c` *) Zabs_pos (* :(x:Z)`0 <= |x|` *) - + (** ** Irreversible simplification lemmas *) (** Probably to be declared as hints, when no other simplification is possible *) - + (** Lemmas ending by eq *) BinInt.Z_eq_mult (* :(x,y:Z)`y = 0`->`y*x = 0` *) Zplus_eq_compat (* :(n,m,p,q:Z)`n = m`->`p = q`->`n+p = m+q` *) - + (** Lemmas ending by Zge *) Zorder.Zmult_ge_compat_r (* :(a,b,c:Z)`a >= b`->`c >= 0`->`a*c >= b*c` *) Zorder.Zmult_ge_compat_l (* :(a,b,c:Z)`a >= b`->`c >= 0`->`c*a >= c*b` *) Zorder.Zmult_ge_compat (* : (a,b,c,d:Z)`a >= c`->`b >= d`->`c >= 0`->`d >= 0`->`a*b >= c*d` *) - + (** Lemmas ending by Zlt *) Zorder.Zmult_gt_0_compat (* :(a,b:Z)`a > 0`->`b > 0`->`a*b > 0` *) Zlt_lt_succ (* :(n,m:Z)`n < m`->`n < (Zs m)` *) - + (** Lemmas ending by Zle *) Zorder.Zmult_le_0_compat (* :(x,y:Z)`0 <= x`->`0 <= y`->`0 <= x*y` *) Zorder.Zmult_le_compat_r (* :(a,b,c:Z)`a <= b`->`0 <= c`->`a*c <= b*c` *) @@ -98,9 +98,9 @@ Hint Resolve Zplus_le_0_compat (* :(x,y:Z)`0 <= x`->`0 <= y`->`0 <= x+y` *) Zle_le_succ (* :(x,y:Z)`x <= y`->`x <= (Zs y)` *) Zplus_le_compat (* :(n,m,p,q:Z)`n <= m`->`p <= q`->`n+p <= m+q` *) - + : zarith. - + (**********************************************************************) (** * Reversible lemmas relating operators *) (** Probably to be declared as hints but need to define precedences *) @@ -108,7 +108,7 @@ Hint Resolve (** ** Conversion between comparisons/predicates and arithmetic operators *) (** Lemmas ending by eq *) -(** +(** << Zegal_left: (x,y:Z)`x = y`->`x+(-y) = 0` Zabs_eq: (x:Z)`0 <= x`->`|x| = x` @@ -118,7 +118,7 @@ Zodd_div2: (x:Z)`x >= 0`->(Zodd x)->`x = 2*(Zdiv2 x)+1` *) (** Lemmas ending by Zgt *) -(** +(** << Zgt_left_rev: (x,y:Z)`x+(-y) > 0`->`x > y` Zgt_left_gt: (x,y:Z)`x > y`->`x+(-y) > 0` @@ -126,7 +126,7 @@ Zgt_left_gt: (x,y:Z)`x > y`->`x+(-y) > 0` *) (** Lemmas ending by Zlt *) -(** +(** << Zlt_left_rev: (x,y:Z)`0 < y+(-x)`->`x < y` Zlt_left_lt: (x,y:Z)`x < y`->`0 < y+(-x)` @@ -135,7 +135,7 @@ Zlt_O_minus_lt: (n,m:Z)`0 < n-m`->`m < n` *) (** Lemmas ending by Zle *) -(** +(** << Zle_left: (x,y:Z)`x <= y`->`0 <= y+(-x)` Zle_left_rev: (x,y:Z)`0 <= y+(-x)`->`x <= y` @@ -148,35 +148,35 @@ Zgt_left: (x,y:Z)`x > y`->`0 <= x+(-1)+(-y)` (** ** Conversion between nat comparisons and Z comparisons *) (** Lemmas ending by eq *) -(** +(** << inj_eq: (x,y:nat)x=y->`(inject_nat x) = (inject_nat y)` >> *) (** Lemmas ending by Zge *) -(** +(** << inj_ge: (x,y:nat)(ge x y)->`(inject_nat x) >= (inject_nat y)` >> *) (** Lemmas ending by Zgt *) -(** +(** << inj_gt: (x,y:nat)(gt x y)->`(inject_nat x) > (inject_nat y)` >> *) (** Lemmas ending by Zlt *) -(** +(** << inj_lt: (x,y:nat)(lt x y)->`(inject_nat x) < (inject_nat y)` >> *) (** Lemmas ending by Zle *) -(** +(** << inj_le: (x,y:nat)(le x y)->`(inject_nat x) <= (inject_nat y)` >> @@ -185,7 +185,7 @@ inj_le: (x,y:nat)(le x y)->`(inject_nat x) <= (inject_nat y)` (** ** Conversion between comparisons *) (** Lemmas ending by Zge *) -(** +(** << not_Zlt: (x,y:Z)~`x < y`->`x >= y` Zle_ge: (m,n:Z)`m <= n`->`n >= m` @@ -193,7 +193,7 @@ Zle_ge: (m,n:Z)`m <= n`->`n >= m` *) (** Lemmas ending by Zgt *) -(** +(** << Zle_gt_S: (n,p:Z)`n <= p`->`(Zs p) > n` not_Zle: (x,y:Z)~`x <= y`->`x > y` @@ -203,7 +203,7 @@ Zle_S_gt: (n,m:Z)`(Zs n) <= m`->`m > n` *) (** Lemmas ending by Zlt *) -(** +(** << not_Zge: (x,y:Z)~`x >= y`->`x < y` Zgt_lt: (m,n:Z)`m > n`->`n < m` @@ -212,7 +212,7 @@ Zle_lt_n_Sm: (n,m:Z)`n <= m`->`n < (Zs m)` *) (** Lemmas ending by Zle *) -(** +(** << Zlt_ZERO_pred_le_ZERO: (x:Z)`0 < x`->`0 <= (Zpred x)` not_Zgt: (x,y:Z)~`x > y`->`x <= y` @@ -230,7 +230,7 @@ Zle_refl: (n,m:Z)`n = m`->`n <= m` (** useful with clear precedences *) (** Lemmas ending by Zlt *) -(** +(** << Zlt_le_reg :(a,b,c,d:Z)`a < b`->`c <= d`->`a+c < b+d` Zle_lt_reg : (a,b,c,d:Z)`a <= b`->`c < d`->`a+c < b+d` @@ -240,21 +240,21 @@ Zle_lt_reg : (a,b,c,d:Z)`a <= b`->`c < d`->`a+c < b+d` (** ** What is decreasing here ? *) (** Lemmas ending by eq *) -(** +(** << Zplus_minus: (n,m,p:Z)`n = m+p`->`p = n-m` >> *) (** Lemmas ending by Zgt *) -(** +(** << Zgt_pred: (n,p:Z)`p > (Zs n)`->`(Zpred p) > n` >> *) (** Lemmas ending by Zlt *) -(** +(** << Zlt_pred: (n,p:Z)`(Zs n) < p`->`n < (Zpred p)` >> @@ -266,8 +266,8 @@ Zlt_pred: (n,p:Z)`(Zs n) < p`->`n < (Zpred p)` (** ** Bottom-up simplification: should be used *) (** Lemmas ending by eq *) -(** -<< +(** +<< Zeq_add_S: (n,m:Z)`(Zs n) = (Zs m)`->`n = m` Zsimpl_plus_l: (n,m,p:Z)`n+m = n+p`->`m = p` Zplus_unit_left: (n,m:Z)`n+0 = m`->`n = m` @@ -276,21 +276,21 @@ Zplus_unit_right: (n,m:Z)`n = m+0`->`n = m` *) (** Lemmas ending by Zgt *) -(** -<< +(** +<< Zsimpl_gt_plus_l: (n,m,p:Z)`p+n > p+m`->`n > m` Zsimpl_gt_plus_r: (n,m,p:Z)`n+p > m+p`->`n > m` -Zgt_S_n: (n,p:Z)`(Zs p) > (Zs n)`->`p > n` ->> +Zgt_S_n: (n,p:Z)`(Zs p) > (Zs n)`->`p > n` +>> *) (** Lemmas ending by Zlt *) -(** -<< +(** +<< Zsimpl_lt_plus_l: (n,m,p:Z)`p+n < p+m`->`n < m` Zsimpl_lt_plus_r: (n,m,p:Z)`n+p < m+p`->`n < m` -Zlt_S_n: (n,m:Z)`(Zs n) < (Zs m)`->`n < m` ->> +Zlt_S_n: (n,m:Z)`(Zs n) < (Zs m)`->`n < m` +>> *) (** Lemmas ending by Zle *) @@ -301,7 +301,7 @@ Zle_S_n: (n,m:Z)`(Zs m) <= (Zs n)`->`m <= n` >> *) (** ** Bottom-up irreversible (syntactic) simplification *) (** Lemmas ending by Zle *) -(** +(** << Zle_trans_S: (n,m:Z)`(Zs n) <= m`->`n <= m` >> @@ -310,78 +310,78 @@ Zle_trans_S: (n,m:Z)`(Zs n) <= m`->`n <= m` (** ** Other unclearly simplifying lemmas *) (** Lemmas ending by Zeq *) -(** -<< -Zmult_eq: (x,y:Z)`x <> 0`->`y*x = 0`->`y = 0` ->> +(** +<< +Zmult_eq: (x,y:Z)`x <> 0`->`y*x = 0`->`y = 0` +>> *) (* Lemmas ending by Zgt *) -(** -<< +(** +<< Zmult_gt: (x,y:Z)`x > 0`->`x*y > 0`->`y > 0` >> *) (* Lemmas ending by Zlt *) -(** -<< +(** +<< pZmult_lt: (x,y:Z)`x > 0`->`0 < y*x`->`0 < y` ->> +>> *) (* Lemmas ending by Zle *) -(** -<< +(** +<< Zmult_le: (x,y:Z)`x > 0`->`0 <= y*x`->`0 <= y` OMEGA1: (x,y:Z)`x = y`->`0 <= x`->`0 <= y` ->> +>> *) (**********************************************************************) (** * Irreversible lemmas with meta-variables *) -(** To be used by EAuto *) +(** To be used by EAuto *) (* Hints Immediate *) (** Lemmas ending by eq *) -(** -<< +(** +<< Zle_antisym: (n,m:Z)`n <= m`->`m <= n`->`n = m` >> *) (** Lemmas ending by Zge *) -(** -<< +(** +<< Zge_trans: (n,m,p:Z)`n >= m`->`m >= p`->`n >= p` ->> +>> *) (** Lemmas ending by Zgt *) -(** -<< +(** +<< Zgt_trans: (n,m,p:Z)`n > m`->`m > p`->`n > p` Zgt_trans_S: (n,m,p:Z)`(Zs n) > m`->`m > p`->`n > p` Zle_gt_trans: (n,m,p:Z)`m <= n`->`m > p`->`n > p` Zgt_le_trans: (n,m,p:Z)`n > m`->`p <= m`->`n > p` ->> +>> *) (** Lemmas ending by Zlt *) -(** -<< +(** +<< Zlt_trans: (n,m,p:Z)`n < m`->`m < p`->`n < p` Zlt_le_trans: (n,m,p:Z)`n < m`->`m <= p`->`n < p` Zle_lt_trans: (n,m,p:Z)`n <= m`->`m < p`->`n < p` ->> +>> *) (** Lemmas ending by Zle *) -(** -<< +(** +<< Zle_trans: (n,m,p:Z)`n <= m`->`m <= p`->`n <= p` ->> +>> *) diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v index d8f4f236..70a959c2 100644 --- a/theories/ZArith/Zlogarithm.v +++ b/theories/ZArith/Zlogarithm.v @@ -6,10 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zlogarithm.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id$ i*) (**********************************************************************) -(** The integer logarithms with base 2. +(** The integer logarithms with base 2. There are three logarithms, depending on the rounding of the real 2-based logarithm: @@ -27,7 +27,7 @@ Require Import Zpower. Open Local Scope Z_scope. Section Log_pos. (* Log of positive integers *) - + (** First we build [log_inf] and [log_sup] *) Fixpoint log_inf (p:positive) : Z := @@ -43,31 +43,30 @@ Section Log_pos. (* Log of positive integers *) | xO n => Zsucc (log_sup n) (* 2n *) | xI n => Zsucc (Zsucc (log_inf n)) (* 2n+1 *) end. - + Hint Unfold log_inf log_sup. - - (** Then we give the specifications of [log_inf] and [log_sup] + + (** Then we give the specifications of [log_inf] and [log_sup] and prove their validity *) - + Hint Resolve Zle_trans: zarith. Theorem log_inf_correct : forall x:positive, 0 <= log_inf x /\ two_p (log_inf x) <= Zpos x < two_p (Zsucc (log_inf x)). + Proof. simple induction x; intros; simpl in |- *; [ elim H; intros Hp HR; clear H; split; [ auto with zarith - | conditional apply Zle_le_succ; trivial rewrite - two_p_S with (x := Zsucc (log_inf p)); - conditional trivial rewrite two_p_S; - conditional trivial rewrite two_p_S in HR; rewrite (BinInt.Zpos_xI p); + | rewrite two_p_S with (x := Zsucc (log_inf p)) by (apply Zle_le_succ; trivial); + rewrite two_p_S by trivial; + rewrite two_p_S in HR by trivial; rewrite (BinInt.Zpos_xI p); omega ] | elim H; intros Hp HR; clear H; split; [ auto with zarith - | conditional apply Zle_le_succ; trivial rewrite - two_p_S with (x := Zsucc (log_inf p)); - conditional trivial rewrite two_p_S; - conditional trivial rewrite two_p_S in HR; rewrite (BinInt.Zpos_xO p); + | rewrite two_p_S with (x := Zsucc (log_inf p)) by (apply Zle_le_succ; trivial); + rewrite two_p_S by trivial; + rewrite two_p_S in HR by trivial; rewrite (BinInt.Zpos_xO p); omega ] | unfold two_power_pos in |- *; unfold shift_pos in |- *; simpl in |- *; omega ]. @@ -101,11 +100,11 @@ Section Log_pos. (* Log of positive integers *) [ left; simpl in |- *; rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0)); rewrite (two_p_S (log_sup p0) (log_sup_correct1 p0)); - rewrite <- (proj1 Hif); rewrite <- (proj2 Hif); + rewrite <- (proj1 Hif); rewrite <- (proj2 Hif); auto | right; simpl in |- *; rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0)); - rewrite BinInt.Zpos_xO; unfold Zsucc in |- *; + rewrite BinInt.Zpos_xO; unfold Zsucc in |- *; omega ] | left; auto ]. Qed. @@ -142,7 +141,7 @@ Section Log_pos. (* Log of positive integers *) | xI xH => 2 | xO y => Zsucc (log_near y) | xI y => Zsucc (log_near y) - end. + end. Theorem log_near_correct1 : forall p:positive, 0 <= log_near p. Proof. @@ -187,7 +186,7 @@ End Log_pos. Section divers. (** Number of significative digits. *) - + Definition N_digits (x:Z) := match x with | Zpos p => log_inf p diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v index 0d6fc94a..53c40ae7 100644 --- a/theories/ZArith/Zmax.v +++ b/theories/ZArith/Zmax.v @@ -5,162 +5,102 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zmax.v 10291 2007-11-06 02:18:53Z letouzey $ i*) +(*i $Id$ i*) -Require Import Arith_base. -Require Import BinInt. -Require Import Zcompare. -Require Import Zorder. +(** THIS FILE IS DEPRECATED. Use [Zminmax] instead. *) + +Require Export BinInt Zorder Zminmax. Open Local Scope Z_scope. -(******************************************) -(** Maximum of two binary integer numbers *) +(** [Zmax] is now [Zminmax.Zmax]. Code that do things like + [unfold Zmin.Zmin] will have to be adapted, and neither + a [Definition] or a [Notation] here can help much. *) -Definition Zmax m n := - match m ?= n with - | Eq | Gt => m - | Lt => n - end. (** * Characterization of maximum on binary integer numbers *) -Lemma Zmax_case : forall (n m:Z) (P:Z -> Type), P n -> P m -> P (Zmax n m). -Proof. - intros n m P H1 H2; unfold Zmax in |- *; case (n ?= m); auto with arith. -Qed. - -Lemma Zmax_case_strong : forall (n m:Z) (P:Z -> Type), - (m<=n -> P n) -> (n<=m -> P m) -> P (Zmax n m). -Proof. - intros n m P H1 H2; unfold Zmax, Zle, Zge in *. - rewrite <- (Zcompare_antisym n m) in H1. - destruct (n ?= m); (apply H1|| apply H2); discriminate. -Qed. +Definition Zmax_case := Z.max_case. +Definition Zmax_case_strong := Z.max_case_strong. -Lemma Zmax_spec : forall x y:Z, - x >= y /\ Zmax x y = x \/ - x < y /\ Zmax x y = y. +Lemma Zmax_spec : forall x y, + 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. + intros x y. rewrite Zge_iff_le. destruct (Z.max_spec x y); auto. Qed. -Lemma Zmax_left : forall n m:Z, n>=m -> Zmax n m = n. -Proof. - intros n m; unfold Zmax, Zge; destruct (n ?= m); auto. - intro H; elim H; auto. -Qed. +Lemma Zmax_left : forall n m, n>=m -> Zmax n m = n. +Proof. intros x y. rewrite Zge_iff_le. apply Zmax_l. Qed. -Lemma Zmax_right : forall n m:Z, n<=m -> Zmax n m = m. -Proof. - intros n m; unfold Zmax, Zle. - generalize (Zcompare_Eq_eq n m). - destruct (n ?= m); auto. - intros _ H; elim H; auto. -Qed. +Definition Zmax_right : forall n m, n<=m -> Zmax n m = m := Zmax_r. (** * Least upper bound properties of max *) -Lemma Zle_max_l : forall n m:Z, n <= Zmax n m. -Proof. - intros; apply Zmax_case_strong; auto with zarith. -Qed. +Definition Zle_max_l : forall n m, n <= Zmax n m := Z.le_max_l. +Definition Zle_max_r : forall n m, m <= Zmax n m := Z.le_max_r. -Notation Zmax1 := Zle_max_l (only parsing). +Definition Zmax_lub : forall n m p, n <= p -> m <= p -> Zmax n m <= p + := Z.max_lub. -Lemma Zle_max_r : forall n m:Z, m <= Zmax n m. -Proof. - intros; apply Zmax_case_strong; auto with zarith. -Qed. +Definition Zmax_lub_lt : forall n m p:Z, n < p -> m < p -> Zmax n m < p + := Z.max_lub_lt. -Notation Zmax2 := Zle_max_r (only parsing). -Lemma Zmax_lub : forall n m p:Z, n <= p -> m <= p -> Zmax n m <= p. -Proof. - intros; apply Zmax_case; assumption. -Qed. +(** * Compatibility with order *) -(** * Semi-lattice properties of max *) +Definition Zle_max_compat_r : forall n m p, n <= m -> Zmax n p <= Zmax m p + := Z.max_le_compat_r. -Lemma Zmax_idempotent : forall n:Z, Zmax n n = n. -Proof. - intros; apply Zmax_case; auto. -Qed. +Definition Zle_max_compat_l : forall n m p, n <= m -> Zmax p n <= Zmax p m + := Z.max_le_compat_l. -Lemma Zmax_comm : forall n m:Z, Zmax n m = Zmax m n. -Proof. - intros; do 2 apply Zmax_case_strong; intros; - apply Zle_antisym; auto with zarith. -Qed. -Lemma Zmax_assoc : forall n m p:Z, Zmax n (Zmax m p) = Zmax (Zmax n m) p. -Proof. - intros n m p; repeat apply Zmax_case_strong; intros; - reflexivity || (try apply Zle_antisym); eauto with zarith. -Qed. +(** * Semi-lattice properties of max *) + +Definition Zmax_idempotent : forall n, Zmax n n = n := Z.max_id. +Definition Zmax_comm : forall n m, Zmax n m = Zmax m n := Z.max_comm. +Definition Zmax_assoc : forall n m p, Zmax n (Zmax m p) = Zmax (Zmax n m) p + := Z.max_assoc. (** * Additional properties of max *) -Lemma Zmax_irreducible_inf : forall n m:Z, Zmax n m = n \/ Zmax n m = m. -Proof. - intros; apply Zmax_case; auto. -Qed. +Lemma Zmax_irreducible_dec : forall n m, {Zmax n m = n} + {Zmax n m = m}. +Proof. exact Z.max_dec. Qed. + +Definition Zmax_le_prime : forall n m p, p <= Zmax n m -> p <= n \/ p <= m + := Z.max_le. -Lemma Zmax_le_prime_inf : forall n m p:Z, p <= Zmax n m -> p <= n \/ p <= m. -Proof. - intros n m p; apply Zmax_case; auto. -Qed. (** * Operations preserving max *) -Lemma Zsucc_max_distr : - forall n m:Z, Zsucc (Zmax n m) = Zmax (Zsucc n) (Zsucc m). -Proof. - intros n m; unfold Zmax in |- *; rewrite (Zcompare_succ_compat n m); - elim_compare n m; intros E; rewrite E; auto with arith. -Qed. +Definition Zsucc_max_distr : + forall n m:Z, Zsucc (Zmax n m) = Zmax (Zsucc n) (Zsucc m) + := Z.succ_max_distr. -Lemma Zplus_max_distr_r : forall n m p:Z, Zmax (n + p) (m + p) = Zmax n m + p. -Proof. - intros x y n; unfold Zmax in |- *. - rewrite (Zplus_comm x n); rewrite (Zplus_comm y n); - rewrite (Zcompare_plus_compat x y n). - case (x ?= y); apply Zplus_comm. -Qed. +Definition Zplus_max_distr_l : forall n m p:Z, Zmax (p + n) (p + m) = p + Zmax n m + := Z.plus_max_distr_l. + +Definition Zplus_max_distr_r : forall n m p:Z, Zmax (n + p) (m + p) = Zmax n m + p + := Z.plus_max_distr_r. (** * Maximum and Zpos *) -Lemma Zpos_max : forall p q, Zpos (Pmax p q) = Zmax (Zpos p) (Zpos q). -Proof. - intros; unfold Zmax, Pmax; simpl; generalize (Pcompare_Eq_eq p q). - destruct Pcompare; auto. - intro H; rewrite H; auto. -Qed. +Definition Zpos_max : forall p q, Zpos (Pmax p q) = Zmax (Zpos p) (Zpos q) + := Z.pos_max. -Lemma Zpos_max_1 : forall p, Zmax 1 (Zpos p) = Zpos p. -Proof. - intros; unfold Zmax; simpl; destruct p; simpl; auto. -Qed. +Definition Zpos_max_1 : forall p, Zmax 1 (Zpos p) = Zpos p + := Z.pos_max_1. (** * Characterization of Pminus in term of Zminus and Zmax *) -Lemma Zpos_minus : forall p q, Zpos (Pminus p q) = Zmax 1 (Zpos p - Zpos q). -Proof. - intros. - case_eq (Pcompare p q Eq). - intros H; rewrite (Pcompare_Eq_eq _ _ H). - rewrite Zminus_diag. - unfold Zmax; simpl. - unfold Pminus; rewrite Pminus_mask_diag; auto. - intros; rewrite Pminus_Lt; auto. - destruct (Zmax_spec 1 (Zpos p - Zpos q)) as [(H1,H2)|(H1,H2)]; auto. - elimtype False; clear H2. - assert (H1':=Zlt_trans 0 1 _ Zlt_0_1 H1). - generalize (Zlt_0_minus_lt _ _ H1'). - unfold Zlt; simpl. - rewrite (ZC2 _ _ H); intro; discriminate. - intros; simpl; rewrite H. - symmetry; apply Zpos_max_1. -Qed. +Definition Zpos_minus : + forall p q, Zpos (Pminus p q) = Zmax 1 (Zpos p - Zpos q) + := Zpos_minus. +(* begin hide *) +(* Compatibility *) +Notation Zmax1 := Zle_max_l (only parsing). +Notation Zmax2 := Zle_max_r (only parsing). +Notation Zmax_irreducible_inf := Zmax_irreducible_dec (only parsing). +Notation Zmax_le_prime_inf := Zmax_le_prime (only parsing). +(* end hide *) diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v index bad40a32..5dd26fa3 100644 --- a/theories/ZArith/Zmin.v +++ b/theories/ZArith/Zmin.v @@ -5,142 +5,86 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zmin.v 10028 2007-07-18 22:38:06Z letouzey $ i*) +(*i $Id$ i*) -(** Initial version from Pierre Crégut (CNET, Lannion, France), 1996. - Further extensions by the Coq development team, with suggestions - from Russell O'Connor (Radbout U., Nijmegen, The Netherlands). - *) +(** THIS FILE IS DEPRECATED. Use [Zminmax] instead. *) -Require Import Arith_base. -Require Import BinInt. -Require Import Zcompare. -Require Import Zorder. +Require Import BinInt Zorder Zminmax. Open Local Scope Z_scope. -(**************************************) -(** Minimum on binary integer numbers *) +(** [Zmin] is now [Zminmax.Zmin]. Code that do things like + [unfold Zmin.Zmin] will have to be adapted, and neither + a [Definition] or a [Notation] here can help much. *) -Unboxed Definition Zmin (n m:Z) := - match n ?= m with - | Eq | Lt => n - | Gt => m - end. (** * Characterization of the minimum on binary integer numbers *) -Lemma Zmin_case_strong : forall (n m:Z) (P:Z -> Type), - (n<=m -> P n) -> (m<=n -> P m) -> P (Zmin n m). -Proof. - intros n m P H1 H2; unfold Zmin, Zle, Zge in *. - rewrite <- (Zcompare_antisym n m) in H2. - destruct (n ?= m); (apply H1|| apply H2); discriminate. -Qed. - -Lemma Zmin_case : forall (n m:Z) (P:Z -> Type), P n -> P m -> P (Zmin n m). -Proof. - intros n m P H1 H2; unfold Zmin in |- *; case (n ?= m); auto with arith. -Qed. +Definition Zmin_case := Z.min_case. +Definition Zmin_case_strong := Z.min_case_strong. -Lemma Zmin_spec : forall x y:Z, - x <= y /\ Zmin x y = x \/ - x > y /\ Zmin x y = y. +Lemma Zmin_spec : forall x y, + x <= y /\ Zmin x y = x \/ x > y /\ Zmin x y = y. Proof. - intros; unfold Zmin, Zle, Zgt. - destruct (Zcompare x y); [ left | left | right ]; split; auto; discriminate. + intros x y. rewrite Zgt_iff_lt, Z.min_comm. destruct (Z.min_spec y x); auto. Qed. (** * Greatest lower bound properties of min *) -Lemma Zle_min_l : forall n m:Z, Zmin n m <= n. -Proof. - intros n m; unfold Zmin in |- *; elim_compare n m; intros E; rewrite E; - [ apply Zle_refl - | apply Zle_refl - | apply Zlt_le_weak; apply Zgt_lt; exact E ]. -Qed. +Definition Zle_min_l : forall n m, Zmin n m <= n := Z.le_min_l. +Definition Zle_min_r : forall n m, Zmin n m <= m := Z.le_min_r. -Lemma Zle_min_r : forall n m:Z, Zmin n m <= m. -Proof. - intros n m; unfold Zmin in |- *; elim_compare n m; intros E; rewrite E; - [ unfold Zle in |- *; rewrite E; discriminate - | unfold Zle in |- *; rewrite E; discriminate - | apply Zle_refl ]. -Qed. +Definition Zmin_glb : forall n m p, p <= n -> p <= m -> p <= Zmin n m + := Z.min_glb. +Definition Zmin_glb_lt : forall n m p, p < n -> p < m -> p < Zmin n m + := Z.min_glb_lt. -Lemma Zmin_glb : forall n m p:Z, p <= n -> p <= m -> p <= Zmin n m. -Proof. - intros; apply Zmin_case; assumption. -Qed. +(** * Compatibility with order *) -(** * Semi-lattice properties of min *) +Definition Zle_min_compat_r : forall n m p, n <= m -> Zmin n p <= Zmin m p + := Z.min_le_compat_r. +Definition Zle_min_compat_l : forall n m p, n <= m -> Zmin p n <= Zmin p m + := Z.min_le_compat_l. -Lemma Zmin_idempotent : forall n:Z, Zmin n n = n. -Proof. - unfold Zmin in |- *; intros; elim (n ?= n); auto. -Qed. +(** * Semi-lattice properties of min *) +Definition Zmin_idempotent : forall n, Zmin n n = n := Z.min_id. Notation Zmin_n_n := Zmin_idempotent (only parsing). - -Lemma Zmin_comm : forall n m:Z, Zmin n m = Zmin m n. -Proof. - intros n m; unfold Zmin. - rewrite <- (Zcompare_antisym n m). - assert (H:=Zcompare_Eq_eq n m). - destruct (n ?= m); simpl; auto. -Qed. - -Lemma Zmin_assoc : forall n m p:Z, Zmin n (Zmin m p) = Zmin (Zmin n m) p. -Proof. - intros n m p; repeat apply Zmin_case_strong; intros; - reflexivity || (try apply Zle_antisym); eauto with zarith. -Qed. +Definition Zmin_comm : forall n m, Zmin n m = Zmin m n := Z.min_comm. +Definition Zmin_assoc : forall n m p, Zmin n (Zmin m p) = Zmin (Zmin n m) p + := Z.min_assoc. (** * Additional properties of min *) -Lemma Zmin_irreducible_inf : forall n m:Z, {Zmin n m = n} + {Zmin n m = m}. -Proof. - unfold Zmin in |- *; intros; elim (n ?= m); auto. -Qed. +Lemma Zmin_irreducible_inf : forall n m, {Zmin n m = n} + {Zmin n m = m}. +Proof. exact Z.min_dec. Qed. -Lemma Zmin_irreducible : forall n m:Z, Zmin n m = n \/ Zmin n m = m. -Proof. - intros n m; destruct (Zmin_irreducible_inf n m); [left|right]; trivial. -Qed. +Lemma Zmin_irreducible : forall n m, Zmin n m = n \/ Zmin n m = m. +Proof. intros; destruct (Z.min_dec n m); auto. Qed. Notation Zmin_or := Zmin_irreducible (only parsing). -Lemma Zmin_le_prime_inf : forall n m p:Z, Zmin n m <= p -> {n <= p} + {m <= p}. -Proof. - intros n m p; apply Zmin_case; auto. -Qed. +Lemma Zmin_le_prime_inf : forall n m p, Zmin n m <= p -> {n <= p} + {m <= p}. +Proof. intros n m p; apply Zmin_case; auto. Qed. (** * Operations preserving min *) -Lemma Zsucc_min_distr : - forall n m:Z, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m). -Proof. - intros n m; unfold Zmin in |- *; rewrite (Zcompare_succ_compat n m); - elim_compare n m; intros E; rewrite E; auto with arith. -Qed. +Definition Zsucc_min_distr : + forall n m, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m) + := Z.succ_min_distr. -Notation Zmin_SS := Zsucc_min_distr (only parsing). +Notation Zmin_SS := Z.succ_min_distr (only parsing). -Lemma Zplus_min_distr_r : forall n m p:Z, Zmin (n + p) (m + p) = Zmin n m + p. -Proof. - intros x y n; unfold Zmin in |- *. - rewrite (Zplus_comm x n); rewrite (Zplus_comm y n); - rewrite (Zcompare_plus_compat x y n). - case (x ?= y); apply Zplus_comm. -Qed. +Definition Zplus_min_distr_r : + forall n m p, Zmin (n + p) (m + p) = Zmin n m + p + := Z.plus_min_distr_r. -Notation Zmin_plus := Zplus_min_distr_r (only parsing). +Notation Zmin_plus := Z.plus_min_distr_r (only parsing). (** * Minimum and Zpos *) -Lemma Zpos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q). -Proof. - intros; unfold Zmin, Pmin; simpl; destruct Pcompare; auto. -Qed. +Definition Zpos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q) + := Z.pos_min. + + diff --git a/theories/ZArith/Zminmax.v b/theories/ZArith/Zminmax.v index 95668cf8..c1657e29 100644 --- a/theories/ZArith/Zminmax.v +++ b/theories/ZArith/Zminmax.v @@ -5,72 +5,198 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zminmax.v 9245 2006-10-17 12:53:34Z notin $ i*) -Require Import Zmin Zmax. -Require Import BinInt Zorder. +Require Import Orders BinInt Zcompare Zorder ZOrderedType + GenericMinMax. -Open Local Scope Z_scope. +(** * Maximum and Minimum of two [Z] numbers *) -(** Lattice properties of min and max on Z *) +Local Open Scope Z_scope. -(** Absorption *) +Unboxed Definition Zmax (n m:Z) := + match n ?= m with + | Eq | Gt => n + | Lt => m + end. -Lemma Zmin_max_absorption_r_r : forall n m, Zmax n (Zmin n m) = n. +Unboxed Definition Zmin (n m:Z) := + match n ?= m with + | Eq | Lt => n + | Gt => m + end. + +(** The functions [Zmax] and [Zmin] implement indeed + a maximum and a minimum *) + +Lemma Zmax_l : forall x y, y<=x -> Zmax x y = x. +Proof. + unfold Zle, Zmax. intros x y. rewrite <- (Zcompare_antisym x y). + destruct (x ?= y); intuition. +Qed. + +Lemma Zmax_r : forall x y, x<=y -> Zmax x y = y. +Proof. + unfold Zle, Zmax. intros x y. generalize (Zcompare_Eq_eq x y). + destruct (x ?= y); intuition. +Qed. + +Lemma Zmin_l : forall x y, x<=y -> Zmin x y = x. +Proof. + unfold Zle, Zmin. intros x y. generalize (Zcompare_Eq_eq x y). + destruct (x ?= y); intuition. +Qed. + +Lemma Zmin_r : forall x y, y<=x -> Zmin x y = y. +Proof. + unfold Zle, Zmin. intros x y. + rewrite <- (Zcompare_antisym x y). generalize (Zcompare_Eq_eq x y). + destruct (x ?= y); intuition. +Qed. + +Module ZHasMinMax <: HasMinMax Z_as_OT. + Definition max := Zmax. + Definition min := Zmin. + Definition max_l := Zmax_l. + Definition max_r := Zmax_r. + Definition min_l := Zmin_l. + Definition min_r := Zmin_r. +End ZHasMinMax. + +Module Z. + +(** We obtain hence all the generic properties of max and min. *) + +Include UsualMinMaxProperties Z_as_OT ZHasMinMax. + +(** * Properties specific to the [Z] domain *) + +(** Compatibilities (consequences of monotonicity) *) + +Lemma plus_max_distr_l : forall n m p, Zmax (p + n) (p + m) = p + Zmax n m. Proof. - intros; apply Zmin_case_strong; intro; apply Zmax_case_strong; intro; - reflexivity || apply Zle_antisym; trivial. + intros. apply max_monotone. + intros x y. apply Zplus_le_compat_l. Qed. -Lemma Zmax_min_absorption_r_r : forall n m, Zmin n (Zmax n m) = n. +Lemma plus_max_distr_r : forall n m p, Zmax (n + p) (m + p) = Zmax n m + p. Proof. - intros; apply Zmax_case_strong; intro; apply Zmin_case_strong; intro; - reflexivity || apply Zle_antisym; trivial. + intros. rewrite (Zplus_comm n p), (Zplus_comm m p), (Zplus_comm _ p). + apply plus_max_distr_l. Qed. -(** Distributivity *) +Lemma plus_min_distr_l : forall n m p, Zmin (p + n) (p + m) = p + Zmin n m. +Proof. + intros. apply Z.min_monotone. + intros x y. apply Zplus_le_compat_l. +Qed. -Lemma Zmax_min_distr_r : - forall n m p, Zmax n (Zmin m p) = Zmin (Zmax n m) (Zmax n p). +Lemma plus_min_distr_r : forall n m p, Zmin (n + p) (m + p) = Zmin n m + p. Proof. - intros. - repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros; - reflexivity || - apply Zle_antisym; (assumption || eapply Zle_trans; eassumption). + intros. rewrite (Zplus_comm n p), (Zplus_comm m p), (Zplus_comm _ p). + apply plus_min_distr_l. Qed. -Lemma Zmin_max_distr_r : - forall n m p, Zmin n (Zmax m p) = Zmax (Zmin n m) (Zmin n p). +Lemma succ_max_distr : forall n m, Zsucc (Zmax n m) = Zmax (Zsucc n) (Zsucc m). Proof. - intros. - repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros; - reflexivity || - apply Zle_antisym; (assumption || eapply Zle_trans; eassumption). + unfold Zsucc. intros. symmetry. apply plus_max_distr_r. Qed. -(** Modularity *) +Lemma succ_min_distr : forall n m, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m). +Proof. + unfold Zsucc. intros. symmetry. apply plus_min_distr_r. +Qed. -Lemma Zmax_min_modular_r : - forall n m p, Zmax n (Zmin m (Zmax n p)) = Zmin (Zmax n m) (Zmax n p). +Lemma pred_max_distr : forall n m, Zpred (Zmax n m) = Zmax (Zpred n) (Zpred m). Proof. - intros; repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros; - reflexivity || - apply Zle_antisym; (assumption || eapply Zle_trans; eassumption). + unfold Zpred. intros. symmetry. apply plus_max_distr_r. Qed. -Lemma Zmin_max_modular_r : - forall n m p, Zmin n (Zmax m (Zmin n p)) = Zmax (Zmin n m) (Zmin n p). +Lemma pred_min_distr : forall n m, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m). Proof. - intros; repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros; - reflexivity || - apply Zle_antisym; (assumption || eapply Zle_trans; eassumption). + unfold Zpred. intros. symmetry. apply plus_min_distr_r. Qed. -(** Disassociativity *) +(** Anti-monotonicity swaps the role of [min] and [max] *) + +Lemma opp_max_distr : forall n m : Z, -(Zmax n m) = Zmin (- n) (- m). +Proof. + intros. symmetry. apply min_max_antimonotone. + intros x x'. red. red. rewrite <- Zcompare_opp; auto. +Qed. + +Lemma opp_min_distr : forall n m : Z, - (Zmin n m) = Zmax (- n) (- m). +Proof. + intros. symmetry. apply max_min_antimonotone. + intros x x'. red. red. rewrite <- Zcompare_opp; auto. +Qed. -Lemma max_min_disassoc : forall n m p, Zmin n (Zmax m p) <= Zmax (Zmin n m) p. +Lemma minus_max_distr_l : forall n m p, Zmax (p - n) (p - m) = p - Zmin n m. Proof. - intros; repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros; - apply Zle_refl || (assumption || eapply Zle_trans; eassumption). + unfold Zminus. intros. rewrite opp_min_distr. apply plus_max_distr_l. Qed. +Lemma minus_max_distr_r : forall n m p, Zmax (n - p) (m - p) = Zmax n m - p. +Proof. + unfold Zminus. intros. apply plus_max_distr_r. +Qed. + +Lemma minus_min_distr_l : forall n m p, Zmin (p - n) (p - m) = p - Zmax n m. +Proof. + unfold Zminus. intros. rewrite opp_max_distr. apply plus_min_distr_l. +Qed. + +Lemma minus_min_distr_r : forall n m p, Zmin (n - p) (m - p) = Zmin n m - p. +Proof. + unfold Zminus. intros. apply plus_min_distr_r. +Qed. + +(** Compatibility with [Zpos] *) + +Lemma pos_max : forall p q, Zpos (Pmax p q) = Zmax (Zpos p) (Zpos q). +Proof. + intros; unfold Zmax, Pmax; simpl; generalize (Pcompare_Eq_eq p q). + destruct Pcompare; auto. + intro H; rewrite H; auto. +Qed. + +Lemma pos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q). +Proof. + intros; unfold Zmin, Pmin; simpl; generalize (Pcompare_Eq_eq p q). + destruct Pcompare; auto. +Qed. + +Lemma pos_max_1 : forall p, Zmax 1 (Zpos p) = Zpos p. +Proof. + intros; unfold Zmax; simpl; destruct p; simpl; auto. +Qed. + +Lemma pos_min_1 : forall p, Zmin 1 (Zpos p) = 1. +Proof. + intros; unfold Zmax; simpl; destruct p; simpl; auto. +Qed. + +End Z. + + +(** * Characterization of Pminus in term of Zminus and Zmax *) + +Lemma Zpos_minus : forall p q, Zpos (Pminus p q) = Zmax 1 (Zpos p - Zpos q). +Proof. + intros; simpl. destruct (Pcompare p q Eq) as [ ]_eqn:H. + rewrite (Pcompare_Eq_eq _ _ H). + unfold Pminus; rewrite Pminus_mask_diag; reflexivity. + rewrite Pminus_Lt; auto. + symmetry. apply Z.pos_max_1. +Qed. + + +(*begin hide*) +(* Compatibility with names of the old Zminmax file *) +Notation Zmin_max_absorption_r_r := Z.min_max_absorption (only parsing). +Notation Zmax_min_absorption_r_r := Z.max_min_absorption (only parsing). +Notation Zmax_min_distr_r := Z.max_min_distr (only parsing). +Notation Zmin_max_distr_r := Z.min_max_distr (only parsing). +Notation Zmax_min_modular_r := Z.max_min_modular (only parsing). +Notation Zmin_max_modular_r := Z.min_max_modular (only parsing). +Notation max_min_disassoc := Z.max_min_disassoc (only parsing). +(*end hide*)
\ No newline at end of file diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v index 0634096e..178ae5f1 100644 --- a/theories/ZArith/Zmisc.v +++ b/theories/ZArith/Zmisc.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zmisc.v 11072 2008-06-08 16:13:37Z herbelin $ i*) +(*i $Id$ i*) Require Import Wf_nat. Require Import BinInt. @@ -20,7 +20,7 @@ Open Local Scope Z_scope. (** [n]th iteration of the function [f] *) -Fixpoint iter_pos (n:positive) (A:Type) (f:A -> A) (x:A) {struct n} : A := +Fixpoint iter_pos (n:positive) (A:Type) (f:A -> A) (x:A) : A := match n with | xH => f x | xO n' => iter_pos n' A f (iter_pos n' A f x) @@ -37,22 +37,29 @@ Definition iter (n:Z) (A:Type) (f:A -> A) (x:A) := Theorem iter_nat_of_P : forall (p:positive) (A:Type) (f:A -> A) (x:A), iter_pos p A f x = iter_nat (nat_of_P p) A f x. -Proof. +Proof. intro n; induction n as [p H| p H| ]; [ intros; simpl in |- *; rewrite (H A f x); - rewrite (H A f (iter_nat (nat_of_P p) A f x)); + rewrite (H A f (iter_nat (nat_of_P p) A f x)); rewrite (ZL6 p); symmetry in |- *; apply f_equal with (f := f); apply iter_nat_plus | intros; unfold nat_of_P in |- *; simpl in |- *; rewrite (H A f x); - rewrite (H A f (iter_nat (nat_of_P p) A f x)); + rewrite (H A f (iter_nat (nat_of_P p) A f x)); rewrite (ZL6 p); symmetry in |- *; apply iter_nat_plus | simpl in |- *; auto with arith ]. Qed. +Lemma iter_nat_of_Z : forall n A f x, 0 <= n -> + iter n A f x = iter_nat (Zabs_nat n) A f x. +intros n A f x; case n; auto. +intros p _; unfold iter, Zabs_nat; apply iter_nat_of_P. +intros p abs; case abs; trivial. +Qed. + Theorem iter_pos_plus : forall (p q:positive) (A:Type) (f:A -> A) (x:A), iter_pos (p + q) A f x = iter_pos p A f (iter_pos q A f x). -Proof. +Proof. intros n m; intros. rewrite (iter_nat_of_P m A f x). rewrite (iter_nat_of_P n A f (iter_nat (nat_of_P m) A f x)). @@ -61,14 +68,14 @@ Proof. apply iter_nat_plus. Qed. -(** Preservation of invariants : if [f : A->A] preserves the invariant [Inv], +(** Preservation of invariants : if [f : A->A] preserves the invariant [Inv], then the iterates of [f] also preserve it. *) Theorem iter_nat_invariant : forall (n:nat) (A:Type) (f:A -> A) (Inv:A -> Prop), (forall x:A, Inv x -> Inv (f x)) -> forall x:A, Inv x -> Inv (iter_nat n A f x). -Proof. +Proof. simple induction n; intros; [ trivial with arith | simpl in |- *; apply H0 with (x := iter_nat n0 A f x); apply H; @@ -79,6 +86,6 @@ Theorem iter_pos_invariant : forall (p:positive) (A:Type) (f:A -> A) (Inv:A -> Prop), (forall x:A, Inv x -> Inv (f x)) -> forall x:A, Inv x -> Inv (iter_pos p A f x). -Proof. +Proof. intros; rewrite iter_nat_of_P; apply iter_nat_invariant; trivial with arith. Qed. diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v index c5b5edc1..dfd9b545 100644 --- a/theories/ZArith/Znat.v +++ b/theories/ZArith/Znat.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -6,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Znat.v 10726 2008-03-28 18:15:23Z notin $ i*) +(*i $Id$ i*) (** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) @@ -57,15 +58,15 @@ Proof. | discriminate H0 | discriminate H0 | simpl in H0; injection H0; - do 2 rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ; + do 2 rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ; intros E; rewrite E; auto with arith ]. -Qed. +Qed. Theorem inj_eq_rev : forall n m:nat, Z_of_nat n = Z_of_nat m -> n = m. Proof. intros x y H. destruct (eq_nat_dec x y) as [H'|H']; auto. - elimtype False. + exfalso. exact (inj_neq _ _ H' H). Qed. @@ -90,7 +91,7 @@ Qed. Theorem inj_lt : forall n m:nat, (n < m)%nat -> Z_of_nat n < Z_of_nat m. Proof. - intros x y H; apply Zgt_lt; apply Zlt_succ_gt; rewrite <- inj_S; apply inj_le; + intros x y H; apply Zgt_lt; apply Zle_succ_gt; rewrite <- inj_S; apply inj_le; exact H. Qed. @@ -110,7 +111,7 @@ Theorem inj_le_rev : forall n m:nat, Z_of_nat n <= Z_of_nat m -> (n <= m)%nat. Proof. intros x y H. destruct (le_lt_dec x y) as [H0|H0]; auto. - elimtype False. + exfalso. assert (H1:=inj_lt _ _ H0). red in H; red in H1. rewrite <- Zcompare_antisym in H; rewrite H1 in H; auto. @@ -120,7 +121,7 @@ Theorem inj_lt_rev : forall n m:nat, Z_of_nat n < Z_of_nat m -> (n < m)%nat. Proof. intros x y H. destruct (le_lt_dec y x) as [H0|H0]; auto. - elimtype False. + exfalso. assert (H1:=inj_le _ _ H0). red in H; red in H1. rewrite <- Zcompare_antisym in H1; rewrite H in H1; auto. @@ -130,7 +131,7 @@ Theorem inj_ge_rev : forall n m:nat, Z_of_nat n >= Z_of_nat m -> (n >= m)%nat. Proof. intros x y H. destruct (le_lt_dec y x) as [H0|H0]; auto. - elimtype False. + exfalso. assert (H1:=inj_gt _ _ H0). red in H; red in H1. rewrite <- Zcompare_antisym in H; rewrite H1 in H; auto. @@ -140,7 +141,7 @@ Theorem inj_gt_rev : forall n m:nat, Z_of_nat n > Z_of_nat m -> (n > m)%nat. Proof. intros x y H. destruct (le_lt_dec x y) as [H0|H0]; auto. - elimtype False. + exfalso. assert (H1:=inj_ge _ _ H0). red in H; red in H1. rewrite <- Zcompare_antisym in H1; rewrite H in H1; auto. @@ -169,7 +170,7 @@ Proof. Qed. (** Injection and usual operations *) - + Theorem inj_plus : forall n m:nat, Z_of_nat (n + m) = Z_of_nat n + Z_of_nat m. Proof. intro x; induction x as [| n H]; intro y; destruct y as [| m]; @@ -186,7 +187,7 @@ Proof. intro x; induction x as [| n H]; [ simpl in |- *; trivial with arith | intro y; rewrite inj_S; rewrite <- Zmult_succ_l_reverse; rewrite <- H; - rewrite <- inj_plus; simpl in |- *; rewrite plus_comm; + rewrite <- inj_plus; simpl in |- *; rewrite plus_comm; trivial with arith ]. Qed. @@ -195,17 +196,17 @@ Theorem inj_minus1 : Proof. intros x y H; apply (Zplus_reg_l (Z_of_nat y)); unfold Zminus in |- *; rewrite Zplus_permute; rewrite Zplus_opp_r; rewrite <- inj_plus; - rewrite <- (le_plus_minus y x H); rewrite Zplus_0_r; + rewrite <- (le_plus_minus y x H); rewrite Zplus_0_r; trivial with arith. Qed. - + Theorem inj_minus2 : forall n m:nat, (m > n)%nat -> Z_of_nat (n - m) = 0. Proof. intros x y H; rewrite not_le_minus_0; [ trivial with arith | apply gt_not_le; assumption ]. Qed. -Theorem inj_minus : forall n m:nat, +Theorem inj_minus : forall n m:nat, Z_of_nat (minus n m) = Zmax 0 (Z_of_nat n - Z_of_nat m). Proof. intros. @@ -225,7 +226,7 @@ Proof. unfold Zminus; rewrite H'; auto. Qed. -Theorem inj_min : forall n m:nat, +Theorem inj_min : forall n m:nat, Z_of_nat (min n m) = Zmin (Z_of_nat n) (Z_of_nat m). Proof. induction n; destruct m; try (compute; auto; fail). @@ -234,7 +235,7 @@ Proof. rewrite <- Zsucc_min_distr; f_equal; auto. Qed. -Theorem inj_max : forall n m:nat, +Theorem inj_max : forall n m:nat, Z_of_nat (max n m) = Zmax (Z_of_nat n) (Z_of_nat m). Proof. induction n; destruct m; try (compute; auto; fail). @@ -269,11 +270,11 @@ Proof. intros x; exists (Z_of_nat x); split; [ trivial with arith | rewrite Zmult_comm; rewrite Zmult_1_l; rewrite Zplus_0_r; - unfold Zle in |- *; elim x; intros; simpl in |- *; + unfold Zle in |- *; elim x; intros; simpl in |- *; discriminate ]. Qed. -Lemma Zpos_P_of_succ_nat : forall n:nat, +Lemma Zpos_P_of_succ_nat : forall n:nat, Zpos (P_of_succ_nat n) = Zsucc (Z_of_nat n). Proof. intros. diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v index 9be372a3..2a2751c9 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 11282 2008-07-28 11:51:53Z msozeau $ i*) +(*i $Id$ i*) Require Import ZArith_base. Require Import ZArithRing. @@ -15,13 +15,13 @@ Require Import Zdiv. Require Import Wf_nat. Open Local Scope Z_scope. -(** This file contains some notions of number theory upon Z numbers: +(** This file contains some notions of number theory upon Z numbers: - a divisibility predicate [Zdivide] - a gcd predicate [gcd] - Euclid algorithm [euclid] - a relatively prime predicate [rel_prime] - a prime predicate [prime] - - an efficient [Zgcd] function + - an efficient [Zgcd] function *) (** * Divisibility *) @@ -171,7 +171,7 @@ Proof. rewrite H1 in H0; left; omega. rewrite H1 in H0; right; omega. Qed. - + Theorem Zdivide_trans: forall a b c, (a | b) -> (b | c) -> (a | c). Proof. intros a b c [d H1] [e H2]; exists (d * e); auto with zarith. @@ -201,19 +201,17 @@ Qed. (** [Zdivide] can be expressed using [Zmod]. *) -Lemma Zmod_divide : forall a b:Z, b > 0 -> a mod b = 0 -> (b | a). +Lemma Zmod_divide : forall a b, b<>0 -> a mod b = 0 -> (b | a). Proof. - intros a b H H0. - apply Zdivide_intro with (a / b). - pattern a at 1 in |- *; rewrite (Z_div_mod_eq a b H). - rewrite H0; ring. + intros a b NZ EQ. + apply Zdivide_intro with (a/b). + rewrite (Z_div_mod_eq_full a b NZ) at 1. + rewrite EQ; ring. Qed. -Lemma Zdivide_mod : forall a b:Z, b > 0 -> (b | a) -> a mod b = 0. +Lemma Zdivide_mod : forall a b, (b | a) -> a mod b = 0. Proof. - intros a b; simple destruct 2; intros; subst. - change (q * b) with (0 + q * b) in |- *. - rewrite Z_mod_plus; auto. + intros a b (c,->); apply Z_mod_mult. Qed. (** [Zdivide] is hence decidable *) @@ -222,7 +220,7 @@ Lemma Zdivide_dec : forall a b:Z, {(a | b)} + {~ (a | b)}. Proof. intros a b; elim (Ztrichotomy_inf a 0). (* a<0 *) - intros H; elim H; intros. + intros H; elim H; intros. case (Z_eq_dec (b mod - a) 0). left; apply Zdivide_opp_l_rev; apply Zmod_divide; auto with zarith. intro H1; right; intro; elim H1; apply Zdivide_mod; auto with zarith. @@ -236,7 +234,7 @@ Proof. intro H1; right; intro; elim H1; apply Zdivide_mod; auto with zarith. Qed. -Theorem Zdivide_Zdiv_eq: forall a b : Z, +Theorem Zdivide_Zdiv_eq: forall a b : Z, 0 < a -> (a | b) -> b = a * (b / a). Proof. intros a b Hb Hc. @@ -244,7 +242,7 @@ Proof. rewrite (Zdivide_mod b a); auto with zarith. Qed. -Theorem Zdivide_Zdiv_eq_2: forall a b c : Z, +Theorem Zdivide_Zdiv_eq_2: forall a b c : Z, 0 < a -> (a | b) -> (c * b)/a = c * (b / a). Proof. intros a b c H1 H2. @@ -252,7 +250,7 @@ Proof. rewrite Hz; rewrite Zmult_assoc. repeat rewrite Z_div_mult; auto with zarith. Qed. - + Theorem Zdivide_Zabs_l: forall a b, (Zabs a | b) -> (a | b). Proof. intros a b [x H]; subst b. @@ -260,7 +258,7 @@ Proof. exists (- x); ring. exists x; ring. Qed. - + Theorem Zdivide_Zabs_inv_l: forall a b, (a | b) -> (Zabs a | b). Proof. intros a b [x H]; subst b. @@ -269,7 +267,7 @@ Proof. exists x; ring. Qed. -Theorem Zdivide_le: forall a b : Z, +Theorem Zdivide_le: forall a b : Z, 0 <= a -> 0 < b -> (a | b) -> a <= b. Proof. intros a b H1 H2 [q H3]; subst b. @@ -280,7 +278,7 @@ Proof. intros H4; subst q; omega. Qed. -Theorem Zdivide_Zdiv_lt_pos: forall a b : Z, +Theorem Zdivide_Zdiv_lt_pos: forall a b : Z, 1 < a -> 0 < b -> (a | b) -> 0 < b / a < b . Proof. intros a b H1 H2 H3; split. @@ -307,7 +305,7 @@ Proof. rewrite Zplus_0_l; rewrite Zmod_mod; auto with zarith. Qed. -Lemma Zmod_divide_minus: forall a b c : Z, 0 < b -> +Lemma Zmod_divide_minus: forall a b c : Z, 0 < b -> a mod b = c -> (b | a - c). Proof. intros a b c H H1; apply Zmod_divide; auto with zarith. @@ -317,7 +315,7 @@ Proof. subst; apply Z_mod_lt; auto with zarith. Qed. -Lemma Zdivide_mod_minus: forall a b c : Z, 0 <= c < b -> +Lemma Zdivide_mod_minus: forall a b c : Z, 0 <= c < b -> (b | a - c) -> a mod b = c. Proof. intros a b c (H1, H2) H3; assert (0 < b); try apply Zle_lt_trans with c; auto. @@ -328,9 +326,9 @@ Proof. Qed. (** * Greatest common divisor (gcd). *) - -(** There is no unicity of the gcd; hence we define the predicate [gcd a b d] - expressing that [d] is a gcd of [a] and [b]. + +(** There is no unicity of the gcd; hence we define the predicate [gcd a b d] + expressing that [d] is a gcd of [a] and [b]. (We show later that the [gcd] is actually unique if we discard its sign.) *) Inductive Zis_gcd (a b d:Z) : Prop := @@ -379,8 +377,8 @@ Proof. Qed. Hint Resolve Zis_gcd_sym Zis_gcd_0 Zis_gcd_minus Zis_gcd_opp: zarith. - -Theorem Zis_gcd_unique: forall a b c d : Z, + +Theorem Zis_gcd_unique: forall a b c d : Z, Zis_gcd a b c -> Zis_gcd a b d -> c = d \/ c = (- d). Proof. intros a b c d H1 H2. @@ -431,7 +429,7 @@ Section extended_euclid_algorithm. (** The recursive part of Euclid's algorithm uses well-founded recursion of non-negative integers. It maintains 6 integers [u1,u2,u3,v1,v2,v3] such that the following invariant holds: - [u1*a+u2*b=u3] and [v1*a+v2*b=v3] and [gcd(u2,v3)=gcd(a,b)]. + [u1*a+u2*b=u3] and [v1*a+v2*b=v3] and [gcd(u2,v3)=gcd(a,b)]. *) Lemma euclid_rec : @@ -455,8 +453,8 @@ Section extended_euclid_algorithm. replace (u3 - q * x) with (u3 mod x). apply Z_mod_lt; omega. assert (xpos : x > 0). omega. - generalize (Z_div_mod_eq u3 x xpos). - unfold q in |- *. + generalize (Z_div_mod_eq u3 x xpos). + unfold q in |- *. intro eq; pattern u3 at 2 in |- *; rewrite eq; ring. apply (H (u3 - q * x) Hq (proj1 Hq) v1 v2 x (u1 - q * v1) (u2 - q * v2)). tauto. @@ -531,7 +529,7 @@ Proof. rewrite H6; rewrite H7; ring. ring. Qed. - + (** * Relative primality *) @@ -612,16 +610,16 @@ Proof. intros a b g; intros. assert (g <> 0). intro. - elim H1; intros. + elim H1; intros. elim H4; intros. rewrite H2 in H6; subst b; omega. unfold rel_prime in |- *. destruct H1. destruct H1 as (a',H1). destruct H3 as (b',H3). - replace (a/g) with a'; + replace (a/g) with a'; [|rewrite H1; rewrite Z_div_mult; auto with zarith]. - replace (b/g) with b'; + replace (b/g) with b'; [|rewrite H3; rewrite Z_div_mult; auto with zarith]. constructor. exists a'; auto with zarith. @@ -643,7 +641,7 @@ Proof. red; apply Zis_gcd_sym; auto with zarith. Qed. -Theorem rel_prime_div: forall p q r, +Theorem rel_prime_div: forall p q r, rel_prime p q -> (r | p) -> rel_prime r q. Proof. intros p q r H (u, H1); subst. @@ -670,7 +668,7 @@ Proof. exists 1; auto with zarith. Qed. -Theorem rel_prime_mod: forall p q, 0 < q -> +Theorem rel_prime_mod: forall p q, 0 < q -> rel_prime p q -> rel_prime (p mod q) q. Proof. intros p q H H0. @@ -683,7 +681,7 @@ Proof. pattern p at 3; rewrite (Z_div_mod_eq p q); try ring; auto with zarith. Qed. -Theorem rel_prime_mod_rev: forall p q, 0 < q -> +Theorem rel_prime_mod_rev: forall p q, 0 < q -> rel_prime (p mod q) q -> rel_prime p q. Proof. intros p q H H0. @@ -715,7 +713,7 @@ Proof. assert (a = - p \/ - p < a < -1 \/ a = -1 \/ a = 0 \/ a = 1 \/ 1 < a < p \/ a = p). assert (Zabs a <= Zabs p). apply Zdivide_bounds; [ assumption | omega ]. - generalize H3. + generalize H3. pattern (Zabs a) in |- *; apply Zabs_ind; pattern (Zabs p) in |- *; apply Zabs_ind; intros; omega. intuition idtac. @@ -785,7 +783,7 @@ Proof. intros H1; absurd (1 < 1); auto with zarith. inversion H1; auto. Qed. - + Lemma prime_2: prime 2. Proof. apply prime_intro; auto with zarith. @@ -795,7 +793,7 @@ Proof. subst n; red; auto with zarith. apply Zis_gcd_intro; auto with zarith. Qed. - + Theorem prime_3: prime 3. Proof. apply prime_intro; auto with zarith. @@ -812,7 +810,7 @@ Proof. subst n; red; auto with zarith. apply Zis_gcd_intro; auto with zarith. Qed. - + Theorem prime_ge_2: forall p, prime p -> 2 <= p. Proof. intros p Hp; inversion Hp; auto with zarith. @@ -820,7 +818,7 @@ Qed. Definition prime' p := 1<p /\ (forall n, 1<n<p -> ~ (n|p)). -Theorem prime_alt: +Theorem prime_alt: forall p, prime' p <-> prime p. Proof. split; destruct 1; intros. @@ -848,7 +846,7 @@ Proof. apply Zis_gcd_intro; auto with zarith. apply H0; auto with zarith. Qed. - + Theorem square_not_prime: forall a, ~ prime (a * a). Proof. intros a Ha. @@ -864,10 +862,10 @@ Proof. exists b; auto. Qed. -Theorem prime_div_prime: forall p q, +Theorem prime_div_prime: forall p q, prime p -> prime q -> (p | q) -> p = q. Proof. - intros p q H H1 H2; + intros p q H H1 H2; assert (Hp: 0 < p); try apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith. assert (Hq: 0 < q); try apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith. case prime_divisors with (2 := H2); auto. @@ -878,10 +876,10 @@ Proof. Qed. -(** We could obtain a [Zgcd] function via Euclid algorithm. But we propose +(** We could obtain a [Zgcd] function via Euclid algorithm. But we propose here a binary version of [Zgcd], faster and executable within Coq. - Algorithm: + Algorithm: gcd 0 b = b gcd a 0 = a @@ -889,23 +887,23 @@ Qed. gcd (2a+1) (2b) = gcd (2a+1) b gcd (2a) (2b+1) = gcd a (2b+1) gcd (2a+1) (2b+1) = gcd (b-a) (2*a+1) - or gcd (a-b) (2*b+1), depending on whether a<b -*) + or gcd (a-b) (2*b+1), depending on whether a<b +*) Open Scope positive_scope. -Fixpoint Pgcdn (n: nat) (a b : positive) { struct n } : positive := - match n with +Fixpoint Pgcdn (n: nat) (a b : positive) : positive := + match n with | O => 1 - | S n => - match a,b with - | xH, _ => 1 + | S n => + match a,b with + | xH, _ => 1 | _, xH => 1 | xO a, xO b => xO (Pgcdn n a b) | a, xO b => Pgcdn n a b | xO a, b => Pgcdn n a b - | xI a', xI b' => - match Pcompare a' b' Eq with + | xI a', xI b' => + match Pcompare a' b' Eq with | Eq => a | Lt => Pgcdn n (b'-a') a | Gt => Pgcdn n (a'-b') b @@ -919,7 +917,7 @@ Close Scope positive_scope. Definition Zgcd (a b : Z) : Z := match a,b with - | Z0, _ => Zabs b + | Z0, _ => Zabs b | _, Z0 => Zabs a | Zpos a, Zpos b => Zpos (Pgcd a b) | Zpos a, Zneg b => Zpos (Pgcd a b) @@ -932,8 +930,8 @@ Proof. unfold Zgcd; destruct a; destruct b; auto with zarith. Qed. -Lemma Zis_gcd_even_odd : forall a b g, Zis_gcd (Zpos a) (Zpos (xI b)) g -> - Zis_gcd (Zpos (xO a)) (Zpos (xI b)) g. +Lemma Zis_gcd_even_odd : forall a b g, Zis_gcd (Zpos a) (Zpos (xI b)) g -> + Zis_gcd (Zpos (xO a)) (Zpos (xI b)) g. Proof. intros. destruct H. @@ -951,7 +949,7 @@ Proof. omega. Qed. -Lemma Pgcdn_correct : forall n a b, (Psize a + Psize b<=n)%nat -> +Lemma Pgcdn_correct : forall n a b, (Psize a + Psize b<=n)%nat -> Zis_gcd (Zpos a) (Zpos b) (Zpos (Pgcdn n a b)). Proof. intro n; pattern n; apply lt_wf_ind; clear n; intros. @@ -977,7 +975,7 @@ Proof. rewrite (Zpos_minus_morphism _ _ H1). assert (0 < Zpos a) by (compute; auto). omega. - omega. + omega. rewrite Zpos_xO; do 2 rewrite Zpos_xI. rewrite Zpos_minus_morphism; auto. omega. @@ -995,7 +993,7 @@ Proof. assert (0 < Zpos b) by (compute; auto). omega. rewrite ZC4; rewrite H1; auto. - omega. + omega. rewrite Zpos_xO; do 2 rewrite Zpos_xI. rewrite Zpos_minus_morphism; auto. omega. @@ -1062,7 +1060,7 @@ Proof. split; [apply Zgcd_is_gcd | apply Zgcd_is_pos]. Qed. -Theorem Zdivide_Zgcd: forall p q r : Z, +Theorem Zdivide_Zgcd: forall p q r : Z, (p | q) -> (p | r) -> (p | Zgcd q r). Proof. intros p q r H1 H2. @@ -1071,7 +1069,7 @@ Proof. inversion_clear H3; auto. Qed. -Theorem Zis_gcd_gcd: forall a b c : Z, +Theorem Zis_gcd_gcd: forall a b c : Z, 0 <= c -> Zis_gcd a b c -> Zgcd a b = c. Proof. intros a b c H1 H2. @@ -1103,7 +1101,7 @@ Proof. rewrite H1; ring. Qed. -Theorem Zgcd_div_swap0 : forall a b : Z, +Theorem Zgcd_div_swap0 : forall a b : Z, 0 < Zgcd a b -> 0 < b -> (a / Zgcd a b) * b = a * (b/Zgcd a b). @@ -1116,7 +1114,7 @@ Proof. rewrite <- Zdivide_Zdiv_eq; auto. Qed. -Theorem Zgcd_div_swap : forall a b c : Z, +Theorem Zgcd_div_swap : forall a b c : Z, 0 < Zgcd a b -> 0 < b -> (c * a) / Zgcd a b * b = c * a * (b/Zgcd a b). @@ -1131,7 +1129,43 @@ Proof. rewrite <- Zdivide_Zdiv_eq; auto. Qed. -Theorem Zgcd_1_rel_prime : forall a b, +Lemma Zgcd_comm : forall a b, Zgcd a b = Zgcd b a. +Proof. + intros. + apply Zis_gcd_gcd. + apply Zgcd_is_pos. + apply Zis_gcd_sym. + apply Zgcd_is_gcd. +Qed. + +Lemma Zgcd_ass : forall a b c, Zgcd (Zgcd a b) c = Zgcd a (Zgcd b c). +Proof. + intros. + apply Zis_gcd_gcd. + apply Zgcd_is_pos. + destruct (Zgcd_is_gcd a b). + destruct (Zgcd_is_gcd b c). + destruct (Zgcd_is_gcd a (Zgcd b c)). + constructor; eauto using Zdivide_trans. +Qed. + +Lemma Zgcd_Zabs : forall a b, Zgcd (Zabs a) b = Zgcd a b. +Proof. + destruct a; simpl; auto. +Qed. + +Lemma Zgcd_0 : forall a, Zgcd a 0 = Zabs a. +Proof. + destruct a; simpl; auto. +Qed. + +Lemma Zgcd_1 : forall a, Zgcd a 1 = 1. +Proof. + intros; apply Zis_gcd_gcd; auto with zarith; apply Zis_gcd_1. +Qed. +Hint Resolve Zgcd_0 Zgcd_1 : zarith. + +Theorem Zgcd_1_rel_prime : forall a b, Zgcd a b = 1 <-> rel_prime a b. Proof. unfold rel_prime; split; intro H. @@ -1142,7 +1176,7 @@ Proof. generalize (Zgcd_is_pos a b); auto with zarith. Qed. -Definition rel_prime_dec: forall a b, +Definition rel_prime_dec: forall a b, { rel_prime a b }+{ ~ rel_prime a b }. Proof. intros a b; case (Z_eq_dec (Zgcd a b) 1); intros H1. @@ -1156,10 +1190,10 @@ Definition prime_dec_aux: { exists n, 1 < n < m /\ ~ rel_prime n p }. Proof. intros p m. - case (Z_lt_dec 1 m); intros H1; - [ | left; intros; elimtype False; omega ]. + case (Z_lt_dec 1 m); intros H1; + [ | left; intros; exfalso; omega ]. pattern m; apply natlike_rec; auto with zarith. - left; intros; elimtype False; omega. + left; intros; exfalso; omega. intros x Hx IH; destruct IH as [F|E]. destruct (rel_prime_dec x p) as [Y|N]. left; intros n [HH1 HH2]. @@ -1221,34 +1255,34 @@ Qed. Open Scope positive_scope. -Fixpoint Pggcdn (n: nat) (a b : positive) { struct n } : (positive*(positive*positive)) := - match n with +Fixpoint Pggcdn (n: nat) (a b : positive) : (positive*(positive*positive)) := + match n with | O => (1,(a,b)) - | S n => - match a,b with - | xH, b => (1,(1,b)) + | S n => + match a,b with + | xH, b => (1,(1,b)) | a, xH => (1,(a,1)) - | xO a, xO b => - let (g,p) := Pggcdn n a b in + | xO a, xO b => + let (g,p) := Pggcdn n a b in (xO g,p) - | a, xO b => - let (g,p) := Pggcdn n a b in - let (aa,bb) := p in + | a, xO b => + let (g,p) := Pggcdn n a b in + let (aa,bb) := p in (g,(aa, xO bb)) - | xO a, b => - let (g,p) := Pggcdn n a b in - let (aa,bb) := p in + | xO a, b => + let (g,p) := Pggcdn n a b in + let (aa,bb) := p in (g,(xO aa, bb)) - | xI a', xI b' => - match Pcompare a' b' Eq with + | xI a', xI b' => + match Pcompare a' b' Eq with | Eq => (a,(1,1)) - | Lt => - let (g,p) := Pggcdn n (b'-a') a in - let (ba,aa) := p in + | Lt => + let (g,p) := Pggcdn n (b'-a') a in + let (ba,aa) := p in (g,(aa, aa + xO ba)) - | Gt => - let (g,p) := Pggcdn n (a'-b') b in - let (ab,bb) := p in + | Gt => + let (g,p) := Pggcdn n (a'-b') b in + let (ab,bb) := p in (g,(bb+xO ab, bb)) end end @@ -1260,28 +1294,28 @@ Open Scope Z_scope. Definition Zggcd (a b : Z) : Z*(Z*Z) := match a,b with - | Z0, _ => (Zabs b,(0, Zsgn b)) + | Z0, _ => (Zabs b,(0, Zsgn b)) | _, Z0 => (Zabs a,(Zsgn a, 0)) - | Zpos a, Zpos b => - let (g,p) := Pggcd a b in - let (aa,bb) := p in + | Zpos a, Zpos b => + let (g,p) := Pggcd a b in + let (aa,bb) := p in (Zpos g, (Zpos aa, Zpos bb)) - | Zpos a, Zneg b => - let (g,p) := Pggcd a b in - let (aa,bb) := p in + | Zpos a, Zneg b => + let (g,p) := Pggcd a b in + let (aa,bb) := p in (Zpos g, (Zpos aa, Zneg bb)) - | Zneg a, Zpos b => - let (g,p) := Pggcd a b in - let (aa,bb) := p in + | Zneg a, Zpos b => + let (g,p) := Pggcd a b in + let (aa,bb) := p in (Zpos g, (Zneg aa, Zpos bb)) | Zneg a, Zneg b => - let (g,p) := Pggcd a b in - let (aa,bb) := p in + let (g,p) := Pggcd a b in + let (aa,bb) := p in (Zpos g, (Zneg aa, Zneg bb)) end. -Lemma Pggcdn_gcdn : forall n a b, +Lemma Pggcdn_gcdn : forall n a b, fst (Pggcdn n a b) = Pgcdn n a b. Proof. induction n. @@ -1302,15 +1336,15 @@ Qed. Lemma Zggcd_gcd : forall a b, fst (Zggcd a b) = Zgcd a b. Proof. - destruct a; destruct b; simpl; auto; rewrite <- Pggcd_gcd; + destruct a; destruct b; simpl; auto; rewrite <- Pggcd_gcd; destruct (Pggcd p p0) as (g,(aa,bb)); simpl; auto. Qed. Open Scope positive_scope. -Lemma Pggcdn_correct_divisors : forall n a b, - let (g,p) := Pggcdn n a b in - let (aa,bb):=p in +Lemma Pggcdn_correct_divisors : forall n a b, + let (g,p) := Pggcdn n a b in + let (aa,bb):=p in (a=g*aa) /\ (b=g*bb). Proof. induction n. @@ -1337,7 +1371,7 @@ Proof. rewrite <- H1; rewrite <- H0. simpl; f_equal; symmetry. apply Pplus_minus; auto. - (* Then... *) + (* Then... *) generalize (IHn (xI a) b); destruct (Pggcdn n (xI a) b) as (g,(ab,bb)); simpl. intros (H0,H1); split; auto. rewrite Pmult_xO_permute_r; rewrite H1; auto. @@ -1348,9 +1382,9 @@ Proof. intros (H0,H1); split; subst; auto. Qed. -Lemma Pggcd_correct_divisors : forall a b, - let (g,p) := Pggcd a b in - let (aa,bb):=p in +Lemma Pggcd_correct_divisors : forall a b, + let (g,p) := Pggcd a b in + let (aa,bb):=p in (a=g*aa) /\ (b=g*bb). Proof. intros a b; exact (Pggcdn_correct_divisors (Psize a + Psize b)%nat a b). @@ -1358,17 +1392,17 @@ Qed. Close Scope positive_scope. -Lemma Zggcd_correct_divisors : forall a b, - let (g,p) := Zggcd a b in - let (aa,bb):=p in +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. - destruct a; destruct b; simpl; auto; try solve [rewrite Pmult_comm; simpl; auto]; - generalize (Pggcd_correct_divisors p p0); destruct (Pggcd p p0) as (g,(aa,bb)); + destruct a; destruct b; simpl; auto; try solve [rewrite Pmult_comm; simpl; auto]; + generalize (Pggcd_correct_divisors p p0); destruct (Pggcd p p0) as (g,(aa,bb)); destruct 1; subst; auto. Qed. -Theorem Zggcd_opp: forall x y, +Theorem Zggcd_opp: forall x y, Zggcd (-x) y = let (p1,p) := Zggcd x y in let (p2,p3) := p in (p1,(-p2,p3)). diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v index 73808f92..511c364b 100644 --- a/theories/ZArith/Zorder.v +++ b/theories/ZArith/Zorder.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -5,9 +6,9 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zorder.v 12888 2010-03-28 19:35:03Z herbelin $ i*) +(*i $Id$ i*) -(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *) +(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) Require Import BinPos. Require Import BinInt. @@ -49,7 +50,7 @@ Proof. [ tauto | intros H3; right; unfold not in |- *; intros H4; elim H3; rewrite (H2 H4); intros H5; discriminate H5 ]. -Qed. +Qed. Theorem dec_Zne : forall n m:Z, decidable (Zne n m). Proof. @@ -79,7 +80,7 @@ Proof. intros x y; unfold decidable, Zge in |- *; elim (x ?= y); [ left; discriminate | right; unfold not in |- *; intros H; apply H; trivial with arith - | left; discriminate ]. + | left; discriminate ]. Qed. Theorem dec_Zlt : forall n m:Z, decidable (n < m). @@ -96,7 +97,7 @@ Proof. | unfold Zlt in |- *; intros H; elim H; intros H1; [ auto with arith | right; elim (Zcompare_Gt_Lt_antisym x y); auto with arith ] ]. -Qed. +Qed. (** * Relating strict and large orders *) @@ -180,7 +181,7 @@ Proof. intros x y. split. intro. apply Zgt_lt. assumption. intro. apply Zlt_gt. assumption. Qed. - + (** * Equivalence and order properties *) (** Reflexivity *) @@ -188,7 +189,7 @@ Qed. Lemma Zle_refl : forall n:Z, n <= n. Proof. intros n; unfold Zle in |- *; rewrite (Zcompare_refl n); discriminate. -Qed. +Qed. Lemma Zeq_le : forall n m:Z, n = m -> n <= m. Proof. @@ -201,7 +202,7 @@ Hint Resolve Zle_refl: zarith. Lemma Zle_antisym : forall n m:Z, n <= m -> m <= n -> n = m. Proof. - intros n m H1 H2; destruct (Ztrichotomy n m) as [Hlt| [Heq| Hgt]]. + intros n m H1 H2; destruct (Ztrichotomy n m) as [Hlt| [Heq| Hgt]]. absurd (m > n); [ apply Zle_not_gt | apply Zlt_gt ]; assumption. assumption. absurd (n > m); [ apply Zle_not_gt | idtac ]; assumption. @@ -256,6 +257,13 @@ Proof. | absurd (n > m); [ apply Zle_not_gt | idtac ]; assumption ]. Qed. +Lemma Zle_lt_or_eq_iff : forall n m, n <= m <-> n < m \/ n = m. +Proof. + unfold Zle, Zlt. intros. + generalize (Zcompare_Eq_iff_eq n m). + destruct (n ?= m); intuition; discriminate. +Qed. + (** Dichotomy *) Lemma Zle_or_lt : forall n m:Z, n <= m \/ m < n. @@ -276,8 +284,7 @@ Qed. Lemma Zlt_trans : forall n m p:Z, n < m -> m < p -> n < p. Proof. - intros n m p H1 H2; apply Zgt_lt; apply Zgt_trans with (m := m); apply Zlt_gt; - assumption. + exact Zcompare_Lt_trans. Qed. (** Mixed transitivity *) @@ -400,13 +407,13 @@ Qed. Lemma Zgt_le_succ : forall n m:Z, m > n -> Zsucc n <= m. Proof. unfold Zgt, Zle in |- *; intros n p H; elim (Zcompare_Gt_not_Lt p n); - intros H1 H2; unfold not in |- *; intros H3; unfold not in H1; + intros H1 H2; unfold not in |- *; intros H3; unfold not in H1; apply H1; [ assumption | elim (Zcompare_Gt_Lt_antisym (n + 1) p); intros H4 H5; apply H4; exact H3 ]. Qed. -Lemma Zlt_gt_succ : forall n m:Z, n <= m -> Zsucc m > n. +Lemma Zle_gt_succ : forall n m:Z, n <= m -> Zsucc m > n. Proof. intros n p H; apply Zgt_le_trans with p. apply Zgt_succ. @@ -415,7 +422,7 @@ Qed. Lemma Zle_lt_succ : forall n m:Z, n <= m -> n < Zsucc m. Proof. - intros n m H; apply Zgt_lt; apply Zlt_gt_succ; assumption. + intros n m H; apply Zgt_lt; apply Zle_gt_succ; assumption. Qed. Lemma Zlt_le_succ : forall n m:Z, n < m -> Zsucc n <= m. @@ -433,12 +440,17 @@ Proof. intros n m H; apply Zgt_succ_le; apply Zlt_gt; assumption. Qed. -Lemma Zlt_succ_gt : forall n m:Z, Zsucc n <= m -> m > n. +Lemma Zle_succ_gt : forall n m:Z, Zsucc n <= m -> m > n. Proof. intros n m H; apply Zle_gt_trans with (m := Zsucc n); [ assumption | apply Zgt_succ ]. Qed. +Lemma Zlt_succ_r : forall n m, n < Zsucc m <-> n <= m. +Proof. + split; [apply Zlt_succ_le | apply Zle_lt_succ]. +Qed. + (** Weakening order *) Lemma Zle_succ : forall n:Z, n <= Zsucc n. @@ -478,9 +490,9 @@ Hint Resolve Zle_le_succ: zarith. Lemma Zgt_succ_pred : forall n m:Z, m > Zsucc n -> Zpred m > n. Proof. unfold Zgt, Zsucc, Zpred in |- *; intros n p H; - rewrite <- (fun x y => Zcompare_plus_compat x y 1); + rewrite <- (fun x y => Zcompare_plus_compat x y 1); rewrite (Zplus_comm p); rewrite Zplus_assoc; - rewrite (fun x => Zplus_comm x n); simpl in |- *; + rewrite (fun x => Zplus_comm x n); simpl in |- *; assumption. Qed. @@ -563,7 +575,7 @@ Proof. assert (Hle : m <= n). apply Zgt_succ_le; assumption. destruct (Zle_lt_or_eq _ _ Hle) as [Hlt| Heq]. - left; apply Zlt_gt; assumption. + left; apply Zlt_gt; assumption. right; assumption. Qed. @@ -680,7 +692,7 @@ Proof. rewrite (Zplus_comm p n); rewrite (Zplus_comm p m); trivial. Qed. -(** ** Multiplication *) +(** ** Multiplication *) (** Compatibility of multiplication by a positive wrt to order *) Lemma Zmult_le_compat_r : forall n m p:Z, n <= m -> 0 <= p -> n * p <= m * p. @@ -777,7 +789,7 @@ Proof. intros a b c d H0 H1 H2 H3. apply Zge_trans with (a * d). apply Zmult_ge_compat_l; trivial. - apply Zge_trans with c; trivial. + apply Zge_trans with c; trivial. apply Zmult_ge_compat_r; trivial. Qed. @@ -965,17 +977,17 @@ Qed. Lemma Zeq_plus_swap : forall n m p:Z, n + p = m <-> n = m - p. Proof. - intros x y z; intros. split. intro. apply Zplus_minus_eq. symmetry in |- *. rewrite Zplus_comm. + intros x y z; intros. split. intro. apply Zplus_minus_eq. symmetry in |- *. rewrite Zplus_comm. assumption. - intro. rewrite H. unfold Zminus in |- *. rewrite Zplus_assoc_reverse. + intro. rewrite H. unfold Zminus in |- *. rewrite Zplus_assoc_reverse. rewrite Zplus_opp_l. apply Zplus_0_r. Qed. Lemma Zlt_minus_simpl_swap : forall n m:Z, 0 < m -> n - m < n. Proof. intros n m H; apply Zplus_lt_reg_l with (p := m); rewrite Zplus_minus; - pattern n at 1 in |- *; rewrite <- (Zplus_0_r n); - rewrite (Zplus_comm m n); apply Zplus_lt_compat_l; + pattern n at 1 in |- *; rewrite <- (Zplus_0_r n); + rewrite (Zplus_comm m n); apply Zplus_lt_compat_l; assumption. Qed. @@ -993,8 +1005,8 @@ Qed. Lemma Zle_minus_le_0 : forall n m:Z, m <= n -> 0 <= n - m. Proof. - intros n m H; unfold Zminus; apply Zplus_le_reg_r with (p := m); - rewrite <- Zplus_assoc; rewrite Zplus_opp_l; rewrite Zplus_0_r; exact H. + intros n m H; unfold Zminus; apply Zplus_le_reg_r with (p := m); + rewrite <- Zplus_assoc; rewrite Zplus_opp_l; rewrite Zplus_0_r; exact H. Qed. Lemma Zmult_lt_compat: @@ -1012,7 +1024,7 @@ Proof. rewrite <- H5; simpl; apply Zmult_lt_0_compat; auto with zarith. Qed. -Lemma Zmult_lt_compat2: +Lemma Zmult_lt_compat2: forall n m p q : Z, 0 < n <= p -> 0 < m < q -> n * m < p * q. Proof. intros n m p q (H1, H2) (H3, H4). @@ -1025,5 +1037,3 @@ Qed. (** For compatibility *) Notation Zlt_O_minus_lt := Zlt_0_minus_lt (only parsing). -Notation Zle_gt_succ := Zlt_gt_succ (only parsing). -Notation Zle_succ_gt := Zlt_succ_gt (only parsing). diff --git a/theories/ZArith/Zpow_def.v b/theories/ZArith/Zpow_def.v index b0f372de..620d6324 100644 --- a/theories/ZArith/Zpow_def.v +++ b/theories/ZArith/Zpow_def.v @@ -2,11 +2,11 @@ Require Import ZArith_base. Require Import Ring_theory. Open Local Scope Z_scope. - + (** [Zpower_pos z n] is the n-th power of [z] when [n] is an binary - integer (type [positive]) and [z] a signed integer (type [Z]) *) + integer (type [positive]) and [z] a signed integer (type [Z]) *) Definition Zpower_pos (z:Z) (n:positive) := iter_pos n Z (fun x:Z => z * x) 1. - + Definition Zpower (x y:Z) := match y with | Zpos p => Zpower_pos x p @@ -24,4 +24,4 @@ Proof. repeat rewrite Zmult_assoc;trivial. rewrite H;rewrite Zmult_1_r;trivial. Qed. - + diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v index 3d4d235a..1d9b3dfc 100644 --- a/theories/ZArith/Zpow_facts.v +++ b/theories/ZArith/Zpow_facts.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zpow_facts.v 11098 2008-06-11 09:16:22Z letouzey $ i*) +(*i $Id$ i*) Require Import ZArith_base. Require Import ZArithRing. @@ -37,7 +37,7 @@ Proof. Qed. Lemma Zpower_pos_0_l: forall p, Zpower_pos 0 p = 0. -Proof. +Proof. induction p. change (xI p) with (1 + (xO p))%positive. rewrite Zpower_pos_is_exp, Zpower_pos_1_r; auto. @@ -133,7 +133,7 @@ Proof. apply Zle_ge; replace 0 with (0 * r1); try apply Zmult_le_compat_r; auto. Qed. -Theorem Zpower_le_monotone: forall a b c, +Theorem Zpower_le_monotone: forall a b c, 0 < a -> 0 <= b <= c -> a^b <= a^c. Proof. intros a b c H (H1, H2). @@ -145,7 +145,7 @@ Proof. apply Zlt_le_weak; apply Zpower_gt_0; auto with zarith. Qed. -Theorem Zpower_lt_monotone: forall a b c, +Theorem Zpower_lt_monotone: forall a b c, 1 < a -> 0 <= b < c -> a^b < a^c. Proof. intros a b c H (H1, H2). @@ -160,7 +160,7 @@ Proof. apply Zpower_le_monotone; auto with zarith. Qed. -Theorem Zpower_gt_1 : forall x y, +Theorem Zpower_gt_1 : forall x y, 1 < x -> 0 < y -> 1 < x^y. Proof. intros x y H1 H2. @@ -168,14 +168,14 @@ Proof. apply Zpower_lt_monotone; auto with zarith. Qed. -Theorem Zpower_ge_0: forall x y, 0 <= x -> 0 <= x^y. +Theorem Zpower_ge_0: forall x y, 0 <= x -> 0 <= x^y. Proof. intros x y; case y; auto with zarith. simpl ; auto with zarith. intros p H1; assert (H: 0 <= Zpos p); auto with zarith. generalize H; pattern (Zpos p); apply natlike_ind; auto with zarith. - intros p1 H2 H3 _; unfold Zsucc; rewrite Zpower_exp; simpl; auto with zarith. - apply Zmult_le_0_compat; auto with zarith. + intros p1 H2 H3 _; unfold Zsucc; rewrite Zpower_exp; simpl; auto with zarith. + apply Zmult_le_0_compat; auto with zarith. generalize H1; case x; compute; intros; auto; try discriminate. Qed. @@ -195,7 +195,7 @@ Proof. destruct b;trivial;unfold Zgt in z;discriminate z. Qed. -Theorem Zmult_power: forall p q r, 0 <= r -> +Theorem Zmult_power: forall p q r, 0 <= r -> (p*q)^r = p^r * q^r. Proof. intros p q r H1; generalize H1; pattern r; apply natlike_ind; auto. @@ -206,7 +206,7 @@ Qed. Hint Resolve Zpower_ge_0 Zpower_gt_0: zarith. -Theorem Zpower_le_monotone3: forall a b c, +Theorem Zpower_le_monotone3: forall a b c, 0 <= c -> 0 <= a <= b -> a^c <= b^c. Proof. intros a b c H (H1, H2). @@ -216,7 +216,7 @@ Proof. apply Zle_trans with (a^x * b); auto with zarith. Qed. -Lemma Zpower_le_monotone_inv: forall a b c, +Lemma Zpower_le_monotone_inv: forall a b c, 1 < a -> 0 < b -> a^b <= a^c -> b <= c. Proof. intros a b c H H0 H1. @@ -227,14 +227,14 @@ Proof. apply Zpower_le_monotone;auto with zarith. apply Zpower_le_monotone3;auto with zarith. assert (c > 0). - destruct (Z_le_gt_dec 0 c);trivial. + destruct (Z_le_gt_dec 0 c);trivial. destruct (Zle_lt_or_eq _ _ z0);auto with zarith. - rewrite <- H3 in H1;simpl in H1; elimtype False;omega. - destruct c;try discriminate z0. simpl in H1. elimtype False;omega. - assert (H4 := Zpower_lt_monotone a c b H). elimtype False;omega. + rewrite <- H3 in H1;simpl in H1; exfalso;omega. + destruct c;try discriminate z0. simpl in H1. exfalso;omega. + assert (H4 := Zpower_lt_monotone a c b H). exfalso;omega. Qed. -Theorem Zpower_nat_Zpower: forall p q, 0 <= q -> +Theorem Zpower_nat_Zpower: forall p q, 0 <= q -> p^q = Zpower_nat p (Zabs_nat q). Proof. intros p1 q1; case q1; simpl. @@ -262,7 +262,7 @@ Proof. intros; apply Zlt_le_weak; apply Zpower2_lt_lin; auto. Qed. -Lemma Zpower2_Psize : +Lemma Zpower2_Psize : forall n p, Zpos p < 2^(Z_of_nat n) <-> (Psize p <= n)%nat. Proof. induction n. @@ -294,7 +294,7 @@ Qed. (** A direct way to compute Zpower modulo **) -Fixpoint Zpow_mod_pos (a: Z)(m: positive)(n : Z) {struct m} : Z := +Fixpoint Zpow_mod_pos (a: Z)(m: positive)(n : Z) : Z := match m with | xH => a mod n | xO m' => @@ -311,14 +311,14 @@ Fixpoint Zpow_mod_pos (a: Z)(m: positive)(n : Z) {struct m} : Z := end end. -Definition Zpow_mod a m n := - match m with - | 0 => 1 - | Zpos p => Zpow_mod_pos a p n - | Zneg p => 0 +Definition Zpow_mod a m n := + match m with + | 0 => 1 + | Zpos p => Zpow_mod_pos a p n + | Zneg p => 0 end. -Theorem Zpow_mod_pos_correct: forall a m n, 0 < n -> +Theorem Zpow_mod_pos_correct: forall a m n, 0 < n -> Zpow_mod_pos a m n = (Zpower_pos a m) mod n. Proof. intros a m; elim m; simpl; auto. @@ -327,12 +327,12 @@ Proof. repeat rewrite Rec; auto. rewrite Zpower_pos_1_r. repeat rewrite (fun x => (Zmult_mod x a)); auto with zarith. - rewrite (Zmult_mod (Zpower_pos a p)); auto with zarith. + rewrite (Zmult_mod (Zpower_pos a p)); auto with zarith. case (Zpower_pos a p mod n); auto. intros p Rec n H1; rewrite <- Pplus_diag; auto. repeat rewrite Zpower_pos_is_exp; auto. repeat rewrite Rec; auto. - rewrite (Zmult_mod (Zpower_pos a p)); auto with zarith. + rewrite (Zmult_mod (Zpower_pos a p)); auto with zarith. case (Zpower_pos a p mod n); auto. unfold Zpower_pos; simpl; rewrite Zmult_1_r; auto with zarith. Qed. @@ -354,7 +354,7 @@ Proof. pattern p at 3; rewrite <- (Zpower_1_r p); rewrite <- Zpower_exp; try f_equal; auto with zarith. Qed. -Theorem rel_prime_Zpower_r: forall i p q, 0 < i -> +Theorem rel_prime_Zpower_r: forall i p q, 0 < i -> rel_prime p q -> rel_prime p (q^i). Proof. intros i p q Hi Hpq; generalize Hi; pattern i; apply natlike_ind; auto with zarith; clear i Hi. @@ -365,7 +365,7 @@ Proof. rewrite Zpower_0_r; apply rel_prime_sym; apply rel_prime_1. Qed. -Theorem rel_prime_Zpower: forall i j p q, 0 <= i -> 0 <= j -> +Theorem rel_prime_Zpower: forall i j p q, 0 <= i -> 0 <= j -> rel_prime p q -> rel_prime (p^i) (q^j). Proof. intros i j p q Hi; generalize Hi j p q; pattern i; apply natlike_ind; auto with zarith; clear i Hi j p q. @@ -379,7 +379,7 @@ Proof. rewrite Zpower_0_r; apply rel_prime_sym; apply rel_prime_1. Qed. -Theorem prime_power_prime: forall p q n, 0 <= n -> +Theorem prime_power_prime: forall p q n, 0 <= n -> prime p -> prime q -> (p | q^n) -> p = q. Proof. intros p q n Hn Hp Hq; pattern n; apply natlike_ind; auto; clear n Hn. @@ -442,15 +442,15 @@ Fixpoint Psquare (p: positive): positive := end. Definition Zsquare p := - match p with - | Z0 => Z0 - | Zpos p => Zpos (Psquare p) + match p with + | Z0 => Z0 + | Zpos p => Zpos (Psquare p) | Zneg p => Zpos (Psquare p) end. Theorem Psquare_correct: forall p, Psquare p = (p * p)%positive. Proof. - induction p; simpl; auto; f_equal; rewrite IHp. + induction p; simpl; auto; f_equal; rewrite IHp. apply trans_equal with (xO p + xO (p*p))%positive; auto. rewrite (Pplus_comm (xO p)); auto. rewrite Pmult_xI_permute_r; rewrite Pplus_assoc. diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v index 1912f5e1..508e6601 100644 --- a/theories/ZArith/Zpower.v +++ b/theories/ZArith/Zpower.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zpower.v 11072 2008-06-08 16:13:37Z herbelin $ i*) +(*i $Id$ i*) Require Import Wf_nat. Require Import ZArith_base. @@ -20,7 +20,7 @@ Infix "^" := Zpower : Z_scope. (** * Definition of powers over [Z]*) (** [Zpower_nat z n] is the n-th power of [z] when [n] is an unary - integer (type [nat]) and [z] a signed integer (type [Z]) *) + integer (type [nat]) and [z] a signed integer (type [Z]) *) Definition Zpower_nat (z:Z) (n:nat) := iter_nat n Z (fun x:Z => z * x) 1. @@ -83,12 +83,12 @@ Section Powers_of_2. (** For the powers of two, that will be widely used, a more direct calculus is possible. We will also prove some properties such as [(x:positive) x < 2^x] that are true for all integers bigger - than 2 but more difficult to prove and useless. *) + than 2 but more difficult to prove and useless. *) (** [shift n m] computes [2^n * m], or [m] shifted by [n] positions *) - Definition shift_nat (n:nat) (z:positive) := iter_nat n positive xO z. - Definition shift_pos (n z:positive) := iter_pos n positive xO z. + Definition shift_nat (n:nat) (z:positive) := iter_nat n positive xO z. + Definition shift_pos (n z:positive) := iter_pos n positive xO z. Definition shift (n:Z) (z:positive) := match n with | Z0 => z @@ -130,7 +130,7 @@ Section Powers_of_2. rewrite (shift_nat_correct n). omega. Qed. - + (** Second we show that [two_power_pos] and [two_power_nat] are the same *) Lemma shift_pos_nat : forall p x:positive, shift_pos p x = shift_nat (nat_of_P p) x. @@ -181,12 +181,12 @@ Section Powers_of_2. apply Zpower_pos_is_exp. Qed. - (** The exponentiation [z -> 2^z] for [z] a signed integer. + (** The exponentiation [z -> 2^z] for [z] a signed integer. For convenience, we assume that [2^z = 0] for all [z < 0] We could also define a inductive type [Log_result] with 3 contructors [ Zero | Pos positive -> | minus_infty] but it's more complexe and not so useful. *) - + Definition two_p (x:Z) := match x with | Z0 => 1 @@ -227,7 +227,7 @@ Section Powers_of_2. Lemma two_p_S : forall x:Z, 0 <= x -> two_p (Zsucc x) = 2 * two_p x. Proof. - intros; unfold Zsucc in |- *. + intros; unfold Zsucc in |- *. rewrite (two_p_is_exp x 1 H (Zorder.Zle_0_pos 1)). apply Zmult_comm. Qed. @@ -247,10 +247,10 @@ Section Powers_of_2. | intro Hx0; rewrite <- Hx0; simpl in |- *; unfold Zlt in |- *; auto with zarith ] | assumption ]. - Qed. + Qed. Lemma Zlt_lt_double : forall x y:Z, 0 <= x < y -> x < 2 * y. - intros; omega. Qed. + intros; omega. Qed. End Powers_of_2. @@ -286,13 +286,13 @@ Section power_div_with_rest. let (qr, d) := iter_pos p _ Zdiv_rest_aux (x, 0, 1) in d = two_power_pos p. Proof. intros x p; rewrite (iter_nat_of_P p _ Zdiv_rest_aux (x, 0, 1)); - rewrite (two_power_pos_nat p); elim (nat_of_P p); + rewrite (two_power_pos_nat p); elim (nat_of_P p); simpl in |- *; [ trivial with zarith | intro n; rewrite (two_power_nat_S n); unfold Zdiv_rest_aux at 2 in |- *; - elim (iter_nat n (Z * Z * Z) Zdiv_rest_aux (x, 0, 1)); + elim (iter_nat n (Z * Z * Z) Zdiv_rest_aux (x, 0, 1)); destruct a; intros; apply f_equal with (f := fun z:Z => 2 * z); - assumption ]. + assumption ]. Qed. Lemma Zdiv_rest_correct2 : @@ -327,7 +327,7 @@ Section power_div_with_rest. apply f_equal with (f := fun z:Z => z + r); do 2 rewrite Zmult_plus_distr_l; rewrite Zmult_assoc; rewrite (Zmult_comm (Zneg p0) 2); rewrite <- Zplus_assoc; - apply f_equal with (f := fun z:Z => 2 * Zneg p0 * d + z); + apply f_equal with (f := fun z:Z => 2 * Zneg p0 * d + z); omega | omega ] | rewrite BinInt.Zneg_xO; unfold Zminus in |- *; intro; elim H; intros; diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v index 6ea952e6..b845cf47 100644 --- a/theories/ZArith/Zsqrt.v +++ b/theories/ZArith/Zsqrt.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Zsqrt.v 10295 2007-11-06 22:46:21Z letouzey $ *) +(* $Id$ *) Require Import ZArithRing. Require Import Omega. @@ -119,7 +119,7 @@ Definition Zsqrt : | Zneg p => fun h => False_rec - {s : Z & + {s : Z & {r : Z | Zneg p = s * s + r /\ s * s <= Zneg p < (s + 1) * (s + 1)}} (h (refl_equal Datatypes.Gt)) @@ -199,7 +199,7 @@ Qed. Theorem Zsqrt_le: forall p q, 0 <= p <= q -> Zsqrt_plain p <= Zsqrt_plain q. Proof. - intros p q [H1 H2]; case Zle_lt_or_eq with (1:=H2); clear H2; intros H2; + intros p q [H1 H2]; case Zle_lt_or_eq with (1:=H2); clear H2; intros H2; [ | subst q; auto with zarith]. case (Zle_or_lt (Zsqrt_plain p) (Zsqrt_plain q)); auto; intros H3. assert (Hp: (0 <= Zsqrt_plain q)). diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v index bd617204..32d6de19 100644 --- a/theories/ZArith/Zwf.v +++ b/theories/ZArith/Zwf.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Zwf.v 9245 2006-10-17 12:53:34Z notin $ *) +(* $Id$ *) Require Import ZArith_base. Require Export Wf_nat. @@ -15,7 +15,7 @@ Open Local Scope Z_scope. (** Well-founded relations on Z. *) -(** We define the following family of relations on [Z x Z]: +(** We define the following family of relations on [Z x Z]: [x (Zwf c) y] iff [x < y & c <= y] *) diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v index ffc3e70f..7af99ece 100644 --- a/theories/ZArith/auxiliary.v +++ b/theories/ZArith/auxiliary.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -6,9 +7,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: auxiliary.v 11739 2009-01-02 19:33:19Z herbelin $ i*) +(*i $Id$ i*) -(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) +(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) Require Export Arith_base. Require Import BinInt. @@ -25,7 +26,7 @@ Open Local Scope Z_scope. Theorem Zne_left : forall n m:Z, Zne n m -> Zne (n + - m) 0. Proof. intros x y; unfold Zne in |- *; unfold not in |- *; intros H1 H2; apply H1; - apply Zplus_reg_l with (- y); rewrite Zplus_opp_l; + apply Zplus_reg_l with (- y); rewrite Zplus_opp_l; rewrite Zplus_comm; trivial with arith. Qed. @@ -97,7 +98,7 @@ Proof. intros x y z H1 H2 H3; apply Zle_trans with (m := y * x); [ apply Zmult_gt_0_le_0_compat; assumption | pattern (y * x) at 1 in |- *; rewrite <- Zplus_0_r; - apply Zplus_le_compat_l; apply Zlt_le_weak; apply Zgt_lt; + apply Zplus_le_compat_l; apply Zlt_le_weak; apply Zgt_lt; assumption ]. Qed. diff --git a/theories/ZArith/vo.itarget b/theories/ZArith/vo.itarget new file mode 100644 index 00000000..3efa7055 --- /dev/null +++ b/theories/ZArith/vo.itarget @@ -0,0 +1,32 @@ +auxiliary.vo +BinInt.vo +Int.vo +Wf_Z.vo +Zabs.vo +ZArith_base.vo +ZArith_dec.vo +ZArith.vo +Zdigits.vo +Zbool.vo +Zcompare.vo +Zcomplements.vo +Zdiv.vo +Zeven.vo +Zgcd_alt.vo +Zhints.vo +Zlogarithm.vo +Zmax.vo +Zminmax.vo +Zmin.vo +Zmisc.vo +Znat.vo +Znumtheory.vo +ZOdiv_def.vo +ZOdiv.vo +Zorder.vo +Zpow_def.vo +Zpower.vo +Zpow_facts.vo +Zsqrt.vo +Zwf.vo +ZOrderedType.vo |