diff options
Diffstat (limited to 'theories/ZArith/BinInt.v')
| -rw-r--r-- | theories/ZArith/BinInt.v | 2205 |
1 files changed, 1403 insertions, 802 deletions
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index e2b89d84..eeec9042 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -1,1158 +1,1759 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: BinInt.v 14641 2011-11-06 11:59:10Z herbelin $ i*) +Require Export BinNums BinPos Pnat. +Require Import BinNat Bool Plus Mult Equalities GenericMinMax + OrdersFacts ZAxioms ZProperties. +Require BinIntDef. (***********************************************************) -(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) +(** * Binary Integers *) (***********************************************************) -Require Export BinPos. -Require Export Pnat. -Require Import BinNat. -Require Import Plus. -Require Import Mult. - -Unset Boxed Definitions. - -(*****************************) -(** * Binary integer numbers *) - -Inductive Z : Set := - | Z0 : Z - | Zpos : positive -> Z - | Zneg : positive -> Z. - - -(** Automatically open scope positive_scope for the constructors of Z *) -Delimit Scope Z_scope with 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 p~1 - | Zneg p => Zneg (Pdouble_minus_one p) - end. - -Definition Zdouble_minus_one (x:Z) := - match x with - | Z0 => Zneg 1 - | Zneg p => Zneg p~1 - | Zpos p => Zpos (Pdouble_minus_one p) - end. - -Definition Zdouble (x:Z) := - match x with - | Z0 => Z0 - | Zpos p => Zpos p~0 - | Zneg p => Zneg p~0 - end. - -Open Local Scope positive_scope. - -Fixpoint ZPminus (x y:positive) {struct y} : Z := - match x, y with - | p~1, q~1 => Zdouble (ZPminus p q) - | p~1, q~0 => Zdouble_plus_one (ZPminus p q) - | p~1, 1 => Zpos p~0 - | p~0, q~1 => Zdouble_minus_one (ZPminus p q) - | p~0, q~0 => Zdouble (ZPminus p q) - | p~0, 1 => Zpos (Pdouble_minus_one p) - | 1, q~1 => Zneg q~0 - | 1, q~0 => Zneg (Pdouble_minus_one q) - | 1, 1 => Z0 - end. - -Close Local Scope positive_scope. - -(** ** Addition on integers *) - -Definition Zplus (x y:Z) := - match x, y with - | Z0, y => y - | Zpos x', Z0 => Zpos x' - | Zneg x', Z0 => Zneg 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. +(** Initial author: Pierre Crégut, CNET, Lannion, France *) -Ltac elim_compare com1 com2 := - case (Dcompare (com1 ?= com2)%Z); - [ idtac | let x := fresh "H" in - (intro x; case x; clear x) ]. +(** The type [Z] and its constructors [Z0] and [Zpos] and [Zneg] + are now defined in [BinNums.v] *) -(** ** Sign function *) +Local Open Scope Z_scope. -Definition Zsgn (z:Z) : Z := - match z with - | Z0 => Z0 - | Zpos p => Zpos 1 - | Zneg p => Zneg 1 - end. +(** Every definitions and early properties about binary integers + are placed in a module [Z] for qualification purpose. *) -(** ** Direct, easier to handle variants of successor and addition *) +Module Z + <: ZAxiomsSig + <: UsualOrderedTypeFull + <: UsualDecidableTypeFull + <: TotalOrder. -Definition Zsucc' (x:Z) := - match x with - | Z0 => Zpos 1 - | Zpos x' => Zpos (Psucc x') - | Zneg x' => ZPminus 1 x' - end. +(** * Definitions of operations, now in a separate file *) -Definition Zpred' (x:Z) := - match x with - | Z0 => Zneg 1 - | Zpos x' => ZPminus x' 1 - | Zneg x' => Zneg (Psucc x') - end. +Include BinIntDef.Z. -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. +(** When including property functors, only inline t eq zero one two *) -Open Local Scope Z_scope. +Set Inline Level 30. -(**********************************************************************) -(** ** Inductive specification of Z *) +(** * Logic Predicates *) -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. +Definition eq := @Logic.eq Z. +Definition eq_equiv := @eq_equivalence Z. -(**********************************************************************) -(** * Misc properties about binary integer operations *) +Definition lt x y := (x ?= y) = Lt. +Definition gt x y := (x ?= y) = Gt. +Definition le x y := (x ?= y) <> Gt. +Definition ge x y := (x ?= y) <> Lt. +Infix "<=" := le : Z_scope. +Infix "<" := lt : Z_scope. +Infix ">=" := ge : Z_scope. +Infix ">" := gt : Z_scope. -(**********************************************************************) -(** ** Properties of opposite on binary integer numbers *) +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. + +Definition divide x y := exists z, y = z*x. +Notation "( x | y )" := (divide x y) (at level 0). + +Definition Even a := exists b, a = 2*b. +Definition Odd a := exists b, a = 2*b+1. -Theorem Zopp_0 : Zopp Z0 = Z0. +(** * Decidability of equality. *) + +Definition eq_dec (x y : Z) : {x = y} + {x <> y}. Proof. - reflexivity. + decide equality; apply Pos.eq_dec. +Defined. + +(** * Properties of [pos_sub] *) + +(** [pos_sub] can be written in term of positive comparison + and subtraction (cf. earlier definition of addition of Z) *) + +Lemma pos_sub_spec p q : + pos_sub p q = + match (p ?= q)%positive with + | Eq => 0 + | Lt => neg (q - p) + | Gt => pos (p - q) + end. +Proof. + revert q. induction p; destruct q; simpl; trivial; + rewrite ?Pos.compare_xI_xI, ?Pos.compare_xO_xI, + ?Pos.compare_xI_xO, ?Pos.compare_xO_xO, IHp; simpl; + case Pos.compare_spec; intros; simpl; trivial; + (now rewrite Pos.sub_xI_xI) || (now rewrite Pos.sub_xO_xO) || + (now rewrite Pos.sub_xO_xI) || (now rewrite Pos.sub_xI_xO) || + subst; unfold Pos.sub; simpl; now rewrite Pos.sub_mask_diag. Qed. -Theorem Zopp_neg : forall p:positive, - Zneg p = Zpos p. +Lemma pos_sub_discr p q : + match pos_sub p q with + | Z0 => p = q + | pos k => p = q + k + | neg k => q = p + k + end%positive. Proof. - reflexivity. + rewrite pos_sub_spec. + case Pos.compare_spec; auto; intros; + now rewrite Pos.add_comm, Pos.sub_add. Qed. -(** [opp] is involutive *) +(** Particular cases of the previous result *) -Theorem Zopp_involutive : forall n:Z, - - n = n. +Lemma pos_sub_diag p : pos_sub p p = 0. Proof. - intro x; destruct x; reflexivity. + now rewrite pos_sub_spec, Pos.compare_refl. Qed. -(** Injectivity of the opposite *) +Lemma pos_sub_lt p q : (p < q)%positive -> pos_sub p q = neg (q - p). +Proof. + intros H. now rewrite pos_sub_spec, H. +Qed. -Theorem Zopp_inj : forall n m:Z, - n = - m -> n = m. +Lemma pos_sub_gt p q : (q < p)%positive -> pos_sub p q = pos (p - q). 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 ]. + intros H. now rewrite pos_sub_spec, Pos.compare_antisym, H. Qed. -(**********************************************************************) -(** ** Other properties of binary integer numbers *) +(** The opposite of [pos_sub] is [pos_sub] with reversed arguments *) -Lemma ZL0 : 2%nat = (1 + 1)%nat. +Lemma pos_sub_opp p q : - pos_sub p q = pos_sub q p. Proof. - reflexivity. + revert q; induction p; destruct q; simpl; trivial; + rewrite <- IHp; now destruct pos_sub. Qed. -(**********************************************************************) -(** * Properties of the addition on integers *) +(** In the following module, we group results that are needed now + to prove specifications of operations, but will also be provided + later by the generic functor of properties. *) -(** ** Zero is left neutral for addition *) +Module Import Private_BootStrap. -Theorem Zplus_0_l : forall n:Z, Z0 + n = n. -Proof. - intro x; destruct x; reflexivity. -Qed. +(** * Properties of addition *) -(** ** Zero is right neutral for addition *) +(** ** Zero is neutral for addition *) -Theorem Zplus_0_r : forall n:Z, n + Z0 = n. +Lemma add_0_r n : n + 0 = n. Proof. - intro x; destruct x; reflexivity. + now destruct n. Qed. (** ** Addition is commutative *) -Theorem Zplus_comm : forall n m:Z, n + m = m + n. +Lemma add_comm n m : 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. + destruct n, m; simpl; trivial; now rewrite Pos.add_comm. Qed. (** ** Opposite distributes over addition *) -Theorem Zopp_plus_distr : forall n m:Z, - (n + m) = - n + - m. +Lemma opp_add_distr n m : - (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. + destruct n, m; simpl; trivial using pos_sub_opp. Qed. -Theorem Zopp_succ : forall n:Z, Zopp (Zsucc n) = Zpred (Zopp n). +(** ** Opposite is injective *) + +Lemma opp_inj n m : -n = -m -> n = m. Proof. -intro; unfold Zsucc; now rewrite Zopp_plus_distr. + destruct n, m; simpl; intros H; destr_eq H; now f_equal. +Qed. + +(** ** Addition is associative *) + +Lemma pos_sub_add p q r : + pos_sub (p + q) r = pos p + pos_sub q r. +Proof. + simpl. rewrite !pos_sub_spec. + case (Pos.compare_spec q r); intros E0. + - (* q = r *) + subst. + assert (H := Pos.lt_add_r r p). + rewrite Pos.add_comm in H. apply Pos.lt_gt in H. + now rewrite H, Pos.add_sub. + - (* q < r *) + rewrite pos_sub_spec. + assert (Hr : (r = (r-q)+q)%positive) by (now rewrite Pos.sub_add). + rewrite Hr at 1. rewrite Pos.add_compare_mono_r. + case Pos.compare_spec; intros E1; trivial; f_equal. + rewrite Pos.add_comm. apply Pos.sub_add_distr. + rewrite Hr, Pos.add_comm. now apply Pos.add_lt_mono_r. + symmetry. apply Pos.sub_sub_distr; trivial. + - (* r < q *) + assert (LT : (r < p + q)%positive). + { apply Pos.lt_trans with q; trivial. + rewrite Pos.add_comm. apply Pos.lt_add_r. } + apply Pos.lt_gt in LT. rewrite LT. f_equal. + symmetry. now apply Pos.add_sub_assoc. +Qed. + +Lemma add_assoc n m p : n + (m + p) = n + m + p. +Proof. + assert (AUX : forall x y z, pos x + (y + z) = pos x + y + z). + { intros x [|y|y] [|z|z]; rewrite ?add_0_r; trivial. + - simpl. now rewrite Pos.add_assoc. + - simpl (_ + neg _). symmetry. apply pos_sub_add. + - simpl (neg _ + _); simpl (_ + neg _). + now rewrite (add_comm _ (pos _)), <- 2 pos_sub_add, Pos.add_comm. + - apply opp_inj. rewrite !opp_add_distr. simpl opp. + simpl (neg _ + _); simpl (_ + neg _). + rewrite add_comm, Pos.add_comm. apply pos_sub_add. } + destruct n. + - trivial. + - apply AUX. + - apply opp_inj. rewrite !opp_add_distr. simpl opp. apply AUX. +Qed. + +(** ** Subtraction and successor *) + +Lemma sub_succ_l n m : succ n - m = succ (n - m). +Proof. + unfold sub, succ. now rewrite <- 2 add_assoc, (add_comm 1). Qed. (** ** Opposite is inverse for addition *) -Theorem Zplus_opp_r : forall n:Z, n + - n = Z0. +Lemma add_opp_diag_r n : n + - n = 0. Proof. - intro x; destruct x as [| p| p]; simpl in |- *; - [ reflexivity - | rewrite (Pcompare_refl p); reflexivity - | rewrite (Pcompare_refl p); reflexivity ]. + destruct n; simpl; trivial; now rewrite pos_sub_diag. Qed. -Theorem Zplus_opp_l : forall n:Z, - n + n = Z0. +Lemma add_opp_diag_l n : - n + n = 0. Proof. - intro; rewrite Zplus_comm; apply Zplus_opp_r. + rewrite add_comm. apply add_opp_diag_r. Qed. -Hint Local Resolve Zplus_0_l Zplus_0_r. +(** ** Commutativity of multiplication *) -(** ** Addition is associative *) +Lemma mul_comm n m : n * m = m * n. +Proof. + destruct n, m; simpl; trivial; f_equal; apply Pos.mul_comm. +Qed. -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_reverse : forall n m:Z, Zsucc (n + m) = n + Zsucc m. -Proof. - intros n m; unfold Zsucc in |- *; rewrite Zplus_assoc; trivial with arith. +(** ** Associativity of multiplication *) + +Lemma mul_assoc n m p : n * (m * p) = n * m * p. +Proof. + destruct n, m, p; simpl; trivial; f_equal; apply Pos.mul_assoc. Qed. -Notation Zplus_succ_r := Zplus_succ_r_reverse (only parsing). +(** Multiplication and constants *) -Lemma Zplus_succ_comm : forall n m:Z, Zsucc n + m = n + Zsucc m. +Lemma mul_1_l n : 1 * n = n. Proof. - unfold Zsucc in |- *; intros n m; rewrite <- Zplus_assoc; - rewrite (Zplus_comm (Zpos 1)); trivial with arith. + now destruct n. Qed. -(** ** Misc properties, usually redundant or non natural *) +Lemma mul_1_r n : n * 1 = n. +Proof. + destruct n; simpl; now rewrite ?Pos.mul_1_r. +Qed. + +(** ** Multiplication and Opposite *) -Lemma Zplus_0_r_reverse : forall n:Z, n = n + Z0. +Lemma mul_opp_l n m : - n * m = - (n * m). Proof. - symmetry in |- *; apply Zplus_0_r. + now destruct n, m. Qed. -Lemma Zplus_0_simpl_l : forall n m:Z, n + Z0 = m -> n = m. +Lemma mul_opp_r n m : n * - m = - (n * m). Proof. - intros n m; rewrite Zplus_0_r; intro; assumption. + now destruct n, m. Qed. -Lemma Zplus_0_simpl_l_reverse : forall n m:Z, n = m + Z0 -> n = m. +Lemma mul_opp_opp n m : - n * - m = n * m. Proof. - intros n m; rewrite Zplus_0_r; intro; assumption. + now destruct n, m. Qed. -Lemma Zplus_eq_compat : forall n m p q:Z, n = m -> p = q -> n + p = m + q. +Lemma mul_opp_comm n m : - n * m = n * - m. Proof. - intros; rewrite H; rewrite H0; reflexivity. + now destruct n, m. Qed. -Lemma Zplus_opp_expand : forall n m p:Z, n + - m = n + - p + (p + - m). +(** ** Distributivity of multiplication over addition *) + +Lemma mul_add_distr_pos (p:positive) n m : + pos p * (n + m) = pos p * n + pos p * m. Proof. - intros x y z. - rewrite <- (Zplus_assoc x). - rewrite (Zplus_assoc (- z)). - rewrite Zplus_opp_l. - reflexivity. + destruct n as [|n|n], m as [|m|m]; simpl; trivial; + rewrite ?pos_sub_spec, ?Pos.mul_compare_mono_l; try case Pos.compare_spec; + intros; now rewrite ?Pos.mul_add_distr_l, ?Pos.mul_sub_distr_l. Qed. -(************************************************************************) -(** * Properties of successor and predecessor on binary integer numbers *) +Lemma mul_add_distr_l n m p : n * (m + p) = n * m + n * p. +Proof. + destruct n as [|n|n]. trivial. + apply mul_add_distr_pos. + change (neg n) with (- pos n). + rewrite !mul_opp_l, <- opp_add_distr. f_equal. + apply mul_add_distr_pos. +Qed. -Theorem Zsucc_discr : forall n:Z, n <> Zsucc n. +Lemma mul_add_distr_r n m p : (n + m) * p = n * p + m * p. 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 ]. + rewrite !(mul_comm _ p). apply mul_add_distr_l. Qed. -Theorem Zpos_succ_morphism : - forall p:positive, Zpos (Psucc p) = Zsucc (Zpos p). +(** ** Basic properties of divisibility *) + +Lemma divide_Zpos p q : (pos p|pos q) <-> (p|q)%positive. Proof. - intro; rewrite Pplus_one_succ_r; unfold Zsucc in |- *; simpl in |- *; - trivial with arith. + split. + intros ([ |r|r],H); simpl in *; destr_eq H. exists r; auto. + intros (r,H). exists (pos r); simpl; now f_equal. Qed. -(** ** Successor and predecessor are inverse functions *) +Lemma divide_Zpos_Zneg_r n p : (n|pos p) <-> (n|neg p). +Proof. + split; intros (m,H); exists (-m); now rewrite mul_opp_l, <- H. +Qed. -Theorem Zsucc_pred : forall n:Z, n = Zsucc (Zpred n). +Lemma divide_Zpos_Zneg_l n p : (pos p|n) <-> (neg p|n). Proof. - intros n; unfold Zsucc, Zpred in |- *; rewrite <- Zplus_assoc; simpl in |- *; - rewrite Zplus_0_r; trivial with arith. + split; intros (m,H); exists (-m); now rewrite mul_opp_l, <- mul_opp_r. Qed. -Hint Immediate Zsucc_pred: zarith. +(** ** Conversions between [Z.testbit] and [N.testbit] *) -Theorem Zpred_succ : forall n:Z, n = Zpred (Zsucc n). +Lemma testbit_of_N a n : + testbit (of_N a) (of_N n) = N.testbit a n. Proof. - intros m; unfold Zpred, Zsucc in |- *; rewrite <- Zplus_assoc; simpl in |- *; - rewrite Zplus_comm; auto with arith. + destruct a as [|a], n; simpl; trivial. now destruct a. Qed. -Theorem Zsucc_inj : forall n m:Z, Zsucc n = Zsucc m -> n = m. +Lemma testbit_of_N' a n : 0<=n -> + testbit (of_N a) n = N.testbit a (to_N n). 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. + intro Hn. rewrite <- testbit_of_N. f_equal. + destruct n; trivial; now destruct Hn. Qed. -(*************************************************************************) -(** ** Properties of the direct definition of successor and predecessor *) +Lemma testbit_Zpos a n : 0<=n -> + testbit (pos a) n = N.testbit (N.pos a) (to_N n). +Proof. + intro Hn. now rewrite <- testbit_of_N'. +Qed. -Theorem Zsucc_succ' : forall n:Z, Zsucc n = Zsucc' n. +Lemma testbit_Zneg a n : 0<=n -> + testbit (neg a) n = negb (N.testbit (Pos.pred_N a) (to_N n)). Proof. -destruct n as [| p | p]; simpl. -reflexivity. -now rewrite Pplus_one_succ_r. -now destruct p as [q | q |]. + intro Hn. + rewrite <- testbit_of_N' by trivial. + destruct n as [ |n|n]; + [ | simpl; now destruct (Pos.pred_N a) | now destruct Hn]. + unfold testbit. + now destruct a as [|[ | | ]| ]. Qed. -Theorem Zpred_pred' : forall n:Z, Zpred n = Zpred' n. +End Private_BootStrap. + +(** * Proofs of specifications *) + +(** ** Specification of constants *) + +Lemma one_succ : 1 = succ 0. Proof. -destruct n as [| p | p]; simpl. reflexivity. -now destruct p as [q | q |]. -now rewrite Pplus_one_succ_r. Qed. -Theorem Zsucc'_inj : forall n m:Z, Zsucc' n = Zsucc' m -> n = m. +Lemma two_succ : 2 = succ 1. Proof. -intros n m; do 2 rewrite <- Zsucc_succ'; now apply Zsucc_inj. +reflexivity. Qed. -Theorem Zsucc'_pred' : forall n:Z, Zsucc' (Zpred' n) = n. +(** ** Specification of addition *) + +Lemma add_0_l n : 0 + n = n. Proof. -intro; rewrite <- Zsucc_succ'; rewrite <- Zpred_pred'; -symmetry; apply Zsucc_pred. + now destruct n. Qed. -Theorem Zpred'_succ' : forall n:Z, Zpred' (Zsucc' n) = n. +Lemma add_succ_l n m : succ n + m = succ (n + m). Proof. -intro; apply Zsucc'_inj; now rewrite Zsucc'_pred'. + unfold succ. now rewrite 2 (add_comm _ 1), add_assoc. Qed. -Theorem Zpred'_inj : forall n m:Z, Zpred' n = Zpred' m -> n = m. +(** ** Specification of opposite *) + +Lemma opp_0 : -0 = 0. Proof. -intros n m H. -rewrite <- (Zsucc'_pred' n); rewrite <- (Zsucc'_pred' m); now rewrite H. + reflexivity. Qed. -Theorem Zsucc'_discr : forall n:Z, n <> Zsucc' n. +Lemma opp_succ n : -(succ n) = pred (-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. + unfold succ, pred. apply opp_add_distr. Qed. -(** Misc properties, usually redundant or non natural *) +(** ** Specification of successor and predecessor *) -Lemma Zsucc_eq_compat : forall n m:Z, n = m -> Zsucc n = Zsucc m. +Lemma succ_pred n : succ (pred n) = n. Proof. - intros n m H; rewrite H; reflexivity. + unfold succ, pred. now rewrite <- add_assoc, add_opp_diag_r, add_0_r. Qed. -Lemma Zsucc_inj_contrapositive : forall n m:Z, n <> m -> Zsucc n <> Zsucc m. +Lemma pred_succ n : pred (succ n) = n. Proof. - unfold not in |- *; intros n m H1 H2; apply H1; apply Zsucc_inj; assumption. + unfold succ, pred. now rewrite <- add_assoc, add_opp_diag_r, add_0_r. Qed. -(**********************************************************************) -(** * Properties of subtraction on binary integer numbers *) +(** ** Specification of subtraction *) -(** ** [minus] and [Z0] *) - -Lemma Zminus_0_r : forall n:Z, n - Z0 = n. +Lemma sub_0_r n : n - 0 = n. Proof. - intro; unfold Zminus in |- *; simpl in |- *; rewrite Zplus_0_r; - trivial with arith. + apply add_0_r. Qed. -Lemma Zminus_0_l_reverse : forall n:Z, n = n - Z0. +Lemma sub_succ_r n m : n - succ m = pred (n - m). Proof. - intro; symmetry in |- *; apply Zminus_0_r. + unfold sub, succ, pred. now rewrite opp_add_distr, add_assoc. Qed. -Lemma Zminus_diag : forall n:Z, n - n = Z0. +(** ** Specification of multiplication *) + +Lemma mul_0_l n : 0 * n = 0. Proof. - intro; unfold Zminus in |- *; rewrite Zplus_opp_r; trivial with arith. + reflexivity. Qed. -Lemma Zminus_diag_reverse : forall n:Z, Z0 = n - n. +Lemma mul_succ_l n m : succ n * m = n * m + m. Proof. - intro; symmetry in |- *; apply Zminus_diag. + unfold succ. now rewrite mul_add_distr_r, mul_1_l. Qed. +(** ** Specification of comparisons and order *) -(** ** Relating [minus] with [plus] and [Zsucc] *) +Lemma eqb_eq n m : (n =? m) = true <-> n = m. +Proof. + destruct n, m; simpl; try (now split); rewrite Pos.eqb_eq; + split; (now injection 1) || (intros; now f_equal). +Qed. -Lemma Zminus_plus_distr : forall n m p:Z, n - (m + p) = n - m - p. +Lemma ltb_lt n m : (n <? m) = true <-> n < m. Proof. -intros; unfold Zminus; rewrite Zopp_plus_distr; apply Zplus_assoc. + unfold ltb, lt. destruct compare; easy'. Qed. -Lemma Zminus_succ_l : forall n m:Z, Zsucc (n - m) = Zsucc n - m. +Lemma leb_le n m : (n <=? m) = true <-> n <= m. Proof. - intros n m; unfold Zminus, Zsucc in |- *; rewrite (Zplus_comm n (- m)); - rewrite <- Zplus_assoc; apply Zplus_comm. + unfold leb, le. destruct compare; easy'. Qed. -Lemma Zminus_succ_r : forall n m:Z, n - (Zsucc m) = Zpred (n - m). +Lemma compare_eq_iff n m : (n ?= m) = Eq <-> n = m. Proof. -intros; unfold Zsucc; now rewrite Zminus_plus_distr. +destruct n, m; simpl; rewrite ?CompOpp_iff, ?Pos.compare_eq_iff; + split; congruence. Qed. -Lemma Zplus_minus_eq : forall n m p:Z, n = m + p -> p = n - m. +Lemma compare_sub n m : (n ?= m) = (n - m ?= 0). 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. + destruct n as [|n|n], m as [|m|m]; simpl; trivial; + rewrite <- ? Pos.compare_antisym, ?pos_sub_spec; + case Pos.compare_spec; trivial. Qed. -Lemma Zminus_plus : forall n m:Z, n + m - n = m. +Lemma compare_antisym n m : (m ?= n) = CompOpp (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. +destruct n, m; simpl; trivial; now rewrite <- ?Pos.compare_antisym. Qed. -Lemma Zplus_minus : forall n m:Z, n + (m - n) = m. +Lemma compare_lt_iff n m : (n ?= m) = Lt <-> n < m. +Proof. reflexivity. Qed. + +Lemma compare_le_iff n m : (n ?= m) <> Gt <-> n <= m. +Proof. reflexivity. Qed. + +(** Some more advanced properties of comparison and orders, + including [compare_spec] and [lt_irrefl] and [lt_eq_cases]. *) + +Include BoolOrderFacts. + +(** Remaining specification of [lt] and [le] *) + +Lemma lt_succ_r n m : n < succ m <-> n<=m. Proof. - unfold Zminus in |- *; intros n m; rewrite Zplus_permute; rewrite Zplus_opp_r; - apply Zplus_0_r. + unfold lt, le. rewrite compare_sub, sub_succ_r. + rewrite (compare_sub n m). + destruct (n-m) as [|[ | | ]|]; easy'. Qed. -Lemma Zminus_plus_simpl_l : forall n m p:Z, p + n - (p + m) = n - m. +(** ** Specification of minimum and maximum *) + +Lemma max_l n m : m<=n -> max n m = n. 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. + unfold le, max. rewrite (compare_antisym n m). + case compare; intuition. Qed. -Lemma Zminus_plus_simpl_l_reverse : forall n m p:Z, n - m = p + n - (p + m). +Lemma max_r n m : n<=m -> max n m = m. Proof. - intros; symmetry in |- *; apply Zminus_plus_simpl_l. + unfold le, max. case compare_spec; intuition. Qed. -Lemma Zminus_plus_simpl_r : forall n m p:Z, n + p - (m + p) = n - m. +Lemma min_l n m : n<=m -> min n m = n. Proof. - 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. + unfold le, min. case compare_spec; intuition. Qed. -Lemma Zpos_minus_morphism : forall a b:positive, Pcompare a b Eq = Lt -> - Zpos (b-a) = Zpos b - Zpos a. +Lemma min_r n m : m<=n -> min n m = m. Proof. - intros. - simpl. - change Eq with (CompOpp Eq). - rewrite <- Pcompare_antisym. - rewrite H; simpl; auto. + unfold le, min. + rewrite (compare_antisym n m). case compare_spec; intuition. Qed. -(** ** Misc redundant properties *) +(** ** Specification of absolute value *) -Lemma Zeq_minus : forall n m:Z, n = m -> n - m = Z0. +Lemma abs_eq n : 0 <= n -> abs n = n. Proof. - intros x y H; rewrite H; symmetry in |- *; apply Zminus_diag_reverse. + destruct n; trivial. now destruct 1. Qed. -Lemma Zminus_eq : forall n m:Z, n - m = Z0 -> n = m. +Lemma abs_neq n : n <= 0 -> abs n = - n. Proof. - intros x y H; rewrite <- (Zplus_minus y x); rewrite H; apply Zplus_0_r. + destruct n; trivial. now destruct 1. Qed. +(** ** Specification of sign *) -(**********************************************************************) -(** * Properties of multiplication on binary integer numbers *) - -Theorem Zpos_mult_morphism : - forall p q:positive, Zpos (p*q) = Zpos p * Zpos q. +Lemma sgn_null n : n = 0 -> sgn n = 0. Proof. - auto. + intros. now subst. Qed. -(** ** One is neutral for multiplication *) - -Theorem Zmult_1_l : forall n:Z, Zpos 1 * n = n. +Lemma sgn_pos n : 0 < n -> sgn n = 1. Proof. - intro x; destruct x; reflexivity. + now destruct n. Qed. -Theorem Zmult_1_r : forall n:Z, n * Zpos 1 = n. +Lemma sgn_neg n : n < 0 -> sgn n = -1. Proof. - intro x; destruct x; simpl in |- *; try rewrite Pmult_1_r; reflexivity. + now destruct n. Qed. -(** ** Zero property of multiplication *) +(** ** Specification of power *) -Theorem Zmult_0_l : forall n:Z, Z0 * n = Z0. +Lemma pow_0_r n : n^0 = 1. Proof. - intro x; destruct x; reflexivity. + reflexivity. Qed. -Theorem Zmult_0_r : forall n:Z, n * Z0 = Z0. +Lemma pow_succ_r n m : 0<=m -> n^(succ m) = n * n^m. Proof. - intro x; destruct x; reflexivity. + destruct m as [|m|m]; (now destruct 1) || (intros _); simpl; trivial. + unfold pow_pos. now rewrite Pos.add_comm, Pos.iter_add. Qed. -Hint Local Resolve Zmult_0_l Zmult_0_r. +Lemma pow_neg_r n m : m<0 -> n^m = 0. +Proof. + now destruct m. +Qed. -Lemma Zmult_0_r_reverse : forall n:Z, Z0 = n * Z0. +(** For folding back a [pow_pos] into a [pow] *) + +Lemma pow_pos_fold n p : pow_pos n p = n ^ (pos p). Proof. - intro x; destruct x; reflexivity. + reflexivity. Qed. -(** ** Commutativity of multiplication *) +(** ** Specification of square *) -Theorem Zmult_comm : forall n m:Z, n * m = m * n. +Lemma square_spec n : square n = n * n. Proof. - intros x y; destruct x as [| p| p]; destruct y as [| q| q]; simpl in |- *; - try rewrite (Pmult_comm p q); reflexivity. + destruct n; trivial; simpl; f_equal; apply Pos.square_spec. Qed. -(** ** Associativity of multiplication *) +(** ** Specification of square root *) -Theorem Zmult_assoc : forall n m p:Z, n * (m * p) = n * m * p. +Lemma sqrtrem_spec n : 0<=n -> + let (s,r) := sqrtrem n in n = s*s + r /\ 0 <= r <= 2*s. Proof. - intros x y z; destruct x; destruct y; destruct z; simpl in |- *; - try rewrite Pmult_assoc; reflexivity. + destruct n. now repeat split. + generalize (Pos.sqrtrem_spec p). simpl. + destruct 1; simpl; subst; now repeat split. + now destruct 1. Qed. -Lemma Zmult_assoc_reverse : forall n m p:Z, n * m * p = n * (m * p). +Lemma sqrt_spec n : 0<=n -> + let s := sqrt n in s*s <= n < (succ s)*(succ s). Proof. - intros n m p; rewrite Zmult_assoc; trivial with arith. + destruct n. now repeat split. unfold sqrt. + intros _. simpl succ. rewrite Pos.add_1_r. apply (Pos.sqrt_spec p). + now destruct 1. Qed. -(** ** Associativity mixed with commutativity *) +Lemma sqrt_neg n : n<0 -> sqrt n = 0. +Proof. + now destruct n. +Qed. -Theorem Zmult_permute : forall n m p:Z, n * (m * p) = m * (n * p). +Lemma sqrtrem_sqrt n : fst (sqrtrem n) = sqrt n. Proof. - intros x y z; rewrite (Zmult_assoc y x z); rewrite (Zmult_comm y x). - apply Zmult_assoc. + destruct n; try reflexivity. + unfold sqrtrem, sqrt, Pos.sqrt. + destruct (Pos.sqrtrem p) as (s,r). now destruct r. Qed. -(** ** Z is integral *) +(** ** Specification of logarithm *) -Theorem Zmult_integral_l : forall n m:Z, n <> Z0 -> m * n = Z0 -> m = Z0. +Lemma log2_spec n : 0 < n -> 2^(log2 n) <= n < 2^(succ (log2 n)). 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. + assert (Pow : forall p q, pos (p^q) = (pos p)^(pos q)). + { intros. now apply Pos.iter_swap_gen. } + destruct n as [|[p|p|]|]; intros Hn; split; try easy; unfold log2; + simpl succ; rewrite ?Pos.add_1_r, <- Pow. + change (2^Pos.size p <= Pos.succ (p~0))%positive. + apply Pos.lt_le_incl, Pos.lt_succ_r, Pos.size_le. + apply Pos.size_gt. + apply Pos.size_le. + apply Pos.size_gt. Qed. - -Theorem Zmult_integral : forall n m:Z, n * m = Z0 -> n = Z0 \/ m = Z0. +Lemma log2_nonpos n : n<=0 -> log2 n = 0. Proof. - intros x y; destruct x; destruct y; auto; simpl in |- *; intro H; - discriminate H. + destruct n as [|p|p]; trivial; now destruct 1. Qed. +(** Specification of parity functions *) + +Lemma even_spec n : even n = true <-> Even n. +Proof. + split. + exists (div2 n). now destruct n as [|[ | | ]|[ | | ]]. + intros (m,->). now destruct m. +Qed. -Lemma Zmult_1_inversion_l : - forall n m:Z, n * m = Zpos 1 -> n = Zpos 1 \/ n = Zneg 1. +Lemma odd_spec n : odd n = true <-> Odd n. 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). + split. + exists (div2 n). destruct n as [|[ | | ]|[ | | ]]; simpl; try easy. + now rewrite Pos.pred_double_succ. + intros (m,->). now destruct m as [|[ | | ]|[ | | ]]. Qed. (** ** Multiplication and Doubling *) -Lemma Zdouble_mult : forall z, Zdouble z = (Zpos 2) * z. +Lemma double_spec n : double n = 2*n. +Proof. + reflexivity. +Qed. + +Lemma succ_double_spec n : succ_double n = 2*n + 1. +Proof. + now destruct n. +Qed. + +Lemma pred_double_spec n : pred_double n = 2*n - 1. +Proof. + now destruct n. +Qed. + +(** ** Correctness proofs for Trunc division *) + +Lemma pos_div_eucl_eq a b : 0 < b -> + let (q, r) := pos_div_eucl a b in pos a = q * b + r. +Proof. + intros Hb. + induction a; unfold pos_div_eucl; fold pos_div_eucl. + - (* ~1 *) + destruct pos_div_eucl as (q,r). + change (pos a~1) with (2*(pos a)+1). + rewrite IHa, mul_add_distr_l, mul_assoc. + destruct ltb. + now rewrite add_assoc. + rewrite mul_add_distr_r, mul_1_l, <- !add_assoc. f_equal. + unfold sub. now rewrite (add_comm _ (-b)), add_assoc, add_opp_diag_r. + - (* ~0 *) + destruct pos_div_eucl as (q,r). + change (pos a~0) with (2*pos a). + rewrite IHa, mul_add_distr_l, mul_assoc. + destruct ltb. + trivial. + rewrite mul_add_distr_r, mul_1_l, <- !add_assoc. f_equal. + unfold sub. now rewrite (add_comm _ (-b)), add_assoc, add_opp_diag_r. + - (* 1 *) + case leb_spec; trivial. + intros Hb'. + destruct b as [|b|b]; try easy; clear Hb. + replace b with 1%positive; trivial. + apply Pos.le_antisym. apply Pos.le_1_l. now apply Pos.lt_succ_r. +Qed. + +Lemma div_eucl_eq a b : b<>0 -> + let (q, r) := div_eucl a b in a = b * q + r. +Proof. + destruct a as [ |a|a], b as [ |b|b]; unfold div_eucl; trivial; + (now destruct 1) || intros _; + generalize (pos_div_eucl_eq a (pos b) (eq_refl _)); + destruct pos_div_eucl as (q,r); rewrite mul_comm. + - (* pos pos *) + trivial. + - (* pos neg *) + intros ->. + destruct r as [ |r|r]; rewrite <- !mul_opp_comm; trivial; + rewrite mul_add_distr_l, mul_1_r, <- add_assoc; f_equal; + now rewrite add_assoc, add_opp_diag_r. + - (* neg pos *) + change (neg a) with (- pos a). intros ->. + rewrite (opp_add_distr _ r), <- mul_opp_r. + destruct r as [ |r|r]; trivial; + rewrite opp_add_distr, mul_add_distr_l, <- add_assoc; f_equal; + unfold sub; now rewrite add_assoc, mul_opp_r, mul_1_r, add_opp_diag_l. + - (* neg neg *) + change (neg a) with (- pos a). intros ->. + now rewrite opp_add_distr, <- mul_opp_l. +Qed. + +Lemma div_mod a b : b<>0 -> a = b*(a/b) + (a mod b). +Proof. + intros Hb. generalize (div_eucl_eq a b Hb). + unfold div, modulo. now destruct div_eucl. +Qed. + +Lemma pos_div_eucl_bound a b : 0<b -> 0 <= snd (pos_div_eucl a b) < b. +Proof. + assert (AUX : forall m p, m < pos (p~0) -> m - pos p < pos p). + intros m p. unfold lt. + rewrite (compare_sub m), (compare_sub _ (pos _)). unfold sub. + rewrite <- add_assoc. simpl opp; simpl (neg _ + _). + now rewrite Pos.add_diag. + intros Hb. + destruct b as [|b|b]; discriminate Hb || clear Hb. + induction a; unfold pos_div_eucl; fold pos_div_eucl. + (* ~1 *) + destruct pos_div_eucl as (q,r). + simpl in IHa; destruct IHa as (Hr,Hr'). + case ltb_spec; intros H; unfold snd. split; trivial. now destruct r. + split. unfold le. + now rewrite compare_antisym, <- compare_sub, <- compare_antisym. + apply AUX. rewrite <- succ_double_spec. + destruct r; try easy. unfold lt in *; simpl in *. + now rewrite Pos.compare_xI_xO, Hr'. + (* ~0 *) + destruct pos_div_eucl as (q,r). + simpl in IHa; destruct IHa as (Hr,Hr'). + case ltb_spec; intros H; unfold snd. split; trivial. now destruct r. + split. unfold le. + now rewrite compare_antisym, <- compare_sub, <- compare_antisym. + apply AUX. destruct r; try easy. + (* 1 *) + case leb_spec; intros H; simpl; split; try easy. + red; simpl. now apply Pos.le_succ_l. +Qed. + +Lemma mod_pos_bound a b : 0 < b -> 0 <= a mod b < b. +Proof. + destruct b as [|b|b]; try easy; intros _. + destruct a as [|a|a]; unfold modulo, div_eucl. + now split. + now apply pos_div_eucl_bound. + generalize (pos_div_eucl_bound a (pos b) (eq_refl _)). + destruct pos_div_eucl as (q,r); unfold snd; intros (Hr,Hr'). + destruct r as [|r|r]; (now destruct Hr) || clear Hr. + now split. + split. unfold le. + now rewrite compare_antisym, <- compare_sub, <- compare_antisym, Hr'. + unfold lt in *; simpl in *. rewrite pos_sub_gt by trivial. + simpl. now apply Pos.sub_decr. +Qed. + +Definition mod_bound_pos a b (_:0<=a) := mod_pos_bound a b. + +Lemma mod_neg_bound a b : b < 0 -> b < a mod b <= 0. +Proof. + destruct b as [|b|b]; try easy; intros _. + destruct a as [|a|a]; unfold modulo, div_eucl. + now split. + generalize (pos_div_eucl_bound a (pos b) (eq_refl _)). + destruct pos_div_eucl as (q,r); unfold snd; intros (Hr,Hr'). + destruct r as [|r|r]; (now destruct Hr) || clear Hr. + now split. + split. + unfold lt in *; simpl in *. rewrite pos_sub_lt by trivial. + rewrite <- Pos.compare_antisym. now apply Pos.sub_decr. + change (neg b - neg r <= 0). unfold le, lt in *. + rewrite <- compare_sub. simpl in *. + now rewrite <- Pos.compare_antisym, Hr'. + generalize (pos_div_eucl_bound a (pos b) (eq_refl _)). + destruct pos_div_eucl as (q,r); unfold snd; intros (Hr,Hr'). + split; destruct r; try easy. + red; simpl; now rewrite <- Pos.compare_antisym. +Qed. + +(** ** Correctness proofs for Floor division *) + +Theorem quotrem_eq a b : let (q,r) := quotrem a b in a = q * b + r. Proof. - reflexivity. + destruct a as [|a|a], b as [|b|b]; simpl; trivial; + generalize (N.pos_div_eucl_spec a (N.pos b)); case N.pos_div_eucl; trivial; + intros q r; + try change (neg a) with (-pos a); + change (pos a) with (of_N (N.pos a)); intros ->; now destruct q, r. Qed. -Lemma Zdouble_plus_one_mult : forall z, - Zdouble_plus_one z = (Zpos 2) * z + (Zpos 1). +Lemma quot_rem' a b : a = b*(a÷b) + rem a b. Proof. - destruct z; simpl; auto with zarith. + rewrite mul_comm. generalize (quotrem_eq a b). + unfold quot, rem. now destruct quotrem. Qed. -(** ** Multiplication and Opposite *) +Lemma quot_rem a b : b<>0 -> a = b*(a÷b) + rem a b. +Proof. intros _. apply quot_rem'. Qed. -Theorem Zopp_mult_distr_l : forall n m:Z, - (n * m) = - n * m. +Lemma rem_bound_pos a b : 0<=a -> 0<b -> 0 <= rem a b < b. Proof. - intros x y; destruct x; destruct y; reflexivity. + intros Ha Hb. + destruct b as [|b|b]; (now discriminate Hb) || clear Hb; + destruct a as [|a|a]; (now destruct Ha) || clear Ha. + compute. now split. + unfold rem, quotrem. + assert (H := N.pos_div_eucl_remainder a (N.pos b)). + destruct N.pos_div_eucl as (q,[|r]); simpl; split; try easy. + now apply H. Qed. -Theorem Zopp_mult_distr_r : forall n m:Z, - (n * m) = n * - m. +Lemma rem_opp_l' a b : rem (-a) b = - (rem a b). Proof. - intros x y; rewrite (Zmult_comm x y); rewrite Zopp_mult_distr_l; - apply Zmult_comm. + destruct a, b; trivial; unfold rem; simpl; + now destruct N.pos_div_eucl as (q,[|r]). Qed. -Lemma Zopp_mult_distr_l_reverse : forall n m:Z, - n * m = - (n * m). +Lemma rem_opp_r' a b : rem a (-b) = rem a b. Proof. - intros x y; symmetry in |- *; apply Zopp_mult_distr_l. + destruct a, b; trivial; unfold rem; simpl; + now destruct N.pos_div_eucl as (q,[|r]). Qed. -Theorem Zmult_opp_comm : forall n m:Z, - n * m = n * - m. +Lemma rem_opp_l a b : b<>0 -> rem (-a) b = - (rem a b). +Proof. intros _. apply rem_opp_l'. Qed. + +Lemma rem_opp_r a b : b<>0 -> rem a (-b) = rem a b. +Proof. intros _. apply rem_opp_r'. Qed. + +(** ** Correctness proofs for gcd *) + +Lemma ggcd_gcd a b : fst (ggcd a b) = gcd a b. Proof. - intros x y; rewrite Zopp_mult_distr_l_reverse; rewrite Zopp_mult_distr_r; - trivial with arith. + destruct a as [ |p|p], b as [ |q|q]; simpl; auto; + generalize (Pos.ggcd_gcd p q); destruct Pos.ggcd as (g,(aa,bb)); + simpl; congruence. Qed. -Theorem Zmult_opp_opp : forall n m:Z, - n * - m = n * m. +Lemma ggcd_correct_divisors a b : + let '(g,(aa,bb)) := ggcd a b in + a = g*aa /\ b = g*bb. Proof. - intros x y; destruct x; destruct y; reflexivity. + destruct a as [ |p|p], b as [ |q|q]; simpl; rewrite ?Pos.mul_1_r; auto; + generalize (Pos.ggcd_correct_divisors p q); + destruct Pos.ggcd as (g,(aa,bb)); simpl; destruct 1; now subst. Qed. -Theorem Zopp_eq_mult_neg_1 : forall n:Z, - n = n * Zneg 1. +Lemma gcd_divide_l a b : (gcd a b | a). Proof. - intro x; induction x; intros; rewrite Zmult_comm; auto with arith. + rewrite <- ggcd_gcd. generalize (ggcd_correct_divisors a b). + destruct ggcd as (g,(aa,bb)); simpl. intros (H,_). exists aa. + now rewrite mul_comm. Qed. -(** ** Distributivity of multiplication over addition *) +Lemma gcd_divide_r a b : (gcd a b | b). +Proof. + rewrite <- ggcd_gcd. generalize (ggcd_correct_divisors a b). + destruct ggcd as (g,(aa,bb)); simpl. intros (_,H). exists bb. + now rewrite mul_comm. +Qed. -Lemma weak_Zmult_plus_distr_r : - forall (p:positive) (n m:Z), Zpos p * (n + m) = Zpos p * n + Zpos p * m. +Lemma gcd_greatest a b c : (c|a) -> (c|b) -> (c | gcd a b). 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) ] ]). + assert (H : forall p q r, (r|pos p) -> (r|pos q) -> (r|pos (Pos.gcd p q))). + { intros p q [|r|r] H H'. + destruct H; now rewrite mul_comm in *. + apply divide_Zpos, Pos.gcd_greatest; now apply divide_Zpos. + apply divide_Zpos_Zneg_l, divide_Zpos, Pos.gcd_greatest; + now apply divide_Zpos, divide_Zpos_Zneg_l. + } + destruct a, b; simpl; auto; intros; try apply H; trivial; + now apply divide_Zpos_Zneg_r. Qed. -Theorem Zmult_plus_distr_r : forall n m p:Z, n * (m + p) = n * m + n * p. +Lemma gcd_nonneg a b : 0 <= gcd a b. 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 ]. + now destruct a, b. Qed. -Theorem Zmult_plus_distr_l : forall n m p:Z, (n + m) * p = n * p + m * p. +(** ggcd and opp : an auxiliary result used in QArith *) + +Theorem ggcd_opp a b : + ggcd (-a) b = (let '(g,(aa,bb)) := ggcd a b in (g,(-aa,bb))). Proof. - intros n m p; rewrite Zmult_comm; rewrite Zmult_plus_distr_r; - do 2 rewrite (Zmult_comm p); trivial with arith. + destruct a as [|a|a], b as [|b|b]; unfold ggcd, opp; auto; + destruct (Pos.ggcd a b) as (g,(aa,bb)); auto. Qed. -(** ** Distributivity of multiplication over subtraction *) +(** ** Proofs of specifications for bitwise operations *) -Lemma Zmult_minus_distr_r : forall n m p:Z, (n - m) * p = n * p - m * p. +Lemma div2_spec a : div2 a = shiftr a 1. Proof. - intros x y z; unfold Zminus in |- *. - rewrite <- Zopp_mult_distr_l_reverse. - apply Zmult_plus_distr_l. + reflexivity. Qed. +Lemma testbit_0_l n : testbit 0 n = false. +Proof. + now destruct n. +Qed. -Lemma Zmult_minus_distr_l : forall n m p:Z, p * (n - m) = p * n - p * m. +Lemma testbit_neg_r a n : n<0 -> testbit a n = false. 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. + now destruct n. Qed. -(** ** Simplification of multiplication for non-zero integers *) +Lemma testbit_odd_0 a : testbit (2*a+1) 0 = true. +Proof. + now destruct a as [|a|[a|a|]]. +Qed. -Lemma Zmult_reg_l : forall n m p:Z, p <> Z0 -> p * n = p * m -> n = m. +Lemma testbit_even_0 a : testbit (2*a) 0 = false. 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. + now destruct a. Qed. -Lemma Zmult_reg_r : forall n m p:Z, p <> Z0 -> n * p = m * p -> n = m. +Lemma testbit_odd_succ a n : 0<=n -> + testbit (2*a+1) (succ n) = testbit a n. Proof. - intros x y z Hz. - rewrite (Zmult_comm x z). - rewrite (Zmult_comm y z). - intro; apply Zmult_reg_l with z; assumption. + destruct n as [|n|n]; (now destruct 1) || intros _. + destruct a as [|[a|a|]|[a|a|]]; simpl; trivial. now destruct a. + unfold testbit; simpl. + destruct a as [|a|[a|a|]]; simpl; trivial; + rewrite ?Pos.add_1_r, ?Pos.pred_N_succ; now destruct n. Qed. -(** ** Addition and multiplication by 2 *) +Lemma testbit_even_succ a n : 0<=n -> + testbit (2*a) (succ n) = testbit a n. +Proof. + destruct n as [|n|n]; (now destruct 1) || intros _. + destruct a as [|[a|a|]|[a|a|]]; simpl; trivial. now destruct a. + unfold testbit; simpl. + destruct a as [|a|[a|a|]]; simpl; trivial; + rewrite ?Pos.add_1_r, ?Pos.pred_N_succ; now destruct n. +Qed. -Lemma Zplus_diag_eq_mult_2 : forall n:Z, n + n = n * Zpos 2. +(** Correctness proofs about [Z.shiftr] and [Z.shiftl] *) + +Lemma shiftr_spec_aux a n m : 0<=n -> 0<=m -> + testbit (shiftr a n) m = testbit a (m+n). Proof. - intros x; pattern x at 1 2 in |- *; rewrite <- (Zmult_1_r x); - rewrite <- Zmult_plus_distr_r; reflexivity. + intros Hn Hm. unfold shiftr. + destruct n as [ |n|n]; (now destruct Hn) || clear Hn; simpl. + now rewrite add_0_r. + assert (forall p, to_N (m + pos p) = (to_N m + N.pos p)%N). + destruct m; trivial; now destruct Hm. + assert (forall p, 0 <= m + pos p). + destruct m; easy || now destruct Hm. + destruct a as [ |a|a]. + (* a = 0 *) + replace (Pos.iter n div2 0) with 0 + by (apply Pos.iter_invariant; intros; subst; trivial). + now rewrite 2 testbit_0_l. + (* a > 0 *) + change (pos a) with (of_N (N.pos a)) at 1. + rewrite <- (Pos.iter_swap_gen _ _ _ N.div2) by now intros [|[ | | ]]. + rewrite testbit_Zpos, testbit_of_N', H; trivial. + exact (N.shiftr_spec' (N.pos a) (N.pos n) (to_N m)). + (* a < 0 *) + rewrite <- (Pos.iter_swap_gen _ _ _ Pos.div2_up) by trivial. + rewrite 2 testbit_Zneg, H; trivial. f_equal. + rewrite (Pos.iter_swap_gen _ _ _ _ N.div2) by exact N.pred_div2_up. + exact (N.shiftr_spec' (Pos.pred_N a) (N.pos n) (to_N m)). Qed. -(** ** Multiplication and successor *) +Lemma shiftl_spec_low a n m : m<n -> + testbit (shiftl a n) m = false. +Proof. + intros H. destruct n as [|n|n], m as [|m|m]; try easy; simpl shiftl. + destruct (Pos.succ_pred_or n) as [-> | <-]; + rewrite ?Pos.iter_succ; apply testbit_even_0. + destruct a as [ |a|a]. + (* a = 0 *) + replace (Pos.iter n (mul 2) 0) with 0 + by (apply Pos.iter_invariant; intros; subst; trivial). + apply testbit_0_l. + (* a > 0 *) + rewrite <- (Pos.iter_swap_gen _ _ _ xO) by trivial. + rewrite testbit_Zpos by easy. + exact (N.shiftl_spec_low (N.pos a) (N.pos n) (N.pos m) H). + (* a < 0 *) + rewrite <- (Pos.iter_swap_gen _ _ _ xO) by trivial. + rewrite testbit_Zneg by easy. + now rewrite (N.pos_pred_shiftl_low a (N.pos n)). +Qed. + +Lemma shiftl_spec_high a n m : 0<=m -> n<=m -> + testbit (shiftl a n) m = testbit a (m-n). +Proof. + intros Hm H. + destruct n as [ |n|n]. simpl. now rewrite sub_0_r. + (* n > 0 *) + destruct m as [ |m|m]; try (now destruct H). + assert (0 <= pos m - pos n). + red. now rewrite compare_antisym, <- compare_sub, <- compare_antisym. + assert (EQ : to_N (pos m - pos n) = (N.pos m - N.pos n)%N). + red in H. simpl in H. simpl to_N. + rewrite pos_sub_spec, Pos.compare_antisym. + destruct (Pos.compare_spec n m) as [H'|H'|H']; try (now destruct H). + subst. now rewrite N.sub_diag. + simpl. destruct (Pos.sub_mask_pos' m n H') as (p & -> & <-). + f_equal. now rewrite Pos.add_comm, Pos.add_sub. + destruct a; unfold shiftl. + (* ... a = 0 *) + replace (Pos.iter n (mul 2) 0) with 0 + by (apply Pos.iter_invariant; intros; subst; trivial). + now rewrite 2 testbit_0_l. + (* ... a > 0 *) + rewrite <- (Pos.iter_swap_gen _ _ _ xO) by trivial. + rewrite 2 testbit_Zpos, EQ by easy. + exact (N.shiftl_spec_high' (N.pos p) (N.pos n) (N.pos m) H). + (* ... a < 0 *) + rewrite <- (Pos.iter_swap_gen _ _ _ xO) by trivial. + rewrite 2 testbit_Zneg, EQ by easy. f_equal. + simpl to_N. + rewrite <- N.shiftl_spec_high by easy. + now apply (N.pos_pred_shiftl_high p (N.pos n)). + (* n < 0 *) + unfold sub. simpl. + now apply (shiftr_spec_aux a (pos n) m). +Qed. + +Lemma shiftr_spec a n m : 0<=m -> + testbit (shiftr a n) m = testbit a (m+n). +Proof. + intros Hm. + destruct (leb_spec 0 n). + now apply shiftr_spec_aux. + destruct (leb_spec (-n) m) as [LE|GT]. + unfold shiftr. + rewrite (shiftl_spec_high a (-n) m); trivial. now destruct n. + unfold shiftr. + rewrite (shiftl_spec_low a (-n) m); trivial. + rewrite testbit_neg_r; trivial. + red in GT. rewrite compare_sub in GT. now destruct n. +Qed. + +(** Correctness proofs for bitwise operations *) + +Lemma lor_spec a b n : + testbit (lor a b) n = testbit a n || testbit b n. +Proof. + destruct (leb_spec 0 n) as [Hn|Hn]; [|now rewrite !testbit_neg_r]. + destruct a as [ |a|a], b as [ |b|b]; + rewrite ?testbit_0_l, ?orb_false_r; trivial; unfold lor; + rewrite ?testbit_Zpos, ?testbit_Zneg, ?N.pos_pred_succ by trivial. + now rewrite <- N.lor_spec. + now rewrite N.ldiff_spec, negb_andb, negb_involutive, orb_comm. + now rewrite N.ldiff_spec, negb_andb, negb_involutive. + now rewrite N.land_spec, negb_andb. +Qed. + +Lemma land_spec a b n : + testbit (land a b) n = testbit a n && testbit b n. +Proof. + destruct (leb_spec 0 n) as [Hn|Hn]; [|now rewrite !testbit_neg_r]. + destruct a as [ |a|a], b as [ |b|b]; + rewrite ?testbit_0_l, ?andb_false_r; trivial; unfold land; + rewrite ?testbit_Zpos, ?testbit_Zneg, ?testbit_of_N', ?N.pos_pred_succ + by trivial. + now rewrite <- N.land_spec. + now rewrite N.ldiff_spec. + now rewrite N.ldiff_spec, andb_comm. + now rewrite N.lor_spec, negb_orb. +Qed. + +Lemma ldiff_spec a b n : + testbit (ldiff a b) n = testbit a n && negb (testbit b n). +Proof. + destruct (leb_spec 0 n) as [Hn|Hn]; [|now rewrite !testbit_neg_r]. + destruct a as [ |a|a], b as [ |b|b]; + rewrite ?testbit_0_l, ?andb_true_r; trivial; unfold ldiff; + rewrite ?testbit_Zpos, ?testbit_Zneg, ?testbit_of_N', ?N.pos_pred_succ + by trivial. + now rewrite <- N.ldiff_spec. + now rewrite N.land_spec, negb_involutive. + now rewrite N.lor_spec, negb_orb. + now rewrite N.ldiff_spec, negb_involutive, andb_comm. +Qed. + +Lemma lxor_spec a b n : + testbit (lxor a b) n = xorb (testbit a n) (testbit b n). +Proof. + destruct (leb_spec 0 n) as [Hn|Hn]; [|now rewrite !testbit_neg_r]. + destruct a as [ |a|a], b as [ |b|b]; + rewrite ?testbit_0_l, ?xorb_false_l, ?xorb_false_r; trivial; unfold lxor; + rewrite ?testbit_Zpos, ?testbit_Zneg, ?testbit_of_N', ?N.pos_pred_succ + by trivial. + now rewrite <- N.lxor_spec. + now rewrite N.lxor_spec, negb_xorb_r. + now rewrite N.lxor_spec, negb_xorb_l. + now rewrite N.lxor_spec, xorb_negb_negb. +Qed. -Lemma Zmult_succ_r : forall n m:Z, n * Zsucc m = n * m + n. +(** ** Induction principles based on successor / predecessor *) + +Lemma peano_ind (P : Z -> Prop) : + P 0 -> + (forall x, P x -> P (succ x)) -> + (forall x, P x -> P (pred x)) -> + forall z, P z. 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. + intros H0 Hs Hp z; destruct z. + assumption. + induction p using Pos.peano_ind. + now apply (Hs 0). + rewrite <- Pos.add_1_r. + now apply (Hs (pos p)). + induction p using Pos.peano_ind. + now apply (Hp 0). + rewrite <- Pos.add_1_r. + now apply (Hp (neg p)). Qed. -Lemma Zmult_succ_r_reverse : forall n m:Z, n * m + n = n * Zsucc m. +Lemma bi_induction (P : Z -> Prop) : + Proper (eq ==> iff) P -> + P 0 -> + (forall x, P x <-> P (succ x)) -> + forall z, P z. Proof. - intros; symmetry in |- *; apply Zmult_succ_r. + intros _ H0 Hs. induction z using peano_ind. + assumption. + now apply -> Hs. + apply Hs. now rewrite succ_pred. Qed. -Lemma Zmult_succ_l : forall n m:Z, Zsucc n * m = n * m + m. + +(** * Proofs of morphisms, obvious since eq is Leibniz *) + +Local Obligation Tactic := simpl_relation. +Program Definition succ_wd : Proper (eq==>eq) succ := _. +Program Definition pred_wd : Proper (eq==>eq) pred := _. +Program Definition opp_wd : Proper (eq==>eq) opp := _. +Program Definition add_wd : Proper (eq==>eq==>eq) add := _. +Program Definition sub_wd : Proper (eq==>eq==>eq) sub := _. +Program Definition mul_wd : Proper (eq==>eq==>eq) mul := _. +Program Definition lt_wd : Proper (eq==>eq==>iff) lt := _. +Program Definition div_wd : Proper (eq==>eq==>eq) div := _. +Program Definition mod_wd : Proper (eq==>eq==>eq) modulo := _. +Program Definition quot_wd : Proper (eq==>eq==>eq) quot := _. +Program Definition rem_wd : Proper (eq==>eq==>eq) rem := _. +Program Definition pow_wd : Proper (eq==>eq==>eq) pow := _. +Program Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _. + +(** The Bind Scope prevents Z to stay associated with abstract_scope. + (TODO FIX) *) + +Include ZProp. Bind Scope Z_scope with Z. +Include UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties. + +(** In generic statements, the predicates [lt] and [le] have been + favored, whereas [gt] and [ge] don't even exist in the abstract + layers. The use of [gt] and [ge] is hence not recommended. We provide + here the bare minimal results to related them with [lt] and [le]. *) + +Lemma gt_lt_iff n m : n > m <-> m < n. Proof. - intros n m; unfold Zsucc in |- *; rewrite Zmult_plus_distr_l; - rewrite Zmult_1_l; trivial with arith. + unfold lt, gt. now rewrite compare_antisym, CompOpp_iff. Qed. -Lemma Zmult_succ_l_reverse : forall n m:Z, n * m + m = Zsucc n * m. +Lemma gt_lt n m : n > m -> m < n. Proof. - intros; symmetry in |- *; apply Zmult_succ_l. + apply gt_lt_iff. Qed. +Lemma lt_gt n m : n < m -> m > n. +Proof. + apply gt_lt_iff. +Qed. +Lemma ge_le_iff n m : n >= m <-> m <= n. +Proof. + unfold le, ge. now rewrite compare_antisym, CompOpp_iff. +Qed. -(** ** Misc redundant properties *) +Lemma ge_le n m : n >= m -> m <= n. +Proof. + apply ge_le_iff. +Qed. -Lemma Z_eq_mult : forall n m:Z, m = Z0 -> m * n = Z0. +Lemma le_ge n m : n <= m -> m >= n. Proof. - intros x y H; rewrite H; auto with arith. + apply ge_le_iff. Qed. +(** We provide a tactic converting from one style to the other. *) +Ltac swap_greater := rewrite ?gt_lt_iff in *; rewrite ?ge_le_iff in *. -(**********************************************************************) -(** * Relating binary positive numbers and binary integers *) +(** Similarly, the boolean comparisons [ltb] and [leb] are favored + over their dual [gtb] and [geb]. We prove here the equivalence + and a few minimal results. *) -Lemma Zpos_eq : forall p q:positive, p = q -> Zpos p = Zpos q. +Lemma gtb_ltb n m : (n >? m) = (m <? n). Proof. - intros; f_equal; auto. + unfold gtb, ltb. rewrite compare_antisym. now case compare. Qed. -Lemma Zpos_eq_rev : forall p q:positive, Zpos p = Zpos q -> p = q. +Lemma geb_leb n m : (n >=? m) = (m <=? n). Proof. - inversion 1; auto. + unfold geb, leb. rewrite compare_antisym. now case compare. Qed. -Lemma Zpos_eq_iff : forall p q:positive, p = q <-> Zpos p = Zpos q. +Lemma gtb_lt n m : (n >? m) = true <-> m < n. Proof. - split; [apply Zpos_eq|apply Zpos_eq_rev]. + rewrite gtb_ltb. apply ltb_lt. Qed. -Lemma Zpos_xI : forall p:positive, Zpos p~1 = Zpos 2 * Zpos p + Zpos 1. +Lemma geb_le n m : (n >=? m) = true <-> m <= n. Proof. - intro; apply refl_equal. + rewrite geb_leb. apply leb_le. Qed. -Lemma Zpos_xO : forall p:positive, Zpos p~0 = Zpos 2 * Zpos p. +Lemma gtb_spec n m : BoolSpec (m<n) (n<=m) (n >? m). Proof. - intro; apply refl_equal. + rewrite gtb_ltb. apply ltb_spec. Qed. -Lemma Zneg_xI : forall p:positive, Zneg p~1 = Zpos 2 * Zneg p - Zpos 1. +Lemma geb_spec n m : BoolSpec (m<=n) (n<m) (n >=? m). Proof. - intro; apply refl_equal. + rewrite geb_leb. apply leb_spec. Qed. -Lemma Zneg_xO : forall p:positive, Zneg p~0 = Zpos 2 * Zneg p. +(** TODO : to add in Numbers ? *) + +Lemma add_reg_l n m p : n + m = n + p -> m = p. Proof. - reflexivity. + exact (proj1 (add_cancel_l m p n)). Qed. -Lemma Zpos_plus_distr : forall p q:positive, Zpos (p + q) = Zpos p + Zpos q. +Lemma mul_reg_l n m p : p <> 0 -> p * n = p * m -> n = m. Proof. - intros p p'; destruct p; - [ destruct p' as [p0| p0| ] - | destruct p' as [p0| p0| ] - | destruct p' as [p| p| ] ]; reflexivity. + exact (fun Hp => proj1 (mul_cancel_l n m p Hp)). Qed. -Lemma Zneg_plus_distr : forall p q:positive, Zneg (p + q) = Zneg p + Zneg q. +Lemma mul_reg_r n m p : p <> 0 -> n * p = m * p -> n = m. Proof. - intros p p'; destruct p; - [ destruct p' as [p0| p0| ] - | destruct p' as [p0| p0| ] - | destruct p' as [p| p| ] ]; reflexivity. + exact (fun Hp => proj1 (mul_cancel_r n m p Hp)). Qed. -(**********************************************************************) -(** * Order relations *) +Lemma opp_eq_mul_m1 n : - n = n * -1. +Proof. + rewrite mul_comm. now destruct n. +Qed. -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. +Lemma add_diag n : n + n = 2 * n. +Proof. + change 2 with (1+1). now rewrite mul_add_distr_r, !mul_1_l. +Qed. + +(** * Comparison and opposite *) -Infix "<=" := Zle : Z_scope. -Infix "<" := Zlt : Z_scope. -Infix ">=" := Zge : Z_scope. -Infix ">" := Zgt : Z_scope. +Lemma compare_opp n m : (- n ?= - m) = (m ?= n). +Proof. + destruct n, m; simpl; trivial; intros; now rewrite <- Pos.compare_antisym. +Qed. +(** * Comparison and addition *) + +Lemma add_compare_mono_l n m p : (n + m ?= n + p) = (m ?= p). +Proof. + rewrite (compare_sub m p), compare_sub. f_equal. + unfold sub. rewrite opp_add_distr, (add_comm n m), add_assoc. + f_equal. now rewrite <- add_assoc, add_opp_diag_r, add_0_r. +Qed. + +End Z. + +(** Re-export Notations *) + +Infix "+" := Z.add : Z_scope. +Notation "- x" := (Z.opp x) : Z_scope. +Infix "-" := Z.sub : Z_scope. +Infix "*" := Z.mul : Z_scope. +Infix "^" := Z.pow : Z_scope. +Infix "/" := Z.div : Z_scope. +Infix "mod" := Z.modulo (at level 40, no associativity) : Z_scope. +Infix "÷" := Z.quot (at level 40, left associativity) : Z_scope. +Infix "?=" := Z.compare (at level 70, no associativity) : Z_scope. +Infix "=?" := Z.eqb (at level 70, no associativity) : Z_scope. +Infix "<=?" := Z.leb (at level 70, no associativity) : Z_scope. +Infix "<?" := Z.ltb (at level 70, no associativity) : Z_scope. +Infix ">=?" := Z.geb (at level 70, no associativity) : Z_scope. +Infix ">?" := Z.gtb (at level 70, no associativity) : Z_scope. +Notation "( x | y )" := (Z.divide x y) (at level 0) : Z_scope. +Infix "<=" := Z.le : Z_scope. +Infix "<" := Z.lt : Z_scope. +Infix ">=" := Z.ge : Z_scope. +Infix ">" := Z.gt : 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. +(** Conversions from / to positive numbers *) + +Module Pos2Z. + +Lemma id p : Z.to_pos (Z.pos p) = p. +Proof. reflexivity. Qed. + +Lemma inj p q : Z.pos p = Z.pos q -> p = q. +Proof. now injection 1. Qed. + +Lemma inj_iff p q : Z.pos p = Z.pos q <-> p = q. +Proof. split. apply inj. intros; now f_equal. Qed. + +Lemma is_pos p : 0 < Z.pos p. +Proof. reflexivity. Qed. + +Lemma is_nonneg p : 0 <= Z.pos p. +Proof. easy. Qed. + +Lemma inj_1 : Z.pos 1 = 1. +Proof. reflexivity. Qed. + +Lemma inj_xO p : Z.pos p~0 = 2 * Z.pos p. +Proof. reflexivity. Qed. + +Lemma inj_xI p : Z.pos p~1 = 2 * Z.pos p + 1. +Proof. reflexivity. Qed. + +Lemma inj_succ p : Z.pos (Pos.succ p) = Z.succ (Z.pos p). +Proof. simpl. now rewrite Pos.add_1_r. Qed. + +Lemma inj_add p q : Z.pos (p+q) = Z.pos p + Z.pos q. +Proof. reflexivity. Qed. + +Lemma inj_sub p q : (p < q)%positive -> + Z.pos (q-p) = Z.pos q - Z.pos p. +Proof. intros. simpl. now rewrite Z.pos_sub_gt. Qed. + +Lemma inj_sub_max p q : Z.pos (p - q) = Z.max 1 (Z.pos p - Z.pos q). +Proof. + simpl. rewrite Z.pos_sub_spec. case Pos.compare_spec; intros. + - subst; now rewrite Pos.sub_diag. + - now rewrite Pos.sub_lt. + - now destruct (p-q)%positive. +Qed. + +Lemma inj_pred p : p <> 1%positive -> + Z.pos (Pos.pred p) = Z.pred (Z.pos p). +Proof. destruct p; easy || now destruct 1. Qed. + +Lemma inj_mul p q : Z.pos (p*q) = Z.pos p * Z.pos q. +Proof. reflexivity. Qed. + +Lemma inj_pow_pos p q : Z.pos (p^q) = Z.pow_pos (Z.pos p) q. +Proof. now apply Pos.iter_swap_gen. Qed. + +Lemma inj_pow p q : Z.pos (p^q) = (Z.pos p)^(Z.pos q). +Proof. apply inj_pow_pos. Qed. + +Lemma inj_square p : Z.pos (Pos.square p) = Z.square (Z.pos p). +Proof. reflexivity. Qed. + +Lemma inj_compare p q : (p ?= q)%positive = (Z.pos p ?= Z.pos q). +Proof. reflexivity. Qed. + +Lemma inj_leb p q : (p <=? q)%positive = (Z.pos p <=? Z.pos q). +Proof. reflexivity. Qed. + +Lemma inj_ltb p q : (p <? q)%positive = (Z.pos p <? Z.pos q). +Proof. reflexivity. Qed. + +Lemma inj_eqb p q : (p =? q)%positive = (Z.pos p =? Z.pos q). +Proof. reflexivity. Qed. + +Lemma inj_max p q : Z.pos (Pos.max p q) = Z.max (Z.pos p) (Z.pos q). +Proof. + unfold Z.max, Pos.max. rewrite inj_compare. now case Z.compare_spec. +Qed. + +Lemma inj_min p q : Z.pos (Pos.min p q) = Z.min (Z.pos p) (Z.pos q). +Proof. + unfold Z.min, Pos.min. rewrite inj_compare. now case Z.compare_spec. +Qed. + +Lemma inj_sqrt p : Z.pos (Pos.sqrt p) = Z.sqrt (Z.pos p). +Proof. reflexivity. Qed. + +Lemma inj_gcd p q : Z.pos (Pos.gcd p q) = Z.gcd (Z.pos p) (Z.pos q). +Proof. reflexivity. Qed. + +Definition inj_divide p q : (Z.pos p|Z.pos q) <-> (p|q)%positive. +Proof. apply Z.Private_BootStrap.divide_Zpos. Qed. + +Lemma inj_testbit a n : 0<=n -> + Z.testbit (Z.pos a) n = N.testbit (N.pos a) (Z.to_N n). +Proof. apply Z.Private_BootStrap.testbit_Zpos. Qed. + +(** Some results concerning Z.neg *) + +Lemma inj_neg p q : Z.neg p = Z.neg q -> p = q. +Proof. now injection 1. Qed. + +Lemma inj_neg_iff p q : Z.neg p = Z.neg q <-> p = q. +Proof. split. apply inj_neg. intros; now f_equal. Qed. + +Lemma neg_is_neg p : Z.neg p < 0. +Proof. reflexivity. Qed. + +Lemma neg_is_nonpos p : Z.neg p <= 0. +Proof. easy. Qed. + +Lemma neg_xO p : Z.neg p~0 = 2 * Z.neg p. +Proof. reflexivity. Qed. + +Lemma neg_xI p : Z.neg p~1 = 2 * Z.neg p - 1. +Proof. reflexivity. Qed. + +Lemma opp_neg p : - Z.neg p = Z.pos p. +Proof. reflexivity. Qed. + +Lemma opp_pos p : - Z.pos p = Z.neg p. +Proof. reflexivity. Qed. + +Lemma add_neg_neg p q : Z.neg p + Z.neg q = Z.neg (p+q). +Proof. reflexivity. Qed. + +Lemma add_pos_neg p q : Z.pos p + Z.neg q = Z.pos_sub p q. +Proof. reflexivity. Qed. + +Lemma add_neg_pos p q : Z.neg p + Z.pos q = Z.pos_sub q p. +Proof. reflexivity. Qed. + +Lemma divide_pos_neg_r n p : (n|Z.pos p) <-> (n|Z.neg p). +Proof. apply Z.Private_BootStrap.divide_Zpos_Zneg_r. Qed. + +Lemma divide_pos_neg_l n p : (Z.pos p|n) <-> (Z.neg p|n). +Proof. apply Z.Private_BootStrap.divide_Zpos_Zneg_l. Qed. + +Lemma testbit_neg a n : 0<=n -> + Z.testbit (Z.neg a) n = negb (N.testbit (Pos.pred_N a) (Z.to_N n)). +Proof. apply Z.Private_BootStrap.testbit_Zneg. Qed. + +End Pos2Z. + +Module Z2Pos. + +Lemma id x : 0 < x -> Z.pos (Z.to_pos x) = x. +Proof. now destruct x. Qed. + +Lemma inj x y : 0 < x -> 0 < y -> Z.to_pos x = Z.to_pos y -> x = y. +Proof. + destruct x; simpl; try easy. intros _ H ->. now apply id. +Qed. + +Lemma inj_iff x y : 0 < x -> 0 < y -> (Z.to_pos x = Z.to_pos y <-> x = y). +Proof. split. now apply inj. intros; now f_equal. Qed. + +Lemma to_pos_nonpos x : x <= 0 -> Z.to_pos x = 1%positive. +Proof. destruct x; trivial. now destruct 1. Qed. + +Lemma inj_1 : Z.to_pos 1 = 1%positive. +Proof. reflexivity. Qed. + +Lemma inj_double x : 0 < x -> + Z.to_pos (Z.double x) = (Z.to_pos x)~0%positive. +Proof. now destruct x. Qed. + +Lemma inj_succ_double x : 0 < x -> + Z.to_pos (Z.succ_double x) = (Z.to_pos x)~1%positive. +Proof. now destruct x. Qed. + +Lemma inj_succ x : 0 < x -> Z.to_pos (Z.succ x) = Pos.succ (Z.to_pos x). +Proof. + destruct x; try easy. simpl. now rewrite Pos.add_1_r. +Qed. + +Lemma inj_add x y : 0 < x -> 0 < y -> + Z.to_pos (x+y) = (Z.to_pos x + Z.to_pos y)%positive. +Proof. destruct x; easy || now destruct y. Qed. + +Lemma inj_sub x y : 0 < x < y -> + Z.to_pos (y-x) = (Z.to_pos y - Z.to_pos x)%positive. +Proof. + destruct x; try easy. destruct y; try easy. simpl. + intros. now rewrite Z.pos_sub_gt. +Qed. + +Lemma inj_pred x : 1 < x -> Z.to_pos (Z.pred x) = Pos.pred (Z.to_pos x). +Proof. now destruct x as [|[x|x|]|]. Qed. + +Lemma inj_mul x y : 0 < x -> 0 < y -> + Z.to_pos (x*y) = (Z.to_pos x * Z.to_pos y)%positive. +Proof. destruct x; easy || now destruct y. Qed. + +Lemma inj_pow x y : 0 < x -> 0 < y -> + Z.to_pos (x^y) = (Z.to_pos x ^ Z.to_pos y)%positive. +Proof. + intros. apply Pos2Z.inj. rewrite Pos2Z.inj_pow, !id; trivial. + apply Z.pow_pos_nonneg. trivial. now apply Z.lt_le_incl. +Qed. + +Lemma inj_pow_pos x p : 0 < x -> + Z.to_pos (Z.pow_pos x p) = ((Z.to_pos x)^p)%positive. +Proof. intros. now apply (inj_pow x (Z.pos p)). Qed. + +Lemma inj_compare x y : 0 < x -> 0 < y -> + (x ?= y) = (Z.to_pos x ?= Z.to_pos y)%positive. +Proof. destruct x; easy || now destruct y. Qed. + +Lemma inj_leb x y : 0 < x -> 0 < y -> + (x <=? y) = (Z.to_pos x <=? Z.to_pos y)%positive. +Proof. destruct x; easy || now destruct y. Qed. + +Lemma inj_ltb x y : 0 < x -> 0 < y -> + (x <? y) = (Z.to_pos x <? Z.to_pos y)%positive. +Proof. destruct x; easy || now destruct y. Qed. + +Lemma inj_eqb x y : 0 < x -> 0 < y -> + (x =? y) = (Z.to_pos x =? Z.to_pos y)%positive. +Proof. destruct x; easy || now destruct y. Qed. + +Lemma inj_max x y : + Z.to_pos (Z.max x y) = Pos.max (Z.to_pos x) (Z.to_pos y). +Proof. + destruct x; simpl; try rewrite Pos.max_1_l. + - now destruct y. + - destruct y; simpl; now rewrite ?Pos.max_1_r, <- ?Pos2Z.inj_max. + - destruct y; simpl; rewrite ?Pos.max_1_r; trivial. + apply to_pos_nonpos. now apply Z.max_lub. +Qed. + +Lemma inj_min x y : + Z.to_pos (Z.min x y) = Pos.min (Z.to_pos x) (Z.to_pos y). +Proof. + destruct x; simpl; try rewrite Pos.min_1_l. + - now destruct y. + - destruct y; simpl; now rewrite ?Pos.min_1_r, <- ?Pos2Z.inj_min. + - destruct y; simpl; rewrite ?Pos.min_1_r; trivial. + apply to_pos_nonpos. apply Z.min_le_iff. now left. +Qed. + +Lemma inj_sqrt x : Z.to_pos (Z.sqrt x) = Pos.sqrt (Z.to_pos x). +Proof. now destruct x. Qed. + +Lemma inj_gcd x y : 0 < x -> 0 < y -> + Z.to_pos (Z.gcd x y) = Pos.gcd (Z.to_pos x) (Z.to_pos y). +Proof. destruct x; easy || now destruct y. Qed. + +End Z2Pos. + +(** Compatibility Notations *) + +Notation Zdouble_plus_one := Z.succ_double (compat "8.3"). +Notation Zdouble_minus_one := Z.pred_double (compat "8.3"). +Notation Zdouble := Z.double (compat "8.3"). +Notation ZPminus := Z.pos_sub (compat "8.3"). +Notation Zsucc' := Z.succ (compat "8.3"). +Notation Zpred' := Z.pred (compat "8.3"). +Notation Zplus' := Z.add (compat "8.3"). +Notation Zplus := Z.add (compat "8.3"). (* Slightly incompatible *) +Notation Zopp := Z.opp (compat "8.3"). +Notation Zsucc := Z.succ (compat "8.3"). +Notation Zpred := Z.pred (compat "8.3"). +Notation Zminus := Z.sub (compat "8.3"). +Notation Zmult := Z.mul (compat "8.3"). +Notation Zcompare := Z.compare (compat "8.3"). +Notation Zsgn := Z.sgn (compat "8.3"). +Notation Zle := Z.le (compat "8.3"). +Notation Zge := Z.ge (compat "8.3"). +Notation Zlt := Z.lt (compat "8.3"). +Notation Zgt := Z.gt (compat "8.3"). +Notation Zmax := Z.max (compat "8.3"). +Notation Zmin := Z.min (compat "8.3"). +Notation Zabs := Z.abs (compat "8.3"). +Notation Zabs_nat := Z.abs_nat (compat "8.3"). +Notation Zabs_N := Z.abs_N (compat "8.3"). +Notation Z_of_nat := Z.of_nat (compat "8.3"). +Notation Z_of_N := Z.of_N (compat "8.3"). + +Notation Zind := Z.peano_ind (compat "8.3"). +Notation Zopp_0 := Z.opp_0 (compat "8.3"). +Notation Zopp_involutive := Z.opp_involutive (compat "8.3"). +Notation Zopp_inj := Z.opp_inj (compat "8.3"). +Notation Zplus_0_l := Z.add_0_l (compat "8.3"). +Notation Zplus_0_r := Z.add_0_r (compat "8.3"). +Notation Zplus_comm := Z.add_comm (compat "8.3"). +Notation Zopp_plus_distr := Z.opp_add_distr (compat "8.3"). +Notation Zopp_succ := Z.opp_succ (compat "8.3"). +Notation Zplus_opp_r := Z.add_opp_diag_r (compat "8.3"). +Notation Zplus_opp_l := Z.add_opp_diag_l (compat "8.3"). +Notation Zplus_assoc := Z.add_assoc (compat "8.3"). +Notation Zplus_permute := Z.add_shuffle3 (compat "8.3"). +Notation Zplus_reg_l := Z.add_reg_l (compat "8.3"). +Notation Zplus_succ_l := Z.add_succ_l (compat "8.3"). +Notation Zplus_succ_comm := Z.add_succ_comm (compat "8.3"). +Notation Zsucc_discr := Z.neq_succ_diag_r (compat "8.3"). +Notation Zsucc_inj := Z.succ_inj (compat "8.3"). +Notation Zsucc'_inj := Z.succ_inj (compat "8.3"). +Notation Zsucc'_pred' := Z.succ_pred (compat "8.3"). +Notation Zpred'_succ' := Z.pred_succ (compat "8.3"). +Notation Zpred'_inj := Z.pred_inj (compat "8.3"). +Notation Zsucc'_discr := Z.neq_succ_diag_r (compat "8.3"). +Notation Zminus_0_r := Z.sub_0_r (compat "8.3"). +Notation Zminus_diag := Z.sub_diag (compat "8.3"). +Notation Zminus_plus_distr := Z.sub_add_distr (compat "8.3"). +Notation Zminus_succ_r := Z.sub_succ_r (compat "8.3"). +Notation Zminus_plus := Z.add_simpl_l (compat "8.3"). +Notation Zmult_0_l := Z.mul_0_l (compat "8.3"). +Notation Zmult_0_r := Z.mul_0_r (compat "8.3"). +Notation Zmult_1_l := Z.mul_1_l (compat "8.3"). +Notation Zmult_1_r := Z.mul_1_r (compat "8.3"). +Notation Zmult_comm := Z.mul_comm (compat "8.3"). +Notation Zmult_assoc := Z.mul_assoc (compat "8.3"). +Notation Zmult_permute := Z.mul_shuffle3 (compat "8.3"). +Notation Zmult_1_inversion_l := Z.mul_eq_1 (compat "8.3"). +Notation Zdouble_mult := Z.double_spec (compat "8.3"). +Notation Zdouble_plus_one_mult := Z.succ_double_spec (compat "8.3"). +Notation Zopp_mult_distr_l_reverse := Z.mul_opp_l (compat "8.3"). +Notation Zmult_opp_opp := Z.mul_opp_opp (compat "8.3"). +Notation Zmult_opp_comm := Z.mul_opp_comm (compat "8.3"). +Notation Zopp_eq_mult_neg_1 := Z.opp_eq_mul_m1 (compat "8.3"). +Notation Zmult_plus_distr_r := Z.mul_add_distr_l (compat "8.3"). +Notation Zmult_plus_distr_l := Z.mul_add_distr_r (compat "8.3"). +Notation Zmult_minus_distr_r := Z.mul_sub_distr_r (compat "8.3"). +Notation Zmult_reg_l := Z.mul_reg_l (compat "8.3"). +Notation Zmult_reg_r := Z.mul_reg_r (compat "8.3"). +Notation Zmult_succ_l := Z.mul_succ_l (compat "8.3"). +Notation Zmult_succ_r := Z.mul_succ_r (compat "8.3"). + +Notation Zpos_xI := Pos2Z.inj_xI (compat "8.3"). +Notation Zpos_xO := Pos2Z.inj_xO (compat "8.3"). +Notation Zneg_xI := Pos2Z.neg_xI (compat "8.3"). +Notation Zneg_xO := Pos2Z.neg_xO (compat "8.3"). +Notation Zopp_neg := Pos2Z.opp_neg (compat "8.3"). +Notation Zpos_succ_morphism := Pos2Z.inj_succ (compat "8.3"). +Notation Zpos_mult_morphism := Pos2Z.inj_mul (compat "8.3"). +Notation Zpos_minus_morphism := Pos2Z.inj_sub (compat "8.3"). +Notation Zpos_eq_rev := Pos2Z.inj (compat "8.3"). +Notation Zpos_plus_distr := Pos2Z.inj_add (compat "8.3"). +Notation Zneg_plus_distr := Pos2Z.add_neg_neg (compat "8.3"). + +Notation Z := Z (only parsing). +Notation Z_rect := Z_rect (only parsing). +Notation Z_rec := Z_rec (only parsing). +Notation Z_ind := Z_ind (only parsing). +Notation Z0 := Z0 (only parsing). +Notation Zpos := Zpos (only parsing). +Notation Zneg := Zneg (only parsing). + +(** Compatibility lemmas. These could be notations, + but scope information would be lost. +*) + +Notation SYM1 lem := (fun n => eq_sym (lem n)). +Notation SYM2 lem := (fun n m => eq_sym (lem n m)). +Notation SYM3 lem := (fun n m p => eq_sym (lem n m p)). + +Lemma Zplus_assoc_reverse : forall n m p, n+m+p = n+(m+p). +Proof (SYM3 Z.add_assoc). +Lemma Zplus_succ_r_reverse : forall n m, Z.succ (n+m) = n+Z.succ m. +Proof (SYM2 Z.add_succ_r). +Notation Zplus_succ_r := Zplus_succ_r_reverse (only parsing). +Lemma Zplus_0_r_reverse : forall n, n = n + 0. +Proof (SYM1 Z.add_0_r). +Lemma Zplus_eq_compat : forall n m p q, n=m -> p=q -> n+p=m+q. +Proof (f_equal2 Z.add). +Lemma Zsucc_pred : forall n, n = Z.succ (Z.pred n). +Proof (SYM1 Z.succ_pred). +Lemma Zpred_succ : forall n, n = Z.pred (Z.succ n). +Proof (SYM1 Z.pred_succ). +Lemma Zsucc_eq_compat : forall n m, n = m -> Z.succ n = Z.succ m. +Proof (f_equal Z.succ). +Lemma Zminus_0_l_reverse : forall n, n = n - 0. +Proof (SYM1 Z.sub_0_r). +Lemma Zminus_diag_reverse : forall n, 0 = n-n. +Proof (SYM1 Z.sub_diag). +Lemma Zminus_succ_l : forall n m, Z.succ (n - m) = Z.succ n - m. +Proof (SYM2 Z.sub_succ_l). +Lemma Zplus_minus_eq : forall n m p, n = m + p -> p = n - m. +Proof. intros. now apply Z.add_move_l. Qed. +Lemma Zplus_minus : forall n m, n + (m - n) = m. +Proof (fun n m => eq_trans (Z.add_comm n (m-n)) (Z.sub_add n m)). +Lemma Zminus_plus_simpl_l : forall n m p, p + n - (p + m) = n - m. +Proof (fun n m p => Z.add_add_simpl_l_l p n m). +Lemma Zminus_plus_simpl_l_reverse : forall n m p, n - m = p + n - (p + m). +Proof (SYM3 Zminus_plus_simpl_l). +Lemma Zminus_plus_simpl_r : forall n m p, n + p - (m + p) = n - m. +Proof (fun n m p => Z.add_add_simpl_r_r n p m). +Lemma Zeq_minus : forall n m, n = m -> n - m = 0. +Proof (fun n m => proj2 (Z.sub_move_0_r n m)). +Lemma Zminus_eq : forall n m, n - m = 0 -> n = m. +Proof (fun n m => proj1 (Z.sub_move_0_r n m)). +Lemma Zmult_0_r_reverse : forall n, 0 = n * 0. +Proof (SYM1 Z.mul_0_r). +Lemma Zmult_assoc_reverse : forall n m p, n * m * p = n * (m * p). +Proof (SYM3 Z.mul_assoc). +Lemma Zmult_integral : forall n m, n * m = 0 -> n = 0 \/ m = 0. +Proof (fun n m => proj1 (Z.mul_eq_0 n m)). +Lemma Zmult_integral_l : forall n m, n <> 0 -> m * n = 0 -> m = 0. +Proof (fun n m H H' => Z.mul_eq_0_l m n H' H). +Lemma Zopp_mult_distr_l : forall n m, - (n * m) = - n * m. +Proof (SYM2 Z.mul_opp_l). +Lemma Zopp_mult_distr_r : forall n m, - (n * m) = n * - m. +Proof (SYM2 Z.mul_opp_r). +Lemma Zmult_minus_distr_l : forall n m p, p * (n - m) = p * n - p * m. +Proof (fun n m p => Z.mul_sub_distr_l p n m). +Lemma Zmult_succ_r_reverse : forall n m, n * m + n = n * Z.succ m. +Proof (SYM2 Z.mul_succ_r). +Lemma Zmult_succ_l_reverse : forall n m, n * m + m = Z.succ n * m. +Proof (SYM2 Z.mul_succ_l). +Lemma Zpos_eq : forall p q, p = q -> Z.pos p = Z.pos q. +Proof. congruence. Qed. +Lemma Zpos_eq_iff : forall p q, p = q <-> Z.pos p = Z.pos q. +Proof (fun p q => iff_sym (Pos2Z.inj_iff p q)). + +Hint Immediate Zsucc_pred: zarith. + +(* Not kept : +Zplus_0_simpl_l +Zplus_0_simpl_l_reverse +Zplus_opp_expand +Zsucc_inj_contrapositive +Zsucc_succ' +Zpred_pred' +*) + +(* No compat notation for : +weak_assoc (now Z.add_assoc_pos) +weak_Zmult_plus_distr_r (now Z.mul_add_distr_pos) +*) + +(** Obsolete stuff *) + +Definition Zne (x y:Z) := x <> y. (* TODO : to remove someday ? *) + +Ltac elim_compare com1 com2 := + case (Dcompare (com1 ?= com2)%Z); + [ idtac | let x := fresh "H" in + (intro x; case x; clear x) ]. + +Lemma ZL0 : 2%nat = (1 + 1)%nat. +Proof. + reflexivity. +Qed. + +Lemma Zplus_diag_eq_mult_2 n : n + n = n * 2. +Proof. + rewrite Z.mul_comm. apply Z.add_diag. +Qed. + +Lemma Z_eq_mult n m : m = 0 -> m * n = 0. +Proof. + intros; now subst. +Qed. |