diff options
Diffstat (limited to 'theories/ZArith/BinInt.v')
| -rw-r--r-- | theories/ZArith/BinInt.v | 2011 |
1 files changed, 1219 insertions, 792 deletions
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index e2b89d84..3a5eb885 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -1,1158 +1,1585 @@ (* -*- 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-2010 *) (* \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. +(** Initial author: Pierre Crégut, CNET, Lannion, France *) -Unset Boxed Definitions. +(** The type [Z] and its constructors [Z0] and [Zpos] and [Zneg] + are now defined in [BinNums.v] *) -(*****************************) -(** * Binary integer numbers *) +Local Open Scope Z_scope. -Inductive Z : Set := - | Z0 : Z - | Zpos : positive -> Z - | Zneg : positive -> Z. +(** Every definitions and early properties about binary integers + are placed in a module [Z] for qualification purpose. *) +Module Z + <: ZAxiomsSig + <: UsualOrderedTypeFull + <: UsualDecidableTypeFull + <: TotalOrder. -(** 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. +(** * Definitions of operations, now in a separate file *) -Ltac elim_compare com1 com2 := - case (Dcompare (com1 ?= com2)%Z); - [ idtac | let x := fresh "H" in - (intro x; case x; clear x) ]. +Include BinIntDef.Z. + +(** When including property functors, only inline t eq zero one two *) -(** ** Sign function *) +Set Inline Level 30. -Definition Zsgn (z:Z) : Z := - match z with - | Z0 => Z0 - | Zpos p => Zpos 1 - | Zneg p => Zneg 1 - end. +(** * Logic Predicates *) + +Definition eq := @Logic.eq Z. +Definition eq_equiv := @eq_equivalence Z. + +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. + +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. -(** ** Direct, easier to handle variants of successor and addition *) +Definition divide x y := exists z, y = z*x. +Notation "( x | y )" := (divide x y) (at level 0). -Definition Zsucc' (x:Z) := - match x with - | Z0 => Zpos 1 - | Zpos x' => Zpos (Psucc x') - | Zneg x' => ZPminus 1 x' - end. +Definition Even a := exists b, a = 2*b. +Definition Odd a := exists b, a = 2*b+1. -Definition Zpred' (x:Z) := - match x with - | Z0 => Zneg 1 - | Zpos x' => ZPminus x' 1 - | Zneg x' => Zneg (Psucc x') - end. +(** * Decidability of equality. *) -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. +Definition eq_dec (x y : Z) : {x = y} + {x <> y}. +Proof. + decide equality; apply Pos.eq_dec. +Defined. -Open Local Scope Z_scope. +(** * Properties of [pos_sub] *) -(**********************************************************************) -(** ** Inductive specification of Z *) +(** [pos_sub] can be written in term of positive comparison + and subtraction (cf. earlier definition of addition 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. +Lemma pos_sub_spec p q : + pos_sub p q = + match (p ?= q)%positive with + | Eq => 0 + | Lt => Zneg (q - p) + | Gt => Zpos (p - q) + end. 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)). + 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. -(**********************************************************************) -(** * Misc properties about binary integer operations *) +(** Particular cases of the previous result *) +Lemma pos_sub_diag p : pos_sub p p = 0. +Proof. + now rewrite pos_sub_spec, Pos.compare_refl. +Qed. -(**********************************************************************) -(** ** Properties of opposite on binary integer numbers *) +Lemma pos_sub_lt p q : (p < q)%positive -> pos_sub p q = Zneg (q - p). +Proof. + intros H. now rewrite pos_sub_spec, H. +Qed. -Theorem Zopp_0 : Zopp Z0 = Z0. +Lemma pos_sub_gt p q : (q < p)%positive -> pos_sub p q = Zpos (p - q). Proof. - reflexivity. + intros H. now rewrite pos_sub_spec, Pos.compare_antisym, H. Qed. -Theorem Zopp_neg : forall p:positive, - Zneg p = Zpos p. +(** The opposite of [pos_sub] is [pos_sub] with reversed arguments *) + +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. -(** [opp] is involutive *) +(** * Results concerning [Zpos] and [Zneg] and the operators *) -Theorem Zopp_involutive : forall n:Z, - - n = n. +Lemma opp_Zneg p : - Zneg p = Zpos p. Proof. - intro x; destruct x; reflexivity. + reflexivity. Qed. -(** Injectivity of the opposite *) +Lemma opp_Zpos p : - Zpos p = Zneg p. +Proof. + reflexivity. +Qed. -Theorem Zopp_inj : forall n m:Z, - n = - m -> n = m. +Lemma succ_Zpos p : succ (Zpos p) = Zpos (Pos.succ p). 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 ]. + simpl. f_equal. apply Pos.add_1_r. Qed. -(**********************************************************************) -(** ** Other properties of binary integer numbers *) +Lemma add_Zpos p q : Zpos p + Zpos q = Zpos (p+q). +Proof. + reflexivity. +Qed. -Lemma ZL0 : 2%nat = (1 + 1)%nat. +Lemma add_Zneg p q : Zneg p + Zneg q = Zneg (p+q). Proof. - reflexivity. + reflexivity. Qed. -(**********************************************************************) -(** * Properties of the addition on integers *) +Lemma add_Zpos_Zneg p q : Zpos p + Zneg q = pos_sub p q. +Proof. + reflexivity. +Qed. -(** ** Zero is left neutral for addition *) +Lemma add_Zneg_Zpos p q : Zneg p + Zpos q = pos_sub q p. +Proof. + reflexivity. +Qed. -Theorem Zplus_0_l : forall n:Z, Z0 + n = n. +Lemma sub_Zpos n m : (n < m)%positive -> Zpos m - Zpos n = Zpos (m-n). Proof. - intro x; destruct x; reflexivity. + intros H. simpl. now apply pos_sub_gt. Qed. -(** ** Zero is right neutral for addition *) +Lemma mul_Zpos (p q : positive) : Zpos p * Zpos q = Zpos (p*q). +Proof. + reflexivity. +Qed. -Theorem Zplus_0_r : forall n:Z, n + Z0 = n. +Lemma pow_Zpos p q : (Zpos p)^(Zpos q) = Zpos (p^q). Proof. - intro x; destruct x; reflexivity. + unfold Pos.pow, pow, pow_pos. + symmetry. now apply Pos.iter_swap_gen. Qed. -(** ** Addition is commutative *) +Lemma inj_Zpos p q : Zpos p = Zpos q <-> p = q. +Proof. + split; intros H. now injection H. now f_equal. +Qed. -Theorem Zplus_comm : forall n m:Z, n + m = m + n. +Lemma inj_Zneg p q : Zneg p = Zneg q <-> p = q. 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. + split; intros H. now injection H. now f_equal. Qed. -(** ** Opposite distributes over addition *) +Lemma pos_xI p : Zpos p~1 = 2 * Zpos p + 1. +Proof. + reflexivity. +Qed. -Theorem Zopp_plus_distr : forall n m:Z, - (n + m) = - n + - m. +Lemma pos_xO p : Zpos p~0 = 2 * Zpos p. Proof. - intro x; destruct x as [| p| p]; intro y; destruct y as [| q| q]; - simpl in |- *; reflexivity || destruct ((p ?= q)%positive Eq); - reflexivity. + reflexivity. Qed. -Theorem Zopp_succ : forall n:Z, Zopp (Zsucc n) = Zpred (Zopp n). +Lemma neg_xI p : Zneg p~1 = 2 * Zneg p - 1. Proof. -intro; unfold Zsucc; now rewrite Zopp_plus_distr. + reflexivity. Qed. -(** ** Opposite is inverse for addition *) +Lemma neg_xO p : Zneg p~0 = 2 * Zneg p. +Proof. + reflexivity. +Qed. + +(** 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. *) + +Module Import Private_BootStrap. + +(** * Properties of addition *) + +(** ** Zero is neutral for addition *) -Theorem Zplus_opp_r : forall n:Z, n + - n = Z0. +Lemma add_0_r n : n + 0 = n. Proof. - intro x; destruct x as [| p| p]; simpl in |- *; - [ reflexivity - | rewrite (Pcompare_refl p); reflexivity - | rewrite (Pcompare_refl p); reflexivity ]. + now destruct n. Qed. -Theorem Zplus_opp_l : forall n:Z, - n + n = Z0. +(** ** Addition is commutative *) + +Lemma add_comm n m : n + m = m + n. +Proof. + destruct n, m; simpl; trivial; now rewrite Pos.add_comm. +Qed. + +(** ** Opposite distributes over addition *) + +Lemma opp_add_distr n m : - (n + m) = - n + - m. Proof. - intro; rewrite Zplus_comm; apply Zplus_opp_r. + destruct n, m; simpl; trivial using pos_sub_opp. Qed. -Hint Local Resolve Zplus_0_l Zplus_0_r. +(** ** Opposite is injective *) + +Lemma opp_inj n m : -n = -m -> n = m. +Proof. + destruct n, m; simpl; intros H; destr_eq H; now f_equal. +Qed. (** ** 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_reverse : forall n m:Z, Zsucc (n + m) = n + Zsucc m. -Proof. - intros n m; unfold Zsucc in |- *; rewrite Zplus_assoc; trivial with arith. +Lemma pos_sub_add p q r : + pos_sub (p + q) r = Zpos 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, Zpos x + (y + z) = Zpos x + y + z). + { intros x [|y|y] [|z|z]; rewrite ?add_0_r; trivial. + - simpl. now rewrite Pos.add_assoc. + - simpl (_ + Zneg _). symmetry. apply pos_sub_add. + - simpl (Zneg _ + _); simpl (_ + Zneg _). + now rewrite (add_comm _ (Zpos _)), <- 2 pos_sub_add, Pos.add_comm. + - apply opp_inj. rewrite !opp_add_distr, opp_Zpos, !opp_Zneg. + simpl (Zneg _ + _); simpl (_ + Zneg _). + rewrite add_comm, Pos.add_comm. apply pos_sub_add. } + destruct n. + - trivial. + - apply AUX. + - apply opp_inj. rewrite !opp_add_distr, opp_Zneg. 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. -Notation Zplus_succ_r := Zplus_succ_r_reverse (only parsing). +(** ** Opposite is inverse for addition *) -Lemma Zplus_succ_comm : forall n m:Z, Zsucc n + m = n + Zsucc m. +Lemma add_opp_diag_r n : n + - n = 0. Proof. - unfold Zsucc in |- *; intros n m; rewrite <- Zplus_assoc; - rewrite (Zplus_comm (Zpos 1)); trivial with arith. + destruct n; simpl; trivial; now rewrite pos_sub_diag. Qed. -(** ** Misc properties, usually redundant or non natural *) - -Lemma Zplus_0_r_reverse : forall n:Z, n = n + Z0. +Lemma add_opp_diag_l n : - n + n = 0. Proof. - symmetry in |- *; apply Zplus_0_r. + rewrite add_comm. apply add_opp_diag_r. Qed. -Lemma Zplus_0_simpl_l : forall n m:Z, n + Z0 = m -> n = m. +(** ** Commutativity of multiplication *) + +Lemma mul_comm n m : n * m = m * n. Proof. - intros n m; rewrite Zplus_0_r; intro; assumption. + destruct n, m; simpl; trivial; f_equal; apply Pos.mul_comm. Qed. -Lemma Zplus_0_simpl_l_reverse : forall n m:Z, n = m + Z0 -> n = m. +(** ** Associativity of multiplication *) + +Lemma mul_assoc n m p : n * (m * p) = n * m * p. Proof. - intros n m; rewrite Zplus_0_r; intro; assumption. + destruct n, m, p; simpl; trivial; f_equal; apply Pos.mul_assoc. Qed. -Lemma Zplus_eq_compat : forall n m p q:Z, n = m -> p = q -> n + p = m + q. +(** Multiplication and constants *) + +Lemma mul_1_l n : 1 * n = n. Proof. - intros; rewrite H; rewrite H0; reflexivity. + now destruct n. Qed. -Lemma Zplus_opp_expand : forall n m p:Z, n + - m = n + - p + (p + - m). +Lemma mul_1_r n : n * 1 = n. Proof. - intros x y z. - rewrite <- (Zplus_assoc x). - rewrite (Zplus_assoc (- z)). - rewrite Zplus_opp_l. - reflexivity. + destruct n; simpl; now rewrite ?Pos.mul_1_r. Qed. -(************************************************************************) -(** * Properties of successor and predecessor on binary integer numbers *) +(** ** Multiplication and Opposite *) -Theorem Zsucc_discr : forall n:Z, n <> Zsucc n. +Lemma mul_opp_l n m : - n * m = - (n * m). 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 ]. + now destruct n, m. Qed. -Theorem Zpos_succ_morphism : - forall p:positive, Zpos (Psucc p) = Zsucc (Zpos p). +Lemma mul_opp_r n m : n * - m = - (n * m). Proof. - intro; rewrite Pplus_one_succ_r; unfold Zsucc in |- *; simpl in |- *; - trivial with arith. + now destruct n, m. Qed. -(** ** Successor and predecessor are inverse functions *) +Lemma mul_opp_opp n m : - n * - m = n * m. +Proof. + now destruct n, m. +Qed. -Theorem Zsucc_pred : forall n:Z, n = Zsucc (Zpred n). +Lemma mul_opp_comm n m : - n * m = n * - m. Proof. - intros n; unfold Zsucc, Zpred in |- *; rewrite <- Zplus_assoc; simpl in |- *; - rewrite Zplus_0_r; trivial with arith. + now destruct n, m. Qed. -Hint Immediate Zsucc_pred: zarith. +(** ** Distributivity of multiplication over addition *) + +Lemma mul_add_distr_pos (p:positive) n m : + Zpos p * (n + m) = Zpos p * n + Zpos p * m. +Proof. + 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. -Theorem Zpred_succ : forall n:Z, n = Zpred (Zsucc n). +Lemma mul_add_distr_l n m p : n * (m + p) = n * m + n * p. Proof. - intros m; unfold Zpred, Zsucc in |- *; rewrite <- Zplus_assoc; simpl in |- *; - rewrite Zplus_comm; auto with arith. + destruct n as [|n|n]. trivial. + apply mul_add_distr_pos. + rewrite <- opp_Zpos, !mul_opp_l, <- opp_add_distr. f_equal. + apply mul_add_distr_pos. Qed. -Theorem Zsucc_inj : forall n m:Z, Zsucc n = Zsucc m -> n = m. +Lemma mul_add_distr_r n m p : (n + m) * p = n * p + m * p. 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. + rewrite !(mul_comm _ p). apply mul_add_distr_l. Qed. -(*************************************************************************) -(** ** Properties of the direct definition of successor and predecessor *) +End Private_BootStrap. + +(** * Proofs of specifications *) + +(** ** Specification of constants *) -Theorem Zsucc_succ' : forall n:Z, Zsucc n = Zsucc' n. +Lemma one_succ : 1 = succ 0. Proof. -destruct n as [| p | p]; simpl. reflexivity. -now rewrite Pplus_one_succ_r. -now destruct p as [q | q |]. Qed. -Theorem Zpred_pred' : forall n:Z, Zpred n = Zpred' n. +Lemma two_succ : 2 = succ 1. 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. +(** ** Specification of addition *) + +Lemma add_0_l n : 0 + n = n. +Proof. + now destruct n. +Qed. + +Lemma add_succ_l n m : succ n + m = succ (n + m). Proof. -intros n m; do 2 rewrite <- Zsucc_succ'; now apply Zsucc_inj. + unfold succ. now rewrite 2 (add_comm _ 1), add_assoc. Qed. -Theorem Zsucc'_pred' : forall n:Z, Zsucc' (Zpred' n) = n. +(** ** Specification of opposite *) + +Lemma opp_0 : -0 = 0. Proof. -intro; rewrite <- Zsucc_succ'; rewrite <- Zpred_pred'; -symmetry; apply Zsucc_pred. + reflexivity. Qed. -Theorem Zpred'_succ' : forall n:Z, Zpred' (Zsucc' n) = n. +Lemma opp_succ n : -(succ n) = pred (-n). Proof. -intro; apply Zsucc'_inj; now rewrite Zsucc'_pred'. + unfold succ, pred. apply opp_add_distr. Qed. -Theorem Zpred'_inj : forall n m:Z, Zpred' n = Zpred' m -> n = m. +(** ** Specification of successor and predecessor *) + +Lemma succ_pred n : succ (pred n) = n. Proof. -intros n m H. -rewrite <- (Zsucc'_pred' n); rewrite <- (Zsucc'_pred' m); now rewrite H. + unfold succ, pred. now rewrite <- add_assoc, add_opp_diag_r, add_0_r. Qed. -Theorem Zsucc'_discr : forall n:Z, n <> Zsucc' n. +Lemma pred_succ n : pred (succ n) = 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. now rewrite <- add_assoc, add_opp_diag_r, add_0_r. Qed. -(** Misc properties, usually redundant or non natural *) +(** ** Specification of subtraction *) -Lemma Zsucc_eq_compat : forall n m:Z, n = m -> Zsucc n = Zsucc m. +Lemma sub_0_r n : n - 0 = n. Proof. - intros n m H; rewrite H; reflexivity. + apply add_0_r. Qed. -Lemma Zsucc_inj_contrapositive : forall n m:Z, n <> m -> Zsucc n <> Zsucc m. +Lemma sub_succ_r n m : n - succ m = pred (n - m). Proof. - unfold not in |- *; intros n m H1 H2; apply H1; apply Zsucc_inj; assumption. + unfold sub, succ, pred. now rewrite opp_add_distr, add_assoc. Qed. -(**********************************************************************) -(** * Properties of subtraction on binary integer numbers *) +(** ** Specification of multiplication *) -(** ** [minus] and [Z0] *) +Lemma mul_0_l n : 0 * n = 0. +Proof. + reflexivity. +Qed. + +Lemma mul_succ_l n m : succ n * m = n * m + m. +Proof. + unfold succ. now rewrite mul_add_distr_r, mul_1_l. +Qed. + +(** ** Specification of comparisons and order *) + +Lemma eqb_eq n m : (n =? m) = true <-> n = m. +Proof. + destruct n, m; simpl; try (now split). + rewrite inj_Zpos. apply Pos.eqb_eq. + rewrite inj_Zneg. apply Pos.eqb_eq. +Qed. + +Lemma ltb_lt n m : (n <? m) = true <-> n < m. +Proof. + unfold ltb, lt. destruct compare; easy'. +Qed. -Lemma Zminus_0_r : forall n:Z, n - Z0 = n. +Lemma leb_le n m : (n <=? m) = true <-> n <= m. Proof. - intro; unfold Zminus in |- *; simpl in |- *; rewrite Zplus_0_r; - trivial with arith. + unfold leb, le. destruct compare; easy'. Qed. -Lemma Zminus_0_l_reverse : forall n:Z, n = n - Z0. +Lemma compare_eq_iff n m : (n ?= m) = Eq <-> n = m. Proof. - intro; symmetry in |- *; apply Zminus_0_r. +destruct n, m; simpl; rewrite ?CompOpp_iff, ?Pos.compare_eq_iff; + split; congruence. Qed. -Lemma Zminus_diag : forall n:Z, n - n = Z0. +Lemma compare_sub n m : (n ?= m) = (n - m ?= 0). Proof. - intro; unfold Zminus in |- *; rewrite Zplus_opp_r; 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_diag_reverse : forall n:Z, Z0 = n - n. +Lemma compare_antisym n m : (m ?= n) = CompOpp (n ?= m). Proof. - intro; symmetry in |- *; apply Zminus_diag. +destruct n, m; simpl; trivial; now rewrite <- ?Pos.compare_antisym. Qed. +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]. *) -(** ** Relating [minus] with [plus] and [Zsucc] *) +Include BoolOrderFacts. -Lemma Zminus_plus_distr : forall n m p:Z, n - (m + p) = n - m - p. +(** Remaining specification of [lt] and [le] *) + +Lemma lt_succ_r n m : n < succ m <-> n<=m. Proof. -intros; unfold Zminus; rewrite Zopp_plus_distr; apply Zplus_assoc. + unfold lt, le. rewrite compare_sub, sub_succ_r. + rewrite (compare_sub n m). + destruct (n-m) as [|[ | | ]|]; easy'. Qed. -Lemma Zminus_succ_l : forall n m:Z, Zsucc (n - m) = Zsucc n - m. +(** ** Specification of minimum and maximum *) + +Lemma max_l n m : m<=n -> max n m = n. Proof. - intros n m; unfold Zminus, Zsucc in |- *; rewrite (Zplus_comm n (- m)); - rewrite <- Zplus_assoc; apply Zplus_comm. + unfold le, max. rewrite (compare_antisym n m). + case compare; intuition. Qed. -Lemma Zminus_succ_r : forall n m:Z, n - (Zsucc m) = Zpred (n - m). +Lemma max_r n m : n<=m -> max n m = m. Proof. -intros; unfold Zsucc; now rewrite Zminus_plus_distr. + unfold le, max. case compare_spec; intuition. Qed. -Lemma Zplus_minus_eq : forall n m p:Z, n = m + p -> p = n - m. +Lemma min_l n m : n<=m -> min n m = n. 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. + unfold le, min. case compare_spec; intuition. Qed. -Lemma Zminus_plus : forall n m:Z, n + m - n = m. +Lemma min_r n m : m<=n -> min n m = m. Proof. - intros n m; unfold Zminus in |- *; rewrite (Zplus_comm n m); - rewrite <- Zplus_assoc; rewrite Zplus_opp_r; apply Zplus_0_r. + unfold le, min. + rewrite (compare_antisym n m). case compare_spec; intuition. Qed. -Lemma Zplus_minus : forall n m:Z, n + (m - n) = m. +(** ** Specification of absolute value *) + +Lemma abs_eq n : 0 <= n -> abs n = n. Proof. - unfold Zminus in |- *; intros n m; rewrite Zplus_permute; rewrite Zplus_opp_r; - apply Zplus_0_r. + destruct n; trivial. now destruct 1. Qed. -Lemma Zminus_plus_simpl_l : forall n m p:Z, p + n - (p + m) = n - m. +Lemma abs_neq n : n <= 0 -> abs n = - 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. + destruct n; trivial. now destruct 1. Qed. -Lemma Zminus_plus_simpl_l_reverse : forall n m p:Z, n - m = p + n - (p + m). +(** ** Specification of sign *) + +Lemma sgn_null n : n = 0 -> sgn n = 0. Proof. - intros; symmetry in |- *; apply Zminus_plus_simpl_l. + intros. now subst. Qed. -Lemma Zminus_plus_simpl_r : forall n m p:Z, n + p - (m + p) = n - m. +Lemma sgn_pos n : 0 < n -> sgn n = 1. 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. + now destruct n. Qed. -Lemma Zpos_minus_morphism : forall a b:positive, Pcompare a b Eq = Lt -> - Zpos (b-a) = Zpos b - Zpos a. +Lemma sgn_neg n : n < 0 -> sgn n = -1. Proof. - intros. - simpl. - change Eq with (CompOpp Eq). - rewrite <- Pcompare_antisym. - rewrite H; simpl; auto. + now destruct n. Qed. -(** ** Misc redundant properties *) +(** ** Specification of power *) -Lemma Zeq_minus : forall n m:Z, n = m -> n - m = Z0. +Lemma pow_0_r n : n^0 = 1. Proof. - intros x y H; rewrite H; symmetry in |- *; apply Zminus_diag_reverse. + reflexivity. Qed. -Lemma Zminus_eq : forall n m:Z, n - m = Z0 -> n = m. +Lemma pow_succ_r n m : 0<=m -> n^(succ m) = n * n^m. Proof. - intros x y H; rewrite <- (Zplus_minus y x); rewrite H; apply Zplus_0_r. + destruct m as [|m|m]; (now destruct 1) || (intros _); simpl; trivial. + unfold pow_pos. now rewrite Pos.add_comm, Pos.iter_add. Qed. +Lemma pow_neg_r n m : m<0 -> n^m = 0. +Proof. + now destruct m. +Qed. -(**********************************************************************) -(** * Properties of multiplication on binary integer numbers *) +(** For folding back a [pow_pos] into a [pow] *) -Theorem Zpos_mult_morphism : - forall p q:positive, Zpos (p*q) = Zpos p * Zpos q. +Lemma pow_pos_fold n p : pow_pos n p = n ^ (Zpos p). Proof. - auto. + reflexivity. Qed. -(** ** One is neutral for multiplication *) +(** ** Specification of square *) -Theorem Zmult_1_l : forall n:Z, Zpos 1 * n = n. +Lemma square_spec n : square n = n * n. Proof. - intro x; destruct x; reflexivity. + destruct n; trivial; simpl; f_equal; apply Pos.square_spec. Qed. -Theorem Zmult_1_r : forall n:Z, n * Zpos 1 = n. +(** ** Specification of square root *) + +Lemma sqrtrem_spec n : 0<=n -> + let (s,r) := sqrtrem n in n = s*s + r /\ 0 <= r <= 2*s. Proof. - intro x; destruct x; simpl in |- *; try rewrite Pmult_1_r; reflexivity. + destruct n. now repeat split. + generalize (Pos.sqrtrem_spec p). simpl. + destruct 1; simpl; subst; now repeat split. + now destruct 1. Qed. -(** ** Zero property of multiplication *) +Lemma sqrt_spec n : 0<=n -> + let s := sqrt n in s*s <= n < (succ s)*(succ s). +Proof. + destruct n. now repeat split. unfold sqrt. + rewrite succ_Zpos. intros _. apply (Pos.sqrt_spec p). + now destruct 1. +Qed. -Theorem Zmult_0_l : forall n:Z, Z0 * n = Z0. +Lemma sqrt_neg n : n<0 -> sqrt n = 0. Proof. - intro x; destruct x; reflexivity. + now destruct n. Qed. -Theorem Zmult_0_r : forall n:Z, n * Z0 = Z0. +Lemma sqrtrem_sqrt n : fst (sqrtrem n) = sqrt n. Proof. - intro x; destruct x; reflexivity. + destruct n; try reflexivity. + unfold sqrtrem, sqrt, Pos.sqrt. + destruct (Pos.sqrtrem p) as (s,r). now destruct r. Qed. -Hint Local Resolve Zmult_0_l Zmult_0_r. +(** ** Specification of logarithm *) -Lemma Zmult_0_r_reverse : forall n:Z, Z0 = n * Z0. +Lemma log2_spec n : 0 < n -> 2^(log2 n) <= n < 2^(succ (log2 n)). Proof. - intro x; destruct x; reflexivity. + destruct n as [|[p|p|]|]; intros Hn; split; try easy; unfold log2; + rewrite ?succ_Zpos, pow_Zpos. + 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. -(** ** Commutativity of multiplication *) +Lemma log2_nonpos n : n<=0 -> log2 n = 0. +Proof. + destruct n as [|p|p]; trivial; now destruct 1. +Qed. + +(** Specification of parity functions *) -Theorem Zmult_comm : forall n m:Z, n * m = m * n. +Lemma even_spec n : even n = true <-> Even n. Proof. - intros x y; destruct x as [| p| p]; destruct y as [| q| q]; simpl in |- *; - try rewrite (Pmult_comm p q); reflexivity. + split. + exists (div2 n). now destruct n as [|[ | | ]|[ | | ]]. + intros (m,->). now destruct m. Qed. -(** ** Associativity of multiplication *) +Lemma odd_spec n : odd n = true <-> Odd n. +Proof. + 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 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 Zpos 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). + rewrite pos_xI, 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). + rewrite (pos_xO a), 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 (Zpos b) (eq_refl _)); + destruct pos_div_eucl as (q,r); rewrite <- ?opp_Zpos, mul_comm; + intros ->. + - (* Zpos Zpos *) + trivial. + - (* Zpos Zneg *) + destruct r as [ |r|r]; rewrite !mul_opp_opp; trivial; + rewrite mul_add_distr_l, mul_1_r, <- add_assoc; f_equal; + now rewrite add_assoc, add_opp_diag_r. + - (* Zneg Zpos *) + 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. + - (* Zneg Zneg *) + 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 < Zpos (p~0) -> m - Zpos p < Zpos p). + intros m p. unfold lt. + rewrite (compare_sub m), (compare_sub _ (Zpos _)). unfold sub. + rewrite <- add_assoc. simpl opp; simpl (Zneg _ + _). + 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. -Theorem Zmult_assoc : forall n m p:Z, n * (m * p) = n * m * p. +Lemma mod_pos_bound a b : 0 < b -> 0 <= a mod b < b. Proof. - intros x y z; destruct x; destruct y; destruct z; simpl in |- *; - try rewrite Pmult_assoc; reflexivity. + 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 (Zpos 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. -Lemma Zmult_assoc_reverse : forall n m p:Z, n * m * p = n * (m * p). +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. - intros n m p; rewrite Zmult_assoc; trivial with arith. + 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 (Zpos 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 (Zneg b - Zneg r <= 0). unfold le, lt in *. + rewrite <- compare_sub. simpl in *. + now rewrite <- Pos.compare_antisym, Hr'. + generalize (pos_div_eucl_bound a (Zpos 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. -(** ** Associativity mixed with commutativity *) +(** ** Correctness proofs for Floor division *) + +Theorem quotrem_eq a b : let (q,r) := quotrem a b in a = q * b + r. +Proof. + destruct a as [|a|a], b as [|b|b]; simpl; trivial; + generalize (N.pos_div_eucl_spec a (Npos b)); case N.pos_div_eucl; trivial; + intros q r; rewrite <- ?opp_Zpos; + change (Zpos a) with (of_N (Npos a)); intros ->; now destruct q, r. +Qed. -Theorem Zmult_permute : forall n m p:Z, n * (m * p) = m * (n * p). +Lemma quot_rem' a b : a = b*(a÷b) + rem a b. Proof. - intros x y z; rewrite (Zmult_assoc y x z); rewrite (Zmult_comm y x). - apply Zmult_assoc. + rewrite mul_comm. generalize (quotrem_eq a b). + unfold quot, rem. now destruct quotrem. Qed. -(** ** Z is integral *) +Lemma quot_rem a b : b<>0 -> a = b*(a÷b) + rem a b. +Proof. intros _. apply quot_rem'. Qed. -Theorem Zmult_integral_l : forall n m:Z, n <> Z0 -> m * n = Z0 -> m = Z0. +Lemma rem_bound_pos a b : 0<=a -> 0<b -> 0 <= rem a b < b. 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. + 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 (Npos b)). + destruct N.pos_div_eucl as (q,[|r]); simpl; split; try easy. + now apply H. Qed. +Lemma rem_opp_l' a b : rem (-a) b = - (rem a b). +Proof. + destruct a, b; trivial; unfold rem; simpl; + now destruct N.pos_div_eucl as (q,[|r]). +Qed. -Theorem Zmult_integral : forall n m:Z, n * m = Z0 -> n = Z0 \/ m = Z0. +Lemma rem_opp_r' a b : rem a (-b) = rem a b. Proof. - intros x y; destruct x; destruct y; auto; simpl in |- *; intro H; - discriminate H. + destruct a, b; trivial; unfold rem; simpl; + now destruct N.pos_div_eucl as (q,[|r]). Qed. +Lemma rem_opp_l a b : b<>0 -> rem (-a) b = - (rem a b). +Proof. intros _. apply rem_opp_l'. Qed. -Lemma Zmult_1_inversion_l : - forall n m:Z, n * m = Zpos 1 -> n = Zpos 1 \/ n = Zneg 1. +Lemma rem_opp_r a b : b<>0 -> rem a (-b) = rem a b. +Proof. intros _. apply rem_opp_r'. Qed. + +(** ** Basic properties of divisibility *) + +Lemma divide_Zpos p q : (Zpos p|Zpos q) <-> (p|q)%positive. 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. + intros ([ |r|r],H); simpl in *; destr_eq H. exists r; auto. + intros (r,H). exists (Zpos r); simpl; now f_equal. Qed. -(** ** Multiplication and Doubling *) +Lemma divide_Zpos_Zneg_r n p : (n|Zpos p) <-> (n|Zneg p). +Proof. + split; intros (m,H); exists (-m); now rewrite mul_opp_l, <- H. +Qed. -Lemma Zdouble_mult : forall z, Zdouble z = (Zpos 2) * z. +Lemma divide_Zpos_Zneg_l n p : (Zpos p|n) <-> (Zneg p|n). Proof. - reflexivity. + split; intros (m,H); exists (-m); now rewrite mul_opp_l, <- mul_opp_r. Qed. -Lemma Zdouble_plus_one_mult : forall z, - Zdouble_plus_one z = (Zpos 2) * z + (Zpos 1). +(** ** Correctness proofs for gcd *) + +Lemma ggcd_gcd a b : fst (ggcd a b) = gcd a b. Proof. - destruct z; simpl; auto with zarith. + 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. -(** ** Multiplication and Opposite *) +Lemma ggcd_correct_divisors a b : + let '(g,(aa,bb)) := ggcd a b in + a = g*aa /\ b = g*bb. +Proof. + 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_mult_distr_l : forall n m:Z, - (n * m) = - n * m. +Lemma gcd_divide_l a b : (gcd a b | a). Proof. - intros x y; destruct x; destruct y; reflexivity. + 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. -Theorem Zopp_mult_distr_r : forall n m:Z, - (n * m) = n * - m. +Lemma gcd_divide_r a b : (gcd a b | b). Proof. - intros x y; rewrite (Zmult_comm x y); rewrite Zopp_mult_distr_l; - apply Zmult_comm. + 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 Zopp_mult_distr_l_reverse : forall n m:Z, - n * m = - (n * m). +Lemma gcd_greatest a b c : (c|a) -> (c|b) -> (c | gcd a b). Proof. - intros x y; symmetry in |- *; apply Zopp_mult_distr_l. + assert (H : forall p q r, (r|Zpos p) -> (r|Zpos q) -> (r|Zpos (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_opp_comm : forall n m:Z, - n * m = n * - m. +Lemma gcd_nonneg a b : 0 <= gcd a b. Proof. - intros x y; rewrite Zopp_mult_distr_l_reverse; rewrite Zopp_mult_distr_r; - trivial with arith. + now destruct a, b. Qed. -Theorem Zmult_opp_opp : forall n m:Z, - n * - m = n * m. +(** 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 x y; destruct x; destruct y; reflexivity. + destruct a as [|a|a], b as [|b|b]; unfold ggcd, opp; auto; + destruct (Pos.ggcd a b) as (g,(aa,bb)); auto. Qed. -Theorem Zopp_eq_mult_neg_1 : forall n:Z, - n = n * Zneg 1. +(** ** Conversions between [Z.testbit] and [N.testbit] *) + +Lemma testbit_of_N a n : + testbit (of_N a) (of_N n) = N.testbit a n. Proof. - intro x; induction x; intros; rewrite Zmult_comm; auto with arith. + destruct a as [|a], n; simpl; trivial. now destruct a. Qed. -(** ** Distributivity of multiplication over addition *) +Lemma testbit_of_N' a n : 0<=n -> + testbit (of_N a) n = N.testbit a (to_N n). +Proof. + intro Hn. rewrite <- testbit_of_N. f_equal. + destruct n; trivial; now destruct Hn. +Qed. -Lemma weak_Zmult_plus_distr_r : - forall (p:positive) (n m:Z), Zpos p * (n + m) = Zpos p * n + Zpos p * m. +Lemma testbit_Zpos a n : 0<=n -> + testbit (Zpos a) n = N.testbit (Npos a) (to_N n). 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) ] ]). + intro Hn. now rewrite <- testbit_of_N'. Qed. -Theorem Zmult_plus_distr_r : forall n m p:Z, n * (m + p) = n * m + n * p. +Lemma testbit_Zneg a n : 0<=n -> + testbit (Zneg a) n = negb (N.testbit (Pos.pred_N a) (to_N n)). 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 ]. + intro Hn. + rewrite <- testbit_of_N' by trivial. + destruct n as [ |n|n]; + [ | simpl; now destruct (Ppred_N a) | now destruct Hn]. + unfold testbit. + now destruct a as [|[ | | ]| ]. Qed. -Theorem Zmult_plus_distr_l : forall n m p:Z, (n + m) * p = n * p + m * p. +(** ** Proofs of specifications for bitwise operations *) + +Lemma div2_spec a : div2 a = shiftr a 1. Proof. - intros n m p; rewrite Zmult_comm; rewrite Zmult_plus_distr_r; - do 2 rewrite (Zmult_comm p); trivial with arith. + reflexivity. Qed. -(** ** Distributivity of multiplication over subtraction *) +Lemma testbit_0_l n : testbit 0 n = false. +Proof. + now destruct n. +Qed. -Lemma Zmult_minus_distr_r : forall n m p:Z, (n - m) * p = n * p - m * p. +Lemma testbit_neg_r a n : n<0 -> testbit a n = false. Proof. - intros x y z; unfold Zminus in |- *. - rewrite <- Zopp_mult_distr_l_reverse. - apply Zmult_plus_distr_l. + now destruct n. Qed. +Lemma testbit_odd_0 a : testbit (2*a+1) 0 = true. +Proof. + now destruct a as [|a|[a|a|]]. +Qed. -Lemma Zmult_minus_distr_l : forall n m p:Z, p * (n - m) = p * n - p * m. +Lemma testbit_even_0 a : testbit (2*a) 0 = 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 a. Qed. -(** ** Simplification of multiplication for non-zero integers *) +Lemma testbit_odd_succ a n : 0<=n -> + testbit (2*a+1) (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. rewrite succ_Zpos. + destruct a as [|a|[a|a|]]; simpl; trivial; + rewrite ?Pos.pred_N_succ; now destruct n. +Qed. -Lemma Zmult_reg_l : forall n m p:Z, p <> Z0 -> p * n = p * m -> n = m. +Lemma testbit_even_succ a n : 0<=n -> + testbit (2*a) (succ n) = testbit a n. 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. + destruct n as [|n|n]; (now destruct 1) || intros _. + destruct a as [|[a|a|]|[a|a|]]; simpl; trivial. now destruct a. + unfold testbit. rewrite succ_Zpos. + destruct a as [|a|[a|a|]]; simpl; trivial; + rewrite ?Pos.pred_N_succ; now destruct n. Qed. -Lemma Zmult_reg_r : forall n m p:Z, p <> Z0 -> n * p = m * p -> n = m. +(** 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 y z Hz. - rewrite (Zmult_comm x z). - rewrite (Zmult_comm y z). - intro; apply Zmult_reg_l with z; assumption. + 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 + Zpos p) = (to_N m + Npos p)%N). + destruct m; trivial; now destruct Hm. + assert (forall p, 0 <= m + Zpos 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 (Zpos a) with (of_N (Npos a)) at 1. + rewrite <- (Pos.iter_swap_gen _ _ _ Ndiv2) by now intros [|[ | | ]]. + rewrite testbit_Zpos, testbit_of_N', H; trivial. + exact (N.shiftr_spec' (Npos a) (Npos n) (to_N m)). + (* a < 0 *) + rewrite <- (Pos.iter_swap_gen _ _ _ Pdiv2_up) by trivial. + rewrite 2 testbit_Zneg, H; trivial. f_equal. + rewrite (Pos.iter_swap_gen _ _ _ _ Ndiv2) by exact N.pred_div2_up. + exact (N.shiftr_spec' (Ppred_N a) (Npos n) (to_N m)). Qed. -(** ** Addition and multiplication by 2 *) +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 (Npos a) (Npos n) (Npos 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 (Npos 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 <= Zpos m - Zpos n). + red. now rewrite compare_antisym, <- compare_sub, <- compare_antisym. + assert (EQ : to_N (Zpos m - Zpos n) = (Npos m - Npos 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' (Npos p) (Npos n) (Npos 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 (Npos n)). + (* n < 0 *) + unfold sub. simpl. + now apply (shiftr_spec_aux a (Zpos 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. + +(** ** 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 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 (Zpos p)). + induction p using Pos.peano_ind. + now apply (Hp 0). + rewrite <- Pos.add_1_r. + now apply (Hp (Zneg p)). +Qed. + +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 _ H0 Hs. induction z using peano_ind. + assumption. + now apply -> Hs. + apply Hs. now rewrite succ_pred. +Qed. + + +(** * 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 := _. + +Include ZProp + <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties. + +(** Otherwise Z stays associated with abstract_scope : (TODO FIX) *) +Bind Scope Z_scope with Z. + +(** 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 Zplus_diag_eq_mult_2 : forall n:Z, n + n = n * Zpos 2. +Lemma gt_lt_iff n m : n > m <-> m < n. Proof. - intros x; pattern x at 1 2 in |- *; rewrite <- (Zmult_1_r x); - rewrite <- Zmult_plus_distr_r; reflexivity. + unfold lt, gt. now rewrite compare_antisym, CompOpp_iff. Qed. -(** ** Multiplication and successor *) +Lemma gt_lt n m : n > m -> m < n. +Proof. + apply gt_lt_iff. +Qed. -Lemma Zmult_succ_r : forall n m:Z, n * Zsucc m = n * m + n. +Lemma lt_gt n m : n < m -> 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. + apply gt_lt_iff. Qed. -Lemma Zmult_succ_r_reverse : forall n m:Z, n * m + n = n * Zsucc m. +Lemma ge_le_iff n m : n >= m <-> m <= n. Proof. - intros; symmetry in |- *; apply Zmult_succ_r. + unfold le, ge. now rewrite compare_antisym, CompOpp_iff. Qed. -Lemma Zmult_succ_l : forall n m:Z, Zsucc n * m = n * m + m. +Lemma ge_le 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. + apply ge_le_iff. Qed. -Lemma Zmult_succ_l_reverse : forall n m:Z, n * m + m = Zsucc n * m. +Lemma le_ge n m : n <= m -> m >= n. Proof. - intros; symmetry in |- *; apply Zmult_succ_l. + 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 *. -(** ** Misc redundant properties *) +(** 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 Z_eq_mult : forall n m:Z, m = Z0 -> m * n = Z0. +Lemma gtb_ltb n m : (n >? m) = (m <? n). Proof. - intros x y H; rewrite H; auto with arith. + unfold gtb, ltb. rewrite compare_antisym. now case compare. Qed. +Lemma geb_leb n m : (n >=? m) = (m <=? n). +Proof. + unfold geb, leb. rewrite compare_antisym. now case compare. +Qed. +Lemma gtb_lt n m : (n >? m) = true <-> m < n. +Proof. + rewrite gtb_ltb. apply ltb_lt. +Qed. -(**********************************************************************) -(** * Relating binary positive numbers and binary integers *) +Lemma geb_le n m : (n >=? m) = true <-> m <= n. +Proof. + rewrite geb_leb. apply leb_le. +Qed. -Lemma Zpos_eq : forall p q:positive, p = q -> Zpos p = Zpos q. +Lemma gtb_spec n m : BoolSpec (m<n) (n<=m) (n >? m). Proof. - intros; f_equal; auto. + rewrite gtb_ltb. apply ltb_spec. Qed. -Lemma Zpos_eq_rev : forall p q:positive, Zpos p = Zpos q -> p = q. +Lemma geb_spec n m : BoolSpec (m<=n) (n<m) (n >=? m). Proof. - inversion 1; auto. + rewrite geb_leb. apply leb_spec. Qed. -Lemma Zpos_eq_iff : forall p q:positive, p = q <-> Zpos p = Zpos q. +(** TODO : to add in Numbers ? *) + +Lemma add_reg_l n m p : n + m = n + p -> m = p. Proof. - split; [apply Zpos_eq|apply Zpos_eq_rev]. + exact (proj1 (add_cancel_l m p n)). Qed. -Lemma Zpos_xI : forall p:positive, Zpos p~1 = Zpos 2 * Zpos p + Zpos 1. +Lemma mul_reg_l n m p : p <> 0 -> p * n = p * m -> n = m. Proof. - intro; apply refl_equal. + exact (fun Hp => proj1 (mul_cancel_l n m p Hp)). Qed. -Lemma Zpos_xO : forall p:positive, Zpos p~0 = Zpos 2 * Zpos p. +Lemma mul_reg_r n m p : p <> 0 -> n * p = m * p -> n = m. Proof. - intro; apply refl_equal. + exact (fun Hp => proj1 (mul_cancel_r n m p Hp)). Qed. -Lemma Zneg_xI : forall p:positive, Zneg p~1 = Zpos 2 * Zneg p - Zpos 1. +Lemma opp_eq_mul_m1 n : - n = n * -1. Proof. - intro; apply refl_equal. + rewrite mul_comm. now destruct n. Qed. -Lemma Zneg_xO : forall p:positive, Zneg p~0 = Zpos 2 * Zneg p. +Lemma add_diag n : n + n = 2 * n. Proof. - reflexivity. + change 2 with (1+1). now rewrite mul_add_distr_r, !mul_1_l. Qed. -Lemma Zpos_plus_distr : forall p q:positive, Zpos (p + q) = Zpos p + Zpos q. +(** * Comparison and opposite *) + +Lemma compare_opp n m : (- n ?= - m) = (m ?= n). Proof. - intros p p'; destruct p; - [ destruct p' as [p0| p0| ] - | destruct p' as [p0| p0| ] - | destruct p' as [p| p| ] ]; reflexivity. + destruct n, m; simpl; trivial; intros; now rewrite <- Pos.compare_antisym. Qed. -Lemma Zneg_plus_distr : forall p q:positive, Zneg (p + q) = Zneg p + Zneg q. +(** * Comparison and addition *) + +Lemma add_compare_mono_l n m p : (n + m ?= n + p) = (m ?= p). Proof. - intros p p'; destruct p; - [ destruct p' as [p0| p0| ] - | destruct p' as [p0| p0| ] - | destruct p' as [p| p| ] ]; reflexivity. + 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. -(**********************************************************************) -(** * Order relations *) +End Z. + +(** 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. + +(* TODO : transition from Zdivide *) +Notation "( x | y )" := (Z.divide x y) (at level 0). -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 "?=" := Z.compare (at level 70, no associativity) : Z_scope. -Infix "<=" := Zle : Z_scope. -Infix "<" := Zlt : Z_scope. -Infix ">=" := Zge : Z_scope. -Infix ">" := Zgt : 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. +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. + +(** Compatibility Notations *) + +Notation Zdouble_plus_one := Z.succ_double (only parsing). +Notation Zdouble_minus_one := Z.pred_double (only parsing). +Notation Zdouble := Z.double (only parsing). +Notation ZPminus := Z.pos_sub (only parsing). +Notation Zsucc' := Z.succ (only parsing). +Notation Zpred' := Z.pred (only parsing). +Notation Zplus' := Z.add (only parsing). +Notation Zplus := Z.add (only parsing). (* Slightly incompatible *) +Notation Zopp := Z.opp (only parsing). +Notation Zsucc := Z.succ (only parsing). +Notation Zpred := Z.pred (only parsing). +Notation Zminus := Z.sub (only parsing). +Notation Zmult := Z.mul (only parsing). +Notation Zcompare := Z.compare (only parsing). +Notation Zsgn := Z.sgn (only parsing). +Notation Zle := Z.le (only parsing). +Notation Zge := Z.ge (only parsing). +Notation Zlt := Z.lt (only parsing). +Notation Zgt := Z.gt (only parsing). +Notation Zmax := Z.max (only parsing). +Notation Zmin := Z.min (only parsing). +Notation Zabs := Z.abs (only parsing). +Notation Zabs_nat := Z.abs_nat (only parsing). +Notation Zabs_N := Z.abs_N (only parsing). +Notation Z_of_nat := Z.of_nat (only parsing). +Notation Z_of_N := Z.of_N (only parsing). + +Notation Zind := Z.peano_ind (only parsing). +Notation Zopp_0 := Z.opp_0 (only parsing). +Notation Zopp_neg := Z.opp_Zneg (only parsing). +Notation Zopp_involutive := Z.opp_involutive (only parsing). +Notation Zopp_inj := Z.opp_inj (only parsing). +Notation Zplus_0_l := Z.add_0_l (only parsing). +Notation Zplus_0_r := Z.add_0_r (only parsing). +Notation Zplus_comm := Z.add_comm (only parsing). +Notation Zopp_plus_distr := Z.opp_add_distr (only parsing). +Notation Zopp_succ := Z.opp_succ (only parsing). +Notation Zplus_opp_r := Z.add_opp_diag_r (only parsing). +Notation Zplus_opp_l := Z.add_opp_diag_l (only parsing). +Notation Zplus_assoc := Z.add_assoc (only parsing). +Notation Zplus_permute := Z.add_shuffle3 (only parsing). +Notation Zplus_reg_l := Z.add_reg_l (only parsing). +Notation Zplus_succ_l := Z.add_succ_l (only parsing). +Notation Zplus_succ_comm := Z.add_succ_comm (only parsing). +Notation Zsucc_discr := Z.neq_succ_diag_r (only parsing). +Notation Zsucc_inj := Z.succ_inj (only parsing). +Notation Zsucc'_inj := Z.succ_inj (only parsing). +Notation Zsucc'_pred' := Z.succ_pred (only parsing). +Notation Zpred'_succ' := Z.pred_succ (only parsing). +Notation Zpred'_inj := Z.pred_inj (only parsing). +Notation Zsucc'_discr := Z.neq_succ_diag_r (only parsing). +Notation Zminus_0_r := Z.sub_0_r (only parsing). +Notation Zminus_diag := Z.sub_diag (only parsing). +Notation Zminus_plus_distr := Z.sub_add_distr (only parsing). +Notation Zminus_succ_r := Z.sub_succ_r (only parsing). +Notation Zminus_plus := Z.add_simpl_l (only parsing). +Notation Zmult_0_l := Z.mul_0_l (only parsing). +Notation Zmult_0_r := Z.mul_0_r (only parsing). +Notation Zmult_1_l := Z.mul_1_l (only parsing). +Notation Zmult_1_r := Z.mul_1_r (only parsing). +Notation Zmult_comm := Z.mul_comm (only parsing). +Notation Zmult_assoc := Z.mul_assoc (only parsing). +Notation Zmult_permute := Z.mul_shuffle3 (only parsing). +Notation Zmult_1_inversion_l := Z.mul_eq_1 (only parsing). +Notation Zdouble_mult := Z.double_spec (only parsing). +Notation Zdouble_plus_one_mult := Z.succ_double_spec (only parsing). +Notation Zopp_mult_distr_l_reverse := Z.mul_opp_l (only parsing). +Notation Zmult_opp_opp := Z.mul_opp_opp (only parsing). +Notation Zmult_opp_comm := Z.mul_opp_comm (only parsing). +Notation Zopp_eq_mult_neg_1 := Z.opp_eq_mul_m1 (only parsing). +Notation Zmult_plus_distr_r := Z.mul_add_distr_l (only parsing). +Notation Zmult_plus_distr_l := Z.mul_add_distr_r (only parsing). +Notation Zmult_minus_distr_r := Z.mul_sub_distr_r (only parsing). +Notation Zmult_reg_l := Z.mul_reg_l (only parsing). +Notation Zmult_reg_r := Z.mul_reg_r (only parsing). +Notation Zmult_succ_l := Z.mul_succ_l (only parsing). +Notation Zmult_succ_r := Z.mul_succ_r (only parsing). +Notation Zpos_xI := Z.pos_xI (only parsing). +Notation Zpos_xO := Z.pos_xO (only parsing). +Notation Zneg_xI := Z.neg_xI (only parsing). +Notation Zneg_xO := Z.neg_xO (only parsing). + +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 Zpos_succ_morphism : forall p, Zpos (Psucc p) = Zsucc (Zpos p). +Proof (SYM1 Z.succ_Zpos). +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 Zpos_minus_morphism : forall a b, + Pcompare a b Eq = Lt -> Zpos (b - a) = Zpos b - Zpos a. +Proof. intros. now rewrite Z.sub_Zpos. Qed. +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 Zpos_mult_morphism : forall p q, Zpos (p * q) = Zpos p * Zpos q. +Proof (SYM2 Z.mul_Zpos). +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 * Zsucc m. +Proof (SYM2 Z.mul_succ_r). +Lemma Zmult_succ_l_reverse : forall n m, n * m + m = Zsucc n * m. +Proof (SYM2 Z.mul_succ_l). +Lemma Zpos_eq : forall p q, p = q -> Zpos p = Zpos q. +Proof (fun p q => proj2 (Z.inj_Zpos p q)). +Lemma Zpos_eq_rev : forall p q, Zpos p = Zpos q -> p = q. +Proof (fun p q => proj1 (Z.inj_Zpos p q)). +Lemma Zpos_eq_iff : forall p q, p = q <-> Zpos p = Zpos q. +Proof (fun p q => iff_sym (Z.inj_Zpos p q)). +Lemma Zpos_plus_distr : forall p q, Zpos (p + q) = Zpos p + Zpos q. +Proof (SYM2 Z.add_Zpos). +Lemma Zneg_plus_distr : forall p q, Zneg (p + q) = Zneg p + Zneg q. +Proof (SYM2 Z.add_Zneg). + +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. |