diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /theories/ZArith |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'theories/ZArith')
-rw-r--r-- | theories/ZArith/BinInt.v | 1038 | ||||
-rw-r--r-- | theories/ZArith/Wf_Z.v | 204 | ||||
-rw-r--r-- | theories/ZArith/ZArith.v | 22 | ||||
-rw-r--r-- | theories/ZArith/ZArith_base.v | 34 | ||||
-rw-r--r-- | theories/ZArith/ZArith_dec.v | 226 | ||||
-rw-r--r-- | theories/ZArith/Zabs.v | 128 | ||||
-rw-r--r-- | theories/ZArith/Zbinary.v | 426 | ||||
-rw-r--r-- | theories/ZArith/Zbool.v | 186 | ||||
-rw-r--r-- | theories/ZArith/Zcompare.v | 501 | ||||
-rw-r--r-- | theories/ZArith/Zcomplements.v | 212 | ||||
-rw-r--r-- | theories/ZArith/Zdiv.v | 423 | ||||
-rw-r--r-- | theories/ZArith/Zeven.v | 204 | ||||
-rw-r--r-- | theories/ZArith/Zhints.v | 386 | ||||
-rw-r--r-- | theories/ZArith/Zlogarithm.v | 265 | ||||
-rw-r--r-- | theories/ZArith/Zmin.v | 106 | ||||
-rw-r--r-- | theories/ZArith/Zmisc.v | 97 | ||||
-rw-r--r-- | theories/ZArith/Znat.v | 138 | ||||
-rw-r--r-- | theories/ZArith/Znumtheory.v | 640 | ||||
-rw-r--r-- | theories/ZArith/Zorder.v | 965 | ||||
-rw-r--r-- | theories/ZArith/Zpower.v | 372 | ||||
-rw-r--r-- | theories/ZArith/Zsqrt.v | 163 | ||||
-rw-r--r-- | theories/ZArith/Zwf.v | 96 | ||||
-rw-r--r-- | theories/ZArith/auxiliary.v | 150 | ||||
-rwxr-xr-x | theories/ZArith/intro.tex | 6 |
24 files changed, 6988 insertions, 0 deletions
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v new file mode 100644 index 00000000..11fa3872 --- /dev/null +++ b/theories/ZArith/BinInt.v @@ -0,0 +1,1038 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(*i $Id: BinInt.v,v 1.5.2.1 2004/07/16 19:31:20 herbelin Exp $ i*) + +(***********************************************************) +(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) +(***********************************************************) + +Require Export BinPos. +Require Export Pnat. +Require Import BinNat. +Require Import Plus. +Require Import Mult. +(**********************************************************************) +(** Binary integer numbers *) + +Inductive Z : Set := + | Z0 : Z + | Zpos : positive -> Z + | Zneg : positive -> Z. + +(** Declare Scope Z_scope with Key Z *) +Delimit Scope Z_scope with Z. + +(** Automatically open scope positive_scope for the constructors of Z *) +Bind Scope Z_scope with Z. +Arguments Scope Zpos [positive_scope]. +Arguments Scope Zneg [positive_scope]. + +(** Subtraction of positive into Z *) + +Definition Zdouble_plus_one (x:Z) := + match x with + | Z0 => Zpos 1 + | Zpos p => Zpos (xI p) + | Zneg p => Zneg (Pdouble_minus_one p) + end. + +Definition Zdouble_minus_one (x:Z) := + match x with + | Z0 => Zneg 1 + | Zneg p => Zneg (xI p) + | Zpos p => Zpos (Pdouble_minus_one p) + end. + +Definition Zdouble (x:Z) := + match x with + | Z0 => Z0 + | Zpos p => Zpos (xO p) + | Zneg p => Zneg (xO p) + end. + +Fixpoint ZPminus (x y:positive) {struct y} : Z := + match x, y with + | xI x', xI y' => Zdouble (ZPminus x' y') + | xI x', xO y' => Zdouble_plus_one (ZPminus x' y') + | xI x', xH => Zpos (xO x') + | xO x', xI y' => Zdouble_minus_one (ZPminus x' y') + | xO x', xO y' => Zdouble (ZPminus x' y') + | xO x', xH => Zpos (Pdouble_minus_one x') + | xH, xI y' => Zneg (xO y') + | xH, xO y' => Zneg (Pdouble_minus_one y') + | xH, xH => Z0 + end. + +(** Addition on integers *) + +Definition Zplus (x y:Z) := + match x, y with + | Z0, y => y + | x, Z0 => x + | Zpos x', Zpos y' => Zpos (x' + y') + | Zpos x', Zneg y' => + match (x' ?= y')%positive Eq with + | Eq => Z0 + | Lt => Zneg (y' - x') + | Gt => Zpos (x' - y') + end + | Zneg x', Zpos y' => + match (x' ?= y')%positive Eq with + | Eq => Z0 + | Lt => Zpos (y' - x') + | Gt => Zneg (x' - y') + end + | Zneg x', Zneg y' => Zneg (x' + y') + end. + +Infix "+" := Zplus : Z_scope. + +(** Opposite *) + +Definition Zopp (x:Z) := + match x with + | Z0 => Z0 + | Zpos x => Zneg x + | Zneg x => Zpos x + end. + +Notation "- x" := (Zopp x) : Z_scope. + +(** Successor on integers *) + +Definition Zsucc (x:Z) := (x + Zpos 1)%Z. + +(** Predecessor on integers *) + +Definition Zpred (x:Z) := (x + Zneg 1)%Z. + +(** Subtraction on integers *) + +Definition Zminus (m n:Z) := (m + - n)%Z. + +Infix "-" := Zminus : Z_scope. + +(** Multiplication on integers *) + +Definition Zmult (x y:Z) := + match x, y with + | Z0, _ => Z0 + | _, Z0 => Z0 + | Zpos x', Zpos y' => Zpos (x' * y') + | Zpos x', Zneg y' => Zneg (x' * y') + | Zneg x', Zpos y' => Zneg (x' * y') + | Zneg x', Zneg y' => Zpos (x' * y') + end. + +Infix "*" := Zmult : Z_scope. + +(** Comparison of integers *) + +Definition Zcompare (x y:Z) := + match x, y with + | Z0, Z0 => Eq + | Z0, Zpos y' => Lt + | Z0, Zneg y' => Gt + | Zpos x', Z0 => Gt + | Zpos x', Zpos y' => (x' ?= y')%positive Eq + | Zpos x', Zneg y' => Gt + | Zneg x', Z0 => Lt + | Zneg x', Zpos y' => Lt + | Zneg x', Zneg y' => CompOpp ((x' ?= y')%positive Eq) + end. + +Infix "?=" := Zcompare (at level 70, no associativity) : Z_scope. + +Ltac elim_compare com1 com2 := + case (Dcompare (com1 ?= com2)%Z); + [ idtac | let x := fresh "H" in + (intro x; case x; clear x) ]. + +(** Sign function *) + +Definition Zsgn (z:Z) : Z := + match z with + | Z0 => Z0 + | Zpos p => Zpos 1 + | Zneg p => Zneg 1 + end. + +(** Direct, easier to handle variants of successor and addition *) + +Definition Zsucc' (x:Z) := + match x with + | Z0 => Zpos 1 + | Zpos x' => Zpos (Psucc x') + | Zneg x' => ZPminus 1 x' + end. + +Definition Zpred' (x:Z) := + match x with + | Z0 => Zneg 1 + | Zpos x' => ZPminus x' 1 + | Zneg x' => Zneg (Psucc x') + end. + +Definition Zplus' (x y:Z) := + match x, y with + | Z0, y => y + | x, Z0 => x + | Zpos x', Zpos y' => Zpos (x' + y') + | Zpos x', Zneg y' => ZPminus x' y' + | Zneg x', Zpos y' => ZPminus y' x' + | Zneg x', Zneg y' => Zneg (x' + y') + end. + +Open Local Scope Z_scope. + +(**********************************************************************) +(** Inductive specification of Z *) + +Theorem Zind : + forall P:Z -> Prop, + P Z0 -> + (forall x:Z, P x -> P (Zsucc' x)) -> + (forall x:Z, P x -> P (Zpred' x)) -> forall n:Z, P n. +Proof. +intros P H0 Hs Hp z; destruct z. + assumption. + apply Pind with (P := fun p => P (Zpos p)). + change (P (Zsucc' Z0)) in |- *; apply Hs; apply H0. + intro n; exact (Hs (Zpos n)). + apply Pind with (P := fun p => P (Zneg p)). + change (P (Zpred' Z0)) in |- *; apply Hp; apply H0. + intro n; exact (Hp (Zneg n)). +Qed. + +(**********************************************************************) +(** Properties of opposite on binary integer numbers *) + +Theorem Zopp_neg : forall p:positive, - Zneg p = Zpos p. +Proof. +reflexivity. +Qed. + +(** [opp] is involutive *) + +Theorem Zopp_involutive : forall n:Z, - - n = n. +Proof. +intro x; destruct x; reflexivity. +Qed. + +(** Injectivity of the opposite *) + +Theorem Zopp_inj : forall n m:Z, - n = - m -> n = m. +Proof. +intros x y; case x; case y; simpl in |- *; intros; + [ trivial + | discriminate H + | discriminate H + | discriminate H + | simplify_eq H; intro E; rewrite E; trivial + | discriminate H + | discriminate H + | discriminate H + | simplify_eq H; intro E; rewrite E; trivial ]. +Qed. + +(**********************************************************************) +(* Properties of the direct definition of successor and predecessor *) + +Lemma Zpred'_succ' : forall n:Z, Zpred' (Zsucc' n) = n. +Proof. +intro x; destruct x; simpl in |- *. + reflexivity. +destruct p; simpl in |- *; try rewrite Pdouble_minus_one_o_succ_eq_xI; + reflexivity. +destruct p; simpl in |- *; try rewrite Psucc_o_double_minus_one_eq_xO; + reflexivity. +Qed. + +Lemma Zsucc'_discr : forall n:Z, n <> Zsucc' n. +Proof. +intro x; destruct x; simpl in |- *. + discriminate. + injection; apply Psucc_discr. + destruct p; simpl in |- *. + discriminate. + intro H; symmetry in H; injection H; apply double_moins_un_xO_discr. + discriminate. +Qed. + +(**********************************************************************) +(** Other properties of binary integer numbers *) + +Lemma ZL0 : 2%nat = (1 + 1)%nat. +Proof. +reflexivity. +Qed. + +(**********************************************************************) +(** Properties of the addition on integers *) + +(** zero is left neutral for addition *) + +Theorem Zplus_0_l : forall n:Z, Z0 + n = n. +Proof. +intro x; destruct x; reflexivity. +Qed. + +(** zero is right neutral for addition *) + +Theorem Zplus_0_r : forall n:Z, n + Z0 = n. +Proof. +intro x; destruct x; reflexivity. +Qed. + +(** addition is commutative *) + +Theorem Zplus_comm : forall n m:Z, n + m = m + n. +Proof. +intro x; induction x as [| p| p]; intro y; destruct y as [| q| q]; + simpl in |- *; try reflexivity. + rewrite Pplus_comm; reflexivity. + rewrite ZC4; destruct ((q ?= p)%positive Eq); reflexivity. + rewrite ZC4; destruct ((q ?= p)%positive Eq); reflexivity. + rewrite Pplus_comm; reflexivity. +Qed. + +(** opposite distributes over addition *) + +Theorem Zopp_plus_distr : forall n m:Z, - (n + m) = - n + - m. +Proof. +intro x; destruct x as [| p| p]; intro y; destruct y as [| q| q]; + simpl in |- *; reflexivity || destruct ((p ?= q)%positive Eq); + reflexivity. +Qed. + +(** opposite is inverse for addition *) + +Theorem Zplus_opp_r : forall n:Z, n + - n = Z0. +Proof. +intro x; destruct x as [| p| p]; simpl in |- *; + [ reflexivity + | rewrite (Pcompare_refl p); reflexivity + | rewrite (Pcompare_refl p); reflexivity ]. +Qed. + +Theorem Zplus_opp_l : forall n:Z, - n + n = Z0. +Proof. +intro; rewrite Zplus_comm; apply Zplus_opp_r. +Qed. + +Hint Local Resolve Zplus_0_l Zplus_0_r. + +(** addition is associative *) + +Lemma weak_assoc : + forall (p q:positive) (n:Z), Zpos p + (Zpos q + n) = Zpos p + Zpos q + n. +Proof. +intros x y z'; case z'; + [ auto with arith + | intros z; simpl in |- *; rewrite Pplus_assoc; auto with arith + | intros z; simpl in |- *; ElimPcompare y z; intros E0; rewrite E0; + ElimPcompare (x + y)%positive z; intros E1; rewrite E1; + [ absurd ((x + y ?= z)%positive Eq = Eq); + [ (* Case 1 *) + 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 |- *; + apply le_n_S; apply le_plus_r ] + | assumption ] + | absurd ((x + y ?= z)%positive Eq = Lt); + [ (* Case 2 *) + 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 |- *; + apply le_n_S; apply le_plus_r ] + | assumption ] + | rewrite (Pcompare_Eq_eq y z E0); + (* Case 3 *) + elim (Pminus_mask_Gt (x + z) z); + [ intros t H; elim H; intros H1 H2; elim H2; intros H3 H4; + unfold Pminus in |- *; rewrite H1; cut (x = t); + [ intros E; rewrite E; auto with arith + | apply Pplus_reg_r with (r := z); rewrite <- H3; + rewrite Pplus_comm; trivial with arith ] + | pattern z at 1 in |- *; rewrite <- (Pcompare_Eq_eq y z E0); + assumption ] + | elim (Pminus_mask_Gt z y); + [ (* Case 4 *) + intros k H; elim H; intros H1 H2; elim H2; intros H3 H4; + unfold Pminus at 1 in |- *; rewrite H1; cut (x = k); + [ intros E; rewrite E; rewrite (Pcompare_refl k); + trivial with arith + | apply Pplus_reg_r with (r := y); rewrite (Pplus_comm k y); + rewrite H3; apply Pcompare_Eq_eq; assumption ] + | apply ZC2; assumption ] + | elim (Pminus_mask_Gt z y); + [ (* Case 5 *) + intros k H; elim H; intros H1 H2; elim H2; intros H3 H4; + unfold Pminus at 1 3 5 in |- *; rewrite H1; + cut ((x ?= k)%positive Eq = Lt); + [ intros E2; rewrite E2; elim (Pminus_mask_Gt k x); + [ 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 |- *; + rewrite H6; rewrite H11; cut (i = j); + [ intros E; rewrite E; auto with arith + | apply (Pplus_reg_l (x + y)); rewrite H13; + rewrite (Pplus_comm x y); rewrite <- Pplus_assoc; + rewrite H8; assumption ] + | apply ZC2; assumption ] + | apply ZC2; assumption ] + | 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; + rewrite H3; rewrite Pplus_comm; assumption ] + | apply ZC2; assumption ] + | elim (Pminus_mask_Gt z y); + [ (* Case 6 *) + intros k H; elim H; intros H1 H2; elim H2; intros H3 H4; + elim (Pminus_mask_Gt (x + y) z); + [ intros i H5; elim H5; intros H6 H7; elim H7; intros H8 H9; + 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; + 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; + 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; + assumption ] + | assumption ] + | apply ZC2; assumption ] + | absurd ((x + y ?= z)%positive Eq = Eq); + [ (* Case 7 *) + rewrite nat_of_P_gt_Gt_compare_complement_morphism; + [ discriminate + | rewrite nat_of_P_plus_morphism; unfold gt in |- *; + apply lt_le_trans with (m := nat_of_P y); + [ apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; assumption + | apply le_plus_r ] ] + | assumption ] + | absurd ((x + y ?= z)%positive Eq = Lt); + [ (* Case 8 *) + rewrite nat_of_P_gt_Gt_compare_complement_morphism; + [ discriminate + | unfold gt in |- *; apply lt_le_trans with (m := nat_of_P y); + [ exact (nat_of_P_gt_Gt_compare_morphism y z E0) + | rewrite nat_of_P_plus_morphism; apply le_plus_r ] ] + | 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; + 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; + trivial with arith ] ] ]. +Qed. + +Hint Local Resolve weak_assoc. + +Theorem Zplus_assoc : forall n m p:Z, n + (m + p) = n + m + p. +Proof. +intros x y z; case x; case y; case z; auto with arith; intros; + [ rewrite (Zplus_comm (Zneg p0)); rewrite weak_assoc; + rewrite (Zplus_comm (Zpos p1 + Zneg p0)); rewrite weak_assoc; + rewrite (Zplus_comm (Zpos p1)); trivial with arith + | apply Zopp_inj; do 4 rewrite Zopp_plus_distr; do 2 rewrite Zopp_neg; + 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)); + trivial with arith + | rewrite Zplus_comm; rewrite (Zplus_comm (Zpos p0) (Zpos p)); + rewrite <- weak_assoc; rewrite Zplus_comm; rewrite (Zplus_comm (Zpos p0)); + trivial with arith + | apply Zopp_inj; do 4 rewrite Zopp_plus_distr; do 2 rewrite Zopp_neg; + rewrite (Zplus_comm (- Zpos p0)); rewrite weak_assoc; + rewrite (Zplus_comm (Zpos p1 + - Zpos p0)); rewrite weak_assoc; + rewrite (Zplus_comm (Zpos p)); trivial with arith + | apply Zopp_inj; do 4 rewrite Zopp_plus_distr; do 2 rewrite Zopp_neg; + apply weak_assoc + | apply Zopp_inj; do 4 rewrite Zopp_plus_distr; do 2 rewrite Zopp_neg; + apply weak_assoc ]. +Qed. + + +Lemma Zplus_assoc_reverse : forall n m p:Z, n + m + p = n + (m + p). +Proof. +intros; symmetry in |- *; apply Zplus_assoc. +Qed. + +(** Associativity mixed with commutativity *) + +Theorem Zplus_permute : forall n m p:Z, n + (m + p) = m + (n + p). +Proof. +intros n m p; rewrite Zplus_comm; rewrite <- Zplus_assoc; + rewrite (Zplus_comm p n); trivial with arith. +Qed. + +(** addition simplifies *) + +Theorem Zplus_reg_l : forall n m p:Z, n + m = n + p -> m = p. +intros n m p H; cut (- n + (n + m) = - n + (n + p)); + [ do 2 rewrite Zplus_assoc; rewrite (Zplus_comm (- n) n); + rewrite Zplus_opp_r; simpl in |- *; trivial with arith + | rewrite H; trivial with arith ]. +Qed. + +(** addition and successor permutes *) + +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)); + trivial with arith. +Qed. + +Lemma Zplus_succ_r : forall n m:Z, Zsucc (n + m) = n + Zsucc m. +Proof. +intros n m; unfold Zsucc in |- *; rewrite Zplus_assoc; trivial with arith. +Qed. + +Lemma Zplus_succ_comm : forall n m:Z, Zsucc n + m = n + Zsucc m. +Proof. +unfold Zsucc in |- *; intros n m; rewrite <- Zplus_assoc; + rewrite (Zplus_comm (Zpos 1)); trivial with arith. +Qed. + +(** Misc properties, usually redundant or non natural *) + +Lemma Zplus_0_r_reverse : forall n:Z, n = n + Z0. +Proof. +symmetry in |- *; apply Zplus_0_r. +Qed. + +Lemma Zplus_0_simpl_l : forall n m:Z, n + Z0 = m -> n = m. +Proof. +intros n m; rewrite Zplus_0_r; intro; assumption. +Qed. + +Lemma Zplus_0_simpl_l_reverse : forall n m:Z, n = m + Z0 -> n = m. +Proof. +intros n m; rewrite Zplus_0_r; intro; assumption. +Qed. + +Lemma Zplus_eq_compat : forall n m p q:Z, n = m -> p = q -> n + p = m + q. +Proof. +intros; rewrite H; rewrite H0; reflexivity. +Qed. + +Lemma Zplus_opp_expand : forall n m p:Z, n + - m = n + - p + (p + - m). +Proof. +intros x y z. +rewrite <- (Zplus_assoc x). +rewrite (Zplus_assoc (- z)). +rewrite Zplus_opp_l. +reflexivity. +Qed. + +(**********************************************************************) +(** Properties of successor and predecessor on binary integer numbers *) + +Theorem Zsucc_discr : forall n:Z, n <> Zsucc n. +Proof. +intros n; cut (Z0 <> Zpos 1); + [ unfold not in |- *; intros H1 H2; apply H1; apply (Zplus_reg_l n); + rewrite Zplus_0_r; exact H2 + | discriminate ]. +Qed. + +Theorem Zpos_succ_morphism : + forall p:positive, Zpos (Psucc p) = Zsucc (Zpos p). +Proof. +intro; rewrite Pplus_one_succ_r; unfold Zsucc in |- *; simpl in |- *; + trivial with arith. +Qed. + +(** successor and predecessor are inverse functions *) + +Theorem Zsucc_pred : forall n:Z, n = Zsucc (Zpred n). +Proof. +intros n; unfold Zsucc, Zpred in |- *; rewrite <- Zplus_assoc; simpl in |- *; + rewrite Zplus_0_r; trivial with arith. +Qed. + +Hint Immediate Zsucc_pred: zarith. + +Theorem Zpred_succ : forall n:Z, n = Zpred (Zsucc n). +Proof. +intros m; unfold Zpred, Zsucc in |- *; rewrite <- Zplus_assoc; simpl in |- *; + rewrite Zplus_comm; auto with arith. +Qed. + +Theorem Zsucc_inj : forall n m:Z, Zsucc n = Zsucc m -> n = m. +Proof. +intros n m H. +change (Zneg 1 + Zpos 1 + n = Zneg 1 + Zpos 1 + m) in |- *; + do 2 rewrite <- Zplus_assoc; do 2 rewrite (Zplus_comm (Zpos 1)); + unfold Zsucc in H; rewrite H; trivial with arith. +Qed. + +(** Misc properties, usually redundant or non natural *) + +Lemma Zsucc_eq_compat : forall n m:Z, n = m -> Zsucc n = Zsucc m. +Proof. +intros n m H; rewrite H; reflexivity. +Qed. + +Lemma Zsucc_inj_contrapositive : forall n m:Z, n <> m -> Zsucc n <> Zsucc m. +Proof. +unfold not in |- *; intros n m H1 H2; apply H1; apply Zsucc_inj; assumption. +Qed. + +(**********************************************************************) +(** Properties of subtraction on binary integer numbers *) + +Lemma Zminus_0_r : forall n:Z, n - Z0 = n. +Proof. +intro; unfold Zminus in |- *; simpl in |- *; rewrite Zplus_0_r; + trivial with arith. +Qed. + +Lemma Zminus_0_l_reverse : forall n:Z, n = n - Z0. +Proof. +intro; symmetry in |- *; apply Zminus_0_r. +Qed. + +Lemma Zminus_diag : forall n:Z, n - n = Z0. +Proof. +intro; unfold Zminus in |- *; rewrite Zplus_opp_r; trivial with arith. +Qed. + +Lemma Zminus_diag_reverse : forall n:Z, Z0 = n - n. +Proof. +intro; symmetry in |- *; apply Zminus_diag. +Qed. + +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; + trivial with arith. +Qed. + +Lemma Zminus_plus : forall n m:Z, n + m - n = m. +Proof. +intros n m; unfold Zminus in |- *; rewrite (Zplus_comm n m); + rewrite <- Zplus_assoc; rewrite Zplus_opp_r; apply Zplus_0_r. +Qed. + +Lemma Zplus_minus : forall n m:Z, n + (m - n) = m. +Proof. +unfold Zminus in |- *; intros n m; rewrite Zplus_permute; rewrite Zplus_opp_r; + apply Zplus_0_r. +Qed. + +Lemma Zminus_succ_l : forall n m:Z, Zsucc (n - m) = Zsucc n - m. +Proof. +intros n m; unfold Zminus, Zsucc in |- *; rewrite (Zplus_comm n (- m)); + rewrite <- Zplus_assoc; apply Zplus_comm. +Qed. + +Lemma Zminus_plus_simpl_l : forall n m p:Z, p + n - (p + m) = n - m. +Proof. +intros n m p; unfold Zminus in |- *; rewrite Zopp_plus_distr; + rewrite Zplus_assoc; rewrite (Zplus_comm p); rewrite <- (Zplus_assoc n p); + rewrite Zplus_opp_r; rewrite Zplus_0_r; trivial with arith. +Qed. + +Lemma Zminus_plus_simpl_l_reverse : forall n m p:Z, n - m = p + n - (p + m). +Proof. +intros; symmetry in |- *; apply Zminus_plus_simpl_l. +Qed. + +Lemma Zminus_plus_simpl_r : forall n m p:Z, n + p - (m + p) = n - m. +intros x y n. +unfold Zminus in |- *. +rewrite Zopp_plus_distr. +rewrite (Zplus_comm (- y) (- n)). +rewrite Zplus_assoc. +rewrite <- (Zplus_assoc x n (- n)). +rewrite (Zplus_opp_r n). +rewrite <- Zplus_0_r_reverse. +reflexivity. +Qed. + +(** Misc redundant properties *) + + +Lemma Zeq_minus : forall n m:Z, n = m -> n - m = Z0. +Proof. +intros x y H; rewrite H; symmetry in |- *; apply Zminus_diag_reverse. +Qed. + +Lemma Zminus_eq : forall n m:Z, n - m = Z0 -> n = m. +Proof. +intros x y H; rewrite <- (Zplus_minus y x); rewrite H; apply Zplus_0_r. +Qed. + + +(**********************************************************************) +(** Properties of multiplication on binary integer numbers *) + +(** One is neutral for multiplication *) + +Theorem Zmult_1_l : forall n:Z, Zpos 1 * n = n. +Proof. +intro x; destruct x; reflexivity. +Qed. + +Theorem Zmult_1_r : forall n:Z, n * Zpos 1 = n. +Proof. +intro x; destruct x; simpl in |- *; try rewrite Pmult_1_r; reflexivity. +Qed. + +(** Zero property of multiplication *) + +Theorem Zmult_0_l : forall n:Z, Z0 * n = Z0. +Proof. +intro x; destruct x; reflexivity. +Qed. + +Theorem Zmult_0_r : forall n:Z, n * Z0 = Z0. +Proof. +intro x; destruct x; reflexivity. +Qed. + +Hint Local Resolve Zmult_0_l Zmult_0_r. + +Lemma Zmult_0_r_reverse : forall n:Z, Z0 = n * Z0. +Proof. +intro x; destruct x; reflexivity. +Qed. + +(** Commutativity of multiplication *) + +Theorem Zmult_comm : forall n m:Z, n * m = m * n. +Proof. +intros x y; destruct x as [| p| p]; destruct y as [| q| q]; simpl in |- *; + try rewrite (Pmult_comm p q); reflexivity. +Qed. + +(** Associativity of multiplication *) + +Theorem Zmult_assoc : forall n m p:Z, n * (m * p) = n * m * p. +Proof. +intros x y z; destruct x; destruct y; destruct z; simpl in |- *; + try rewrite Pmult_assoc; reflexivity. +Qed. + +Lemma Zmult_assoc_reverse : forall n m p:Z, n * m * p = n * (m * p). +Proof. +intros n m p; rewrite Zmult_assoc; trivial with arith. +Qed. + +(** Associativity mixed with commutativity *) + +Theorem Zmult_permute : forall n m p:Z, n * (m * p) = m * (n * p). +Proof. +intros x y z; rewrite (Zmult_assoc y x z); rewrite (Zmult_comm y x). +apply Zmult_assoc. +Qed. + +(** Z is integral *) + +Theorem Zmult_integral_l : forall n m:Z, n <> Z0 -> m * n = Z0 -> m = Z0. +Proof. +intros x y; destruct x as [| p| p]. + intro H; absurd (Z0 = Z0); trivial. + intros _ H; destruct y as [| q| q]; reflexivity || discriminate. + intros _ H; destruct y as [| q| q]; reflexivity || discriminate. +Qed. + + +Theorem Zmult_integral : forall n m:Z, n * m = Z0 -> n = Z0 \/ m = Z0. +Proof. +intros x y; destruct x; destruct y; auto; simpl in |- *; intro H; + discriminate H. +Qed. + + +Lemma Zmult_1_inversion_l : + forall n m:Z, n * m = Zpos 1 -> n = Zpos 1 \/ n = Zneg 1. +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); + reflexivity). +Qed. + +(** Multiplication and Opposite *) + +Theorem Zopp_mult_distr_l : forall n m:Z, - (n * m) = - n * m. +Proof. +intros x y; destruct x; destruct y; reflexivity. +Qed. + +Theorem Zopp_mult_distr_r : forall n m:Z, - (n * m) = n * - m. +intros x y; rewrite (Zmult_comm x y); rewrite Zopp_mult_distr_l; + apply Zmult_comm. +Qed. + +Lemma Zopp_mult_distr_l_reverse : forall n m:Z, - n * m = - (n * m). +Proof. +intros x y; symmetry in |- *; apply Zopp_mult_distr_l. +Qed. + +Theorem Zmult_opp_comm : forall n m:Z, - n * m = n * - m. +intros x y; rewrite Zopp_mult_distr_l_reverse; rewrite Zopp_mult_distr_r; + trivial with arith. +Qed. + +Theorem Zmult_opp_opp : forall n m:Z, - n * - m = n * m. +Proof. +intros x y; destruct x; destruct y; reflexivity. +Qed. + +Theorem Zopp_eq_mult_neg_1 : forall n:Z, - n = n * Zneg 1. +intro x; induction x; intros; rewrite Zmult_comm; auto with arith. +Qed. + +(** Distributivity of multiplication over addition *) + +Lemma weak_Zmult_plus_distr_r : + forall (p:positive) (n m:Z), Zpos p * (n + m) = Zpos p * n + Zpos p * m. +Proof. +intros x y' z'; case y'; case z'; auto with arith; intros y z; + (simpl in |- *; rewrite Pmult_plus_distr_l; trivial with arith) || + (simpl in |- *; ElimPcompare z y; intros E0; rewrite E0; + [ rewrite (Pcompare_Eq_eq z y E0); rewrite (Pcompare_refl (x * y)); + trivial with arith + | cut ((x * z ?= x * y)%positive Eq = Lt); + [ 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); + 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); + intros h H1; rewrite H1; apply mult_S_lt_compat_l; + exact (nat_of_P_gt_Gt_compare_morphism z y E0) ] ]). +Qed. + +Theorem Zmult_plus_distr_r : forall n m p:Z, n * (m + p) = n * m + n * p. +Proof. +intros x y z; case x; + [ auto with arith + | intros x'; apply weak_Zmult_plus_distr_r + | intros p; apply Zopp_inj; rewrite Zopp_plus_distr; + do 3 rewrite <- Zopp_mult_distr_l_reverse; rewrite Zopp_neg; + apply weak_Zmult_plus_distr_r ]. +Qed. + +Theorem Zmult_plus_distr_l : forall n m p:Z, (n + m) * p = n * p + m * p. +Proof. +intros n m p; rewrite Zmult_comm; rewrite Zmult_plus_distr_r; + do 2 rewrite (Zmult_comm p); trivial with arith. +Qed. + +(** Distributivity of multiplication over subtraction *) + +Lemma Zmult_minus_distr_r : forall n m p:Z, (n - m) * p = n * p - m * p. +Proof. +intros x y z; unfold Zminus in |- *. +rewrite <- Zopp_mult_distr_l_reverse. +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)). +rewrite (Zmult_comm z x). +rewrite (Zmult_comm z y). +apply Zmult_minus_distr_r. +Qed. + +(** Simplification of multiplication for non-zero integers *) + +Lemma Zmult_reg_l : forall n m p:Z, p <> Z0 -> p * n = p * m -> n = m. +Proof. +intros x y z H H0. +generalize (Zeq_minus _ _ H0). +intro. +apply Zminus_eq. +rewrite <- Zmult_minus_distr_l in H1. +clear H0; destruct (Zmult_integral _ _ H1). +contradiction. +trivial. +Qed. + +Lemma Zmult_reg_r : forall n m p:Z, p <> Z0 -> n * p = m * p -> n = m. +Proof. +intros x y z Hz. +rewrite (Zmult_comm x z). +rewrite (Zmult_comm y z). +intro; apply Zmult_reg_l with z; assumption. +Qed. + +(** Addition and multiplication by 2 *) + +Lemma Zplus_diag_eq_mult_2 : forall n:Z, n + n = n * Zpos 2. +Proof. +intros x; pattern x at 1 2 in |- *; rewrite <- (Zmult_1_r x); + rewrite <- Zmult_plus_distr_r; reflexivity. +Qed. + +(** Multiplication and successor *) + +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; + trivial with arith. +Qed. + +Lemma Zmult_succ_r_reverse : forall n m:Z, n * m + n = n * Zsucc m. +Proof. +intros; symmetry in |- *; apply Zmult_succ_r. +Qed. + +Lemma Zmult_succ_l : forall n m:Z, Zsucc n * m = n * m + m. +Proof. +intros n m; unfold Zsucc in |- *; rewrite Zmult_plus_distr_l; + rewrite Zmult_1_l; trivial with arith. +Qed. + +Lemma Zmult_succ_l_reverse : forall n m:Z, n * m + m = Zsucc n * m. +Proof. +intros; symmetry in |- *; apply Zmult_succ_l. +Qed. + +(** Misc redundant properties *) + +Lemma Z_eq_mult : forall n m:Z, m = Z0 -> m * n = Z0. +intros x y H; rewrite H; auto with arith. +Qed. + +(**********************************************************************) +(** Relating binary positive numbers and binary integers *) + +Lemma Zpos_xI : forall p:positive, Zpos (xI p) = Zpos 2 * Zpos p + Zpos 1. +Proof. +intro; apply refl_equal. +Qed. + +Lemma Zpos_xO : forall p:positive, Zpos (xO p) = Zpos 2 * Zpos p. +Proof. +intro; apply refl_equal. +Qed. + +Lemma Zneg_xI : forall p:positive, Zneg (xI p) = Zpos 2 * Zneg p - Zpos 1. +Proof. +intro; apply refl_equal. +Qed. + +Lemma Zneg_xO : forall p:positive, Zneg (xO p) = Zpos 2 * Zneg p. +Proof. +reflexivity. +Qed. + +Lemma Zpos_plus_distr : forall p q:positive, Zpos (p + q) = Zpos p + Zpos q. +Proof. +intros p p'; destruct p; + [ destruct p' as [p0| p0| ] + | destruct p' as [p0| p0| ] + | destruct p' as [p| p| ] ]; reflexivity. +Qed. + +Lemma Zneg_plus_distr : forall p q:positive, Zneg (p + q) = Zneg p + Zneg q. +Proof. +intros p p'; destruct p; + [ destruct p' as [p0| p0| ] + | destruct p' as [p0| p0| ] + | destruct p' as [p| p| ] ]; reflexivity. +Qed. + +(**********************************************************************) +(** Order relations *) + +Definition Zlt (x y:Z) := (x ?= y) = Lt. +Definition Zgt (x y:Z) := (x ?= y) = Gt. +Definition Zle (x y:Z) := (x ?= y) <> Gt. +Definition Zge (x y:Z) := (x ?= y) <> Lt. +Definition Zne (x y:Z) := x <> y. + +Infix "<=" := Zle : Z_scope. +Infix "<" := Zlt : Z_scope. +Infix ">=" := Zge : Z_scope. +Infix ">" := Zgt : Z_scope. + +Notation "x <= y <= z" := (x <= y /\ y <= z) : Z_scope. +Notation "x <= y < z" := (x <= y /\ y < z) : Z_scope. +Notation "x < y < z" := (x < y /\ y < z) : Z_scope. +Notation "x < y <= z" := (x < y /\ y <= z) : Z_scope. + +(**********************************************************************) +(** Absolute value on integers *) + +Definition Zabs_nat (x:Z) : nat := + match x with + | Z0 => 0%nat + | Zpos p => nat_of_P p + | Zneg p => nat_of_P p + end. + +Definition Zabs (z:Z) : Z := + match z with + | Z0 => Z0 + | Zpos p => Zpos p + | Zneg p => Zpos p + end. + +(**********************************************************************) +(** From [nat] to [Z] *) + +Definition Z_of_nat (x:nat) := + match x with + | O => Z0 + | S y => Zpos (P_of_succ_nat y) + end. + +Require Import BinNat. + +Definition Zabs_N (z:Z) := + match z with + | Z0 => 0%N + | Zpos p => Npos p + | Zneg p => Npos p + end. + +Definition Z_of_N (x:N) := match x with + | N0 => Z0 + | Npos p => Zpos p + end.
\ No newline at end of file diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v new file mode 100644 index 00000000..069ddd42 --- /dev/null +++ b/theories/ZArith/Wf_Z.v @@ -0,0 +1,204 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(*i $Id: Wf_Z.v,v 1.20.2.1 2004/07/16 19:31:20 herbelin Exp $ i*) + +Require Import BinInt. +Require Import Zcompare. +Require Import Zorder. +Require Import Znat. +Require Import Zmisc. +Require Import Wf_nat. +Open Local Scope Z_scope. + +(** Our purpose is to write an induction shema for {0,1,2,...} + similar to the [nat] schema (Theorem [Natlike_rec]). For that the + following implications will be used : +<< + (n:nat)(Q n)==(n:nat)(P (inject_nat n)) ===> (x:Z)`x > 0) -> (P x) + + /\ + || + || + + (Q O) (n:nat)(Q n)->(Q (S n)) <=== (P 0) (x:Z) (P x) -> (P (Zs x)) + + <=== (inject_nat (S n))=(Zs (inject_nat n)) + + <=== inject_nat_complete +>> + Then the diagram will be closed and the theorem proved. *) + +Lemma Z_of_nat_complete : + forall x:Z, 0 <= x -> exists n : nat, x = Z_of_nat n. +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); + intro Hx0; rewrite <- H0 in Hx0; apply f_equal with (f := Zpos); + apply nat_of_P_inj; auto with arith + | absurd (0 <= Zneg p); + [ unfold Zle in |- *; simpl in |- *; do 2 unfold not in |- *; + auto with arith + | assumption ] ]. +Qed. + +Lemma ZL4_inf : forall y:positive, {h : nat | nat_of_P y = S h}. +intro y; induction y as [p H| p H1| ]; + [ elim H; intros x H1; exists (S x + S x)%nat; unfold nat_of_P in |- *; + simpl in |- *; rewrite ZL0; rewrite Pmult_nat_r_plus_morphism; + unfold nat_of_P in H1; rewrite H1; auto with arith + | elim H1; intros x H2; exists (x + S x)%nat; unfold nat_of_P in |- *; + simpl in |- *; rewrite ZL0; rewrite Pmult_nat_r_plus_morphism; + unfold nat_of_P in H2; rewrite H2; auto with arith + | exists 0%nat; auto with arith ]. +Qed. + +Lemma Z_of_nat_complete_inf : + forall x:Z, 0 <= x -> {n : nat | x = Z_of_nat n}. +intro x; destruct x; intros; + [ exists 0%nat; auto with arith + | specialize (ZL4_inf p); intros Hp; elim Hp; intros x0 H0; exists (S x0); + intros; simpl in |- *; specialize (nat_of_P_o_P_of_succ_nat_eq_succ x0); + intro Hx0; rewrite <- H0 in Hx0; apply f_equal with (f := Zpos); + apply nat_of_P_inj; auto with arith + | absurd (0 <= Zneg p); + [ unfold Zle in |- *; simpl in |- *; do 2 unfold not in |- *; + auto with arith + | assumption ] ]. +Qed. + +Lemma Z_of_nat_prop : + forall P:Z -> Prop, + (forall n:nat, P (Z_of_nat n)) -> forall x:Z, 0 <= x -> P x. +intros P H x H0. +specialize (Z_of_nat_complete x H0). +intros Hn; elim Hn; intros. +rewrite H1; apply H. +Qed. + +Lemma Z_of_nat_set : + forall P:Z -> Set, + (forall n:nat, P (Z_of_nat n)) -> forall x:Z, 0 <= x -> P x. +intros P H x H0. +specialize (Z_of_nat_complete_inf x H0). +intros Hn; elim Hn; intros. +rewrite p; apply H. +Qed. + +Lemma natlike_ind : + forall P:Z -> Prop, + P 0 -> + (forall x:Z, 0 <= x -> P x -> P (Zsucc x)) -> forall x:Z, 0 <= x -> P x. +intros P H H0 x H1; apply Z_of_nat_prop; + [ simple induction n; + [ simpl in |- *; assumption + | intros; rewrite (inj_S n0); exact (H0 (Z_of_nat n0) (Zle_0_nat n0) H2) ] + | assumption ]. +Qed. + +Lemma natlike_rec : + forall P:Z -> Set, + P 0 -> + (forall x:Z, 0 <= x -> P x -> P (Zsucc x)) -> forall x:Z, 0 <= x -> P x. +intros P H H0 x H1; apply Z_of_nat_set; + [ simple induction n; + [ simpl in |- *; assumption + | intros; rewrite (inj_S n0); exact (H0 (Z_of_nat n0) (Zle_0_nat n0) H2) ] + | assumption ]. +Qed. + +Section Efficient_Rec. + +(** [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 + (f := + fun z => + match z with + | Zpos p => nat_of_P p + | Z0 => 0%nat + | Zneg _ => 0%nat + end) in *. +apply well_founded_lt_compat with f. +unfold R, f in |- *; clear f R. +intros x y; case x; intros; elim H; clear H. +case y; intros; apply lt_O_nat_of_P || inversion H0. +case y; intros; apply nat_of_P_lt_Lt_compare_morphism || inversion H0; auto. +intros; elim H; auto. +Qed. + +Lemma natlike_rec2 : + forall P:Z -> Type, + P 0 -> + (forall z:Z, 0 <= z -> P z -> P (Zsucc z)) -> forall z:Z, 0 <= z -> P z. +Proof. +intros P Ho Hrec z; pattern z in |- *; + apply (well_founded_induction_type R_wf). +intro x; case x. +trivial. +intros. +assert (0 <= Zpred (Zpos p)). +apply Zorder.Zlt_0_le_0_pred; unfold Zlt in |- *; simpl in |- *; trivial. +rewrite Zsucc_pred. +apply Hrec. +auto. +apply X; auto; unfold R in |- *; intuition; apply Zlt_pred. +intros; elim H; simpl in |- *; trivial. +Qed. + +(** A variant of the previous using [Zpred] instead of [Zs]. *) + +Lemma natlike_rec3 : + forall P:Z -> Type, + P 0 -> + (forall z:Z, 0 < z -> P (Zpred z) -> P z) -> forall z:Z, 0 <= z -> P z. +Proof. +intros P Ho Hrec z; pattern z in |- *; + apply (well_founded_induction_type R_wf). +intro x; case x. +trivial. +intros; apply Hrec. +unfold Zlt in |- *; trivial. +assert (0 <= Zpred (Zpos p)). +apply Zorder.Zlt_0_le_0_pred; unfold Zlt in |- *; simpl in |- *; trivial. +apply X; auto; unfold R in |- *; intuition; apply Zlt_pred. +intros; elim H; simpl in |- *; trivial. +Qed. + +(** A more general induction principal using [Zlt]. *) + +Lemma Z_lt_rec : + forall P:Z -> Type, + (forall x:Z, (forall y:Z, 0 <= y < x -> P y) -> P x) -> + forall x:Z, 0 <= x -> P x. +Proof. +intros P Hrec z; pattern z in |- *; apply (well_founded_induction_type R_wf). +intro x; case x; intros. +apply Hrec; intros. +assert (H2 : 0 < 0). + apply Zle_lt_trans with y; intuition. +inversion H2. +firstorder. +unfold Zle, Zcompare in H; elim H; auto. +Defined. + +Lemma Z_lt_induction : + forall P:Z -> Prop, + (forall x:Z, (forall y:Z, 0 <= y < x -> P y) -> P x) -> + forall x:Z, 0 <= x -> P x. +Proof. +exact Z_lt_rec. +Qed. + +End Efficient_Rec. diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v new file mode 100644 index 00000000..78295591 --- /dev/null +++ b/theories/ZArith/ZArith.v @@ -0,0 +1,22 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(*i $Id: ZArith.v,v 1.5.2.1 2004/07/16 19:31:20 herbelin Exp $ i*) + +(** Library for manipulating integers based on binary encoding *) + +Require Export ZArith_base. + +(** Extra modules using [Omega] or [Ring]. *) + +Require Export Zcomplements. +Require Export Zsqrt. +Require Export Zpower. +Require Export Zdiv. +Require Export Zlogarithm. +Require Export Zbool.
\ No newline at end of file diff --git a/theories/ZArith/ZArith_base.v b/theories/ZArith/ZArith_base.v new file mode 100644 index 00000000..694e071e --- /dev/null +++ b/theories/ZArith/ZArith_base.v @@ -0,0 +1,34 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(* $Id: ZArith_base.v,v 1.5.2.1 2004/07/16 19:31:20 herbelin Exp $ *) + +(** Library for manipulating integers based on binary encoding. + These are the basic modules, required by [Omega] and [Ring] for instance. + The full library is [ZArith]. *) + +Require Export BinPos. +Require Export BinNat. +Require Export BinInt. +Require Export Zcompare. +Require Export Zorder. +Require Export Zeven. +Require Export Zmin. +Require Export Zabs. +Require Export Znat. +Require Export auxiliary. +Require Export ZArith_dec. +Require Export Zbool. +Require Export Zmisc. +Require Export Wf_Z. + +Hint Resolve Zle_refl Zplus_comm Zplus_assoc Zmult_comm Zmult_assoc Zplus_0_l + Zplus_0_r Zmult_1_l Zplus_opp_l Zplus_opp_r Zmult_plus_distr_l + Zmult_plus_distr_r: zarith. + +Require Export Zhints.
\ No newline at end of file diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v new file mode 100644 index 00000000..dbd0df6c --- /dev/null +++ b/theories/ZArith/ZArith_dec.v @@ -0,0 +1,226 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(*i $Id: ZArith_dec.v,v 1.11.2.1 2004/07/16 19:31:20 herbelin Exp $ i*) + +Require Import Sumbool. + +Require Import BinInt. +Require Import Zorder. +Require Import Zcompare. +Open Local Scope Z_scope. + +Lemma Dcompare_inf : forall r:comparison, {r = Eq} + {r = Lt} + {r = Gt}. +Proof. +simple induction r; auto with arith. +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. +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. + +(** Decidability of order on binary integers *) + +Definition Z_lt_dec : {x < y} + {~ x < y}. +Proof. +unfold Zlt in |- *. +apply Zcompare_rec with (n := x) (m := y); intro H. +right. rewrite H. discriminate. +left; assumption. +right. rewrite H. discriminate. +Defined. + +Definition Z_le_dec : {x <= y} + {~ x <= y}. +Proof. +unfold Zle in |- *. +apply Zcompare_rec with (n := x) (m := y); intro H. +left. rewrite H. discriminate. +left. rewrite H. discriminate. +right. tauto. +Defined. + +Definition Z_gt_dec : {x > y} + {~ x > y}. +Proof. +unfold Zgt in |- *. +apply Zcompare_rec with (n := x) (m := y); intro H. +right. rewrite H. discriminate. +right. rewrite H. discriminate. +left; assumption. +Defined. + +Definition Z_ge_dec : {x >= y} + {~ x >= y}. +Proof. +unfold Zge in |- *. +apply Zcompare_rec with (n := x) (m := y); intro H. +left. rewrite H. discriminate. +right. tauto. +left. rewrite H. discriminate. +Defined. + +Definition Z_lt_ge_dec : {x < y} + {x >= y}. +Proof. +exact Z_lt_dec. +Defined. + +Lemma Z_lt_le_dec : {x < y} + {y <= x}. +Proof. +intros. +elim Z_lt_ge_dec. +intros; left; assumption. +intros; right; apply Zge_le; assumption. +Qed. + +Definition Z_le_gt_dec : {x <= y} + {x > y}. +Proof. +elim Z_le_dec; auto with arith. +intro. right. apply Znot_le_gt; auto with arith. +Defined. + +Definition Z_gt_le_dec : {x > y} + {x <= y}. +Proof. +exact Z_gt_dec. +Defined. + +Definition Z_ge_lt_dec : {x >= y} + {x < y}. +Proof. +elim Z_ge_dec; auto with arith. +intro. right. apply Znot_ge_lt; auto with arith. +Defined. + +Definition Z_le_lt_eq_dec : x <= y -> {x < y} + {x = y}. +Proof. +intro H. +apply Zcompare_rec with (n := x) (m := y). +intro. right. elim (Zcompare_Eq_iff_eq x y); auto with arith. +intro. left. elim (Zcompare_Eq_iff_eq x y); auto with arith. +intro H1. absurd (x > y); auto with arith. +Defined. + +End decidability. + +(** Cotransitivity of order on binary integers *) + +Lemma Zlt_cotrans : forall n m:Z, n < m -> forall p:Z, {n < p} + {p < m}. +Proof. + intros x y H z. + case (Z_lt_ge_dec x z). + intro. + left. + assumption. + intro. + right. + apply Zle_lt_trans with (m := x). + apply Zge_le. + assumption. + assumption. +Defined. + +Lemma Zlt_cotrans_pos : forall n m:Z, 0 < n + m -> {0 < n} + {0 < m}. +Proof. + intros x y H. + case (Zlt_cotrans 0 (x + y) H x). + intro. + left. + assumption. + intro. + right. + apply Zplus_lt_reg_l with (p := x). + rewrite Zplus_0_r. + assumption. +Defined. + +Lemma Zlt_cotrans_neg : forall n m:Z, n + m < 0 -> {n < 0} + {m < 0}. +Proof. + intros x y H; case (Zlt_cotrans (x + y) 0 H x); intro Hxy; + [ right; apply Zplus_lt_reg_l with (p := x); rewrite Zplus_0_r | left ]; + assumption. +Defined. + +Lemma not_Zeq_inf : forall n m:Z, n <> m -> {n < m} + {m < n}. +Proof. + intros x y H. + case Z_lt_ge_dec with x y. + intro. + left. + assumption. + intro H0. + generalize (Zge_le _ _ H0). + intro. + case (Z_le_lt_eq_dec _ _ H1). + intro. + right. + assumption. + intro. + apply False_rec. + apply H. + symmetry in |- *. + assumption. +Defined. + +Lemma Z_dec : forall n m:Z, {n < m} + {n > m} + {n = m}. +Proof. + intros x y. + case (Z_lt_ge_dec x y). + intro H. + left. + left. + assumption. + intro H. + generalize (Zge_le _ _ H). + intro H0. + case (Z_le_lt_eq_dec y x H0). + intro H1. + left. + right. + apply Zlt_gt. + assumption. + intro. + right. + symmetry in |- *. + assumption. +Defined. + + +Lemma Z_dec' : forall n m:Z, {n < m} + {m < n} + {n = m}. +Proof. + intros x y. + case (Z_eq_dec x y); intro H; + [ right; assumption | left; apply (not_Zeq_inf _ _ H) ]. +Defined. + + + +Definition 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). + +Definition Z_noteq_dec (x y:Z) := sumbool_not _ _ (Z_eq_dec x y).
\ No newline at end of file diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v new file mode 100644 index 00000000..90e4c2a4 --- /dev/null +++ b/theories/ZArith/Zabs.v @@ -0,0 +1,128 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) +(*i $Id: Zabs.v,v 1.4.2.1 2004/07/16 19:31:21 herbelin Exp $ i*) + +(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *) + +Require Import Arith. +Require Import BinPos. +Require Import BinInt. +Require Import Zorder. +Require Import ZArith_dec. + +Open Local Scope Z_scope. + +(**********************************************************************) +(** Properties of absolute value *) + +Lemma Zabs_eq : forall n:Z, 0 <= n -> Zabs n = n. +intro x; destruct x; auto with arith. +compute in |- *; intros; absurd (Gt = Gt); trivial with arith. +Qed. + +Lemma Zabs_non_eq : forall n:Z, n <= 0 -> Zabs n = - n. +Proof. +intro x; destruct x; auto with arith. +compute in |- *; intros; absurd (Gt = Gt); trivial with arith. +Qed. + +Theorem Zabs_Zopp : forall n:Z, Zabs (- n) = Zabs n. +Proof. +intros z; case z; simpl in |- *; auto. +Qed. + +(** Proving a property of the absolute value by cases *) + +Lemma Zabs_ind : + forall (P:Z -> Prop) (n:Z), + (n >= 0 -> P n) -> (n <= 0 -> P (- n)) -> P (Zabs n). +Proof. +intros P x H H0; elim (Z_lt_ge_dec x 0); intro. +assert (x <= 0). apply Zlt_le_weak; assumption. +rewrite Zabs_non_eq. apply H0. assumption. assumption. +rewrite Zabs_eq. apply H; assumption. apply Zge_le. assumption. +Qed. + +Theorem Zabs_intro : forall P (n:Z), P (- n) -> P n -> P (Zabs n). +intros P z; case z; simpl in |- *; auto. +Qed. + +Definition Zabs_dec : forall x:Z, {x = Zabs x} + {x = - Zabs x}. +Proof. +intro x; destruct x; auto with arith. +Defined. + +Lemma Zabs_pos : forall n:Z, 0 <= Zabs n. +intro x; destruct x; auto with arith; compute in |- *; intros H; inversion H. +Qed. + +Theorem Zabs_eq_case : forall n m:Z, Zabs n = Zabs m -> n = m \/ n = - m. +Proof. +intros z1 z2; case z1; case z2; simpl in |- *; auto; + try (intros; discriminate); intros p1 p2 H1; injection H1; + (intros H2; rewrite H2); auto. +Qed. + +(** Triangular inequality *) + +Hint Local Resolve Zle_neg_pos: zarith. + +Theorem Zabs_triangle : forall n m:Z, Zabs (n + m) <= Zabs n + Zabs m. +Proof. +intros z1 z2; case z1; case z2; try (simpl in |- *; auto with zarith; fail). +intros p1 p2; + apply Zabs_intro with (P := fun x => x <= Zabs (Zpos p2) + Zabs (Zneg p1)); + try rewrite Zopp_plus_distr; auto with zarith. +apply Zplus_le_compat; simpl in |- *; auto with zarith. +apply Zplus_le_compat; simpl in |- *; auto with zarith. +intros p1 p2; + apply Zabs_intro with (P := fun x => x <= Zabs (Zpos p2) + Zabs (Zneg p1)); + try rewrite Zopp_plus_distr; auto with zarith. +apply Zplus_le_compat; simpl in |- *; auto with zarith. +apply Zplus_le_compat; simpl in |- *; auto with zarith. +Qed. + +(** Absolute value and multiplication *) + +Lemma Zsgn_Zabs : forall n:Z, n * Zsgn n = Zabs n. +Proof. +intro x; destruct x; rewrite Zmult_comm; auto with arith. +Qed. + +Lemma Zabs_Zsgn : forall n:Z, Zabs n * Zsgn n = n. +Proof. +intro x; destruct x; rewrite Zmult_comm; auto with arith. +Qed. + +Theorem Zabs_Zmult : forall n m:Z, Zabs (n * m) = Zabs n * Zabs m. +Proof. +intros z1 z2; case z1; case z2; simpl in |- *; auto. +Qed. + +(** absolute value in nat is compatible with order *) + +Lemma Zabs_nat_lt : + forall n m:Z, 0 <= n /\ n < m -> (Zabs_nat n < Zabs_nat m)%nat. +Proof. +intros x y. case x; simpl in |- *. case y; simpl in |- *. + +intro. absurd (0 < 0). compute in |- *. intro H0. discriminate H0. intuition. +intros. elim (ZL4 p). intros. rewrite H0. auto with arith. +intros. elim (ZL4 p). intros. rewrite H0. auto with arith. + +case y; simpl in |- *. +intros. absurd (Zpos p < 0). compute in |- *. intro H0. discriminate H0. intuition. +intros. change (nat_of_P p > nat_of_P p0)%nat in |- *. +apply nat_of_P_gt_Gt_compare_morphism. +elim H; auto with arith. intro. exact (ZC2 p0 p). + +intros. absurd (Zpos p0 < Zneg p). +compute in |- *. intro H0. discriminate H0. intuition. + +intros. absurd (0 <= Zneg p). compute in |- *. auto with arith. intuition. +Qed.
\ No newline at end of file diff --git a/theories/ZArith/Zbinary.v b/theories/ZArith/Zbinary.v new file mode 100644 index 00000000..fa5f00dc --- /dev/null +++ b/theories/ZArith/Zbinary.v @@ -0,0 +1,426 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(*i $Id: Zbinary.v,v 1.6.2.1 2004/07/16 19:31:21 herbelin Exp $ i*) + +(** Bit vectors interpreted as integers. + Contribution by Jean Duprat (ENS Lyon). *) + +Require Import Bvector. +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`} +*) + + +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. +*) + +Definition bit_value (b:bool) : Z := + match b with + | 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. + +Lemma two_compl_value : forall n:nat, Bvector (S n) -> Z. +Proof. + simple induction n; intros. + inversion H. + exact (- bit_value a)%Z. + + inversion H0. + exact (bit_value a + 2 * H H2)%Z. +Defined. + +(* +Coq < Eval Compute in (binary_value (3) (Bcons true (2) (Bcons false (1) (Bcons true (0) Bnil)))). + = `5` + : Z +*) + +(* +Coq < Eval Compute in (two_compl_value (3) (Bcons true (3) (Bcons false (2) (Bcons true (1) (Bcons true (0) Bnil))))). + = `-3` + : Z +*) + +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. +*) + +Definition Zmod2 (z:Z) := + match z with + | Z0 => 0%Z + | Zpos p => match p with + | xI q => Zpos q + | xO q => Zpos q + | xH => 0%Z + end + | Zneg p => + match p with + | xI q => (Zneg q - 1)%Z + | xO q => Zneg q + | xH => (-1)%Z + end + end. + + +Lemma Zmod2_twice : + forall z:Z, z = (2 * Zmod2 z + bit_value (Zeven.Zodd_bool z))%Z. +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. + +Lemma Z_to_binary : forall n:nat, Z -> Bvector n. +Proof. + simple induction n; intros. + exact Bnil. + + exact (Bcons (Zeven.Zodd_bool H0) n0 (H (Zeven.Zdiv2 H0))). +Defined. + +(* +Eval Compute in (Z_to_binary (5) `5`). + = (Vcons bool true (4) + (Vcons bool false (3) + (Vcons bool true (2) + (Vcons bool false (1) (Vcons bool false (0) (Vnil bool)))))) + : (Bvector (5)) +*) + +Lemma Z_to_two_compl : forall n:nat, Z -> Bvector (S n). +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. + +(* +Eval Compute in (Z_to_two_compl (3) `0`). + = (Vcons bool false (3) + (Vcons bool false (2) + (Vcons bool false (1) (Vcons bool false (0) (Vnil bool))))) + : (vector bool (4)) + +Eval Compute in (Z_to_two_compl (3) `5`). + = (Vcons bool true (3) + (Vcons bool false (2) + (Vcons bool true (1) (Vcons bool false (0) (Vnil bool))))) + : (vector bool (4)) + +Eval Compute in (Z_to_two_compl (3) `-5`). + = (Vcons bool true (3) + (Vcons bool true (2) + (Vcons bool false (1) (Vcons bool true (0) (Vnil bool))))) + : (vector bool (4)) +*) + +End ENCODING_VALUE. + +Section Z_BRIC_A_BRAC. + +(* +Bibliotheque de lemmes utiles dans la section suivante. +Utilise largement ZArith. +Meriterait d'etre reecrite. +*) + +Lemma binary_value_Sn : + forall (n:nat) (b:bool) (bv:Bvector n), + binary_value (S n) (Vcons bool b n bv) = + (bit_value b + 2 * binary_value n bv)%Z. +Proof. + intros; auto. +Qed. + +Lemma Z_to_binary_Sn : + forall (n:nat) (b:bool) (z:Z), + (z >= 0)%Z -> + Z_to_binary (S n) (bit_value b + 2 * z) = Bcons b n (Z_to_binary n z). +Proof. + destruct b; destruct z; simpl in |- *; auto. + intro H; elim H; trivial. +Qed. + +Lemma binary_value_pos : + forall (n:nat) (bv:Bvector n), (binary_value n bv >= 0)%Z. +Proof. + induction bv as [| a n v IHbv]; simpl in |- *. + omega. + + destruct a; destruct (binary_value n v); simpl in |- *; auto. + auto with zarith. +Qed. + + +Lemma two_compl_value_Sn : + forall (n:nat) (bv:Bvector (S n)) (b:bool), + two_compl_value (S n) (Bcons b (S n) bv) = + (bit_value b + 2 * two_compl_value n bv)%Z. +Proof. + intros; auto. +Qed. + +Lemma Z_to_two_compl_Sn : + forall (n:nat) (b:bool) (z:Z), + Z_to_two_compl (S n) (bit_value b + 2 * z) = + Bcons b (S n) (Z_to_two_compl n z). +Proof. + destruct b; destruct z as [| p| p]; auto. + destruct p as [p| p| ]; auto. + destruct p as [p| p| ]; simpl in |- *; auto. + intros; rewrite (Psucc_o_double_minus_one_eq_xO p); trivial. +Qed. + +Lemma Z_to_binary_Sn_z : + forall (n:nat) (z:Z), + Z_to_binary (S n) z = + Bcons (Zeven.Zodd_bool z) n (Z_to_binary n (Zeven.Zdiv2 z)). +Proof. + intros; auto. +Qed. + +Lemma Z_div2_value : + forall z:Z, + (z >= 0)%Z -> (bit_value (Zeven.Zodd_bool z) + 2 * Zeven.Zdiv2 z)%Z = z. +Proof. + destruct z as [| p| p]; auto. + destruct p; auto. + intro H; elim H; trivial. +Qed. + +Lemma Pdiv2 : forall z:Z, (z >= 0)%Z -> (Zeven.Zdiv2 z >= 0)%Z. +Proof. + destruct z as [| p| p]. + auto. + + destruct p; auto. + simpl in |- *; intros; omega. + + intro H; elim H; trivial. + +Qed. + +Lemma Zdiv2_two_power_nat : + forall (z:Z) (n:nat), + (z >= 0)%Z -> + (z < two_power_nat (S n))%Z -> (Zeven.Zdiv2 z < two_power_nat n)%Z. +Proof. + 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. + +(* + +Lemma Z_minus_one_or_zero : (z:Z) + `z >= -1` -> + `z < 1` -> + {`z=-1`} + {`z=0`}. +Proof. + NewDestruct z; Auto. + NewDestruct p; Auto. + Tauto. + + Tauto. + + Intros. + Right; Omega. + + NewDestruct p. + Tauto. + + Tauto. + + Intros; Left; Omega. +Save. +*) + +Lemma Z_to_two_compl_Sn_z : + forall (n:nat) (z:Z), + Z_to_two_compl (S n) z = + Bcons (Zeven.Zodd_bool z) (S n) (Z_to_two_compl n (Zmod2 z)). +Proof. + intros; auto. +Qed. + +Lemma Zeven_bit_value : + forall z:Z, Zeven.Zeven z -> bit_value (Zeven.Zodd_bool z) = 0%Z. +Proof. + destruct z; unfold bit_value in |- *; auto. + 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. + destruct z; unfold bit_value in |- *; auto. + intros; elim H. + 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. +Proof. + intros n z; rewrite (two_power_nat_S n). + generalize (Zmod2_twice z). + destruct (Zeven.Zeven_odd_dec z) as [H| H]. + rewrite (Zeven_bit_value z H); intros; omega. + + 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. +Proof. + intros n z; rewrite (two_power_nat_S n). + generalize (Zmod2_twice z). + destruct (Zeven.Zeven_odd_dec z) as [H| H]. + rewrite (Zeven_bit_value z H); intros; omega. + + rewrite (Zodd_bit_value z H); intros; omega. +Qed. + +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. +*) + +Lemma binary_to_Z_to_binary : + forall (n:nat) (bv:Bvector n), Z_to_binary n (binary_value n bv) = bv. +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 -> + (z < two_power_nat n)%Z -> binary_value n (Z_to_binary n z) = z. +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 -> + (z < two_power_nat n)%Z -> two_compl_value n (Z_to_two_compl n z) = z. +Proof. + induction n as [| n IHn]. + unfold two_power_nat, shift_nat in |- *; simpl in |- *; intros. + assert (z = (-1)%Z \/ z = 0%Z). omega. +intuition; subst z; trivial. + + intros; rewrite Z_to_two_compl_Sn_z. + rewrite two_compl_value_Sn. + rewrite IHn. + generalize (Zmod2_twice z); omega. + + apply Zge_minus_two_power_nat_S; auto. + + apply Zlt_two_power_nat_S; auto. +Qed. + +End COHERENT_VALUE. diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v new file mode 100644 index 00000000..bb8abef4 --- /dev/null +++ b/theories/ZArith/Zbool.v @@ -0,0 +1,186 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(* $Id: Zbool.v,v 1.4.2.1 2004/07/16 19:31:21 herbelin Exp $ *) + +Require Import BinInt. +Require Import Zeven. +Require Import Zorder. +Require Import Zcompare. +Require Import ZArith_dec. +Require Import Sumbool. + +(** The decidability of equality and order relations over + type [Z] give some boolean functions with the adequate specification. *) + +Definition Z_lt_ge_bool (x y:Z) := bool_of_sumbool (Z_lt_ge_dec x y). +Definition Z_ge_lt_bool (x y:Z) := bool_of_sumbool (Z_ge_lt_dec x y). + +Definition Z_le_gt_bool (x y:Z) := bool_of_sumbool (Z_le_gt_dec x y). +Definition Z_gt_le_bool (x y:Z) := bool_of_sumbool (Z_gt_le_dec x y). + +Definition Z_eq_bool (x y:Z) := bool_of_sumbool (Z_eq_dec x y). +Definition Z_noteq_bool (x y:Z) := bool_of_sumbool (Z_noteq_dec x y). + +Definition Zeven_odd_bool (x:Z) := bool_of_sumbool (Zeven_odd_dec x). + +(**********************************************************************) +(** Boolean comparisons of binary integers *) + +Definition Zle_bool (x y:Z) := + match (x ?= y)%Z with + | Gt => false + | _ => true + end. +Definition Zge_bool (x y:Z) := + match (x ?= y)%Z with + | Lt => false + | _ => true + end. +Definition Zlt_bool (x y:Z) := + match (x ?= y)%Z with + | Lt => true + | _ => false + end. +Definition Zgt_bool (x y:Z) := + match (x ?= y)%Z with + | Gt => true + | _ => false + end. +Definition Zeq_bool (x y:Z) := + match (x ?= y)%Z with + | Eq => true + | _ => false + end. +Definition Zneq_bool (x y:Z) := + match (x ?= y)%Z with + | Eq => false + | _ => true + end. + +Lemma Zle_cases : + forall n m:Z, if Zle_bool n m then (n <= m)%Z else (n > m)%Z. +Proof. +intros x y; unfold Zle_bool, Zle, Zgt in |- *. +case (x ?= y)%Z; auto; discriminate. +Qed. + +Lemma Zlt_cases : + forall n m:Z, if Zlt_bool n m then (n < m)%Z else (n >= m)%Z. +Proof. +intros x y; unfold Zlt_bool, Zlt, Zge in |- *. +case (x ?= y)%Z; auto; discriminate. +Qed. + +Lemma Zge_cases : + forall n m:Z, if Zge_bool n m then (n >= m)%Z else (n < m)%Z. +Proof. +intros x y; unfold Zge_bool, Zge, Zlt in |- *. +case (x ?= y)%Z; auto; discriminate. +Qed. + +Lemma Zgt_cases : + forall n m:Z, if Zgt_bool n m then (n > m)%Z else (n <= m)%Z. +Proof. +intros x y; unfold Zgt_bool, Zgt, Zle in |- *. +case (x ?= y)%Z; auto; discriminate. +Qed. + +(** Lemmas on [Zle_bool] used in contrib/graphs *) + +Lemma Zle_bool_imp_le : forall n m:Z, Zle_bool n m = true -> (n <= m)%Z. +Proof. + unfold Zle_bool, Zle in |- *. intros x y. unfold not in |- *. + case (x ?= y)%Z; intros; discriminate. +Qed. + +Lemma Zle_imp_le_bool : forall n m:Z, (n <= m)%Z -> Zle_bool n m = true. +Proof. + unfold Zle, Zle_bool in |- *. intros x y. case (x ?= y)%Z; trivial. intro. elim (H (refl_equal _)). +Qed. + +Lemma Zle_bool_refl : forall n:Z, Zle_bool n n = true. +Proof. + intro. apply Zle_imp_le_bool. apply Zeq_le. reflexivity. +Qed. + +Lemma Zle_bool_antisym : + forall n m:Z, Zle_bool n m = true -> Zle_bool m n = true -> n = m. +Proof. + intros. apply Zle_antisym. apply Zle_bool_imp_le. assumption. + apply Zle_bool_imp_le. assumption. +Qed. + +Lemma Zle_bool_trans : + forall n m p:Z, + Zle_bool n m = true -> Zle_bool m p = true -> Zle_bool n p = true. +Proof. + intros x y z; intros. apply Zle_imp_le_bool. apply Zle_trans with (m := y). apply Zle_bool_imp_le. assumption. + apply Zle_bool_imp_le. assumption. +Qed. + +Definition Zle_bool_total : + forall x y:Z, {Zle_bool x y = true} + {Zle_bool y x = true}. +Proof. + intros x y; intros. unfold Zle_bool in |- *. cut ((x ?= y)%Z = Gt <-> (y ?= x)%Z = Lt). + case (x ?= y)%Z. left. reflexivity. + left. reflexivity. + right. rewrite (proj1 H (refl_equal _)). reflexivity. + apply Zcompare_Gt_Lt_antisym. +Defined. + +Lemma Zle_bool_plus_mono : + forall n m p q:Z, + Zle_bool n m = true -> + Zle_bool p q = true -> Zle_bool (n + p) (m + q) = true. +Proof. + intros. apply Zle_imp_le_bool. apply Zplus_le_compat. apply Zle_bool_imp_le. assumption. + apply Zle_bool_imp_le. assumption. +Qed. + +Lemma Zone_pos : Zle_bool 1 0 = false. +Proof. + reflexivity. +Qed. + +Lemma Zone_min_pos : forall n:Z, Zle_bool n 0 = false -> Zle_bool 1 n = true. +Proof. + intros x; intros. apply Zle_imp_le_bool. change (Zsucc 0 <= x)%Z in |- *. apply Zgt_le_succ. generalize H. + unfold Zle_bool, Zgt in |- *. case (x ?= 0)%Z. intro H0. discriminate H0. + intro H0. discriminate H0. + reflexivity. +Qed. + + + Lemma Zle_is_le_bool : forall n m:Z, (n <= m)%Z <-> Zle_bool n m = true. + Proof. + intros. split. intro. apply Zle_imp_le_bool. assumption. + intro. apply Zle_bool_imp_le. assumption. + Qed. + + Lemma Zge_is_le_bool : forall n m:Z, (n >= m)%Z <-> Zle_bool m n = true. + Proof. + intros. split. intro. apply Zle_imp_le_bool. apply Zge_le. assumption. + intro. apply Zle_ge. apply Zle_bool_imp_le. assumption. + Qed. + + Lemma Zlt_is_le_bool : + forall n m:Z, (n < m)%Z <-> Zle_bool n (m - 1) = true. + Proof. + intros x y. split. intro. apply Zle_imp_le_bool. apply Zlt_succ_le. rewrite (Zsucc_pred y) in H. + assumption. + intro. rewrite (Zsucc_pred y). apply Zle_lt_succ. apply Zle_bool_imp_le. assumption. + Qed. + + Lemma Zgt_is_le_bool : + forall n m:Z, (n > m)%Z <-> Zle_bool m (n - 1) = true. + Proof. + intros x y. apply iff_trans with (y < x)%Z. split. exact (Zgt_lt x y). + exact (Zlt_gt y x). + exact (Zlt_is_le_bool y x). + Qed. diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v new file mode 100644 index 00000000..714abfc4 --- /dev/null +++ b/theories/ZArith/Zcompare.v @@ -0,0 +1,501 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(*i $$ i*) + +Require Export BinPos. +Require Export BinInt. +Require Import Lt. +Require Import Gt. +Require Import Plus. +Require Import Mult. + +Open Local Scope Z_scope. + +(**********************************************************************) +(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) +(**********************************************************************) + +(**********************************************************************) +(** Comparison on integers *) + +Lemma Zcompare_refl : forall n:Z, (n ?= n) = Eq. +Proof. +intro x; destruct x as [| p| p]; simpl in |- *; + [ reflexivity | apply Pcompare_refl | rewrite Pcompare_refl; reflexivity ]. +Qed. + +Lemma Zcompare_Eq_eq : forall n m:Z, (n ?= m) = Eq -> n = m. +Proof. +intros x y; destruct x as [| x'| x']; destruct y as [| y'| y']; simpl in |- *; + intro H; reflexivity || (try discriminate H); + [ rewrite (Pcompare_Eq_eq x' y' H); reflexivity + | rewrite (Pcompare_Eq_eq x' y'); + [ reflexivity + | destruct ((x' ?= y')%positive Eq); reflexivity || discriminate ] ]. +Qed. + +Lemma Zcompare_Eq_iff_eq : forall n m:Z, (n ?= m) = Eq <-> n = m. +Proof. +intros x y; split; intro E; + [ apply Zcompare_Eq_eq; assumption | rewrite E; apply Zcompare_refl ]. +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. +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 ]. +Qed. + +(** Transitivity of comparison *) + +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 ]. +Qed. + +(** Comparison and opposite *) + +Lemma Zcompare_opp : forall n m:Z, (n ?= m) = (- m ?= - n). +Proof. +intros x y; case x; case y; simpl in |- *; auto with arith; intros; + rewrite <- ZC4; trivial with arith. +Qed. + +Hint Local Resolve Pcompare_refl. + +(** Comparison first-order specification *) + +Lemma Zcompare_Gt_spec : + forall n m:Z, (n ?= m) = Gt -> exists h : positive, n + - m = Zpos h. +Proof. +intros x y; case x; case y; + [ simpl in |- *; intros H; discriminate H + | simpl in |- *; intros p H; discriminate H + | intros p H; exists p; simpl in |- *; auto with arith + | intros p H; exists p; simpl in |- *; auto with arith + | intros q p H; exists (p - q)%positive; unfold Zplus, Zopp in |- *; + unfold Zcompare in H; rewrite H; trivial with arith + | intros q p H; exists (p + q)%positive; simpl in |- *; trivial with arith + | simpl in |- *; intros p H; discriminate H + | simpl in |- *; intros q p H; discriminate H + | unfold Zcompare in |- *; intros q p; rewrite <- ZC4; intros H; + exists (q - p)%positive; simpl in |- *; rewrite (ZC1 q p H); + trivial with arith ]. +Qed. + +(** Comparison and addition *) + +Lemma weaken_Zcompare_Zplus_compatible : + (forall (n m:Z) (p:positive), (Zpos p + n ?= Zpos p + m) = (n ?= m)) -> + forall n m p:Z, (p + n ?= p + m) = (n ?= m). +Proof. +intros H x y z; destruct z; + [ reflexivity + | apply H + | rewrite (Zcompare_opp x y); rewrite Zcompare_opp; + do 2 rewrite Zopp_plus_distr; rewrite Zopp_neg; + apply H ]. +Qed. + +Hint Local Resolve ZC4. + +Lemma weak_Zcompare_Zplus_compatible : + forall (n m:Z) (p:positive), (Zpos p + n ?= Zpos p + m) = (n ?= m). +Proof. +intros x y z; case x; case y; simpl in |- *; auto with arith; + [ intros p; apply nat_of_P_lt_Lt_compare_complement_morphism; apply ZL17 + | intros p; ElimPcompare z p; intros E; rewrite E; auto with arith; + apply nat_of_P_gt_Gt_compare_complement_morphism; + 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; + 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 + | apply nat_of_P_lt_Lt_compare_complement_morphism; + do 2 rewrite nat_of_P_plus_morphism; apply plus_lt_compat_l; + apply nat_of_P_lt_Lt_compare_morphism with (1 := E) + | apply nat_of_P_gt_Gt_compare_complement_morphism; unfold gt in |- *; + do 2 rewrite nat_of_P_plus_morphism; apply plus_lt_compat_l; + exact (nat_of_P_gt_Gt_compare_morphism q p E) ] + | intros p q; ElimPcompare z p; intros E; rewrite E; auto with arith; + apply nat_of_P_gt_Gt_compare_complement_morphism; + rewrite nat_of_P_minus_morphism; + [ unfold gt in |- *; apply lt_trans with (m := nat_of_P z); + [ apply ZL16 | apply ZL17 ] + | assumption ] + | intros p; ElimPcompare z p; intros E; rewrite E; auto with arith; + simpl in |- *; apply nat_of_P_lt_Lt_compare_complement_morphism; + rewrite nat_of_P_minus_morphism; [ apply ZL16 | assumption ] + | intros p q; ElimPcompare z q; intros E; rewrite E; auto with arith; + simpl in |- *; apply nat_of_P_lt_Lt_compare_complement_morphism; + rewrite nat_of_P_minus_morphism; + [ 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; + rewrite E2; auto with arith; + [ absurd ((q ?= p)%positive Eq = Lt); + [ rewrite <- (Pcompare_Eq_eq z q E0); + rewrite <- (Pcompare_Eq_eq z p E1); rewrite (Pcompare_refl z); + discriminate + | assumption ] + | absurd ((q ?= p)%positive Eq = Gt); + [ rewrite <- (Pcompare_Eq_eq z q E0); + rewrite <- (Pcompare_Eq_eq z p E1); rewrite (Pcompare_refl z); + discriminate + | assumption ] + | absurd ((z ?= p)%positive Eq = Lt); + [ rewrite (Pcompare_Eq_eq z q E0); rewrite <- (Pcompare_Eq_eq q p E2); + rewrite (Pcompare_refl q); discriminate + | assumption ] + | absurd ((z ?= p)%positive Eq = Lt); + [ rewrite (Pcompare_Eq_eq z q E0); rewrite E2; discriminate + | assumption ] + | absurd ((z ?= p)%positive Eq = Gt); + [ rewrite (Pcompare_Eq_eq z q E0); rewrite <- (Pcompare_Eq_eq q p E2); + rewrite (Pcompare_refl q); discriminate + | assumption ] + | absurd ((z ?= p)%positive Eq = Gt); + [ rewrite (Pcompare_Eq_eq z q E0); rewrite E2; discriminate + | assumption ] + | absurd ((z ?= q)%positive Eq = Lt); + [ rewrite (Pcompare_Eq_eq z p E1); rewrite (Pcompare_Eq_eq q p E2); + rewrite (Pcompare_refl p); discriminate + | assumption ] + | absurd ((p ?= q)%positive Eq = Gt); + [ rewrite <- (Pcompare_Eq_eq z p E1); rewrite E0; discriminate + | apply ZC2; assumption ] + | simpl in |- *; rewrite (Pcompare_Eq_eq q p E2); + rewrite (Pcompare_refl (p - z)); auto with arith + | simpl in |- *; rewrite <- ZC4; + apply nat_of_P_gt_Gt_compare_complement_morphism; + rewrite nat_of_P_minus_morphism; + [ rewrite nat_of_P_minus_morphism; + [ unfold gt in |- *; apply plus_lt_reg_l with (p := nat_of_P z); + rewrite le_plus_minus_r; + [ rewrite le_plus_minus_r; + [ apply nat_of_P_lt_Lt_compare_morphism; assumption + | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; + assumption ] + | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; + assumption ] + | apply ZC2; assumption ] + | apply ZC2; assumption ] + | simpl in |- *; rewrite <- ZC4; + apply nat_of_P_lt_Lt_compare_complement_morphism; + rewrite nat_of_P_minus_morphism; + [ rewrite nat_of_P_minus_morphism; + [ apply plus_lt_reg_l with (p := nat_of_P z); + rewrite le_plus_minus_r; + [ rewrite le_plus_minus_r; + [ apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; + assumption + | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; + assumption ] + | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; + assumption ] + | apply ZC2; assumption ] + | apply ZC2; assumption ] + | absurd ((z ?= q)%positive Eq = Lt); + [ rewrite (Pcompare_Eq_eq q p E2); rewrite E1; discriminate + | assumption ] + | absurd ((q ?= p)%positive Eq = Lt); + [ cut ((q ?= p)%positive Eq = Gt); + [ intros E; rewrite E; discriminate + | apply nat_of_P_gt_Gt_compare_complement_morphism; + unfold gt in |- *; apply lt_trans with (m := nat_of_P z); + [ apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; assumption + | apply nat_of_P_lt_Lt_compare_morphism; assumption ] ] + | assumption ] + | absurd ((z ?= q)%positive Eq = Gt); + [ rewrite (Pcompare_Eq_eq z p E1); rewrite (Pcompare_Eq_eq q p E2); + rewrite (Pcompare_refl p); discriminate + | assumption ] + | absurd ((z ?= q)%positive Eq = Gt); + [ rewrite (Pcompare_Eq_eq z p E1); rewrite ZC1; + [ discriminate | assumption ] + | assumption ] + | absurd ((z ?= q)%positive Eq = Gt); + [ rewrite (Pcompare_Eq_eq q p E2); rewrite E1; discriminate + | assumption ] + | absurd ((q ?= p)%positive Eq = Gt); + [ rewrite ZC1; + [ discriminate + | apply nat_of_P_gt_Gt_compare_complement_morphism; + unfold gt in |- *; apply lt_trans with (m := nat_of_P z); + [ apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; assumption + | apply nat_of_P_lt_Lt_compare_morphism; assumption ] ] + | assumption ] + | simpl in |- *; rewrite (Pcompare_Eq_eq q p E2); apply Pcompare_refl + | simpl in |- *; apply nat_of_P_gt_Gt_compare_complement_morphism; + unfold gt in |- *; rewrite nat_of_P_minus_morphism; + [ rewrite nat_of_P_minus_morphism; + [ apply plus_lt_reg_l with (p := nat_of_P p); + rewrite le_plus_minus_r; + [ 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; + assumption + | apply lt_le_weak; 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 ] + | assumption ] + | assumption ] + | simpl in |- *; apply nat_of_P_lt_Lt_compare_complement_morphism; + rewrite nat_of_P_minus_morphism; + [ rewrite nat_of_P_minus_morphism; + [ apply plus_lt_reg_l with (p := nat_of_P q); + rewrite le_plus_minus_r; + [ 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 ZC1; assumption + | apply lt_le_weak; 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 ] + | assumption ] + | assumption ] ] ]. +Qed. + +Lemma Zcompare_plus_compat : forall n m p:Z, (p + n ?= p + m) = (n ?= m). +Proof. +exact (weaken_Zcompare_Zplus_compatible weak_Zcompare_Zplus_compatible). +Qed. + +Lemma Zplus_compare_compat : + forall (r:comparison) (n m p q:Z), + (n ?= m) = r -> (p ?= q) = r -> (n + p ?= m + q) = r. +Proof. +intros r x y z t; case r; + [ intros H1 H2; elim (Zcompare_Eq_iff_eq x y); elim (Zcompare_Eq_iff_eq z t); + intros H3 H4 H5 H6; rewrite H3; + [ rewrite H5; + [ elim (Zcompare_Eq_iff_eq (y + t) (y + t)); auto with arith + | auto with arith ] + | auto with arith ] + | intros H1 H2; elim (Zcompare_Gt_Lt_antisym (y + t) (x + z)); intros H3 H4; + apply H3; apply Zcompare_Gt_trans with (m := y + z); + [ rewrite Zcompare_plus_compat; elim (Zcompare_Gt_Lt_antisym t z); + auto with arith + | do 2 rewrite <- (Zplus_comm z); rewrite Zcompare_plus_compat; + elim (Zcompare_Gt_Lt_antisym y x); auto with arith ] + | intros H1 H2; apply Zcompare_Gt_trans with (m := x + t); + [ rewrite Zcompare_plus_compat; assumption + | do 2 rewrite <- (Zplus_comm t); rewrite Zcompare_plus_compat; + assumption ] ]. +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; + reflexivity. +Qed. + +Lemma Zcompare_Gt_not_Lt : forall n m:Z, (n ?= m) = Gt <-> (n ?= m + 1) <> Lt. +Proof. +intros x y; split; + [ intro H; elim_compare x (y + 1); + [ intro H1; rewrite H1; discriminate + | intros H1; elim Zcompare_Gt_spec with (1 := H); intros h H2; + absurd ((nat_of_P h > 0)%nat /\ (nat_of_P h < 1)%nat); + [ unfold not in |- *; intros H3; elim H3; intros H4 H5; + absurd (nat_of_P h > 0)%nat; + [ unfold gt in |- *; apply le_not_lt; apply le_S_n; exact H5 + | assumption ] + | split; + [ elim (ZL4 h); intros i H3; rewrite H3; apply gt_Sn_O + | change (nat_of_P h < nat_of_P 1)%nat in |- *; + 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_opp_r; simpl in |- *; exact H1 ] ] + | intros H1; rewrite H1; discriminate ] + | intros H; elim_compare x (y + 1); + [ intros H1; elim (Zcompare_Eq_iff_eq x (y + 1)); intros H2 H3; + rewrite (H2 H1); exact (Zcompare_succ_Gt y) + | intros H1; absurd ((x ?= y + 1) = Lt); assumption + | intros H1; apply Zcompare_Gt_trans with (m := Zsucc y); + [ exact H1 | exact (Zcompare_succ_Gt y) ] ] ]. +Qed. + +(** Successor and comparison *) + +Lemma Zcompare_succ_compat : forall n m:Z, (Zsucc n ?= Zsucc m) = (n ?= m). +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 : + forall (p:positive) (n m:Z), (Zpos p * n ?= Zpos p * m) = (n ?= m). +Proof. +intros x; induction x as [p H| p H| ]; + [ intros y z; cut (Zpos (xI p) = Zpos p + Zpos p + 1); + [ intros E; rewrite E; do 4 rewrite Zmult_plus_distr_l; + do 2 rewrite Zmult_1_l; apply Zplus_compare_compat; + [ apply Zplus_compare_compat; apply H | trivial with arith ] + | simpl in |- *; rewrite (Pplus_diag p); trivial with arith ] + | intros y z; cut (Zpos (xO p) = Zpos p + Zpos p); + [ intros E; rewrite E; do 2 rewrite Zmult_plus_distr_l; + apply Zplus_compare_compat; apply H + | simpl in |- *; rewrite (Pplus_diag p); trivial with arith ] + | intros y z; do 2 rewrite Zmult_1_l; trivial with arith ]. +Qed. + + +(** Reverting [x ?= y] to trichotomy *) + +Lemma rename : + forall (A:Set) (P:A -> Prop) (x:A), (forall y:A, x = y -> P y) -> P x. +Proof. +auto with arith. +Qed. + +Lemma Zcompare_elim : + forall (c1 c2 c3:Prop) (n m:Z), + (n = m -> c1) -> + (n < m -> c2) -> + (n > m -> c3) -> match n ?= m with + | Eq => c1 + | Lt => c2 + | Gt => c3 + end. +Proof. +intros c1 c2 c3 x y; intros. +apply rename with (x := x ?= y); intro r; elim r; + [ intro; apply H; apply (Zcompare_Eq_eq x y); assumption + | unfold Zlt in H0; assumption + | unfold Zgt in H1; assumption ]. +Qed. + +Lemma Zcompare_eq_case : + forall (c1 c2 c3:Prop) (n m:Z), + c1 -> n = m -> match n ?= m with + | Eq => c1 + | Lt => c2 + | Gt => c3 + end. +Proof. +intros c1 c2 c3 x y; intros. +rewrite H0; rewrite Zcompare_refl. +assumption. +Qed. + +(** Decompose an egality between two [?=] relations into 3 implications *) + +Lemma Zcompare_egal_dec : + forall n m p q:Z, + (n < m -> p < q) -> + ((n ?= m) = Eq -> (p ?= q) = Eq) -> + (n > m -> p > q) -> (n ?= m) = (p ?= q). +Proof. +intros x1 y1 x2 y2. +unfold Zgt in |- *; unfold Zlt in |- *; case (x1 ?= y1); case (x2 ?= y2); + auto with arith; symmetry in |- *; auto with arith. +Qed. + +(** Relating [x ?= y] to [Zle], [Zlt], [Zge] or [Zgt] *) + +Lemma Zle_compare : + forall n m:Z, + n <= m -> match n ?= m with + | Eq => True + | Lt => True + | Gt => False + end. +Proof. +intros x y; unfold Zle in |- *; elim (x ?= y); auto with arith. +Qed. + +Lemma Zlt_compare : + forall n m:Z, + n < m -> match n ?= m with + | Eq => False + | Lt => True + | Gt => False + end. +Proof. +intros x y; unfold Zlt in |- *; elim (x ?= y); intros; + discriminate || trivial with arith. +Qed. + +Lemma Zge_compare : + forall n m:Z, + n >= m -> match n ?= m with + | Eq => True + | Lt => False + | Gt => True + end. +Proof. +intros x y; unfold Zge in |- *; elim (x ?= y); auto with arith. +Qed. + +Lemma Zgt_compare : + forall n m:Z, + n > m -> match n ?= m with + | Eq => False + | Lt => False + | Gt => True + end. +Proof. +intros x y; unfold Zgt in |- *; elim (x ?= y); intros; + discriminate || trivial with arith. +Qed. + +(**********************************************************************) +(* Other properties *) + + +Lemma Zmult_compare_compat_l : + forall n m p:Z, p > 0 -> (n ?= m) = (p * n ?= p * m). +Proof. +intros x y z H; destruct z. + discriminate H. + rewrite Zcompare_mult_compat; reflexivity. + discriminate H. +Qed. + +Lemma Zmult_compare_compat_r : + forall n m p:Z, p > 0 -> (n ?= m) = (n * p ?= m * p). +Proof. +intros x y z H; rewrite (Zmult_comm x z); rewrite (Zmult_comm y z); + apply Zmult_compare_compat_l; assumption. +Qed. + diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v new file mode 100644 index 00000000..b60cd37c --- /dev/null +++ b/theories/ZArith/Zcomplements.v @@ -0,0 +1,212 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(*i $Id: Zcomplements.v,v 1.26.2.1 2004/07/16 19:31:21 herbelin Exp $ i*) + +Require Import ZArithRing. +Require Import ZArith_base. +Require Import Omega. +Require Import Wf_nat. +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}. +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. + +(**********************************************************************) +(** The biggest power of 2 that is stricly less than [a] + + Easy to compute: replace all "1" of the binary representation by + "0", except the first "1" (or the first one :-) *) + +Fixpoint floor_pos (a:positive) : positive := + match a with + | xH => 1%positive + | xO a' => xO (floor_pos a') + | xI b' => xO (floor_pos b') + end. + +Definition floor (a:positive) := Zpos (floor_pos a). + +Lemma floor_gt0 : forall p:positive, floor p > 0. +Proof. +intro. +compute in |- *. +trivial. +Qed. + +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 (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. + +(**********************************************************************) +(** Two more induction principles over [Z]. *) + +Theorem Z_lt_abs_rec : + forall P:Z -> Set, + (forall n:Z, (forall m:Z, Zabs m < Zabs n -> P m) -> P n) -> + forall n:Z, P n. +Proof. +intros P HP p. +set (Q := fun z => 0 <= z -> P z * P (- z)) in *. +cut (Q (Zabs p)); [ intros | apply (Z_lt_rec Q); auto with zarith ]. +elim (Zabs_dec p); intro eq; rewrite eq; elim H; auto with zarith. +unfold Q in |- *; clear Q; intros. +apply pair; apply HP. +rewrite Zabs_eq; auto; intros. +elim (H (Zabs m)); intros; auto with zarith. +elim (Zabs_dec m); intro eq; rewrite eq; trivial. +rewrite Zabs_non_eq; auto with zarith. +rewrite Zopp_involutive; intros. +elim (H (Zabs m)); intros; auto with zarith. +elim (Zabs_dec m); intro eq; rewrite eq; trivial. +Qed. + +Theorem Z_lt_abs_induction : + forall P:Z -> Prop, + (forall n:Z, (forall m:Z, Zabs m < Zabs n -> P m) -> P n) -> + forall n:Z, P n. +Proof. +intros P HP p. +set (Q := fun z => 0 <= z -> P z /\ P (- z)) in *. +cut (Q (Zabs p)); [ intros | apply (Z_lt_induction Q); auto with zarith ]. +elim (Zabs_dec p); intro eq; rewrite eq; elim H; auto with zarith. +unfold Q in |- *; clear Q; intros. +split; apply HP. +rewrite Zabs_eq; auto; intros. +elim (H (Zabs m)); intros; auto with zarith. +elim (Zabs_dec m); intro eq; rewrite eq; trivial. +rewrite Zabs_non_eq; auto with zarith. +rewrite Zopp_involutive; intros. +elim (H (Zabs m)); intros; auto with zarith. +elim (Zabs_dec m); intro eq; rewrite eq; trivial. +Qed. + +(** 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. +Proof. +intros x P Hzero Hpos Hneg. +induction x as [| p| p]. +apply Hzero; trivial. +apply Hpos; apply Zorder.Zgt_pos_0. +apply Hneg; apply Zorder.Zlt_neg_0. +Qed. + +Lemma sqr_pos : forall n:Z, n * n >= 0. +Proof. +intro x. +apply (Zcase_sign x (x * x >= 0)). +intros H; rewrite H; omega. +intros H; replace 0 with (0 * 0). +apply Zmult_ge_compat; omega. +omega. +intros H; replace 0 with (0 * 0). +replace (x * x) with (- x * - x). +apply Zmult_ge_compat; omega. +ring. +omega. +Qed. + +(**********************************************************************) +(** A list length in Z, tail recursive. *) + +Require Import List. + +Fixpoint Zlength_aux (acc:Z) (A:Set) (l:list A) {struct l} : Z := + match l with + | nil => acc + | _ :: l => Zlength_aux (Zsucc acc) A l + end. + +Definition Zlength := Zlength_aux 0. +Implicit Arguments Zlength [A]. + +Section Zlength_properties. + +Variable A : Set. + +Implicit Type l : list A. + +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)). +simple induction l. +simpl in |- *; auto with zarith. +intros; simpl (length (a :: l0)) in |- *; rewrite Znat.inj_S. +simpl in |- *; rewrite H; auto with zarith. +unfold Zlength in |- *; intros; rewrite H; auto. +Qed. + +Lemma Zlength_nil : Zlength (A:=A) nil = 0. +Proof. +auto. +Qed. + +Lemma Zlength_cons : forall (x:A) l, Zlength (x :: l) = Zsucc (Zlength l). +Proof. +intros; do 2 rewrite Zlength_correct. +simpl (length (x :: l)) in |- *; rewrite Znat.inj_S; auto. +Qed. + +Lemma Zlength_nil_inv : forall l, Zlength l = 0 -> l = nil. +Proof. +intro l; rewrite Zlength_correct. +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. +Qed. + +End Zlength_properties. + +Implicit Arguments Zlength_correct [A]. +Implicit Arguments Zlength_cons [A]. +Implicit Arguments Zlength_nil_inv [A].
\ No newline at end of file diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v new file mode 100644 index 00000000..84eb2259 --- /dev/null +++ b/theories/ZArith/Zdiv.v @@ -0,0 +1,423 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(*i $Id: Zdiv.v,v 1.21.2.1 2004/07/16 19:31:21 herbelin Exp $ i*) + +(* Contribution by Claude Marché and Xavier Urbain *) + +(** + +Euclidean Division + +Defines first of function that allows Coq to normalize. +Then only after proves the main required property. + +*) + +Require Export ZArith_base. +Require Import Zbool. +Require Import Omega. +Require Import ZArithRing. +Require Import Zcomplements. +Open Local Scope Z_scope. + +(** + + 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 + +*) + +Fixpoint Zdiv_eucl_POS (a:positive) (b:Z) {struct a} : + Z * Z := + match a with + | xH => if Zge_bool b 2 then (0, 1) else (1, 0) + | xO a' => + let (q, r) := Zdiv_eucl_POS a' b in + let r' := 2 * r in + if Zgt_bool b r' then (2 * q, r') else (2 * q + 1, r' - b) + | xI a' => + let (q, r) := Zdiv_eucl_POS a' b in + let r' := 2 * r + 1 in + if Zgt_bool b r' then (2 * q, r') else (2 * q + 1, r' - b) + end. + + +(** + + Euclidean division of integers. + + 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 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 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|. + +*) + +Definition Zdiv_eucl (a b:Z) : Z * Z := + match a, b with + | Z0, _ => (0, 0) + | _, Z0 => (0, 0) + | Zpos a', Zpos _ => Zdiv_eucl_POS a' b + | Zneg a', Zpos _ => + let (q, r) := Zdiv_eucl_POS a' b in + match r with + | Z0 => (- q, 0) + | _ => (- (q + 1), b - r) + end + | Zneg a', Zneg b' => let (q, r) := Zdiv_eucl_POS a' (Zpos b') in (q, - r) + | Zpos a', Zneg b' => + let (q, r) := Zdiv_eucl_POS a' (Zpos b') in + match r with + | Z0 => (- q, 0) + | _ => (- (q + 1), b + r) + end + end. + + +(** Division and modulo are projections of [Zdiv_eucl] *) + +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. + +(* Tests: + +Eval Compute in `(Zdiv_eucl 7 3)`. + +Eval Compute in `(Zdiv_eucl (-7) 3)`. + +Eval Compute in `(Zdiv_eucl 7 (-3))`. + +Eval Compute in `(Zdiv_eucl (-7) (-3))`. + +*) + + +(** + + Main division theorem. + + First a lemma for positive + +*) + +Lemma Z_div_mod_POS : + forall b:Z, + b > 0 -> + forall a:positive, + let (q, r) := Zdiv_eucl_POS a b in Zpos a = b * q + r /\ 0 <= r < b. +Proof. +simple induction a; unfold Zdiv_eucl_POS in |- *; fold Zdiv_eucl_POS in |- *. + +intro p; case (Zdiv_eucl_POS p b); intros q r [H0 H1]. +generalize (Zgt_cases b (2 * r + 1)). +case (Zgt_bool b (2 * r + 1)); + (rewrite BinInt.Zpos_xI; rewrite H0; split; [ ring | omega ]). + +intros p; case (Zdiv_eucl_POS p b); intros q r [H0 H1]. +generalize (Zgt_cases b (2 * r)). +case (Zgt_bool b (2 * r)); rewrite BinInt.Zpos_xO; + change (Zpos (xO p)) with (2 * Zpos p) in |- *; rewrite H0; + (split; [ ring | omega ]). + +generalize (Zge_cases b 2). +case (Zge_bool b 2); (intros; split; [ ring | omega ]). +omega. +Qed. + + +Theorem Z_div_mod : + forall a b:Z, + b > 0 -> let (q, r) := Zdiv_eucl a b in a = b * q + r /\ 0 <= r < b. +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. +generalize (Z_div_mod_POS (Zpos p) H p0). +unfold Zdiv_eucl in |- *. +case (Zdiv_eucl_POS p0 (Zpos p)). +intros z z0. +case z0. + +intros [H1 H2]. +split; trivial. +replace (Zneg p0) with (- Zpos p0); [ rewrite H1; ring | trivial ]. + +intros p1 [H1 H2]. +split; trivial. +replace (Zneg p0) with (- Zpos p0); [ rewrite H1; ring | trivial ]. +generalize (Zorder.Zgt_pos_0 p1); omega. + +intros p1 [H1 H2]. +split; trivial. +replace (Zneg p0) with (- Zpos p0); [ rewrite H1; ring | trivial ]. +generalize (Zorder.Zlt_neg_0 p1); omega. + +intros; discriminate. +Qed. + +(** Existence theorems *) + +Theorem Zdiv_eucl_exist : + forall b:Z, + b > 0 -> + forall a:Z, {qr : Z * Z | let (q, r) := qr in a = b * q + r /\ 0 <= r < b}. +Proof. +intros b Hb a. +exists (Zdiv_eucl a b). +exact (Z_div_mod a b Hb). +Qed. + +Implicit Arguments Zdiv_eucl_exist. + +Theorem Zdiv_eucl_extended : + forall b:Z, + b <> 0 -> + forall a:Z, + {qr : Z * Z | let (q, r) := qr in a = b * q + r /\ 0 <= r < Zabs b}. +Proof. +intros b Hb a. +elim (Z_le_gt_dec 0 b); intro Hb'. +cut (b > 0); [ intro Hb'' | omega ]. +rewrite Zabs_eq; [ apply Zdiv_eucl_exist; assumption | assumption ]. +cut (- b > 0); [ intro Hb'' | omega ]. +elim (Zdiv_eucl_exist Hb'' a); intros qr. +elim qr; intros q r Hqr. +exists (- q, r). +elim Hqr; intros. +split. +rewrite <- Zmult_opp_comm; assumption. +rewrite Zabs_non_eq; [ assumption | omega ]. +Qed. + +Implicit Arguments Zdiv_eucl_extended. + +(** Auxiliary lemmas about [Zdiv] and [Zmod] *) + +Lemma Z_div_mod_eq : forall a b:Z, b > 0 -> a = b * Zdiv a b + Zmod a b. +Proof. +unfold Zdiv, Zmod in |- *. +intros a b Hb. +generalize (Z_div_mod a b Hb). +case Zdiv_eucl; tauto. +Qed. + +Lemma Z_mod_lt : forall a b:Z, b > 0 -> 0 <= Zmod a b < b. +Proof. +unfold Zmod in |- *. +intros a b Hb. +generalize (Z_div_mod a b Hb). +case (Zdiv_eucl a b); tauto. +Qed. + +Lemma Z_div_POS_ge0 : + forall (b:Z) (a:positive), let (q, _) := Zdiv_eucl_POS a b in q >= 0. +Proof. +simple induction a; unfold Zdiv_eucl_POS in |- *; fold Zdiv_eucl_POS in |- *. +intro p; case (Zdiv_eucl_POS p b). +intros; case (Zgt_bool b (2 * z0 + 1)); intros; omega. +intro p; case (Zdiv_eucl_POS p b). +intros; case (Zgt_bool b (2 * z0)); intros; omega. +case (Zge_bool b 2); simpl in |- *; omega. +Qed. + +Lemma Z_div_ge0 : forall a b:Z, b > 0 -> a >= 0 -> Zdiv a b >= 0. +Proof. +intros a b Hb; unfold Zdiv, Zdiv_eucl in |- *; case a; simpl in |- *; intros. +case b; simpl in |- *; trivial. +generalize Hb; case b; try trivial. +auto with zarith. +intros p0 Hp0; generalize (Z_div_POS_ge0 (Zpos p0) p). +case (Zdiv_eucl_POS p (Zpos p0)); simpl in |- *; tauto. +intros; discriminate. +elim H; trivial. +Qed. + +Lemma Z_div_lt : forall a b:Z, b >= 2 -> a > 0 -> Zdiv a b < a. +Proof. +intros. cut (b > 0); [ intro Hb | omega ]. +generalize (Z_div_mod a b Hb). +cut (a >= 0); [ intro Ha | omega ]. +generalize (Z_div_ge0 a b Hb Ha). +unfold Zdiv in |- *; case (Zdiv_eucl a b); intros q r H1 [H2 H3]. +cut (a >= 2 * q -> q < a); [ intro h; apply h; clear h | intros; omega ]. +apply Zge_trans with (b * q). +omega. +auto with zarith. +Qed. + +(** Syntax *) + + + +Infix "/" := Zdiv : Z_scope. +Infix "mod" := Zmod (at level 40, no associativity) : Z_scope. + +(** Other lemmas (now using the syntax for [Zdiv] and [Zmod]). *) + +Lemma Z_div_ge : forall a b c:Z, c > 0 -> a >= b -> a / c >= b / c. +Proof. +intros a b c cPos aGeb. +generalize (Z_div_mod_eq a c cPos). +generalize (Z_mod_lt a c cPos). +generalize (Z_div_mod_eq b c cPos). +generalize (Z_mod_lt b c cPos). +intros. +elim (Z_ge_lt_dec (a / c) (b / c)); trivial. +intro. +absurd (b - a >= 1). +omega. +rewrite H0. +rewrite H2. +assert + (c * (b / c) + b mod c - (c * (a / c) + a mod c) = + c * (b / c - a / c) + b mod c - a mod c). +ring. +rewrite H3. +assert (c * (b / c - a / c) >= c * 1). +apply Zmult_ge_compat_l. +omega. +omega. +assert (c * 1 = c). +ring. +omega. +Qed. + +Lemma Z_mod_plus : forall a b c:Z, c > 0 -> (a + b * c) mod c = a mod c. +Proof. +intros a b c cPos. +generalize (Z_div_mod_eq a c cPos). +generalize (Z_mod_lt a c cPos). +generalize (Z_div_mod_eq (a + b * c) c cPos). +generalize (Z_mod_lt (a + b * c) c cPos). +intros. + +assert ((a + b * c) mod c - a mod c = c * (b + a / c - (a + b * c) / c)). +replace ((a + b * c) mod c) with (a + b * c - c * ((a + b * c) / c)). +replace (a mod c) with (a - c * (a / c)). +ring. +omega. +omega. +set (q := b + a / c - (a + b * c) / c) in *. +apply (Zcase_sign q); intros. +assert (c * q = 0). +rewrite H4; ring. +rewrite H5 in H3. +omega. + +assert (c * q >= c). +pattern c at 2 in |- *; replace c with (c * 1). +apply Zmult_ge_compat_l; omega. +ring. +omega. + +assert (c * q <= - c). +replace (- c) with (c * -1). +apply Zmult_le_compat_l; omega. +ring. +omega. +Qed. + +Lemma Z_div_plus : forall a b c:Z, c > 0 -> (a + b * c) / c = a / c + b. +Proof. +intros a b c cPos. +generalize (Z_div_mod_eq a c cPos). +generalize (Z_mod_lt a c cPos). +generalize (Z_div_mod_eq (a + b * c) c cPos). +generalize (Z_mod_lt (a + b * c) c cPos). +intros. +apply Zmult_reg_l with c. omega. +replace (c * ((a + b * c) / c)) with (a + b * c - (a + b * c) mod c). +rewrite (Z_mod_plus a b c cPos). +pattern a at 1 in |- *; rewrite H2. +ring. +pattern (a + b * c) at 1 in |- *; rewrite H0. +ring. +Qed. + +Lemma Z_div_mult : forall a b:Z, b > 0 -> a * b / b = a. +intros; replace (a * b) with (0 + a * b); auto. +rewrite Z_div_plus; auto. +Qed. + +Lemma Z_mult_div_ge : forall a b:Z, b > 0 -> b * (a / b) <= a. +Proof. +intros a b bPos. +generalize (Z_div_mod_eq a _ bPos); intros. +generalize (Z_mod_lt a _ bPos); intros. +pattern a at 2 in |- *; rewrite H. +omega. +Qed. + +Lemma Z_mod_same : forall a:Z, a > 0 -> a mod a = 0. +Proof. +intros a aPos. +generalize (Z_mod_plus 0 1 a aPos). +replace (0 + 1 * a) with a. +intros. +rewrite H. +compute in |- *. +trivial. +ring. +Qed. + +Lemma Z_div_same : forall a:Z, a > 0 -> a / a = 1. +Proof. +intros a aPos. +generalize (Z_div_plus 0 1 a aPos). +replace (0 + 1 * a) with a. +intros. +rewrite H. +compute in |- *. +trivial. +ring. +Qed. + +Lemma Z_div_exact_1 : forall a b:Z, b > 0 -> a = b * (a / b) -> a mod b = 0. +intros a b Hb; generalize (Z_div_mod a b Hb); unfold Zmod, Zdiv in |- *. +case (Zdiv_eucl a b); intros q r; omega. +Qed. + +Lemma Z_div_exact_2 : forall a b:Z, b > 0 -> a mod b = 0 -> a = b * (a / b). +intros a b Hb; generalize (Z_div_mod a b Hb); unfold Zmod, Zdiv in |- *. +case (Zdiv_eucl a b); intros q r; omega. +Qed. + +Lemma Z_mod_zero_opp : forall a b:Z, b > 0 -> a mod b = 0 -> - a mod b = 0. +intros a b Hb. +intros. +rewrite Z_div_exact_2 with a b; auto. +replace (- (b * (a / b))) with (0 + - (a / b) * b). +rewrite Z_mod_plus; auto. +ring. +Qed. diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v new file mode 100644 index 00000000..a4a9abde --- /dev/null +++ b/theories/ZArith/Zeven.v @@ -0,0 +1,204 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(*i $Id: Zeven.v,v 1.3.2.1 2004/07/16 19:31:21 herbelin Exp $ i*) + +Require Import BinInt. + +(**********************************************************************) +(** About parity: even and odd predicates on Z, division by 2 on Z *) + +(**********************************************************************) +(** [Zeven], [Zodd], [Zdiv2] and their related properties *) + +Definition Zeven (z:Z) := + match z with + | Z0 => True + | Zpos (xO _) => True + | Zneg (xO _) => True + | _ => False + end. + +Definition Zodd (z:Z) := + match z with + | Zpos xH => True + | Zneg xH => True + | Zpos (xI _) => True + | Zneg (xI _) => True + | _ => False + end. + +Definition Zeven_bool (z:Z) := + match z with + | Z0 => true + | Zpos (xO _) => true + | Zneg (xO _) => true + | _ => false + end. + +Definition Zodd_bool (z:Z) := + match z with + | Z0 => false + | Zpos (xO _) => false + | Zneg (xO _) => false + | _ => true + end. + +Definition Zeven_odd_dec : forall z:Z, {Zeven z} + {Zodd z}. +Proof. + intro z. case z; + [ left; compute in |- *; trivial + | intro p; case p; intros; + (right; compute in |- *; exact I) || (left; compute in |- *; exact I) + | intro p; case p; intros; + (right; compute in |- *; exact I) || (left; compute in |- *; exact I) ]. +Defined. + +Definition Zeven_dec : forall z:Z, {Zeven z} + {~ Zeven z}. +Proof. + intro z. case z; + [ left; compute in |- *; trivial + | intro p; case p; intros; + (left; compute in |- *; exact I) || (right; compute in |- *; trivial) + | intro p; case p; intros; + (left; compute in |- *; exact I) || (right; compute in |- *; trivial) ]. +Defined. + +Definition Zodd_dec : forall z:Z, {Zodd z} + {~ Zodd z}. +Proof. + intro z. case z; + [ right; compute in |- *; trivial + | intro p; case p; intros; + (left; compute in |- *; exact I) || (right; compute in |- *; trivial) + | intro p; case p; intros; + (left; compute in |- *; exact I) || (right; compute in |- *; trivial) ]. +Defined. + +Lemma Zeven_not_Zodd : forall n:Z, Zeven n -> ~ Zodd n. +Proof. + intro z; destruct z; [ idtac | destruct p | destruct p ]; compute in |- *; + trivial. +Qed. + +Lemma Zodd_not_Zeven : forall n:Z, Zodd n -> ~ Zeven n. +Proof. + intro z; destruct z; [ idtac | destruct p | destruct p ]; compute in |- *; + trivial. +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. + 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. + 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. + 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. + unfold Pdouble_minus_one in |- *; case p; simpl in |- *; auto. +Qed. + +Hint Unfold Zeven Zodd: zarith. + +(**********************************************************************) +(** [Zdiv2] is defined on all [Z], but notice that for odd negative + integers it is not the euclidean quotient: in that case we have [n = + 2*(n/2)-1] *) + +Definition Zdiv2 (z:Z) := + match z with + | Z0 => 0%Z + | Zpos xH => 0%Z + | Zpos p => Zpos (Pdiv2 p) + | Zneg xH => 0%Z + | Zneg p => Zneg (Pdiv2 p) + end. + +Lemma Zeven_div2 : forall n:Z, Zeven n -> n = (2 * Zdiv2 n)%Z. +Proof. +intro x; destruct x. +auto with arith. +destruct p; auto with arith. +intros. absurd (Zeven (Zpos (xI p))); red in |- *; auto with arith. +intros. absurd (Zeven 1); red in |- *; auto with arith. +destruct p; auto with arith. +intros. absurd (Zeven (Zneg (xI p))); red in |- *; auto with arith. +intros. absurd (Zeven (-1)); red in |- *; auto with arith. +Qed. + +Lemma Zodd_div2 : forall n:Z, (n >= 0)%Z -> Zodd n -> n = (2 * Zdiv2 n + 1)%Z. +Proof. +intro x; destruct x. +intros. absurd (Zodd 0); red in |- *; auto with arith. +destruct p; auto with arith. +intros. absurd (Zodd (Zpos (xO p))); red in |- *; auto with arith. +intros. absurd (Zneg p >= 0)%Z; red in |- *; auto with arith. +Qed. + +Lemma Zodd_div2_neg : + forall n:Z, (n <= 0)%Z -> Zodd n -> n = (2 * Zdiv2 n - 1)%Z. +Proof. +intro x; destruct x. +intros. absurd (Zodd 0); red in |- *; auto with arith. +intros. absurd (Zneg p >= 0)%Z; red in |- *; auto with arith. +destruct p; auto with arith. +intros. absurd (Zodd (Zneg (xO p))); red in |- *; auto with arith. +Qed. + +Lemma Z_modulo_2 : + forall n:Z, {y : Z | n = (2 * y)%Z} + {y : Z | n = (2 * y + 1)%Z}. +Proof. +intros x. +elim (Zeven_odd_dec x); intro. +left. split with (Zdiv2 x). exact (Zeven_div2 x a). +right. generalize b; clear b; case x. +intro b; inversion b. +intro p; split with (Zdiv2 (Zpos p)). apply (Zodd_div2 (Zpos p)); trivial. +unfold Zge, Zcompare in |- *; simpl in |- *; discriminate. +intro p; split with (Zdiv2 (Zpred (Zneg p))). +pattern (Zneg p) at 1 in |- *; rewrite (Zsucc_pred (Zneg p)). +pattern (Zpred (Zneg p)) at 1 in |- *; rewrite (Zeven_div2 (Zpred (Zneg p))). +reflexivity. +apply Zeven_pred; assumption. +Qed. + +Lemma Zsplit2 : + forall n:Z, + {p : Z * Z | + let (x1, x2) := p in n = (x1 + x2)%Z /\ (x1 = x2 \/ x2 = (x1 + 1)%Z)}. +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. +assumption. +left; reflexivity. +exists (y, (y + 1)%Z); split. +rewrite Zplus_assoc; assumption. +right; reflexivity. +Qed.
\ No newline at end of file diff --git a/theories/ZArith/Zhints.v b/theories/ZArith/Zhints.v new file mode 100644 index 00000000..a9ee2c87 --- /dev/null +++ b/theories/ZArith/Zhints.v @@ -0,0 +1,386 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(*i $Id: Zhints.v,v 1.8.2.1 2004/07/16 19:31:21 herbelin Exp $ i*) + +(** This file centralizes the lemmas about [Z], classifying them + according to the way they can be used in automatic search *) + +(*i*) + +(* Lemmas which clearly leads to simplification during proof search are *) +(* declared as Hints. A definite status (Hint or not) for the other lemmas *) +(* remains to be given *) + +(* Structure of the file *) +(* - simplification lemmas (only those are declared as Hints) *) +(* - reversible lemmas relating operators *) +(* - useful Bottom-up lemmas *) +(* - irreversible lemmas with meta-variables *) +(* - unclear or too specific lemmas *) +(* - lemmas to be used as rewrite rules *) + +(* Lemmas involving positive and compare are not taken into account *) + +Require Import BinInt. +Require Import Zorder. +Require Import Zmin. +Require Import Zabs. +Require Import Zcompare. +Require Import Znat. +Require Import auxiliary. +Require Import Zmisc. +Require Import Wf_Z. + +(**********************************************************************) +(* Simplification lemmas *) +(* No subgoal or smaller subgoals *) + +Hint Resolve + (* A) Reversible simplification lemmas (no loss of information) *) + (* Should clearly 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)` *) + Zle_refl (* :(n:Z)`n <= n` *) + Zle_succ (* :(n:Z)`n <= (Zs n)` *) + Zsucc_le_compat (* :(n,m:Z)`m <= n`->`(Zs m) <= (Zs n)` *) + Zle_pred (* :(n:Z)`(Zpred n) <= n` *) + Zle_min_l (* :(n,m:Z)`(Zmin n m) <= n` *) + Zle_min_r (* :(n,m:Z)`(Zmin n m) <= m` *) + 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|` *) + + (* B) 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` *) + Zorder.Zmult_le_compat_l (* :(a,b,c:Z)`a <= b`->`0 <= c`->`c*a <= c*b` *) + 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 *) + +(* A) 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` +Zeven_div2: (x:Z)(Zeven x)->`x = 2*(Zdiv2 x)` +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` + +(* 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)` +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` +Zlt_left: (x,y:Z)`x < y`->`0 <= y+(-1)+(-x)` +Zge_left: (x,y:Z)`x >= y`->`0 <= x+(-y)` +Zgt_left: (x,y:Z)`x > y`->`0 <= x+(-1)+(-y)` + +(* B) 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)` + +(* C) 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` + +(* Lemmas ending by Zgt *) +Zle_gt_S: (n,p:Z)`n <= p`->`(Zs p) > n` +not_Zle: (x,y:Z)~`x <= y`->`x > y` +Zlt_gt: (m,n:Z)`m < n`->`n > m` +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` +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` +Zgt_le_S: (n,p:Z)`p > n`->`(Zs n) <= p` +Zgt_S_le: (n,p:Z)`(Zs p) > n`->`n <= p` +Zge_le: (m,n:Z)`m >= n`->`n <= m` +Zlt_le_S: (n,p:Z)`n < p`->`(Zs n) <= p` +Zlt_n_Sm_le: (n,m:Z)`n < (Zs m)`->`n <= m` +Zlt_le_weak: (n,m:Z)`n < m`->`n <= m` +Zle_refl: (n,m:Z)`n = m`->`n <= m` + +(* D) Irreversible simplification involving several comparaisons, *) +(* 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` + +(* 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)` + +*) + +(**********************************************************************) +(* Useful Bottom-up lemmas *) + +(* A) 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` +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` + +(* 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` + +(* Lemmas ending by Zle *) +Zsimpl_le_plus_l: (p,n,m:Z)`p+n <= p+m`->`n <= m` +Zsimpl_le_plus_r: (p,n,m:Z)`n+p <= m+p`->`n <= m` +Zle_S_n: (n,m:Z)`(Zs m) <= (Zs n)`->`m <= n` + +(* B) Bottom-up irreversible (syntactic) simplification *) + +(* Lemmas ending by Zle *) +Zle_trans_S: (n,m:Z)`(Zs n) <= m`->`n <= m` + +(* C) Other unclearly simplifying lemmas *) + +(* Lemmas ending by Zeq *) +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 + +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` +*) + +(**********************************************************************) +(* Unclear or too specific lemmas *) +(* Not to be used ?? *) + +(* A) Irreversible and too specific (not enough regular) + +(* Lemmas ending by Zle *) +Zle_mult: (x,y:Z)`x > 0`->`0 <= y`->`0 <= y*x` +Zle_mult_approx: (x,y,z:Z)`x > 0`->`z > 0`->`0 <= y`->`0 <= y*x+z` +OMEGA6: (x,y,z:Z)`0 <= x`->`y = 0`->`0 <= x+y*z` +OMEGA7: (x,y,z,t:Z)`z > 0`->`t > 0`->`0 <= x`->`0 <= y`->`0 <= x*z+y*t` + + +(* B) Expansion and too specific ? *) + +(* Lemmas ending by Zge *) +Zge_mult_simpl: (a,b,c:Z)`c > 0`->`a*c >= b*c`->`a >= b` + +(* Lemmas ending by Zgt *) +Zgt_mult_simpl: (a,b,c:Z)`c > 0`->`a*c > b*c`->`a > b` +Zgt_square_simpl: (x,y:Z)`x >= 0`->`y >= 0`->`x*x > y*y`->`x > y` + +(* Lemmas ending by Zle *) +Zle_mult_simpl: (a,b,c:Z)`c > 0`->`a*c <= b*c`->`a <= b` +Zmult_le_approx: (x,y,z:Z)`x > 0`->`x > z`->`0 <= y*x+z`->`0 <= y` + +(* C) Reversible but too specific ? *) + +(* Lemmas ending by Zlt *) +Zlt_minus: (n,m:Z)`0 < m`->`n-m < n` +*) + +(**********************************************************************) +(* Lemmas to be used as rewrite rules *) +(* but can also be used as hints + +(* Left-to-right simplification lemmas (a symbol disappears) *) + +Zcompare_n_S: (n,m:Z)(Zcompare (Zs n) (Zs m))=(Zcompare n m) +Zmin_n_n: (n:Z)`(Zmin n n) = n` +Zmult_1_n: (n:Z)`1*n = n` +Zmult_n_1: (n:Z)`n*1 = n` +Zminus_plus: (n,m:Z)`n+m-n = m` +Zle_plus_minus: (n,m:Z)`n+(m-n) = m` +Zopp_Zopp: (x:Z)`(-(-x)) = x` +Zero_left: (x:Z)`0+x = x` +Zero_right: (x:Z)`x+0 = x` +Zplus_inverse_r: (x:Z)`x+(-x) = 0` +Zplus_inverse_l: (x:Z)`(-x)+x = 0` +Zopp_intro: (x,y:Z)`(-x) = (-y)`->`x = y` +Zmult_one: (x:Z)`1*x = x` +Zero_mult_left: (x:Z)`0*x = 0` +Zero_mult_right: (x:Z)`x*0 = 0` +Zmult_Zopp_Zopp: (x,y:Z)`(-x)*(-y) = x*y` + +(* Right-to-left simplification lemmas (a symbol disappears) *) + +Zpred_Sn: (m:Z)`m = (Zpred (Zs m))` +Zs_pred: (n:Z)`n = (Zs (Zpred n))` +Zplus_n_O: (n:Z)`n = n+0` +Zmult_n_O: (n:Z)`0 = n*0` +Zminus_n_O: (n:Z)`n = n-0` +Zminus_n_n: (n:Z)`0 = n-n` +Zred_factor6: (x:Z)`x = x+0` +Zred_factor0: (x:Z)`x = x*1` + +(* Unclear orientation (no symbol disappears) *) + +Zplus_n_Sm: (n,m:Z)`(Zs (n+m)) = n+(Zs m)` +Zmult_n_Sm: (n,m:Z)`n*m+n = n*(Zs m)` +Zmin_SS: (n,m:Z)`(Zs (Zmin n m)) = (Zmin (Zs n) (Zs m))` +Zplus_assoc_l: (n,m,p:Z)`n+(m+p) = n+m+p` +Zplus_assoc_r: (n,m,p:Z)`n+m+p = n+(m+p)` +Zplus_permute: (n,m,p:Z)`n+(m+p) = m+(n+p)` +Zplus_Snm_nSm: (n,m:Z)`(Zs n)+m = n+(Zs m)` +Zminus_plus_simpl: (n,m,p:Z)`n-m = p+n-(p+m)` +Zminus_Sn_m: (n,m:Z)`(Zs (n-m)) = (Zs n)-m` +Zmult_plus_distr_l: (n,m,p:Z)`(n+m)*p = n*p+m*p` +Zmult_minus_distr: (n,m,p:Z)`(n-m)*p = n*p-m*p` +Zmult_assoc_r: (n,m,p:Z)`n*m*p = n*(m*p)` +Zmult_assoc_l: (n,m,p:Z)`n*(m*p) = n*m*p` +Zmult_permute: (n,m,p:Z)`n*(m*p) = m*(n*p)` +Zmult_Sm_n: (n,m:Z)`n*m+m = (Zs n)*m` +Zmult_Zplus_distr: (x,y,z:Z)`x*(y+z) = x*y+x*z` +Zmult_plus_distr: (n,m,p:Z)`(n+m)*p = n*p+m*p` +Zopp_Zplus: (x,y:Z)`(-(x+y)) = (-x)+(-y)` +Zplus_sym: (x,y:Z)`x+y = y+x` +Zplus_assoc: (x,y,z:Z)`x+(y+z) = x+y+z` +Zmult_sym: (x,y:Z)`x*y = y*x` +Zmult_assoc: (x,y,z:Z)`x*(y*z) = x*y*z` +Zopp_Zmult: (x,y:Z)`(-x)*y = (-(x*y))` +Zplus_S_n: (x,y:Z)`(Zs x)+y = (Zs (x+y))` +Zopp_one: (x:Z)`(-x) = x*(-1)` +Zopp_Zmult_r: (x,y:Z)`(-(x*y)) = x*(-y)` +Zmult_Zopp_left: (x,y:Z)`(-x)*y = x*(-y)` +Zopp_Zmult_l: (x,y:Z)`(-(x*y)) = (-x)*y` +Zred_factor1: (x:Z)`x+x = x*2` +Zred_factor2: (x,y:Z)`x+x*y = x*(1+y)` +Zred_factor3: (x,y:Z)`x*y+x = x*(1+y)` +Zred_factor4: (x,y,z:Z)`x*y+x*z = x*(y+z)` +Zminus_Zplus_compatible: (x,y,n:Z)`x+n-(y+n) = x-y` +Zmin_plus: (x,y,n:Z)`(Zmin (x+n) (y+n)) = (Zmin x y)+n` + +(* nat <-> Z *) +inj_S: (y:nat)`(inject_nat (S y)) = (Zs (inject_nat y))` +inj_plus: (x,y:nat)`(inject_nat (plus x y)) = (inject_nat x)+(inject_nat y)` +inj_mult: (x,y:nat)`(inject_nat (mult x y)) = (inject_nat x)*(inject_nat y)` +inj_minus1: + (x,y:nat)(le y x)->`(inject_nat (minus x y)) = (inject_nat x)-(inject_nat y)` +inj_minus2: (x,y:nat)(gt y x)->`(inject_nat (minus x y)) = 0` + +(* Too specific ? *) +Zred_factor5: (x,y:Z)`x*0+y = y` +*) + +(*i*)
\ No newline at end of file diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v new file mode 100644 index 00000000..b575de88 --- /dev/null +++ b/theories/ZArith/Zlogarithm.v @@ -0,0 +1,265 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(*i $Id: Zlogarithm.v,v 1.14.2.1 2004/07/16 19:31:21 herbelin Exp $ i*) + +(**********************************************************************) +(** The integer logarithms with base 2. + + There are three logarithms, + depending on the rounding of the real 2-based logarithm: + - [Log_inf]: [y = (Log_inf x) iff 2^y <= x < 2^(y+1)] + i.e. [Log_inf x] is the biggest integer that is smaller than [Log x] + - [Log_sup]: [y = (Log_sup x) iff 2^(y-1) < x <= 2^y] + i.e. [Log_inf x] is the smallest integer that is bigger than [Log x] + - [Log_nearest]: [y= (Log_nearest x) iff 2^(y-1/2) < x <= 2^(y+1/2)] + i.e. [Log_nearest x] is the integer nearest from [Log x] *) + +Require Import ZArith_base. +Require Import Omega. +Require Import Zcomplements. +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 := + match p with + | xH => 0 (* 1 *) + | xO q => Zsucc (log_inf q) (* 2n *) + | xI q => Zsucc (log_inf q) (* 2n+1 *) + end. +Fixpoint log_sup (p:positive) : Z := + match p with + | xH => 0 (* 1 *) + | 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] + and prove their validity *) + +(*i Hints Resolve ZERO_le_S : zarith. i*) +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)). +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); + 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); + omega ] + | unfold two_power_pos in |- *; unfold shift_pos in |- *; simpl in |- *; + omega ]. +Qed. + +Definition log_inf_correct1 (p:positive) := proj1 (log_inf_correct p). +Definition log_inf_correct2 (p:positive) := proj2 (log_inf_correct p). + +Opaque log_inf_correct1 log_inf_correct2. + +Hint Resolve log_inf_correct1 log_inf_correct2: zarith. + +Lemma log_sup_correct1 : forall p:positive, 0 <= log_sup p. +simple induction p; intros; simpl in |- *; auto with zarith. +Qed. + +(** For every [p], either [p] is a power of two and [(log_inf p)=(log_sup p)] + either [(log_sup p)=(log_inf p)+1] *) + +Theorem log_sup_log_inf : + forall p:positive, + IF Zpos p = two_p (log_inf p) then Zpos p = two_p (log_sup p) + else log_sup p = Zsucc (log_inf p). + +simple induction p; intros; + [ elim H; right; simpl in |- *; + rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0)); + rewrite BinInt.Zpos_xI; unfold Zsucc in |- *; omega + | elim H; clear H; intro Hif; + [ 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); + auto + | right; simpl in |- *; + rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0)); + rewrite BinInt.Zpos_xO; unfold Zsucc in |- *; + omega ] + | left; auto ]. +Qed. + +Theorem log_sup_correct2 : + forall x:positive, two_p (Zpred (log_sup x)) < Zpos x <= two_p (log_sup x). + +intro. +elim (log_sup_log_inf x). +(* x is a power of two and [log_sup = log_inf] *) +intros [E1 E2]; rewrite E2. +split; [ apply two_p_pred; apply log_sup_correct1 | apply Zle_refl ]. +intros [E1 E2]; rewrite E2. +rewrite <- (Zpred_succ (log_inf x)). +generalize (log_inf_correct2 x); omega. +Qed. + +Lemma log_inf_le_log_sup : forall p:positive, log_inf p <= log_sup p. +simple induction p; simpl in |- *; intros; omega. +Qed. + +Lemma log_sup_le_Slog_inf : forall p:positive, log_sup p <= Zsucc (log_inf p). +simple induction p; simpl in |- *; intros; omega. +Qed. + +(** Now it's possible to specify and build the [Log] rounded to the nearest *) + +Fixpoint log_near (x:positive) : Z := + match x with + | xH => 0 + | xO xH => 1 + | xI xH => 2 + | xO y => Zsucc (log_near y) + | xI y => Zsucc (log_near y) + end. + +Theorem log_near_correct1 : forall p:positive, 0 <= log_near p. +simple induction p; simpl in |- *; intros; + [ elim p0; auto with zarith + | elim p0; auto with zarith + | trivial with zarith ]. +intros; apply Zle_le_succ. +generalize H0; elim p1; intros; simpl in |- *; + [ assumption | assumption | apply Zorder.Zle_0_pos ]. +intros; apply Zle_le_succ. +generalize H0; elim p1; intros; simpl in |- *; + [ assumption | assumption | apply Zorder.Zle_0_pos ]. +Qed. + +Theorem log_near_correct2 : + forall p:positive, log_near p = log_inf p \/ log_near p = log_sup p. +simple induction p. +intros p0 [Einf| Esup]. +simpl in |- *. rewrite Einf. +case p0; [ left | left | right ]; reflexivity. +simpl in |- *; rewrite Esup. +elim (log_sup_log_inf p0). +generalize (log_inf_le_log_sup p0). +generalize (log_sup_le_Slog_inf p0). +case p0; auto with zarith. +intros; omega. +case p0; intros; auto with zarith. +intros p0 [Einf| Esup]. +simpl in |- *. +repeat rewrite Einf. +case p0; intros; auto with zarith. +simpl in |- *. +repeat rewrite Esup. +case p0; intros; auto with zarith. +auto. +Qed. + +(*i****************** +Theorem log_near_correct: (p:positive) + `| (two_p (log_near p)) - (POS p) | <= (POS p)-(two_p (log_inf p))` + /\`| (two_p (log_near p)) - (POS p) | <= (two_p (log_sup p))-(POS p)`. +Intro. +Induction p. +Intros p0 [(Einf1,Einf2)|(Esup1,Esup2)]. +Unfold log_near log_inf log_sup. Fold log_near log_inf log_sup. +Rewrite Einf1. +Repeat Rewrite two_p_S. +Case p0; [Left | Left | Right]. + +Split. +Simpl. +Rewrite E1; Case p0; Try Reflexivity. +Compute. +Unfold log_near; Fold log_near. +Unfold log_inf; Fold log_inf. +Repeat Rewrite E1. +Split. +**********************************i*) + +End Log_pos. + +Section divers. + +(** Number of significative digits. *) + +Definition N_digits (x:Z) := + match x with + | Zpos p => log_inf p + | Zneg p => log_inf p + | Z0 => 0 + end. + +Lemma ZERO_le_N_digits : forall x:Z, 0 <= N_digits x. +simple induction x; simpl in |- *; + [ apply Zle_refl | exact log_inf_correct1 | exact log_inf_correct1 ]. +Qed. + +Lemma log_inf_shift_nat : forall n:nat, log_inf (shift_nat n 1) = Z_of_nat n. +simple induction n; intros; + [ try trivial | rewrite Znat.inj_S; rewrite <- H; reflexivity ]. +Qed. + +Lemma log_sup_shift_nat : forall n:nat, log_sup (shift_nat n 1) = Z_of_nat n. +simple induction n; intros; + [ try trivial | rewrite Znat.inj_S; rewrite <- H; reflexivity ]. +Qed. + +(** [Is_power p] means that p is a power of two *) +Fixpoint Is_power (p:positive) : Prop := + match p with + | xH => True + | xO q => Is_power q + | xI q => False + end. + +Lemma Is_power_correct : + forall p:positive, Is_power p <-> (exists y : nat, p = shift_nat y 1). + +split; + [ elim p; + [ simpl in |- *; tauto + | simpl in |- *; intros; generalize (H H0); intro H1; elim H1; + intros y0 Hy0; exists (S y0); rewrite Hy0; reflexivity + | intro; exists 0%nat; reflexivity ] + | intros; elim H; intros; rewrite H0; elim x; intros; simpl in |- *; trivial ]. +Qed. + +Lemma Is_power_or : forall p:positive, Is_power p \/ ~ Is_power p. +simple induction p; + [ intros; right; simpl in |- *; tauto + | intros; elim H; + [ intros; left; simpl in |- *; exact H0 + | intros; right; simpl in |- *; exact H0 ] + | left; simpl in |- *; trivial ]. +Qed. + +End divers. + + + + + + diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v new file mode 100644 index 00000000..d48e62c5 --- /dev/null +++ b/theories/ZArith/Zmin.v @@ -0,0 +1,106 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) +(*i $Id: Zmin.v,v 1.3.2.1 2004/07/16 19:31:21 herbelin Exp $ i*) + +(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *) + +Require Import Arith. +Require Import BinInt. +Require Import Zcompare. +Require Import Zorder. + +Open Local Scope Z_scope. + +(**********************************************************************) +(** Minimum on binary integer numbers *) + +Definition Zmin (n m:Z) := + match n ?= m return Z with + | Eq => n + | Lt => n + | Gt => m + end. + +(** Properties of minimum on binary integer numbers *) + +Lemma Zmin_SS : 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. + +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. + +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. + +Lemma Zmin_case : forall (n m:Z) (P:Z -> Set), 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. + +Lemma Zmin_or : forall n m:Z, Zmin n m = n \/ Zmin n m = m. +Proof. +unfold Zmin in |- *; intros; elim (n ?= m); auto. +Qed. + +Lemma Zmin_n_n : forall n:Z, Zmin n n = n. +Proof. +unfold Zmin in |- *; intros; elim (n ?= n); auto. +Qed. + +Lemma Zmin_plus : 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. + +(**********************************************************************) +(** Maximum of two binary integer numbers *) + +Definition Zmax a b := match a ?= b with + | Lt => b + | _ => a + end. + +(** Properties of maximum on binary integer numbers *) + +Ltac CaseEq name := + generalize (refl_equal name); pattern name at -1 in |- *; case name. + +Theorem Zmax1 : forall a b, a <= Zmax a b. +Proof. +intros a b; unfold Zmax in |- *; CaseEq (a ?= b); simpl in |- *; + auto with zarith. +unfold Zle in |- *; intros H; rewrite H; red in |- *; intros; discriminate. +Qed. + +Theorem Zmax2 : forall a b, b <= Zmax a b. +Proof. +intros a b; unfold Zmax in |- *; CaseEq (a ?= b); simpl in |- *; + auto with zarith. +intros H; + (case (Zle_or_lt b a); auto; unfold Zlt in |- *; rewrite H; intros; + discriminate). +intros H; + (case (Zle_or_lt b a); auto; unfold Zlt in |- *; rewrite H; intros; + discriminate). +Qed. diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v new file mode 100644 index 00000000..adcaf0ba --- /dev/null +++ b/theories/ZArith/Zmisc.v @@ -0,0 +1,97 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(*i $Id: Zmisc.v,v 1.20.2.1 2004/07/16 19:31:22 herbelin Exp $ i*) + +Require Import BinInt. +Require Import Zcompare. +Require Import Zorder. +Require Import Bool. +Open Local Scope Z_scope. + +(**********************************************************************) +(** Iterators *) + +(** [n]th iteration of the function [f] *) +Fixpoint iter_nat (n:nat) (A:Set) (f:A -> A) (x:A) {struct n} : A := + match n with + | O => x + | S n' => f (iter_nat n' A f x) + end. + +Fixpoint iter_pos (n:positive) (A:Set) (f:A -> A) (x:A) {struct n} : A := + match n with + | xH => f x + | xO n' => iter_pos n' A f (iter_pos n' A f x) + | xI n' => f (iter_pos n' A f (iter_pos n' A f x)) + end. + +Definition iter (n:Z) (A:Set) (f:A -> A) (x:A) := + match n with + | Z0 => x + | Zpos p => iter_pos p A f x + | Zneg p => x + end. + +Theorem iter_nat_plus : + forall (n m:nat) (A:Set) (f:A -> A) (x:A), + iter_nat (n + m) A f x = iter_nat n A f (iter_nat m A f x). +Proof. +simple induction n; + [ simpl in |- *; auto with arith + | intros; simpl in |- *; apply f_equal with (f := f); apply H ]. +Qed. + +Theorem iter_nat_of_P : + forall (p:positive) (A:Set) (f:A -> A) (x:A), + iter_pos p A f x = iter_nat (nat_of_P p) A f x. +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 (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 (ZL6 p); symmetry in |- *; apply iter_nat_plus + | simpl in |- *; auto with arith ]. +Qed. + +Theorem iter_pos_plus : + forall (p q:positive) (A:Set) (f:A -> A) (x:A), + iter_pos (p + q) A f x = iter_pos p A f (iter_pos q A f x). +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)). +rewrite (iter_nat_of_P (n + m) A f x). +rewrite (nat_of_P_plus_morphism n m). +apply iter_nat_plus. +Qed. + +(** 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:Set) (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. +simple induction n; intros; + [ trivial with arith + | simpl in |- *; apply H0 with (x := iter_nat n0 A f x); apply H; + trivial with arith ]. +Qed. + +Theorem iter_pos_invariant : + forall (p:positive) (A:Set) (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. +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 new file mode 100644 index 00000000..d051ed74 --- /dev/null +++ b/theories/ZArith/Znat.v @@ -0,0 +1,138 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(*i $Id: Znat.v,v 1.3.2.1 2004/07/16 19:31:22 herbelin Exp $ i*) + +(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) + +Require Export Arith. +Require Import BinPos. +Require Import BinInt. +Require Import Zcompare. +Require Import Zorder. +Require Import Decidable. +Require Import Peano_dec. +Require Export Compare_dec. + +Open Local Scope Z_scope. + +Definition neq (x y:nat) := x <> y. + +(**********************************************************************) +(** Properties of the injection from nat into Z *) + +Theorem inj_S : forall n:nat, Z_of_nat (S n) = Zsucc (Z_of_nat n). +Proof. +intro y; induction y as [| n H]; + [ unfold Zsucc in |- *; simpl in |- *; trivial with arith + | change (Zpos (Psucc (P_of_succ_nat n)) = Zsucc (Z_of_nat (S n))) in |- *; + rewrite Zpos_succ_morphism; trivial with arith ]. +Qed. + +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]; + [ simpl in |- *; trivial with arith + | simpl in |- *; trivial with arith + | simpl in |- *; rewrite <- plus_n_O; trivial with arith + | change (Z_of_nat (S (n + S m)) = Z_of_nat (S n) + Z_of_nat (S m)) in |- *; + rewrite inj_S; rewrite H; do 2 rewrite inj_S; rewrite Zplus_succ_l; + trivial with arith ]. +Qed. + +Theorem inj_mult : 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]; + [ 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; + trivial with arith ]. +Qed. + +Theorem inj_neq : forall n m:nat, neq n m -> Zne (Z_of_nat n) (Z_of_nat m). +Proof. +unfold neq, Zne, not in |- *; intros x y H1 H2; apply H1; generalize H2; + case x; case y; intros; + [ auto with arith + | discriminate H0 + | discriminate H0 + | simpl in H0; injection H0; + do 2 rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ; + intros E; rewrite E; auto with arith ]. +Qed. + +Theorem inj_le : forall n m:nat, (n <= m)%nat -> Z_of_nat n <= Z_of_nat m. +Proof. +intros x y; intros H; elim H; + [ unfold Zle in |- *; elim (Zcompare_Eq_iff_eq (Z_of_nat x) (Z_of_nat x)); + intros H1 H2; rewrite H2; [ discriminate | trivial with arith ] + | intros m H1 H2; apply Zle_trans with (Z_of_nat m); + [ assumption | rewrite inj_S; apply Zle_succ ] ]. +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; + exact H. +Qed. + +Theorem inj_gt : forall n m:nat, (n > m)%nat -> Z_of_nat n > Z_of_nat m. +Proof. +intros x y H; apply Zlt_gt; apply inj_lt; exact H. +Qed. + +Theorem inj_ge : forall n m:nat, (n >= m)%nat -> Z_of_nat n >= Z_of_nat m. +Proof. +intros x y H; apply Zle_ge; apply inj_le; apply H. +Qed. + +Theorem inj_eq : forall n m:nat, n = m -> Z_of_nat n = Z_of_nat m. +Proof. +intros x y H; rewrite H; trivial with arith. +Qed. + +Theorem intro_Z : + forall n:nat, exists y : Z, Z_of_nat n = y /\ 0 <= y * 1 + 0. +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 |- *; + discriminate ]. +Qed. + +Theorem inj_minus1 : + forall n m:nat, (m <= n)%nat -> Z_of_nat (n - m) = Z_of_nat n - Z_of_nat m. +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; + 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 Zpos_eq_Z_of_nat_o_nat_of_P : + forall p:positive, Zpos p = Z_of_nat (nat_of_P p). +Proof. +intros x; elim x; simpl in |- *; auto. +intros p H; rewrite ZL6. +apply f_equal with (f := Zpos). +apply nat_of_P_inj. +rewrite nat_of_P_o_P_of_succ_nat_eq_succ; unfold nat_of_P in |- *; + simpl in |- *. +rewrite ZL6; auto. +intros p H; unfold nat_of_P in |- *; simpl in |- *. +rewrite ZL6; simpl in |- *. +rewrite inj_plus; repeat rewrite <- H. +rewrite Zpos_xO; simpl in |- *; rewrite Pplus_diag; reflexivity. +Qed. diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v new file mode 100644 index 00000000..715cdc7d --- /dev/null +++ b/theories/ZArith/Znumtheory.v @@ -0,0 +1,640 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(*i $Id: Znumtheory.v,v 1.5.2.1 2004/07/16 19:31:22 herbelin Exp $ i*) + +Require Import ZArith_base. +Require Import ZArithRing. +Require Import Zcomplements. +Require Import Zdiv. +Open Local Scope Z_scope. + +(** This file contains some notions of number theory upon Z numbers: + - a divisibility predicate [Zdivide] + - a gcd predicate [gcd] + - Euclid algorithm [euclid] + - an efficient [Zgcd] function + - a relatively prime predicate [rel_prime] + - a prime predicate [prime] +*) + +(** * Divisibility *) + +Inductive Zdivide (a b:Z) : Prop := + Zdivide_intro : forall q:Z, b = q * a -> Zdivide a b. + +(** Syntax for divisibility *) + +Notation "( a | b )" := (Zdivide a b) (at level 0) : Z_scope. + +(** Results concerning divisibility*) + +Lemma Zdivide_refl : forall a:Z, (a | a). +Proof. +intros; apply Zdivide_intro with 1; ring. +Qed. + +Lemma Zone_divide : forall a:Z, (1 | a). +Proof. +intros; apply Zdivide_intro with a; ring. +Qed. + +Lemma Zdivide_0 : forall a:Z, (a | 0). +Proof. +intros; apply Zdivide_intro with 0; ring. +Qed. + +Hint Resolve Zdivide_refl Zone_divide Zdivide_0: zarith. + +Lemma Zmult_divide_compat_l : forall a b c:Z, (a | b) -> (c * a | c * b). +Proof. +simple induction 1; intros; apply Zdivide_intro with q. +rewrite H0; ring. +Qed. + +Lemma Zmult_divide_compat_r : forall a b c:Z, (a | b) -> (a * c | b * c). +Proof. +intros a b c; rewrite (Zmult_comm a c); rewrite (Zmult_comm b c). +apply Zmult_divide_compat_l; trivial. +Qed. + +Hint Resolve Zmult_divide_compat_l Zmult_divide_compat_r: zarith. + +Lemma Zdivide_plus_r : forall a b c:Z, (a | b) -> (a | c) -> (a | b + c). +Proof. +simple induction 1; intros q Hq; simple induction 1; intros q' Hq'. +apply Zdivide_intro with (q + q'). +rewrite Hq; rewrite Hq'; ring. +Qed. + +Lemma Zdivide_opp_r : forall a b:Z, (a | b) -> (a | - b). +Proof. +simple induction 1; intros; apply Zdivide_intro with (- q). +rewrite H0; ring. +Qed. + +Lemma Zdivide_opp_r_rev : forall a b:Z, (a | - b) -> (a | b). +Proof. +intros; replace b with (- - b). apply Zdivide_opp_r; trivial. ring. +Qed. + +Lemma Zdivide_opp_l : forall a b:Z, (a | b) -> (- a | b). +Proof. +simple induction 1; intros; apply Zdivide_intro with (- q). +rewrite H0; ring. +Qed. + +Lemma Zdivide_opp_l_rev : forall a b:Z, (- a | b) -> (a | b). +Proof. +intros; replace a with (- - a). apply Zdivide_opp_l; trivial. ring. +Qed. + +Lemma Zdivide_minus_l : forall a b c:Z, (a | b) -> (a | c) -> (a | b - c). +Proof. +simple induction 1; intros q Hq; simple induction 1; intros q' Hq'. +apply Zdivide_intro with (q - q'). +rewrite Hq; rewrite Hq'; ring. +Qed. + +Lemma Zdivide_mult_l : forall a b c:Z, (a | b) -> (a | b * c). +Proof. +simple induction 1; intros q Hq; apply Zdivide_intro with (q * c). +rewrite Hq; ring. +Qed. + +Lemma Zdivide_mult_r : forall a b c:Z, (a | c) -> (a | b * c). +Proof. +simple induction 1; intros q Hq; apply Zdivide_intro with (q * b). +rewrite Hq; ring. +Qed. + +Lemma Zdivide_factor_r : forall a b:Z, (a | a * b). +Proof. +intros; apply Zdivide_intro with b; ring. +Qed. + +Lemma Zdivide_factor_l : forall a b:Z, (a | b * a). +Proof. +intros; apply Zdivide_intro with b; ring. +Qed. + +Hint Resolve Zdivide_plus_r Zdivide_opp_r Zdivide_opp_r_rev Zdivide_opp_l + Zdivide_opp_l_rev Zdivide_minus_l Zdivide_mult_l Zdivide_mult_r + Zdivide_factor_r Zdivide_factor_l: zarith. + +(** Auxiliary result. *) + +Lemma Zmult_one : forall x y:Z, x >= 0 -> x * y = 1 -> x = 1. +Proof. +intros x y H H0; destruct (Zmult_1_inversion_l _ _ H0) as [Hpos| Hneg]. + assumption. + rewrite Hneg in H; simpl in H. + contradiction (Zle_not_lt 0 (-1)). + apply Zge_le; assumption. + apply Zorder.Zlt_neg_0. +Qed. + +(** Only [1] and [-1] divide [1]. *) + +Lemma Zdivide_1 : forall x:Z, (x | 1) -> x = 1 \/ x = -1. +Proof. +simple induction 1; intros. +elim (Z_lt_ge_dec 0 x); [ left | right ]. +apply Zmult_one with q; auto with zarith; rewrite H0; ring. +assert (- x = 1); auto with zarith. +apply Zmult_one with (- q); auto with zarith; rewrite H0; ring. +Qed. + +(** If [a] divides [b] and [b] divides [a] then [a] is [b] or [-b]. *) + +Lemma Zdivide_antisym : forall a b:Z, (a | b) -> (b | a) -> a = b \/ a = - b. +Proof. +simple induction 1; intros. +inversion H1. +rewrite H0 in H2; clear H H1. +case (Z_zerop a); intro. +left; rewrite H0; rewrite e; ring. +assert (Hqq0 : q0 * q = 1). +apply Zmult_reg_l with a. +assumption. +ring. +pattern a at 2 in |- *; rewrite H2; ring. +assert (q | 1). +rewrite <- Hqq0; auto with zarith. +elim (Zdivide_1 q H); intros. +rewrite H1 in H0; left; omega. +rewrite H1 in H0; right; omega. +Qed. + +(** If [a] divides [b] and [b<>0] then [|a| <= |b|]. *) + +Lemma Zdivide_bounds : forall a b:Z, (a | b) -> b <> 0 -> Zabs a <= Zabs b. +Proof. +simple induction 1; intros. +assert (Zabs b = Zabs q * Zabs a). + subst; apply Zabs_Zmult. +rewrite H2. +assert (H3 := Zabs_pos q). +assert (H4 := Zabs_pos a). +assert (Zabs q * Zabs a >= 1 * Zabs a); auto with zarith. +apply Zmult_ge_compat; auto with zarith. +elim (Z_lt_ge_dec (Zabs q) 1); [ intros | auto with zarith ]. +assert (Zabs q = 0). + omega. +assert (q = 0). + rewrite <- (Zabs_Zsgn q). +rewrite H5; auto with zarith. +subst q; omega. +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]. + (We show later that the [gcd] is actually unique if we discard its sign.) *) + +Inductive Zis_gcd (a b d:Z) : Prop := + Zis_gcd_intro : + (d | a) -> + (d | b) -> (forall x:Z, (x | a) -> (x | b) -> (x | d)) -> Zis_gcd a b d. + +(** Trivial properties of [gcd] *) + +Lemma Zis_gcd_sym : forall a b d:Z, Zis_gcd a b d -> Zis_gcd b a d. +Proof. +simple induction 1; constructor; intuition. +Qed. + +Lemma Zis_gcd_0 : forall a:Z, Zis_gcd a 0 a. +Proof. +constructor; auto with zarith. +Qed. + +Lemma Zis_gcd_minus : forall a b d:Z, Zis_gcd a (- b) d -> Zis_gcd b a d. +Proof. +simple induction 1; constructor; intuition. +Qed. + +Lemma Zis_gcd_opp : forall a b d:Z, Zis_gcd a b d -> Zis_gcd b a (- d). +Proof. +simple induction 1; constructor; intuition. +Qed. + +Hint Resolve Zis_gcd_sym Zis_gcd_0 Zis_gcd_minus Zis_gcd_opp: zarith. + +(** * Extended Euclid algorithm. *) + +(** Euclid's algorithm to compute the [gcd] mainly relies on + the following property. *) + +Lemma Zis_gcd_for_euclid : + forall a b d q:Z, Zis_gcd b (a - q * b) d -> Zis_gcd a b d. +Proof. +simple induction 1; constructor; intuition. +replace a with (a - q * b + q * b). auto with zarith. ring. +Qed. + +Lemma Zis_gcd_for_euclid2 : + forall b d q r:Z, Zis_gcd r b d -> Zis_gcd b (b * q + r) d. +Proof. +simple induction 1; constructor; intuition. +apply H2; auto. +replace r with (b * q + r - b * q). auto with zarith. ring. +Qed. + +(** We implement the extended version of Euclid's algorithm, + i.e. the one computing Bezout's coefficients as it computes + the [gcd]. We follow the algorithm given in Knuth's + "Art of Computer Programming", vol 2, page 325. *) + +Section extended_euclid_algorithm. + +Variables a b : Z. + +(** The specification of Euclid's algorithm is the existence of + [u], [v] and [d] such that [ua+vb=d] and [(gcd a b d)]. *) + +Inductive Euclid : Set := + Euclid_intro : + forall u v d:Z, u * a + v * b = d -> Zis_gcd a b d -> Euclid. + +(** 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)]. + *) + +Lemma euclid_rec : + forall v3:Z, + 0 <= v3 -> + forall u1 u2 u3 v1 v2:Z, + u1 * a + u2 * b = u3 -> + v1 * a + v2 * b = v3 -> + (forall d:Z, Zis_gcd u3 v3 d -> Zis_gcd a b d) -> Euclid. +Proof. +intros v3 Hv3; generalize Hv3; pattern v3 in |- *. +apply Z_lt_rec. +clear v3 Hv3; intros. +elim (Z_zerop x); intro. +apply Euclid_intro with (u := u1) (v := u2) (d := u3). +assumption. +apply H2. +rewrite a0; auto with zarith. +set (q := u3 / x) in *. +assert (Hq : 0 <= u3 - q * x < x). +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 |- *. +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. +replace ((u1 - q * v1) * a + (u2 - q * v2) * b) with + (u1 * a + u2 * b - q * (v1 * a + v2 * b)). +rewrite H0; rewrite H1; trivial. +ring. +intros; apply H2. +apply Zis_gcd_for_euclid with q; assumption. +assumption. +Qed. + +(** We get Euclid's algorithm by applying [euclid_rec] on + [1,0,a,0,1,b] when [b>=0] and [1,0,a,0,-1,-b] when [b<0]. *) + +Lemma euclid : Euclid. +Proof. +case (Z_le_gt_dec 0 b); intro. +intros; + apply euclid_rec with + (u1 := 1) (u2 := 0) (u3 := a) (v1 := 0) (v2 := 1) (v3 := b); + auto with zarith; ring. +intros; + apply euclid_rec with + (u1 := 1) (u2 := 0) (u3 := a) (v1 := 0) (v2 := -1) (v3 := - b); + auto with zarith; try ring. +Qed. + +End extended_euclid_algorithm. + +Theorem Zis_gcd_uniqueness_apart_sign : + forall a b d d':Z, Zis_gcd a b d -> Zis_gcd a b d' -> d = d' \/ d = - d'. +Proof. +simple induction 1. +intros H1 H2 H3; simple induction 1; intros. +generalize (H3 d' H4 H5); intro Hd'd. +generalize (H6 d H1 H2); intro Hdd'. +exact (Zdivide_antisym d d' Hdd' Hd'd). +Qed. + +(** * Bezout's coefficients *) + +Inductive Bezout (a b d:Z) : Prop := + Bezout_intro : forall u v:Z, u * a + v * b = d -> Bezout a b d. + +(** Existence of Bezout's coefficients for the [gcd] of [a] and [b] *) + +Lemma Zis_gcd_bezout : forall a b d:Z, Zis_gcd a b d -> Bezout a b d. +Proof. +intros a b d Hgcd. +elim (euclid a b); intros u v d0 e g. +generalize (Zis_gcd_uniqueness_apart_sign a b d d0 Hgcd g). +intro H; elim H; clear H; intros. +apply Bezout_intro with u v. +rewrite H; assumption. +apply Bezout_intro with (- u) (- v). +rewrite H; rewrite <- e; ring. +Qed. + +(** gcd of [ca] and [cb] is [c gcd(a,b)]. *) + +Lemma Zis_gcd_mult : + forall a b c d:Z, Zis_gcd a b d -> Zis_gcd (c * a) (c * b) (c * d). +Proof. +intros a b c d; simple induction 1; constructor; intuition. +elim (Zis_gcd_bezout a b d H); intros. +elim H3; intros. +elim H4; intros. +apply Zdivide_intro with (u * q + v * q0). +rewrite <- H5. +replace (c * (u * a + v * b)) with (u * (c * a) + v * (c * b)). +rewrite H6; rewrite H7; ring. +ring. +Qed. + +(** We could obtain a [Zgcd] function via [euclid]. But we propose + here a more direct version of a [Zgcd], with better extraction + (no bezout coeffs). *) + +Definition Zgcd_pos : + forall a:Z, + 0 <= a -> forall b:Z, {g : Z | 0 <= a -> Zis_gcd a b g /\ g >= 0}. +Proof. +intros a Ha. +apply + (Z_lt_rec + (fun a:Z => forall b:Z, {g : Z | 0 <= a -> Zis_gcd a b g /\ g >= 0})); + try assumption. +intro x; case x. +intros _ b; exists (Zabs b). + elim (Z_le_lt_eq_dec _ _ (Zabs_pos b)). + intros H0; split. + apply Zabs_ind. + intros; apply Zis_gcd_sym; apply Zis_gcd_0; auto. + intros; apply Zis_gcd_opp; apply Zis_gcd_0; auto. + auto with zarith. + + intros H0; rewrite <- H0. + rewrite <- (Zabs_Zsgn b); rewrite <- H0; simpl in |- *. + split; [ apply Zis_gcd_0 | idtac ]; auto with zarith. + +intros p Hrec b. +generalize (Z_div_mod b (Zpos p)). +case (Zdiv_eucl b (Zpos p)); intros q r Hqr. +elim Hqr; clear Hqr; intros; auto with zarith. +elim (Hrec r H0 (Zpos p)); intros g Hgkl. +inversion_clear H0. +elim (Hgkl H1); clear Hgkl; intros H3 H4. +exists g; intros. +split; auto. +rewrite H. +apply Zis_gcd_for_euclid2; auto. + +intros p Hrec b. +exists 0; intros. +elim H; auto. +Defined. + +Definition Zgcd_spec : forall a b:Z, {g : Z | Zis_gcd a b g /\ g >= 0}. +Proof. +intros a; case (Z_gt_le_dec 0 a). +intros; assert (0 <= - a). +omega. +elim (Zgcd_pos (- a) H b); intros g Hgkl. +exists g. +intuition. +intros Ha b; elim (Zgcd_pos a Ha b); intros g; exists g; intuition. +Defined. + +Definition Zgcd (a b:Z) := let (g, _) := Zgcd_spec a b in g. + +Lemma Zgcd_is_pos : forall a b:Z, Zgcd a b >= 0. +intros a b; unfold Zgcd in |- *; case (Zgcd_spec a b); tauto. +Qed. + +Lemma Zgcd_is_gcd : forall a b:Z, Zis_gcd a b (Zgcd a b). +intros a b; unfold Zgcd in |- *; case (Zgcd_spec a b); tauto. +Qed. + +(** * Relative primality *) + +Definition rel_prime (a b:Z) : Prop := Zis_gcd a b 1. + +(** Bezout's theorem: [a] and [b] are relatively prime if and + only if there exist [u] and [v] such that [ua+vb = 1]. *) + +Lemma rel_prime_bezout : forall a b:Z, rel_prime a b -> Bezout a b 1. +Proof. +intros a b; exact (Zis_gcd_bezout a b 1). +Qed. + +Lemma bezout_rel_prime : forall a b:Z, Bezout a b 1 -> rel_prime a b. +Proof. +simple induction 1; constructor; auto with zarith. +intros. rewrite <- H0; auto with zarith. +Qed. + +(** Gauss's theorem: if [a] divides [bc] and if [a] and [b] are + relatively prime, then [a] divides [c]. *) + +Theorem Gauss : forall a b c:Z, (a | b * c) -> rel_prime a b -> (a | c). +Proof. +intros. elim (rel_prime_bezout a b H0); intros. +replace c with (c * 1); [ idtac | ring ]. +rewrite <- H1. +replace (c * (u * a + v * b)) with (c * u * a + v * (b * c)); + [ eauto with zarith | ring ]. +Qed. + +(** If [a] is relatively prime to [b] and [c], then it is to [bc] *) + +Lemma rel_prime_mult : + forall a b c:Z, rel_prime a b -> rel_prime a c -> rel_prime a (b * c). +Proof. +intros a b c Hb Hc. +elim (rel_prime_bezout a b Hb); intros. +elim (rel_prime_bezout a c Hc); intros. +apply bezout_rel_prime. +apply Bezout_intro with + (u := u * u0 * a + v0 * c * u + u0 * v * b) (v := v * v0). +rewrite <- H. +replace (u * a + v * b) with ((u * a + v * b) * 1); [ idtac | ring ]. +rewrite <- H0. +ring. +Qed. + +Lemma rel_prime_cross_prod : + forall a b c d:Z, + rel_prime a b -> + rel_prime c d -> b > 0 -> d > 0 -> a * d = b * c -> a = c /\ b = d. +Proof. +intros a b c d; intros. +elim (Zdivide_antisym b d). +split; auto with zarith. +rewrite H4 in H3. +rewrite Zmult_comm in H3. +apply Zmult_reg_l with d; auto with zarith. +intros; omega. +apply Gauss with a. +rewrite H3. +auto with zarith. +red in |- *; auto with zarith. +apply Gauss with c. +rewrite Zmult_comm. +rewrite <- H3. +auto with zarith. +red in |- *; auto with zarith. +Qed. + +(** After factorization by a gcd, the original numbers are relatively prime. *) + +Lemma Zis_gcd_rel_prime : + forall a b g:Z, + b > 0 -> g >= 0 -> Zis_gcd a b g -> rel_prime (a / g) (b / g). +intros a b g; intros. +assert (g <> 0). + intro. + elim H1; intros. + elim H4; intros. + rewrite H2 in H6; subst b; omega. +unfold rel_prime in |- *. +elim (Zgcd_spec (a / g) (b / g)); intros g' [H3 H4]. +assert (H5 := Zis_gcd_mult _ _ g _ H3). +rewrite <- Z_div_exact_2 in H5; auto with zarith. +rewrite <- Z_div_exact_2 in H5; auto with zarith. +elim (Zis_gcd_uniqueness_apart_sign _ _ _ _ H1 H5). +intros; rewrite (Zmult_reg_l 1 g' g); auto with zarith. +intros; rewrite (Zmult_reg_l 1 (- g') g); auto with zarith. +pattern g at 1 in |- *; rewrite H6; ring. + +elim H1; intros. +elim H7; intros. +rewrite H9. +replace (q * g) with (0 + q * g). +rewrite Z_mod_plus. +compute in |- *; auto. +omega. +ring. + +elim H1; intros. +elim H6; intros. +rewrite H9. +replace (q * g) with (0 + q * g). +rewrite Z_mod_plus. +compute in |- *; auto. +omega. +ring. +Qed. + +(** * Primality *) + +Inductive prime (p:Z) : Prop := + prime_intro : + 1 < p -> (forall n:Z, 1 <= n < p -> rel_prime n p) -> prime p. + +(** The sole divisors of a prime number [p] are [-1], [1], [p] and [-p]. *) + +Lemma prime_divisors : + forall p:Z, + prime p -> forall a:Z, (a | p) -> a = -1 \/ a = 1 \/ a = p \/ a = - p. +Proof. +simple induction 1; intros. +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. +pattern (Zabs a) in |- *; apply Zabs_ind; pattern (Zabs p) in |- *; + apply Zabs_ind; intros; omega. +intuition idtac. +(* -p < a < -1 *) +absurd (rel_prime (- a) p); intuition. +inversion H3. +assert (- a | - a); auto with zarith. +assert (- a | p); auto with zarith. +generalize (H8 (- a) H9 H10); intuition idtac. +generalize (Zdivide_1 (- a) H11); intuition. +(* a = 0 *) +inversion H2. subst a; omega. +(* 1 < a < p *) +absurd (rel_prime a p); intuition. +inversion H3. +assert (a | a); auto with zarith. +assert (a | p); auto with zarith. +generalize (H8 a H9 H10); intuition idtac. +generalize (Zdivide_1 a H11); intuition. +Qed. + +(** A prime number is relatively prime with any number it does not divide *) + +Lemma prime_rel_prime : + forall p:Z, prime p -> forall a:Z, ~ (p | a) -> rel_prime p a. +Proof. +simple induction 1; intros. +constructor; intuition. +elim (prime_divisors p H x H3); intuition; subst; auto with zarith. +absurd (p | a); auto with zarith. +absurd (p | a); intuition. +Qed. + +Hint Resolve prime_rel_prime: zarith. + +(** [Zdivide] can be expressed using [Zmod]. *) + +Lemma Zmod_divide : forall a b:Z, b > 0 -> a mod b = 0 -> (b | a). +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. +Qed. + +Lemma Zdivide_mod : forall a b:Z, b > 0 -> (b | a) -> a mod b = 0. +intros a b; simple destruct 2; intros; subst. +change (q * b) with (0 + q * b) in |- *. +rewrite Z_mod_plus; auto. +Qed. + +(** [Zdivide] is hence decidable *) + +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. +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. +(* a=0 *) +case (Z_eq_dec b 0); intro. +left; subst; auto with zarith. +right; subst; intro H0; inversion H0; omega. +(* a>0 *) +intro H; case (Z_eq_dec (b mod a) 0). +left; apply Zmod_divide; auto with zarith. +intro H1; right; intro; elim H1; apply Zdivide_mod; auto with zarith. +Qed. + +(** If a prime [p] divides [ab] then it divides either [a] or [b] *) + +Lemma prime_mult : + forall p:Z, prime p -> forall a b:Z, (p | a * b) -> (p | a) \/ (p | b). +Proof. +intro p; simple induction 1; intros. +case (Zdivide_dec p a); intuition. +right; apply Gauss with a; auto with zarith. +Qed. + diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v new file mode 100644 index 00000000..55d4d958 --- /dev/null +++ b/theories/ZArith/Zorder.v @@ -0,0 +1,965 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) +(*i $Id: Zorder.v,v 1.6.2.1 2004/07/16 19:31:22 herbelin Exp $ i*) + +(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *) + +Require Import BinPos. +Require Import BinInt. +Require Import Arith. +Require Import Decidable. +Require Import Zcompare. + +Open Local Scope Z_scope. + +Implicit Types x y z : Z. + +(**********************************************************************) +(** Properties of the order relations on binary integers *) + +(** Trichotomy *) + +Theorem Ztrichotomy_inf : forall n m:Z, {n < m} + {n = m} + {n > m}. +Proof. +unfold Zgt, Zlt in |- *; intros m n; assert (H := refl_equal (m ?= n)). + set (x := m ?= n) in H at 2 |- *. + destruct x; + [ left; right; rewrite Zcompare_Eq_eq with (1 := H) | left; left | right ]; + reflexivity. +Qed. + +Theorem Ztrichotomy : forall n m:Z, n < m \/ n = m \/ n > m. +Proof. + intros m n; destruct (Ztrichotomy_inf m n) as [[Hlt| Heq]| Hgt]; + [ left | right; left | right; right ]; assumption. +Qed. + +(**********************************************************************) +(** Decidability of equality and order on Z *) + +Theorem dec_eq : forall n m:Z, decidable (n = m). +Proof. +intros x y; unfold decidable in |- *; elim (Zcompare_Eq_iff_eq x y); + intros H1 H2; elim (Dcompare (x ?= y)); + [ tauto + | intros H3; right; unfold not in |- *; intros H4; elim H3; rewrite (H2 H4); + intros H5; discriminate H5 ]. +Qed. + +Theorem dec_Zne : forall n m:Z, decidable (Zne n m). +Proof. +intros x y; unfold decidable, Zne in |- *; elim (Zcompare_Eq_iff_eq x y). +intros H1 H2; elim (Dcompare (x ?= y)); + [ right; rewrite H1; auto + | left; unfold not in |- *; intro; absurd ((x ?= y) = Eq); + [ elim H; intros HR; rewrite HR; discriminate | auto ] ]. +Qed. + +Theorem dec_Zle : forall n m:Z, decidable (n <= m). +Proof. +intros x y; unfold decidable, Zle in |- *; elim (x ?= y); + [ left; discriminate + | left; discriminate + | right; unfold not in |- *; intros H; apply H; trivial with arith ]. +Qed. + +Theorem dec_Zgt : forall n m:Z, decidable (n > m). +Proof. +intros x y; unfold decidable, Zgt in |- *; elim (x ?= y); + [ right; discriminate | right; discriminate | auto with arith ]. +Qed. + +Theorem dec_Zge : forall n m:Z, decidable (n >= m). +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 ]. +Qed. + +Theorem dec_Zlt : forall n m:Z, decidable (n < m). +Proof. +intros x y; unfold decidable, Zlt in |- *; elim (x ?= y); + [ right; discriminate | auto with arith | right; discriminate ]. +Qed. + +Theorem not_Zeq : forall n m:Z, n <> m -> n < m \/ m < n. +Proof. +intros x y; elim (Dcompare (x ?= y)); + [ intros H1 H2; absurd (x = y); + [ assumption | elim (Zcompare_Eq_iff_eq x y); auto with arith ] + | unfold Zlt in |- *; intros H; elim H; intros H1; + [ auto with arith + | right; elim (Zcompare_Gt_Lt_antisym x y); auto with arith ] ]. +Qed. + +(** Relating strict and large orders *) + +Lemma Zgt_lt : forall n m:Z, n > m -> m < n. +Proof. +unfold Zgt, Zlt in |- *; intros m n H; elim (Zcompare_Gt_Lt_antisym m n); + auto with arith. +Qed. + +Lemma Zlt_gt : forall n m:Z, n < m -> m > n. +Proof. +unfold Zgt, Zlt in |- *; intros m n H; elim (Zcompare_Gt_Lt_antisym n m); + auto with arith. +Qed. + +Lemma Zge_le : forall n m:Z, n >= m -> m <= n. +Proof. +intros m n; change (~ m < n -> ~ n > m) in |- *; unfold not in |- *; + intros H1 H2; apply H1; apply Zgt_lt; assumption. +Qed. + +Lemma Zle_ge : forall n m:Z, n <= m -> m >= n. +Proof. +intros m n; change (~ m > n -> ~ n < m) in |- *; unfold not in |- *; + intros H1 H2; apply H1; apply Zlt_gt; assumption. +Qed. + +Lemma Zle_not_gt : forall n m:Z, n <= m -> ~ n > m. +Proof. +trivial. +Qed. + +Lemma Zgt_not_le : forall n m:Z, n > m -> ~ n <= m. +Proof. +intros n m H1 H2; apply H2; assumption. +Qed. + +Lemma Zle_not_lt : forall n m:Z, n <= m -> ~ m < n. +Proof. +intros n m H1 H2. +assert (H3 := Zlt_gt _ _ H2). +apply Zle_not_gt with n m; assumption. +Qed. + +Lemma Zlt_not_le : forall n m:Z, n < m -> ~ m <= n. +Proof. +intros n m H1 H2. +apply Zle_not_lt with m n; assumption. +Qed. + +Lemma Znot_ge_lt : forall n m:Z, ~ n >= m -> n < m. +Proof. +unfold Zge, Zlt in |- *; intros x y H; apply dec_not_not; + [ exact (dec_Zlt x y) | assumption ]. +Qed. + +Lemma Znot_lt_ge : forall n m:Z, ~ n < m -> n >= m. +Proof. +unfold Zlt, Zge in |- *; auto with arith. +Qed. + +Lemma Znot_gt_le : forall n m:Z, ~ n > m -> n <= m. +Proof. +trivial. +Qed. + +Lemma Znot_le_gt : forall n m:Z, ~ n <= m -> n > m. +Proof. +unfold Zle, Zgt in |- *; intros x y H; apply dec_not_not; + [ exact (dec_Zgt x y) | assumption ]. +Qed. + +Lemma Zge_iff_le : forall n m:Z, n >= m <-> m <= n. +Proof. + intros x y; intros. split. intro. apply Zge_le. assumption. + intro. apply Zle_ge. assumption. +Qed. + +Lemma Zgt_iff_lt : forall n m:Z, n > m <-> m < n. +Proof. + intros x y. split. intro. apply Zgt_lt. assumption. + intro. apply Zlt_gt. assumption. +Qed. + +(** Reflexivity *) + +Lemma Zle_refl : forall n:Z, n <= n. +Proof. +intros n; unfold Zle in |- *; rewrite (Zcompare_refl n); discriminate. +Qed. + +Lemma Zeq_le : forall n m:Z, n = m -> n <= m. +Proof. +intros; rewrite H; apply Zle_refl. +Qed. + +Hint Resolve Zle_refl: zarith. + +(** Antisymmetry *) + +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]]. + absurd (m > n); [ apply Zle_not_gt | apply Zlt_gt ]; assumption. + assumption. + absurd (n > m); [ apply Zle_not_gt | idtac ]; assumption. +Qed. + +(** Asymmetry *) + +Lemma Zgt_asym : forall n m:Z, n > m -> ~ m > n. +Proof. +unfold Zgt in |- *; intros n m H; elim (Zcompare_Gt_Lt_antisym n m); + intros H1 H2; rewrite H1; [ discriminate | assumption ]. +Qed. + +Lemma Zlt_asym : forall n m:Z, n < m -> ~ m < n. +Proof. +intros n m H H1; assert (H2 : m > n). apply Zlt_gt; assumption. +assert (H3 : n > m). apply Zlt_gt; assumption. +apply Zgt_asym with m n; assumption. +Qed. + +(** Irreflexivity *) + +Lemma Zgt_irrefl : forall n:Z, ~ n > n. +Proof. +intros n H; apply (Zgt_asym n n H H). +Qed. + +Lemma Zlt_irrefl : forall n:Z, ~ n < n. +Proof. +intros n H; apply (Zlt_asym n n H H). +Qed. + +Lemma Zlt_not_eq : forall n m:Z, n < m -> n <> m. +Proof. +unfold not in |- *; intros x y H H0. +rewrite H0 in H. +apply (Zlt_irrefl _ H). +Qed. + +(** Large = strict or equal *) + +Lemma Zlt_le_weak : forall n m:Z, n < m -> n <= m. +Proof. +intros n m Hlt; apply Znot_gt_le; apply Zgt_asym; apply Zlt_gt; assumption. +Qed. + +Lemma Zle_lt_or_eq : forall n m:Z, n <= m -> n < m \/ n = m. +Proof. +intros n m H; destruct (Ztrichotomy n m) as [Hlt| [Heq| Hgt]]; + [ left; assumption + | right; assumption + | absurd (n > m); [ apply Zle_not_gt | idtac ]; assumption ]. +Qed. + +(** Dichotomy *) + +Lemma Zle_or_lt : forall n m:Z, n <= m \/ m < n. +Proof. +intros n m; destruct (Ztrichotomy n m) as [Hlt| [Heq| Hgt]]; + [ left; apply Znot_gt_le; intro Hgt; assert (Hgt' := Zlt_gt _ _ Hlt); + apply Zgt_asym with m n; assumption + | left; rewrite Heq; apply Zle_refl + | right; apply Zgt_lt; assumption ]. +Qed. + +(** Transitivity of strict orders *) + +Lemma Zgt_trans : forall n m p:Z, n > m -> m > p -> n > p. +Proof. +exact Zcompare_Gt_trans. +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. +Qed. + +(** Mixed transitivity *) + +Lemma Zle_gt_trans : forall n m p:Z, m <= n -> m > p -> n > p. +Proof. +intros n m p H1 H2; destruct (Zle_lt_or_eq m n H1) as [Hlt| Heq]; + [ apply Zgt_trans with m; [ apply Zlt_gt; assumption | assumption ] + | rewrite <- Heq; assumption ]. +Qed. + +Lemma Zgt_le_trans : forall n m p:Z, n > m -> p <= m -> n > p. +Proof. +intros n m p H1 H2; destruct (Zle_lt_or_eq p m H2) as [Hlt| Heq]; + [ apply Zgt_trans with m; [ assumption | apply Zlt_gt; assumption ] + | rewrite Heq; assumption ]. +Qed. + +Lemma Zlt_le_trans : forall n m p:Z, n < m -> m <= p -> n < p. +intros n m p H1 H2; apply Zgt_lt; apply Zle_gt_trans with (m := m); + [ assumption | apply Zlt_gt; assumption ]. +Qed. + +Lemma Zle_lt_trans : forall n m p:Z, n <= m -> m < p -> n < p. +Proof. +intros n m p H1 H2; apply Zgt_lt; apply Zgt_le_trans with (m := m); + [ apply Zlt_gt; assumption | assumption ]. +Qed. + +(** Transitivity of large orders *) + +Lemma Zle_trans : forall n m p:Z, n <= m -> m <= p -> n <= p. +Proof. +intros n m p H1 H2; apply Znot_gt_le. +intro Hgt; apply Zle_not_gt with n m. assumption. +exact (Zgt_le_trans n p m Hgt H2). +Qed. + +Lemma Zge_trans : forall n m p:Z, n >= m -> m >= p -> n >= p. +Proof. +intros n m p H1 H2. +apply Zle_ge. +apply Zle_trans with m; apply Zge_le; trivial. +Qed. + +Hint Resolve Zle_trans: zarith. + +(** Compatibility of successor wrt to order *) + +Lemma Zsucc_le_compat : forall n m:Z, m <= n -> Zsucc m <= Zsucc n. +Proof. +unfold Zle, not in |- *; intros m n H1 H2; apply H1; + rewrite <- (Zcompare_plus_compat n m 1); do 2 rewrite (Zplus_comm 1); + exact H2. +Qed. + +Lemma Zsucc_gt_compat : forall n m:Z, m > n -> Zsucc m > Zsucc n. +Proof. +unfold Zgt in |- *; intros n m H; rewrite Zcompare_succ_compat; + auto with arith. +Qed. + +Lemma Zsucc_lt_compat : forall n m:Z, n < m -> Zsucc n < Zsucc m. +Proof. +intros n m H; apply Zgt_lt; apply Zsucc_gt_compat; apply Zlt_gt; assumption. +Qed. + +Hint Resolve Zsucc_le_compat: zarith. + +(** Simplification of successor wrt to order *) + +Lemma Zsucc_gt_reg : forall n m:Z, Zsucc m > Zsucc n -> m > n. +Proof. +unfold Zsucc, Zgt in |- *; intros n p; + do 2 rewrite (fun m:Z => Zplus_comm m 1); + rewrite (Zcompare_plus_compat p n 1); trivial with arith. +Qed. + +Lemma Zsucc_le_reg : forall n m:Z, Zsucc m <= Zsucc n -> m <= n. +Proof. +unfold Zle, not in |- *; intros m n H1 H2; apply H1; unfold Zsucc in |- *; + do 2 rewrite <- (Zplus_comm 1); rewrite (Zcompare_plus_compat n m 1); + assumption. +Qed. + +Lemma Zsucc_lt_reg : forall n m:Z, Zsucc n < Zsucc m -> n < m. +Proof. +intros n m H; apply Zgt_lt; apply Zsucc_gt_reg; apply Zlt_gt; assumption. +Qed. + +(** Compatibility of addition wrt to order *) + +Lemma Zplus_gt_compat_l : forall n m p:Z, n > m -> p + n > p + m. +Proof. +unfold Zgt in |- *; intros n m p H; rewrite (Zcompare_plus_compat n m p); + assumption. +Qed. + +Lemma Zplus_gt_compat_r : forall n m p:Z, n > m -> n + p > m + p. +Proof. +intros n m p H; rewrite (Zplus_comm n p); rewrite (Zplus_comm m p); + apply Zplus_gt_compat_l; trivial. +Qed. + +Lemma Zplus_le_compat_l : forall n m p:Z, n <= m -> p + n <= p + m. +Proof. +intros n m p; unfold Zle, not in |- *; intros H1 H2; apply H1; + rewrite <- (Zcompare_plus_compat n m p); assumption. +Qed. + +Lemma Zplus_le_compat_r : forall n m p:Z, n <= m -> n + p <= m + p. +Proof. +intros a b c; do 2 rewrite (fun n:Z => Zplus_comm n c); + exact (Zplus_le_compat_l a b c). +Qed. + +Lemma Zplus_lt_compat_l : forall n m p:Z, n < m -> p + n < p + m. +Proof. +unfold Zlt in |- *; intros n m p; rewrite Zcompare_plus_compat; + trivial with arith. +Qed. + +Lemma Zplus_lt_compat_r : forall n m p:Z, n < m -> n + p < m + p. +Proof. +intros n m p H; rewrite (Zplus_comm n p); rewrite (Zplus_comm m p); + apply Zplus_lt_compat_l; trivial. +Qed. + +Lemma Zplus_lt_le_compat : forall n m p q:Z, n < m -> p <= q -> n + p < m + q. +Proof. +intros a b c d H0 H1. +apply Zlt_le_trans with (b + c). +apply Zplus_lt_compat_r; trivial. +apply Zplus_le_compat_l; trivial. +Qed. + +Lemma Zplus_le_lt_compat : forall n m p q:Z, n <= m -> p < q -> n + p < m + q. +Proof. +intros a b c d H0 H1. +apply Zle_lt_trans with (b + c). +apply Zplus_le_compat_r; trivial. +apply Zplus_lt_compat_l; trivial. +Qed. + +Lemma Zplus_le_compat : forall n m p q:Z, n <= m -> p <= q -> n + p <= m + q. +Proof. +intros n m p q; intros H1 H2; apply Zle_trans with (m := n + q); + [ apply Zplus_le_compat_l; assumption + | apply Zplus_le_compat_r; assumption ]. +Qed. + + +Lemma Zplus_lt_compat : forall n m p q:Z, n < m -> p < q -> n + p < m + q. +intros; apply Zplus_le_lt_compat. apply Zlt_le_weak; assumption. assumption. +Qed. + + +(** Compatibility of addition wrt to being positive *) + +Lemma Zplus_le_0_compat : forall n m:Z, 0 <= n -> 0 <= m -> 0 <= n + m. +Proof. +intros x y H1 H2; rewrite <- (Zplus_0_l 0); apply Zplus_le_compat; assumption. +Qed. + +(** Simplification of addition wrt to order *) + +Lemma Zplus_gt_reg_l : forall n m p:Z, p + n > p + m -> n > m. +Proof. +unfold Zgt in |- *; intros n m p H; rewrite <- (Zcompare_plus_compat n m p); + assumption. +Qed. + +Lemma Zplus_gt_reg_r : forall n m p:Z, n + p > m + p -> n > m. +Proof. +intros n m p H; apply Zplus_gt_reg_l with p. +rewrite (Zplus_comm p n); rewrite (Zplus_comm p m); trivial. +Qed. + +Lemma Zplus_le_reg_l : forall n m p:Z, p + n <= p + m -> n <= m. +Proof. +intros n m p; unfold Zle, not in |- *; intros H1 H2; apply H1; + rewrite (Zcompare_plus_compat n m p); assumption. +Qed. + +Lemma Zplus_le_reg_r : forall n m p:Z, n + p <= m + p -> n <= m. +Proof. +intros n m p H; apply Zplus_le_reg_l with p. +rewrite (Zplus_comm p n); rewrite (Zplus_comm p m); trivial. +Qed. + +Lemma Zplus_lt_reg_l : forall n m p:Z, p + n < p + m -> n < m. +Proof. +unfold Zlt in |- *; intros n m p; rewrite Zcompare_plus_compat; + trivial with arith. +Qed. + +Lemma Zplus_lt_reg_r : forall n m p:Z, n + p < m + p -> n < m. +Proof. +intros n m p H; apply Zplus_lt_reg_l with p. +rewrite (Zplus_comm p n); rewrite (Zplus_comm p m); trivial. +Qed. + +(** Special base instances of order *) + +Lemma Zgt_succ : forall n:Z, Zsucc n > n. +Proof. +exact Zcompare_succ_Gt. +Qed. + +Lemma Znot_le_succ : forall n:Z, ~ Zsucc n <= n. +Proof. +intros n; apply Zgt_not_le; apply Zgt_succ. +Qed. + +Lemma Zlt_succ : forall n:Z, n < Zsucc n. +Proof. +intro n; apply Zgt_lt; apply Zgt_succ. +Qed. + +Lemma Zlt_pred : forall n:Z, Zpred n < n. +Proof. +intros n; apply Zsucc_lt_reg; rewrite <- Zsucc_pred; apply Zlt_succ. +Qed. + +(** Relating strict and large order using successor or predecessor *) + +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; + 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. +Proof. +intros n p H; apply Zgt_le_trans with p. + apply Zgt_succ. + assumption. +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. +Qed. + +Lemma Zlt_le_succ : forall n m:Z, n < m -> Zsucc n <= m. +Proof. +intros n p H; apply Zgt_le_succ; apply Zlt_gt; assumption. +Qed. + +Lemma Zgt_succ_le : forall n m:Z, Zsucc m > n -> n <= m. +Proof. +intros n p H; apply Zsucc_le_reg; apply Zgt_le_succ; assumption. +Qed. + +Lemma Zlt_succ_le : forall n m:Z, n < Zsucc m -> n <= m. +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. +Proof. +intros n m H; apply Zle_gt_trans with (m := Zsucc n); + [ assumption | apply Zgt_succ ]. +Qed. + +(** Weakening order *) + +Lemma Zle_succ : forall n:Z, n <= Zsucc n. +Proof. +intros n; apply Zgt_succ_le; apply Zgt_trans with (m := Zsucc n); + apply Zgt_succ. +Qed. + +Hint Resolve Zle_succ: zarith. + +Lemma Zle_pred : forall n:Z, Zpred n <= n. +Proof. +intros n; pattern n at 2 in |- *; rewrite Zsucc_pred; apply Zle_succ. +Qed. + +Lemma Zlt_lt_succ : forall n m:Z, n < m -> n < Zsucc m. +intros n m H; apply Zgt_lt; apply Zgt_trans with (m := m); + [ apply Zgt_succ | apply Zlt_gt; assumption ]. +Qed. + +Lemma Zle_le_succ : forall n m:Z, n <= m -> n <= Zsucc m. +Proof. +intros x y H. +apply Zle_trans with y; trivial with zarith. +Qed. + +Lemma Zle_succ_le : forall n m:Z, Zsucc n <= m -> n <= m. +Proof. +intros n m H; apply Zle_trans with (m := Zsucc n); + [ apply Zle_succ | assumption ]. +Qed. + +Hint Resolve Zle_le_succ: zarith. + +(** Relating order wrt successor and order wrt predecessor *) + +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 (Zplus_comm p); rewrite Zplus_assoc; + rewrite (fun x => Zplus_comm x n); simpl in |- *; + assumption. +Qed. + +Lemma Zlt_succ_pred : forall n m:Z, Zsucc n < m -> n < Zpred m. +Proof. +intros n p H; apply Zsucc_lt_reg; rewrite <- Zsucc_pred; assumption. +Qed. + +(** Relating strict order and large order on positive *) + +Lemma Zlt_0_le_0_pred : forall n:Z, 0 < n -> 0 <= Zpred n. +intros x H. +rewrite (Zsucc_pred x) in H. +apply Zgt_succ_le. +apply Zlt_gt. +assumption. +Qed. + + +Lemma Zgt_0_le_0_pred : forall n:Z, n > 0 -> 0 <= Zpred n. +intros; apply Zlt_0_le_0_pred; apply Zgt_lt. assumption. +Qed. + + +(** Special cases of ordered integers *) + +Lemma Zlt_0_1 : 0 < 1. +Proof. +change (0 < Zsucc 0) in |- *. apply Zlt_succ. +Qed. + +Lemma Zle_0_1 : 0 <= 1. +Proof. +change (0 <= Zsucc 0) in |- *. apply Zle_succ. +Qed. + +Lemma Zle_neg_pos : forall p q:positive, Zneg p <= Zpos q. +Proof. +intros p; red in |- *; simpl in |- *; red in |- *; intros H; discriminate. +Qed. + +Lemma Zgt_pos_0 : forall p:positive, Zpos p > 0. +unfold Zgt in |- *; trivial. +Qed. + + (* weaker but useful (in [Zpower] for instance) *) +Lemma Zle_0_pos : forall p:positive, 0 <= Zpos p. +intro; unfold Zle in |- *; discriminate. +Qed. + +Lemma Zlt_neg_0 : forall p:positive, Zneg p < 0. +unfold Zlt in |- *; trivial. +Qed. + +Lemma Zle_0_nat : forall n:nat, 0 <= Z_of_nat n. +simple induction n; simpl in |- *; intros; + [ apply Zle_refl | unfold Zle in |- *; simpl in |- *; discriminate ]. +Qed. + +Hint Immediate Zeq_le: zarith. + +(** Transitivity using successor *) + +Lemma Zge_trans_succ : forall n m p:Z, Zsucc n > m -> m > p -> n > p. +Proof. +intros n m p H1 H2; apply Zle_gt_trans with (m := m); + [ apply Zgt_succ_le; assumption | assumption ]. +Qed. + +(** Derived lemma *) + +Lemma Zgt_succ_gt_or_eq : forall n m:Z, Zsucc n > m -> n > m \/ m = n. +Proof. +intros n m H. +assert (Hle : m <= n). + apply Zgt_succ_le; assumption. +destruct (Zle_lt_or_eq _ _ Hle) as [Hlt| Heq]. + left; apply Zlt_gt; assumption. + right; assumption. +Qed. + +(** 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. +Proof. +intros a b c H H0; destruct c. + do 2 rewrite Zmult_0_r; assumption. + rewrite (Zmult_comm a); rewrite (Zmult_comm b). + unfold Zle in |- *; rewrite Zcompare_mult_compat; assumption. + unfold Zle in H0; contradiction H0; reflexivity. +Qed. + +Lemma Zmult_le_compat_l : forall n m p:Z, n <= m -> 0 <= p -> p * n <= p * m. +Proof. +intros a b c H1 H2; rewrite (Zmult_comm c a); rewrite (Zmult_comm c b). +apply Zmult_le_compat_r; trivial. +Qed. + +Lemma Zmult_lt_compat_r : forall n m p:Z, 0 < p -> n < m -> n * p < m * p. +Proof. +intros x y z H H0; destruct z. + contradiction (Zlt_irrefl 0). + rewrite (Zmult_comm x); rewrite (Zmult_comm y). + unfold Zlt in |- *; rewrite Zcompare_mult_compat; assumption. + discriminate H. +Qed. + +Lemma Zmult_gt_compat_r : forall n m p:Z, p > 0 -> n > m -> n * p > m * p. +Proof. +intros x y z; intros; apply Zlt_gt; apply Zmult_lt_compat_r; apply Zgt_lt; + assumption. +Qed. + +Lemma Zmult_gt_0_lt_compat_r : + forall n m p:Z, p > 0 -> n < m -> n * p < m * p. +Proof. +intros x y z; intros; apply Zmult_lt_compat_r; + [ apply Zgt_lt; assumption | assumption ]. +Qed. + +Lemma Zmult_gt_0_le_compat_r : + forall n m p:Z, p > 0 -> n <= m -> n * p <= m * p. +Proof. +intros x y z Hz Hxy. +elim (Zle_lt_or_eq x y Hxy). +intros; apply Zlt_le_weak. +apply Zmult_gt_0_lt_compat_r; trivial. +intros; apply Zeq_le. +rewrite H; trivial. +Qed. + +Lemma Zmult_lt_0_le_compat_r : + forall n m p:Z, 0 < p -> n <= m -> n * p <= m * p. +Proof. +intros x y z; intros; apply Zmult_gt_0_le_compat_r; try apply Zlt_gt; + assumption. +Qed. + +Lemma Zmult_gt_0_lt_compat_l : + forall n m p:Z, p > 0 -> n < m -> p * n < p * m. +Proof. +intros x y z; intros. +rewrite (Zmult_comm z x); rewrite (Zmult_comm z y); + apply Zmult_gt_0_lt_compat_r; assumption. +Qed. + +Lemma Zmult_lt_compat_l : forall n m p:Z, 0 < p -> n < m -> p * n < p * m. +Proof. +intros x y z; intros. +rewrite (Zmult_comm z x); rewrite (Zmult_comm z y); + apply Zmult_gt_0_lt_compat_r; try apply Zlt_gt; assumption. +Qed. + +Lemma Zmult_gt_compat_l : forall n m p:Z, p > 0 -> n > m -> p * n > p * m. +Proof. +intros x y z; intros; rewrite (Zmult_comm z x); rewrite (Zmult_comm z y); + apply Zmult_gt_compat_r; assumption. +Qed. + +Lemma Zmult_ge_compat_r : forall n m p:Z, n >= m -> p >= 0 -> n * p >= m * p. +Proof. +intros a b c H1 H2; apply Zle_ge. +apply Zmult_le_compat_r; apply Zge_le; trivial. +Qed. + +Lemma Zmult_ge_compat_l : forall n m p:Z, n >= m -> p >= 0 -> p * n >= p * m. +Proof. +intros a b c H1 H2; apply Zle_ge. +apply Zmult_le_compat_l; apply Zge_le; trivial. +Qed. + +Lemma Zmult_ge_compat : + forall n m p q:Z, n >= p -> m >= q -> p >= 0 -> q >= 0 -> n * m >= p * q. +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 Zmult_ge_compat_r; trivial. +Qed. + +Lemma Zmult_le_compat : + forall n m p q:Z, n <= p -> m <= q -> 0 <= n -> 0 <= m -> n * m <= p * q. +Proof. +intros a b c d H0 H1 H2 H3. +apply Zle_trans with (c * b). +apply Zmult_le_compat_r; assumption. +apply Zmult_le_compat_l. +assumption. +apply Zle_trans with a; assumption. +Qed. + +(** Simplification of multiplication by a positive wrt to being positive *) + +Lemma Zmult_gt_0_lt_reg_r : forall n m p:Z, p > 0 -> n * p < m * p -> n < m. +Proof. +intros x y z; intros; destruct z. + contradiction (Zgt_irrefl 0). + rewrite (Zmult_comm x) in H0; rewrite (Zmult_comm y) in H0. + unfold Zlt in H0; rewrite Zcompare_mult_compat in H0; assumption. + discriminate H. +Qed. + +Lemma Zmult_lt_reg_r : forall n m p:Z, 0 < p -> n * p < m * p -> n < m. +Proof. +intros a b c H0 H1. +apply Zmult_gt_0_lt_reg_r with c; try apply Zlt_gt; assumption. +Qed. + +Lemma Zmult_le_reg_r : forall n m p:Z, p > 0 -> n * p <= m * p -> n <= m. +Proof. +intros x y z Hz Hxy. +elim (Zle_lt_or_eq (x * z) (y * z) Hxy). +intros; apply Zlt_le_weak. +apply Zmult_gt_0_lt_reg_r with z; trivial. +intros; apply Zeq_le. +apply Zmult_reg_r with z. + intro. rewrite H0 in Hz. contradiction (Zgt_irrefl 0). +assumption. +Qed. + +Lemma Zmult_lt_0_le_reg_r : forall n m p:Z, 0 < p -> n * p <= m * p -> n <= m. +intros x y z; intros; apply Zmult_le_reg_r with z. +try apply Zlt_gt; assumption. +assumption. +Qed. + + +Lemma Zmult_ge_reg_r : forall n m p:Z, p > 0 -> n * p >= m * p -> n >= m. +intros a b c H1 H2; apply Zle_ge; apply Zmult_le_reg_r with c; trivial. +apply Zge_le; trivial. +Qed. + +Lemma Zmult_gt_reg_r : forall n m p:Z, p > 0 -> n * p > m * p -> n > m. +intros a b c H1 H2; apply Zlt_gt; apply Zmult_gt_0_lt_reg_r with c; trivial. +apply Zgt_lt; trivial. +Qed. + + +(** Compatibility of multiplication by a positive wrt to being positive *) + +Lemma Zmult_le_0_compat : forall n m:Z, 0 <= n -> 0 <= m -> 0 <= n * m. +Proof. +intros x y; case x. +intros; rewrite Zmult_0_l; trivial. +intros p H1; unfold Zle in |- *. + pattern 0 at 2 in |- *; rewrite <- (Zmult_0_r (Zpos p)). + rewrite Zcompare_mult_compat; trivial. +intros p H1 H2; absurd (0 > Zneg p); trivial. +unfold Zgt in |- *; simpl in |- *; auto with zarith. +Qed. + +Lemma Zmult_gt_0_compat : forall n m:Z, n > 0 -> m > 0 -> n * m > 0. +Proof. +intros x y; case x. +intros H; discriminate H. +intros p H1; unfold Zgt in |- *; pattern 0 at 2 in |- *; + rewrite <- (Zmult_0_r (Zpos p)). + rewrite Zcompare_mult_compat; trivial. +intros p H; discriminate H. +Qed. + +Lemma Zmult_lt_O_compat : forall n m:Z, 0 < n -> 0 < m -> 0 < n * m. +intros a b apos bpos. +apply Zgt_lt. +apply Zmult_gt_0_compat; try apply Zlt_gt; assumption. +Qed. + +Lemma Zmult_gt_0_le_0_compat : forall n m:Z, n > 0 -> 0 <= m -> 0 <= m * n. +Proof. +intros x y H1 H2; apply Zmult_le_0_compat; trivial. +apply Zlt_le_weak; apply Zgt_lt; trivial. +Qed. + +(** Simplification of multiplication by a positive wrt to being positive *) + +Lemma Zmult_le_0_reg_r : forall n m:Z, n > 0 -> 0 <= m * n -> 0 <= m. +Proof. +intros x y; case x; + [ simpl in |- *; unfold Zgt in |- *; simpl in |- *; intros H; discriminate H + | intros p H1; unfold Zle in |- *; rewrite Zmult_comm; + pattern 0 at 1 in |- *; rewrite <- (Zmult_0_r (Zpos p)); + rewrite Zcompare_mult_compat; auto with arith + | intros p; unfold Zgt in |- *; simpl in |- *; intros H; discriminate H ]. +Qed. + +Lemma Zmult_gt_0_lt_0_reg_r : forall n m:Z, n > 0 -> 0 < m * n -> 0 < m. +Proof. +intros x y; case x; + [ simpl in |- *; unfold Zgt in |- *; simpl in |- *; intros H; discriminate H + | intros p H1; unfold Zlt in |- *; rewrite Zmult_comm; + pattern 0 at 1 in |- *; rewrite <- (Zmult_0_r (Zpos p)); + rewrite Zcompare_mult_compat; auto with arith + | intros p; unfold Zgt in |- *; simpl in |- *; intros H; discriminate H ]. +Qed. + +Lemma Zmult_lt_0_reg_r : forall n m:Z, 0 < n -> 0 < m * n -> 0 < m. +Proof. +intros x y; intros; eapply Zmult_gt_0_lt_0_reg_r with x; try apply Zlt_gt; + assumption. +Qed. + +Lemma Zmult_gt_0_reg_l : forall n m:Z, n > 0 -> n * m > 0 -> m > 0. +Proof. +intros x y; case x. + intros H; discriminate H. + intros p H1; unfold Zgt in |- *. + pattern 0 at 1 in |- *; rewrite <- (Zmult_0_r (Zpos p)). + rewrite Zcompare_mult_compat; trivial. +intros p H; discriminate H. +Qed. + +(** Simplification of square wrt order *) + +Lemma Zgt_square_simpl : + forall n m:Z, n >= 0 -> m >= 0 -> n * n > m * m -> n > m. +Proof. +intros x y H0 H1 H2. +case (dec_Zlt y x). +intro; apply Zlt_gt; trivial. +intros H3; cut (y >= x). +intros H. +elim Zgt_not_le with (1 := H2). +apply Zge_le. +apply Zmult_ge_compat; auto. +apply Znot_lt_ge; trivial. +Qed. + +Lemma Zlt_square_simpl : + forall n m:Z, 0 <= n -> 0 <= m -> m * m < n * n -> m < n. +Proof. +intros x y H0 H1 H2. +apply Zgt_lt. +apply Zgt_square_simpl; try apply Zle_ge; try apply Zlt_gt; assumption. +Qed. + +(** Equivalence between inequalities *) + +Lemma Zle_plus_swap : forall n m p:Z, n + p <= m <-> n <= m - p. +Proof. + intros x y z; intros. split. intro. rewrite <- (Zplus_0_r x). rewrite <- (Zplus_opp_r z). + rewrite Zplus_assoc. exact (Zplus_le_compat_r _ _ _ H). + intro. rewrite <- (Zplus_0_r y). rewrite <- (Zplus_opp_l z). rewrite Zplus_assoc. + apply Zplus_le_compat_r. assumption. +Qed. + +Lemma Zlt_plus_swap : forall n m p:Z, n + p < m <-> n < m - p. +Proof. + intros x y z; intros. split. intro. unfold Zminus in |- *. rewrite Zplus_comm. rewrite <- (Zplus_0_l x). + rewrite <- (Zplus_opp_l z). rewrite Zplus_assoc_reverse. apply Zplus_lt_compat_l. rewrite Zplus_comm. + assumption. + intro. rewrite Zplus_comm. rewrite <- (Zplus_0_l y). rewrite <- (Zplus_opp_r z). + rewrite Zplus_assoc_reverse. apply Zplus_lt_compat_l. rewrite Zplus_comm. assumption. +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. + assumption. +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; + assumption. +Qed. + +Lemma Zlt_O_minus_lt : forall n m:Z, 0 < n - m -> m < n. +Proof. +intros n m H; apply Zplus_lt_reg_l with (p := - m); rewrite Zplus_opp_l; + rewrite Zplus_comm; exact H. +Qed.
\ No newline at end of file diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v new file mode 100644 index 00000000..e5bf8b04 --- /dev/null +++ b/theories/ZArith/Zpower.v @@ -0,0 +1,372 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(*i $Id: Zpower.v,v 1.11.2.1 2004/07/16 19:31:22 herbelin Exp $ i*) + +Require Import ZArith_base. +Require Import Omega. +Require Import Zcomplements. +Open Local Scope Z_scope. + +Section section1. + +(** [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]) *) + +Definition Zpower_nat (z:Z) (n:nat) := iter_nat n Z (fun x:Z => z * x) 1. + +(** [Zpower_nat_is_exp] says [Zpower_nat] is a morphism for + [plus : nat->nat] and [Zmult : Z->Z] *) + +Lemma Zpower_nat_is_exp : + forall (n m:nat) (z:Z), + Zpower_nat z (n + m) = Zpower_nat z n * Zpower_nat z m. + +intros; elim n; + [ simpl in |- *; elim (Zpower_nat z m); auto with zarith + | unfold Zpower_nat in |- *; intros; simpl in |- *; rewrite H; + apply Zmult_assoc ]. +Qed. + +(** [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]) *) + +Definition Zpower_pos (z:Z) (n:positive) := iter_pos n Z (fun x:Z => z * x) 1. + +(** This theorem shows that powers of unary and binary integers + are the same thing, modulo the function convert : [positive -> nat] *) + +Theorem Zpower_pos_nat : + forall (z:Z) (p:positive), Zpower_pos z p = Zpower_nat z (nat_of_P p). + +intros; unfold Zpower_pos in |- *; unfold Zpower_nat in |- *; + apply iter_nat_of_P. +Qed. + +(** Using the theorem [Zpower_pos_nat] and the lemma [Zpower_nat_is_exp] we + deduce that the function [[n:positive](Zpower_pos z n)] is a morphism + for [add : positive->positive] and [Zmult : Z->Z] *) + +Theorem Zpower_pos_is_exp : + forall (n m:positive) (z:Z), + Zpower_pos z (n + m) = Zpower_pos z n * Zpower_pos z m. + +intros. +rewrite (Zpower_pos_nat z n). +rewrite (Zpower_pos_nat z m). +rewrite (Zpower_pos_nat z (n + m)). +rewrite (nat_of_P_plus_morphism n m). +apply Zpower_nat_is_exp. +Qed. + +Definition Zpower (x y:Z) := + match y with + | Zpos p => Zpower_pos x p + | Z0 => 1 + | Zneg p => 0 + end. + +Infix "^" := Zpower : Z_scope. + +Hint Immediate Zpower_nat_is_exp: zarith. +Hint Immediate Zpower_pos_is_exp: zarith. +Hint Unfold Zpower_pos: zarith. +Hint Unfold Zpower_nat: zarith. + +Lemma Zpower_exp : + forall x n m:Z, n >= 0 -> m >= 0 -> x ^ (n + m) = x ^ n * x ^ m. +destruct n; destruct m; auto with zarith. +simpl in |- *; intros; apply Zred_factor0. +simpl in |- *; auto with zarith. +intros; compute in H0; absurd (Datatypes.Lt = Datatypes.Lt); auto with zarith. +intros; compute in H0; absurd (Datatypes.Lt = Datatypes.Lt); auto with zarith. +Qed. + +End section1. + +(* Exporting notation "^" *) + +Infix "^" := Zpower : Z_scope. + +Hint Immediate Zpower_nat_is_exp: zarith. +Hint Immediate Zpower_pos_is_exp: zarith. +Hint Unfold Zpower_pos: zarith. +Hint Unfold Zpower_nat: zarith. + +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. *) + +(** [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 (n:Z) (z:positive) := + match n with + | Z0 => z + | Zpos p => iter_pos p positive xO z + | Zneg p => z + end. + +Definition two_power_nat (n:nat) := Zpos (shift_nat n 1). +Definition two_power_pos (x:positive) := Zpos (shift_pos x 1). + +Lemma two_power_nat_S : + forall n:nat, two_power_nat (S n) = 2 * two_power_nat n. +intro; simpl in |- *; apply refl_equal. +Qed. + +Lemma shift_nat_plus : + forall (n m:nat) (x:positive), + shift_nat (n + m) x = shift_nat n (shift_nat m x). + +intros; unfold shift_nat in |- *; apply iter_nat_plus. +Qed. + +Theorem shift_nat_correct : + forall (n:nat) (x:positive), Zpos (shift_nat n x) = Zpower_nat 2 n * Zpos x. + +unfold shift_nat in |- *; simple induction n; + [ simpl in |- *; trivial with zarith + | intros; replace (Zpower_nat 2 (S n0)) with (2 * Zpower_nat 2 n0); + [ rewrite <- Zmult_assoc; rewrite <- (H x); simpl in |- *; reflexivity + | auto with zarith ] ]. +Qed. + +Theorem two_power_nat_correct : + forall n:nat, two_power_nat n = Zpower_nat 2 n. + +intro n. +unfold two_power_nat in |- *. +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. + +unfold shift_pos in |- *. +unfold shift_nat in |- *. +intros; apply iter_nat_of_P. +Qed. + +Lemma two_power_pos_nat : + forall p:positive, two_power_pos p = two_power_nat (nat_of_P p). + +intro; unfold two_power_pos in |- *; unfold two_power_nat in |- *. +apply f_equal with (f := Zpos). +apply shift_pos_nat. +Qed. + +(** Then we deduce that [two_power_pos] is also correct *) + +Theorem shift_pos_correct : + forall p x:positive, Zpos (shift_pos p x) = Zpower_pos 2 p * Zpos x. + +intros. +rewrite (shift_pos_nat p x). +rewrite (Zpower_pos_nat 2 p). +apply shift_nat_correct. +Qed. + +Theorem two_power_pos_correct : + forall x:positive, two_power_pos x = Zpower_pos 2 x. + +intro. +rewrite two_power_pos_nat. +rewrite Zpower_pos_nat. +apply two_power_nat_correct. +Qed. + +(** Some consequences *) + +Theorem two_power_pos_is_exp : + forall x y:positive, + two_power_pos (x + y) = two_power_pos x * two_power_pos y. +intros. +rewrite (two_power_pos_correct (x + y)). +rewrite (two_power_pos_correct x). +rewrite (two_power_pos_correct y). +apply Zpower_pos_is_exp. +Qed. + +(** 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 + | Zpos y => two_power_pos y + | Zneg y => 0 + end. + +Theorem two_p_is_exp : + forall x y:Z, 0 <= x -> 0 <= y -> two_p (x + y) = two_p x * two_p y. +simple induction x; + [ simple induction y; simpl in |- *; auto with zarith + | simple induction y; + [ unfold two_p in |- *; rewrite (Zmult_comm (two_power_pos p) 1); + rewrite (Zmult_1_l (two_power_pos p)); auto with zarith + | unfold Zplus in |- *; unfold two_p in |- *; intros; + apply two_power_pos_is_exp + | intros; unfold Zle in H0; unfold Zcompare in H0; + absurd (Datatypes.Gt = Datatypes.Gt); trivial with zarith ] + | simple induction y; + [ simpl in |- *; auto with zarith + | intros; unfold Zle in H; unfold Zcompare in H; + absurd (Datatypes.Gt = Datatypes.Gt); trivial with zarith + | intros; unfold Zle in H; unfold Zcompare in H; + absurd (Datatypes.Gt = Datatypes.Gt); trivial with zarith ] ]. +Qed. + +Lemma two_p_gt_ZERO : forall x:Z, 0 <= x -> two_p x > 0. +simple induction x; intros; + [ simpl in |- *; omega + | simpl in |- *; unfold two_power_pos in |- *; apply Zorder.Zgt_pos_0 + | absurd (0 <= Zneg p); + [ simpl in |- *; unfold Zle in |- *; unfold Zcompare in |- *; + do 2 unfold not in |- *; auto with zarith + | assumption ] ]. +Qed. + +Lemma two_p_S : forall x:Z, 0 <= x -> two_p (Zsucc x) = 2 * two_p x. +intros; unfold Zsucc in |- *. +rewrite (two_p_is_exp x 1 H (Zorder.Zle_0_pos 1)). +apply Zmult_comm. +Qed. + +Lemma two_p_pred : forall x:Z, 0 <= x -> two_p (Zpred x) < two_p x. +intros; apply natlike_ind with (P := fun x:Z => two_p (Zpred x) < two_p x); + [ simpl in |- *; unfold Zlt in |- *; auto with zarith + | intros; elim (Zle_lt_or_eq 0 x0 H0); + [ intros; + replace (two_p (Zpred (Zsucc x0))) with (two_p (Zsucc (Zpred x0))); + [ rewrite (two_p_S (Zpred x0)); + [ rewrite (two_p_S x0); [ omega | assumption ] + | apply Zorder.Zlt_0_le_0_pred; assumption ] + | rewrite <- (Zsucc_pred x0); rewrite <- (Zpred_succ x0); + trivial with zarith ] + | intro Hx0; rewrite <- Hx0; simpl in |- *; unfold Zlt in |- *; + auto with zarith ] + | assumption ]. +Qed. + +Lemma Zlt_lt_double : forall x y:Z, 0 <= x < y -> x < 2 * y. +intros; omega. Qed. + +End Powers_of_2. + +Hint Resolve two_p_gt_ZERO: zarith. +Hint Immediate two_p_pred two_p_S: zarith. + +Section power_div_with_rest. + +(** Division by a power of two. + To [n:Z] and [p:positive], [q],[r] are associated such that + [n = 2^p.q + r] and [0 <= r < 2^p] *) + +(** Invariant: [d*q + r = d'*q + r /\ d' = 2*d /\ 0<= r < d /\ 0 <= r' < d'] *) +Definition Zdiv_rest_aux (qrd:Z * Z * Z) := + let (qr, d) := qrd in + let (q, r) := qr in + (match q with + | Z0 => (0, r) + | Zpos xH => (0, d + r) + | Zpos (xI n) => (Zpos n, d + r) + | Zpos (xO n) => (Zpos n, r) + | Zneg xH => (-1, d + r) + | Zneg (xI n) => (Zneg n - 1, d + r) + | Zneg (xO n) => (Zneg n, r) + end, 2 * d). + +Definition Zdiv_rest (x:Z) (p:positive) := + let (qr, d) := iter_pos p _ Zdiv_rest_aux (x, 0, 1) in qr. + +Lemma Zdiv_rest_correct1 : + forall (x:Z) (p:positive), + let (qr, d) := iter_pos p _ Zdiv_rest_aux (x, 0, 1) in d = two_power_pos p. + +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); + 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)); + destruct a; intros; apply f_equal with (f := fun z:Z => 2 * z); + assumption ]. +Qed. + +Lemma Zdiv_rest_correct2 : + forall (x:Z) (p:positive), + let (qr, d) := iter_pos p _ Zdiv_rest_aux (x, 0, 1) in + let (q, r) := qr in x = q * d + r /\ 0 <= r < d. + +intros; + apply iter_pos_invariant with + (f := Zdiv_rest_aux) + (Inv := fun qrd:Z * Z * Z => + let (qr, d) := qrd in + let (q, r) := qr in x = q * d + r /\ 0 <= r < d); + [ intro x0; elim x0; intro y0; elim y0; intros q r d; + unfold Zdiv_rest_aux in |- *; elim q; + [ omega + | destruct p0; + [ rewrite BinInt.Zpos_xI; intro; elim H; intros; split; + [ rewrite H0; rewrite Zplus_assoc; rewrite Zmult_plus_distr_l; + rewrite Zmult_1_l; rewrite Zmult_assoc; + rewrite (Zmult_comm (Zpos p0) 2); apply refl_equal + | omega ] + | rewrite BinInt.Zpos_xO; intro; elim H; intros; split; + [ rewrite H0; rewrite Zmult_assoc; rewrite (Zmult_comm (Zpos p0) 2); + apply refl_equal + | omega ] + | omega ] + | destruct p0; + [ rewrite BinInt.Zneg_xI; unfold Zminus in |- *; intro; elim H; intros; + split; + [ rewrite H0; rewrite Zplus_assoc; + 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); + omega + | omega ] + | rewrite BinInt.Zneg_xO; unfold Zminus in |- *; intro; elim H; intros; + split; + [ rewrite H0; rewrite Zmult_assoc; rewrite (Zmult_comm (Zneg p0) 2); + apply refl_equal + | omega ] + | omega ] ] + | omega ]. +Qed. + +Inductive Zdiv_rest_proofs (x:Z) (p:positive) : Set := + Zdiv_rest_proof : + forall q r:Z, + x = q * two_power_pos p + r -> + 0 <= r -> r < two_power_pos p -> Zdiv_rest_proofs x p. + +Lemma Zdiv_rest_correct : forall (x:Z) (p:positive), Zdiv_rest_proofs x p. +intros x p. +generalize (Zdiv_rest_correct1 x p); generalize (Zdiv_rest_correct2 x p). +elim (iter_pos p (Z * Z * Z) Zdiv_rest_aux (x, 0, 1)). +simple induction a. +intros. +elim H; intros H1 H2; clear H. +rewrite H0 in H1; rewrite H0 in H2; elim H2; intros; + apply Zdiv_rest_proof with (q := a0) (r := b); assumption. +Qed. + +End power_div_with_rest.
\ No newline at end of file diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v new file mode 100644 index 00000000..583c5828 --- /dev/null +++ b/theories/ZArith/Zsqrt.v @@ -0,0 +1,163 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(* $Id: Zsqrt.v,v 1.11.2.1 2004/07/16 19:31:22 herbelin Exp $ *) + +Require Import Omega. +Require Export ZArith_base. +Require Export ZArithRing. +Open Local Scope Z_scope. + +(**********************************************************************) +(** Definition and properties of square root on Z *) + +(** The following tactic replaces all instances of (POS (xI ...)) by + `2*(POS ...)+1`, but only when ... is not made only with xO, XI, or xH. *) +Ltac compute_POS := + match goal with + | |- context [(Zpos (xI ?X1))] => + match constr:X1 with + | context [1%positive] => fail + | _ => rewrite (BinInt.Zpos_xI X1) + end + | |- context [(Zpos (xO ?X1))] => + match constr:X1 with + | context [1%positive] => fail + | _ => rewrite (BinInt.Zpos_xO X1) + end + end. + +Inductive sqrt_data (n:Z) : Set := + c_sqrt : forall s r:Z, n = s * s + r -> 0 <= r <= 2 * s -> sqrt_data n. + +Definition sqrtrempos : forall p:positive, sqrt_data (Zpos p). +refine + (fix sqrtrempos (p:positive) : sqrt_data (Zpos p) := + match p return sqrt_data (Zpos p) with + | xH => c_sqrt 1 1 0 _ _ + | xO xH => c_sqrt 2 1 1 _ _ + | xI xH => c_sqrt 3 1 2 _ _ + | xO (xO p') => + match sqrtrempos p' with + | c_sqrt s' r' Heq Hint => + match Z_le_gt_dec (4 * s' + 1) (4 * r') with + | left Hle => + c_sqrt (Zpos (xO (xO p'))) (2 * s' + 1) + (4 * r' - (4 * s' + 1)) _ _ + | right Hgt => c_sqrt (Zpos (xO (xO p'))) (2 * s') (4 * r') _ _ + end + end + | xO (xI p') => + match sqrtrempos p' with + | c_sqrt s' r' Heq Hint => + match Z_le_gt_dec (4 * s' + 1) (4 * r' + 2) with + | left Hle => + c_sqrt (Zpos (xO (xI p'))) (2 * s' + 1) + (4 * r' + 2 - (4 * s' + 1)) _ _ + | right Hgt => + c_sqrt (Zpos (xO (xI p'))) (2 * s') (4 * r' + 2) _ _ + end + end + | xI (xO p') => + match sqrtrempos p' with + | c_sqrt s' r' Heq Hint => + match Z_le_gt_dec (4 * s' + 1) (4 * r' + 1) with + | left Hle => + c_sqrt (Zpos (xI (xO p'))) (2 * s' + 1) + (4 * r' + 1 - (4 * s' + 1)) _ _ + | right Hgt => + c_sqrt (Zpos (xI (xO p'))) (2 * s') (4 * r' + 1) _ _ + end + end + | xI (xI p') => + match sqrtrempos p' with + | c_sqrt s' r' Heq Hint => + match Z_le_gt_dec (4 * s' + 1) (4 * r' + 3) with + | left Hle => + c_sqrt (Zpos (xI (xI p'))) (2 * s' + 1) + (4 * r' + 3 - (4 * s' + 1)) _ _ + | right Hgt => + c_sqrt (Zpos (xI (xI p'))) (2 * s') (4 * r' + 3) _ _ + end + end + end); clear sqrtrempos; repeat compute_POS; + try (try rewrite Heq; ring; fail); try omega. +Defined. + +(** Define with integer input, but with a strong (readable) specification. *) +Definition Zsqrt : + forall x:Z, + 0 <= x -> + {s : Z & {r : Z | x = s * s + r /\ s * s <= x < (s + 1) * (s + 1)}}. +refine + (fun x => + match + x + return + 0 <= x -> + {s : Z & {r : Z | x = s * s + r /\ s * s <= x < (s + 1) * (s + 1)}} + with + | Zpos p => + fun h => + match sqrtrempos p with + | c_sqrt s r Heq Hint => + existS + (fun s:Z => + {r : Z | + Zpos p = s * s + r /\ s * s <= Zpos p < (s + 1) * (s + 1)}) + s + (exist + (fun r:Z => + Zpos p = s * s + r /\ + s * s <= Zpos p < (s + 1) * (s + 1)) r _) + end + | Zneg p => + fun h => + False_rec + {s : Z & + {r : Z | + Zneg p = s * s + r /\ s * s <= Zneg p < (s + 1) * (s + 1)}} + (h (refl_equal Datatypes.Gt)) + | Z0 => + fun h => + existS + (fun s:Z => + {r : Z | 0 = s * s + r /\ s * s <= 0 < (s + 1) * (s + 1)}) 0 + (exist + (fun r:Z => 0 = 0 * 0 + r /\ 0 * 0 <= 0 < (0 + 1) * (0 + 1)) 0 + _) + end); try omega. +split; [ omega | rewrite Heq; ring ((s + 1) * (s + 1)); omega ]. +Defined. + +(** Define a function of type Z->Z that computes the integer square root, + but only for positive numbers, and 0 for others. *) +Definition Zsqrt_plain (x:Z) : Z := + match x with + | Zpos p => + match Zsqrt (Zpos p) (Zorder.Zle_0_pos p) with + | existS s _ => s + end + | Zneg p => 0 + | Z0 => 0 + end. + +(** A basic theorem about Zsqrt_plain *) +Theorem Zsqrt_interval : + forall n:Z, + 0 <= n -> + Zsqrt_plain n * Zsqrt_plain n <= n < + (Zsqrt_plain n + 1) * (Zsqrt_plain n + 1). +intros x; case x. +unfold Zsqrt_plain in |- *; omega. +intros p; unfold Zsqrt_plain in |- *; + case (Zsqrt (Zpos p) (Zorder.Zle_0_pos p)). +intros s [r [Heq Hint]] Hle; assumption. +intros p Hle; elim Hle; auto. +Qed. + diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v new file mode 100644 index 00000000..8633986b --- /dev/null +++ b/theories/ZArith/Zwf.v @@ -0,0 +1,96 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(* $Id: Zwf.v,v 1.7.2.1 2004/07/16 19:31:22 herbelin Exp $ *) + +Require Import ZArith_base. +Require Export Wf_nat. +Require Import Omega. +Open Local Scope Z_scope. + +(** Well-founded relations on Z. *) + +(** We define the following family of relations on [Z x Z]: + + [x (Zwf c) y] iff [x < y & c <= y] + *) + +Definition Zwf (c x y:Z) := c <= y /\ x < y. + +(** and we prove that [(Zwf c)] is well founded *) + +Section wf_proof. + +Variable c : Z. + +(** The proof of well-foundness is classic: we do the proof by induction + on a measure in nat, which is here [|x-c|] *) + +Let f (z:Z) := Zabs_nat (z - c). + +Lemma Zwf_well_founded : well_founded (Zwf c). +red in |- *; intros. +assert (forall (n:nat) (a:Z), (f a < n)%nat \/ a < c -> Acc (Zwf c) a). +clear a; simple induction n; intros. +(** n= 0 *) +case H; intros. +case (lt_n_O (f a)); auto. +apply Acc_intro; unfold Zwf in |- *; intros. +assert False; omega || contradiction. +(** inductive case *) +case H0; clear H0; intro; auto. +apply Acc_intro; intros. +apply H. +unfold Zwf in H1. +case (Zle_or_lt c y); intro; auto with zarith. +left. +red in H0. +apply lt_le_trans with (f a); auto with arith. +unfold f in |- *. +apply Zabs.Zabs_nat_lt; omega. +apply (H (S (f a))); auto. +Qed. + +End wf_proof. + +Hint Resolve Zwf_well_founded: datatypes v62. + + +(** We also define the other family of relations: + + [x (Zwf_up c) y] iff [y < x <= c] + *) + +Definition Zwf_up (c x y:Z) := y < x <= c. + +(** and we prove that [(Zwf_up c)] is well founded *) + +Section wf_proof_up. + +Variable c : Z. + +(** The proof of well-foundness is classic: we do the proof by induction + on a measure in nat, which is here [|c-x|] *) + +Let f (z:Z) := Zabs_nat (c - z). + +Lemma Zwf_up_well_founded : well_founded (Zwf_up c). +Proof. +apply well_founded_lt_compat with (f := f). +unfold Zwf_up, f in |- *. +intros. +apply Zabs.Zabs_nat_lt. +unfold Zminus in |- *. split. +apply Zle_left; intuition. +apply Zplus_lt_compat_l; unfold Zlt in |- *; rewrite <- Zcompare_opp; + intuition. +Qed. + +End wf_proof_up. + +Hint Resolve Zwf_up_well_founded: datatypes v62.
\ No newline at end of file diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v new file mode 100644 index 00000000..ecd2daab --- /dev/null +++ b/theories/ZArith/auxiliary.v @@ -0,0 +1,150 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(*i $Id: auxiliary.v,v 1.12.2.1 2004/07/16 19:31:22 herbelin Exp $ i*) + +(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) + +Require Export Arith. +Require Import BinInt. +Require Import Zorder. +Require Import Decidable. +Require Import Peano_dec. +Require Export Compare_dec. + +Open Local Scope Z_scope. + +(**********************************************************************) +(** Moving terms from one side to the other of an inequality *) + +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; + rewrite Zplus_comm; trivial with arith. +Qed. + +Theorem Zegal_left : forall n m:Z, n = m -> n + - m = 0. +Proof. +intros x y H; apply (Zplus_reg_l y); rewrite Zplus_permute; + rewrite Zplus_opp_r; do 2 rewrite Zplus_0_r; assumption. +Qed. + +Theorem Zle_left : forall n m:Z, n <= m -> 0 <= m + - n. +Proof. +intros x y H; replace 0 with (x + - x). +apply Zplus_le_compat_r; trivial. +apply Zplus_opp_r. +Qed. + +Theorem Zle_left_rev : forall n m:Z, 0 <= m + - n -> n <= m. +Proof. +intros x y H; apply Zplus_le_reg_r with (- x). +rewrite Zplus_opp_r; trivial. +Qed. + +Theorem Zlt_left_rev : forall n m:Z, 0 < m + - n -> n < m. +Proof. +intros x y H; apply Zplus_lt_reg_r with (- x). +rewrite Zplus_opp_r; trivial. +Qed. + +Theorem Zlt_left : forall n m:Z, n < m -> 0 <= m + -1 + - n. +Proof. +intros x y H; apply Zle_left; apply Zsucc_le_reg; + change (Zsucc x <= Zsucc (Zpred y)) in |- *; rewrite <- Zsucc_pred; + apply Zlt_le_succ; assumption. +Qed. + +Theorem Zlt_left_lt : forall n m:Z, n < m -> 0 < m + - n. +Proof. +intros x y H; replace 0 with (x + - x). +apply Zplus_lt_compat_r; trivial. +apply Zplus_opp_r. +Qed. + +Theorem Zge_left : forall n m:Z, n >= m -> 0 <= n + - m. +Proof. +intros x y H; apply Zle_left; apply Zge_le; assumption. +Qed. + +Theorem Zgt_left : forall n m:Z, n > m -> 0 <= n + -1 + - m. +Proof. +intros x y H; apply Zlt_left; apply Zgt_lt; assumption. +Qed. + +Theorem Zgt_left_gt : forall n m:Z, n > m -> n + - m > 0. +Proof. +intros x y H; replace 0 with (y + - y). +apply Zplus_gt_compat_r; trivial. +apply Zplus_opp_r. +Qed. + +Theorem Zgt_left_rev : forall n m:Z, n + - m > 0 -> n > m. +Proof. +intros x y H; apply Zplus_gt_reg_r with (- y). +rewrite Zplus_opp_r; trivial. +Qed. + +(**********************************************************************) +(** Factorization lemmas *) + +Theorem Zred_factor0 : forall n:Z, n = n * 1. +intro x; rewrite (Zmult_1_r x); reflexivity. +Qed. + +Theorem Zred_factor1 : forall n:Z, n + n = n * 2. +Proof. +exact Zplus_diag_eq_mult_2. +Qed. + +Theorem Zred_factor2 : forall n m:Z, n + n * m = n * (1 + m). + +intros x y; pattern x at 1 in |- *; rewrite <- (Zmult_1_r x); + rewrite <- Zmult_plus_distr_r; trivial with arith. +Qed. + +Theorem Zred_factor3 : forall n m:Z, n * m + n = n * (1 + m). + +intros x y; pattern x at 2 in |- *; rewrite <- (Zmult_1_r x); + rewrite <- Zmult_plus_distr_r; rewrite Zplus_comm; + trivial with arith. +Qed. +Theorem Zred_factor4 : forall n m p:Z, n * m + n * p = n * (m + p). +intros x y z; symmetry in |- *; apply Zmult_plus_distr_r. +Qed. + +Theorem Zred_factor5 : forall n m:Z, n * 0 + m = m. + +intros x y; rewrite <- Zmult_0_r_reverse; auto with arith. +Qed. + +Theorem Zred_factor6 : forall n:Z, n = n + 0. + +intro; rewrite Zplus_0_r; trivial with arith. +Qed. + +Theorem Zle_mult_approx : + forall n m p:Z, n > 0 -> p > 0 -> 0 <= m -> 0 <= m * n + p. + +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; + assumption ]. +Qed. + +Theorem Zmult_le_approx : + forall n m p:Z, n > 0 -> n > p -> 0 <= m * n + p -> 0 <= m. + +intros x y z H1 H2 H3; apply Zlt_succ_le; apply Zmult_gt_0_lt_0_reg_r with x; + [ assumption + | apply Zle_lt_trans with (1 := H3); rewrite <- Zmult_succ_l_reverse; + apply Zplus_lt_compat_l; apply Zgt_lt; assumption ]. + +Qed. diff --git a/theories/ZArith/intro.tex b/theories/ZArith/intro.tex new file mode 100755 index 00000000..21e52c19 --- /dev/null +++ b/theories/ZArith/intro.tex @@ -0,0 +1,6 @@ +\section{Binary integers : ZArith} +The {\tt ZArith} library deals with binary integers (those used +by the {\tt Omega} decision tactic). +Here are defined various arithmetical notions and their properties, +similar to those of {\tt Arith}. + |