diff options
Diffstat (limited to 'theories/ZArith/BinInt.v')
| -rw-r--r-- | theories/ZArith/BinInt.v | 977 |
1 files changed, 496 insertions, 481 deletions
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index fda521de..71e48360 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -6,10 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: BinInt.v 8883 2006-05-31 21:56:37Z letouzey $ i*) +(*i $Id: BinInt.v 9245 2006-10-17 12:53:34Z notin $ i*) (***********************************************************) -(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) +(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) (***********************************************************) Require Export BinPos. @@ -19,190 +19,190 @@ Require Import Plus. Require Import Mult. Unset Boxed Definitions. -(**********************************************************************) -(** Binary integer numbers *) + +(*****************************) +(** * Binary integer numbers *) Inductive Z : Set := | Z0 : Z | Zpos : positive -> Z | Zneg : positive -> Z. -(** Declare Scope Z_scope with Key Z *) -Delimit Scope Z_scope with Z. (** Automatically open scope positive_scope for the constructors of Z *) +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 *) +(** ** Subtraction of positive into Z *) Definition Zdouble_plus_one (x:Z) := match x with - | Z0 => Zpos 1 - | Zpos p => Zpos (xI p) - | Zneg p => Zneg (Pdouble_minus_one p) + | Z0 => Zpos 1 + | Zpos p => Zpos (xI p) + | Zneg p => Zneg (Pdouble_minus_one p) end. Definition Zdouble_minus_one (x:Z) := match x with - | Z0 => Zneg 1 - | Zneg p => Zneg (xI p) - | Zpos p => Zpos (Pdouble_minus_one p) + | Z0 => Zneg 1 + | Zneg p => Zneg (xI p) + | Zpos p => Zpos (Pdouble_minus_one p) end. Definition Zdouble (x:Z) := match x with - | Z0 => Z0 - | Zpos p => Zpos (xO p) - | Zneg p => Zneg (xO p) + | Z0 => Z0 + | Zpos p => Zpos (xO p) + | Zneg p => Zneg (xO p) end. Fixpoint ZPminus (x y:positive) {struct y} : Z := match x, y with - | xI x', xI y' => Zdouble (ZPminus x' y') - | xI x', xO y' => Zdouble_plus_one (ZPminus x' y') - | xI x', xH => Zpos (xO x') - | xO x', xI y' => Zdouble_minus_one (ZPminus x' y') - | xO x', xO y' => Zdouble (ZPminus x' y') - | xO x', xH => Zpos (Pdouble_minus_one x') - | xH, xI y' => Zneg (xO y') - | xH, xO y' => Zneg (Pdouble_minus_one y') - | xH, xH => Z0 + | xI x', xI y' => Zdouble (ZPminus x' y') + | xI x', xO y' => Zdouble_plus_one (ZPminus x' y') + | xI x', xH => Zpos (xO x') + | xO x', xI y' => Zdouble_minus_one (ZPminus x' y') + | xO x', xO y' => Zdouble (ZPminus x' y') + | xO x', xH => Zpos (Pdouble_minus_one x') + | xH, xI y' => Zneg (xO y') + | xH, xO y' => Zneg (Pdouble_minus_one y') + | xH, xH => Z0 end. -(** Addition on integers *) +(** ** Addition on integers *) Definition Zplus (x y:Z) := match x, y with - | Z0, y => y - | x, Z0 => x - | Zpos x', Zpos y' => Zpos (x' + y') - | Zpos x', Zneg y' => + | Z0, y => y + | x, Z0 => x + | Zpos x', Zpos y' => Zpos (x' + y') + | Zpos x', Zneg y' => match (x' ?= y')%positive Eq with - | Eq => Z0 - | Lt => Zneg (y' - x') - | Gt => Zpos (x' - y') + | Eq => Z0 + | Lt => Zneg (y' - x') + | Gt => Zpos (x' - y') end - | Zneg x', Zpos y' => + | Zneg x', Zpos y' => match (x' ?= y')%positive Eq with - | Eq => Z0 - | Lt => Zpos (y' - x') - | Gt => Zneg (x' - y') + | Eq => Z0 + | Lt => Zpos (y' - x') + | Gt => Zneg (x' - y') end - | Zneg x', Zneg y' => Zneg (x' + y') + | Zneg x', Zneg y' => Zneg (x' + y') end. Infix "+" := Zplus : Z_scope. -(** Opposite *) +(** ** Opposite *) Definition Zopp (x:Z) := match x with - | Z0 => Z0 - | Zpos x => Zneg x - | Zneg x => Zpos x + | Z0 => Z0 + | Zpos x => Zneg x + | Zneg x => Zpos x end. Notation "- x" := (Zopp x) : Z_scope. -(** Successor on integers *) +(** ** Successor on integers *) Definition Zsucc (x:Z) := (x + Zpos 1)%Z. -(** Predecessor on integers *) +(** ** Predecessor on integers *) Definition Zpred (x:Z) := (x + Zneg 1)%Z. -(** Subtraction on integers *) +(** ** Subtraction on integers *) Definition Zminus (m n:Z) := (m + - n)%Z. Infix "-" := Zminus : Z_scope. -(** Multiplication on integers *) +(** ** 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') + | 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 *) +(** ** 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) + | Z0, Z0 => Eq + | Z0, Zpos y' => Lt + | Z0, Zneg y' => Gt + | Zpos x', Z0 => Gt + | Zpos x', Zpos y' => (x' ?= y')%positive Eq + | Zpos x', Zneg y' => Gt + | Zneg x', Z0 => Lt + | Zneg x', Zpos y' => Lt + | Zneg x', Zneg y' => CompOpp ((x' ?= y')%positive Eq) end. Infix "?=" := Zcompare (at level 70, no associativity) : Z_scope. Ltac elim_compare com1 com2 := case (Dcompare (com1 ?= com2)%Z); - [ idtac | let x := fresh "H" in - (intro x; case x; clear x) ]. + [ idtac | let x := fresh "H" in + (intro x; case x; clear x) ]. -(** Sign function *) +(** ** Sign function *) Definition Zsgn (z:Z) : Z := match z with - | Z0 => Z0 - | Zpos p => Zpos 1 - | Zneg p => Zneg 1 + | Z0 => Z0 + | Zpos p => Zpos 1 + | Zneg p => Zneg 1 end. -(** Direct, easier to handle variants of successor and addition *) +(** ** Direct, easier to handle variants of successor and addition *) Definition Zsucc' (x:Z) := match x with - | Z0 => Zpos 1 - | Zpos x' => Zpos (Psucc x') - | Zneg x' => ZPminus 1 x' + | Z0 => Zpos 1 + | Zpos x' => Zpos (Psucc x') + | Zneg x' => ZPminus 1 x' end. Definition Zpred' (x:Z) := match x with - | Z0 => Zneg 1 - | Zpos x' => ZPminus x' 1 - | Zneg x' => Zneg (Psucc x') + | Z0 => Zneg 1 + | Zpos x' => ZPminus x' 1 + | Zneg x' => Zneg (Psucc x') end. Definition Zplus' (x y:Z) := match x, y with - | Z0, y => y - | x, Z0 => x - | Zpos x', Zpos y' => Zpos (x' + y') - | Zpos x', Zneg y' => ZPminus x' y' - | Zneg x', Zpos y' => ZPminus y' x' - | Zneg x', Zneg y' => Zneg (x' + y') + | Z0, y => y + | x, Z0 => x + | Zpos x', Zpos y' => Zpos (x' + y') + | Zpos x', Zneg y' => ZPminus x' y' + | Zneg x', Zpos y' => ZPminus y' x' + | Zneg x', Zneg y' => Zneg (x' + y') end. Open Local Scope Z_scope. (**********************************************************************) -(** Inductive specification of Z *) +(** ** Inductive specification of Z *) Theorem Zind : - forall P:Z -> Prop, - P Z0 -> - (forall x:Z, P x -> P (Zsucc' x)) -> - (forall x:Z, P x -> P (Zpred' x)) -> forall n:Z, P n. + 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. + 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. @@ -213,52 +213,56 @@ intros P H0 Hs Hp z; destruct z. Qed. (**********************************************************************) -(** Properties of opposite on binary integer numbers *) +(** * Misc properties about binary integer operations *) + + +(**********************************************************************) +(** ** Properties of opposite on binary integer numbers *) Theorem Zopp_neg : forall p:positive, - Zneg p = Zpos p. Proof. -reflexivity. + reflexivity. Qed. (** [opp] is involutive *) Theorem Zopp_involutive : forall n:Z, - - n = n. Proof. -intro x; destruct x; reflexivity. + intro x; destruct x; reflexivity. Qed. (** Injectivity of the opposite *) Theorem Zopp_inj : forall n m:Z, - n = - m -> n = m. Proof. -intros x y; case x; case y; simpl in |- *; intros; - [ trivial - | discriminate H - | discriminate H - | discriminate H - | simplify_eq H; intro E; rewrite E; trivial - | discriminate H - | discriminate H - | discriminate H - | simplify_eq H; intro E; rewrite E; trivial ]. + intros x y; case x; case y; simpl in |- *; intros; + [ trivial + | discriminate H + | discriminate H + | discriminate H + | simplify_eq H; intro E; rewrite E; trivial + | discriminate H + | discriminate H + | discriminate H + | simplify_eq H; intro E; rewrite E; trivial ]. Qed. -(**********************************************************************) -(* Properties of the direct definition of successor and predecessor *) +(*************************************************************************) +(** ** Properties of the direct definition of successor and predecessor *) Lemma Zpred'_succ' : forall n:Z, Zpred' (Zsucc' n) = n. Proof. -intro x; destruct x; simpl in |- *. - reflexivity. -destruct p; simpl in |- *; try rewrite Pdouble_minus_one_o_succ_eq_xI; - reflexivity. -destruct p; simpl in |- *; try rewrite Psucc_o_double_minus_one_eq_xO; - reflexivity. + intro x; destruct x; simpl in |- *. + reflexivity. + destruct p; simpl in |- *; try rewrite Pdouble_minus_one_o_succ_eq_xI; + reflexivity. + destruct p; simpl in |- *; try rewrite Psucc_o_double_minus_one_eq_xO; + reflexivity. Qed. Lemma Zsucc'_discr : forall n:Z, n <> Zsucc' n. Proof. -intro x; destruct x; simpl in |- *. + intro x; destruct x; simpl in |- *. discriminate. injection; apply Psucc_discr. destruct p; simpl in |- *. @@ -268,512 +272,517 @@ intro x; destruct x; simpl in |- *. Qed. (**********************************************************************) -(** Other properties of binary integer numbers *) +(** ** Other properties of binary integer numbers *) Lemma ZL0 : 2%nat = (1 + 1)%nat. Proof. -reflexivity. + reflexivity. Qed. (**********************************************************************) -(** Properties of the addition on integers *) +(** * Properties of the addition on integers *) -(** zero is left neutral for addition *) +(** ** zero is left neutral for addition *) Theorem Zplus_0_l : forall n:Z, Z0 + n = n. Proof. -intro x; destruct x; reflexivity. + intro x; destruct x; reflexivity. Qed. -(** zero is right neutral for addition *) +(** *** zero is right neutral for addition *) Theorem Zplus_0_r : forall n:Z, n + Z0 = n. Proof. -intro x; destruct x; reflexivity. + intro x; destruct x; reflexivity. Qed. -(** addition is commutative *) +(** ** addition is commutative *) Theorem Zplus_comm : forall n m:Z, n + m = m + n. Proof. -intro x; induction x as [| p| p]; intro y; destruct y as [| q| q]; - simpl in |- *; try reflexivity. + intro x; induction x as [| p| p]; intro y; destruct y as [| q| q]; + simpl in |- *; try reflexivity. rewrite Pplus_comm; reflexivity. rewrite ZC4; destruct ((q ?= p)%positive Eq); reflexivity. rewrite ZC4; destruct ((q ?= p)%positive Eq); reflexivity. rewrite Pplus_comm; reflexivity. Qed. -(** opposite distributes over addition *) +(** ** opposite distributes over addition *) Theorem Zopp_plus_distr : forall n m:Z, - (n + m) = - n + - m. Proof. -intro x; destruct x as [| p| p]; intro y; destruct y as [| q| q]; - simpl in |- *; reflexivity || destruct ((p ?= q)%positive Eq); - reflexivity. + intro x; destruct x as [| p| p]; intro y; destruct y as [| q| q]; + simpl in |- *; reflexivity || destruct ((p ?= q)%positive Eq); + reflexivity. Qed. -(** opposite is inverse for addition *) +(** ** opposite is inverse for addition *) Theorem Zplus_opp_r : forall n:Z, n + - n = Z0. Proof. -intro x; destruct x as [| p| p]; simpl in |- *; - [ reflexivity - | rewrite (Pcompare_refl p); reflexivity - | rewrite (Pcompare_refl p); reflexivity ]. + intro x; destruct x as [| p| p]; simpl in |- *; + [ reflexivity + | rewrite (Pcompare_refl p); reflexivity + | rewrite (Pcompare_refl p); reflexivity ]. Qed. Theorem Zplus_opp_l : forall n:Z, - n + n = Z0. Proof. -intro; rewrite Zplus_comm; apply Zplus_opp_r. + intro; rewrite Zplus_comm; apply Zplus_opp_r. Qed. Hint Local Resolve Zplus_0_l Zplus_0_r. -(** addition is associative *) +(** ** 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 ] ] ]. + 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 ]. + 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. + intros; symmetry in |- *; apply Zplus_assoc. Qed. -(** Associativity mixed with commutativity *) +(** ** 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. + intros n m p; rewrite Zplus_comm; rewrite <- Zplus_assoc; + rewrite (Zplus_comm p n); trivial with arith. Qed. -(** addition simplifies *) +(** ** 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 ]. + 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 *) +(** ** 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. + intros x y; unfold Zsucc in |- *; rewrite (Zplus_comm (x + y)); + rewrite Zplus_assoc; rewrite (Zplus_comm (Zpos 1)); + trivial with arith. Qed. Lemma Zplus_succ_r : forall n m:Z, Zsucc (n + m) = n + Zsucc m. Proof. -intros n m; unfold Zsucc in |- *; rewrite Zplus_assoc; trivial with arith. + intros n m; unfold Zsucc in |- *; rewrite Zplus_assoc; trivial with arith. Qed. Lemma Zplus_succ_comm : forall n m:Z, Zsucc n + m = n + Zsucc m. Proof. -unfold Zsucc in |- *; intros n m; rewrite <- Zplus_assoc; - rewrite (Zplus_comm (Zpos 1)); trivial with arith. + unfold Zsucc in |- *; intros n m; rewrite <- Zplus_assoc; + rewrite (Zplus_comm (Zpos 1)); trivial with arith. Qed. -(** Misc properties, usually redundant or non natural *) +(** ** Misc properties, usually redundant or non natural *) Lemma Zplus_0_r_reverse : forall n:Z, n = n + Z0. Proof. -symmetry in |- *; apply Zplus_0_r. + symmetry in |- *; apply Zplus_0_r. Qed. Lemma Zplus_0_simpl_l : forall n m:Z, n + Z0 = m -> n = m. Proof. -intros n m; rewrite Zplus_0_r; intro; assumption. + intros n m; rewrite Zplus_0_r; intro; assumption. Qed. Lemma Zplus_0_simpl_l_reverse : forall n m:Z, n = m + Z0 -> n = m. Proof. -intros n m; rewrite Zplus_0_r; intro; assumption. + intros n m; rewrite Zplus_0_r; intro; assumption. Qed. Lemma Zplus_eq_compat : forall n m p q:Z, n = m -> p = q -> n + p = m + q. Proof. -intros; rewrite H; rewrite H0; reflexivity. + intros; rewrite H; rewrite H0; reflexivity. Qed. Lemma Zplus_opp_expand : forall n m p:Z, n + - m = n + - p + (p + - m). Proof. -intros x y z. -rewrite <- (Zplus_assoc x). -rewrite (Zplus_assoc (- z)). -rewrite Zplus_opp_l. -reflexivity. + intros x y z. + rewrite <- (Zplus_assoc x). + rewrite (Zplus_assoc (- z)). + rewrite Zplus_opp_l. + reflexivity. Qed. -(**********************************************************************) -(** Properties of successor and predecessor on binary integer numbers *) +(************************************************************************) +(** * Properties of successor and predecessor on binary integer numbers *) Theorem Zsucc_discr : forall n:Z, n <> Zsucc n. Proof. -intros n; cut (Z0 <> Zpos 1); - [ unfold not in |- *; intros H1 H2; apply H1; apply (Zplus_reg_l n); - rewrite Zplus_0_r; exact H2 - | discriminate ]. + intros n; cut (Z0 <> Zpos 1); + [ unfold not in |- *; intros H1 H2; apply H1; apply (Zplus_reg_l n); + rewrite Zplus_0_r; exact H2 + | discriminate ]. Qed. Theorem Zpos_succ_morphism : - forall p:positive, Zpos (Psucc p) = Zsucc (Zpos p). + forall p:positive, Zpos (Psucc p) = Zsucc (Zpos p). Proof. -intro; rewrite Pplus_one_succ_r; unfold Zsucc in |- *; simpl in |- *; - trivial with arith. + intro; rewrite Pplus_one_succ_r; unfold Zsucc in |- *; simpl in |- *; + trivial with arith. Qed. (** successor and predecessor are inverse functions *) Theorem Zsucc_pred : forall n:Z, n = Zsucc (Zpred n). Proof. -intros n; unfold Zsucc, Zpred in |- *; rewrite <- Zplus_assoc; simpl in |- *; - rewrite Zplus_0_r; trivial with arith. + intros n; unfold Zsucc, Zpred in |- *; rewrite <- Zplus_assoc; simpl in |- *; + rewrite Zplus_0_r; trivial with arith. Qed. Hint Immediate Zsucc_pred: zarith. Theorem Zpred_succ : forall n:Z, n = Zpred (Zsucc n). Proof. -intros m; unfold Zpred, Zsucc in |- *; rewrite <- Zplus_assoc; simpl in |- *; - rewrite Zplus_comm; auto with arith. + intros m; unfold Zpred, Zsucc in |- *; rewrite <- Zplus_assoc; simpl in |- *; + rewrite Zplus_comm; auto with arith. Qed. Theorem Zsucc_inj : forall n m:Z, Zsucc n = Zsucc m -> n = m. Proof. -intros n m H. -change (Zneg 1 + Zpos 1 + n = Zneg 1 + Zpos 1 + m) in |- *; - do 2 rewrite <- Zplus_assoc; do 2 rewrite (Zplus_comm (Zpos 1)); - unfold Zsucc in H; rewrite H; trivial with arith. + intros n m H. + change (Zneg 1 + Zpos 1 + n = Zneg 1 + Zpos 1 + m) in |- *; + do 2 rewrite <- Zplus_assoc; do 2 rewrite (Zplus_comm (Zpos 1)); + unfold Zsucc in H; rewrite H; trivial with arith. Qed. (** Misc properties, usually redundant or non natural *) Lemma Zsucc_eq_compat : forall n m:Z, n = m -> Zsucc n = Zsucc m. Proof. -intros n m H; rewrite H; reflexivity. + intros n m H; rewrite H; reflexivity. Qed. Lemma Zsucc_inj_contrapositive : forall n m:Z, n <> m -> Zsucc n <> Zsucc m. Proof. -unfold not in |- *; intros n m H1 H2; apply H1; apply Zsucc_inj; assumption. + unfold not in |- *; intros n m H1 H2; apply H1; apply Zsucc_inj; assumption. Qed. (**********************************************************************) -(** Properties of subtraction on binary integer numbers *) +(** * Properties of subtraction on binary integer numbers *) + +(** ** [minus] and [Z0] *) Lemma Zminus_0_r : forall n:Z, n - Z0 = n. Proof. -intro; unfold Zminus in |- *; simpl in |- *; rewrite Zplus_0_r; - trivial with arith. + intro; unfold Zminus in |- *; simpl in |- *; rewrite Zplus_0_r; + trivial with arith. Qed. Lemma Zminus_0_l_reverse : forall n:Z, n = n - Z0. Proof. -intro; symmetry in |- *; apply Zminus_0_r. + intro; symmetry in |- *; apply Zminus_0_r. Qed. Lemma Zminus_diag : forall n:Z, n - n = Z0. Proof. -intro; unfold Zminus in |- *; rewrite Zplus_opp_r; trivial with arith. + intro; unfold Zminus in |- *; rewrite Zplus_opp_r; trivial with arith. Qed. Lemma Zminus_diag_reverse : forall n:Z, Z0 = n - n. Proof. -intro; symmetry in |- *; apply Zminus_diag. + intro; symmetry in |- *; apply Zminus_diag. Qed. + +(** ** Relating [minus] with [plus] and [Zsucc] *) + Lemma Zplus_minus_eq : forall n m p:Z, n = m + p -> p = n - m. Proof. -intros n m p H; unfold Zminus in |- *; apply (Zplus_reg_l m); - rewrite (Zplus_comm m (n + - m)); rewrite <- Zplus_assoc; - rewrite Zplus_opp_l; rewrite Zplus_0_r; rewrite H; - trivial with arith. + intros n m p H; unfold Zminus in |- *; apply (Zplus_reg_l m); + rewrite (Zplus_comm m (n + - m)); rewrite <- Zplus_assoc; + rewrite Zplus_opp_l; rewrite Zplus_0_r; rewrite H; + trivial with arith. Qed. Lemma Zminus_plus : forall n m:Z, n + m - n = m. Proof. -intros n m; unfold Zminus in |- *; rewrite (Zplus_comm n m); - rewrite <- Zplus_assoc; rewrite Zplus_opp_r; apply Zplus_0_r. + intros n m; unfold Zminus in |- *; rewrite (Zplus_comm n m); + rewrite <- Zplus_assoc; rewrite Zplus_opp_r; apply Zplus_0_r. Qed. Lemma Zplus_minus : forall n m:Z, n + (m - n) = m. Proof. -unfold Zminus in |- *; intros n m; rewrite Zplus_permute; rewrite Zplus_opp_r; - apply Zplus_0_r. + unfold Zminus in |- *; intros n m; rewrite Zplus_permute; rewrite Zplus_opp_r; + apply Zplus_0_r. Qed. Lemma Zminus_succ_l : forall n m:Z, Zsucc (n - m) = Zsucc n - m. Proof. -intros n m; unfold Zminus, Zsucc in |- *; rewrite (Zplus_comm n (- m)); - rewrite <- Zplus_assoc; apply Zplus_comm. + intros n m; unfold Zminus, Zsucc in |- *; rewrite (Zplus_comm n (- m)); + rewrite <- Zplus_assoc; apply Zplus_comm. Qed. Lemma Zminus_plus_simpl_l : forall n m p:Z, p + n - (p + m) = n - m. Proof. -intros n m p; unfold Zminus in |- *; rewrite Zopp_plus_distr; - rewrite Zplus_assoc; rewrite (Zplus_comm p); rewrite <- (Zplus_assoc n p); - rewrite Zplus_opp_r; rewrite Zplus_0_r; trivial with arith. + intros n m p; unfold Zminus in |- *; rewrite Zopp_plus_distr; + rewrite Zplus_assoc; rewrite (Zplus_comm p); rewrite <- (Zplus_assoc n p); + rewrite Zplus_opp_r; rewrite Zplus_0_r; trivial with arith. Qed. Lemma Zminus_plus_simpl_l_reverse : forall n m p:Z, n - m = p + n - (p + m). Proof. -intros; symmetry in |- *; apply Zminus_plus_simpl_l. + intros; symmetry in |- *; apply Zminus_plus_simpl_l. Qed. Lemma Zminus_plus_simpl_r : forall n m p:Z, n + p - (m + p) = n - m. -intros x y n. -unfold Zminus in |- *. -rewrite Zopp_plus_distr. -rewrite (Zplus_comm (- y) (- n)). -rewrite Zplus_assoc. -rewrite <- (Zplus_assoc x n (- n)). -rewrite (Zplus_opp_r n). -rewrite <- Zplus_0_r_reverse. -reflexivity. +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. Qed. -(** Misc redundant properties *) - +(** ** Misc redundant properties *) Lemma Zeq_minus : forall n m:Z, n = m -> n - m = Z0. Proof. -intros x y H; rewrite H; symmetry in |- *; apply Zminus_diag_reverse. + intros x y H; rewrite H; symmetry in |- *; apply Zminus_diag_reverse. Qed. Lemma Zminus_eq : forall n m:Z, n - m = Z0 -> n = m. Proof. -intros x y H; rewrite <- (Zplus_minus y x); rewrite H; apply Zplus_0_r. + intros x y H; rewrite <- (Zplus_minus y x); rewrite H; apply Zplus_0_r. Qed. (**********************************************************************) -(** Properties of multiplication on binary integer numbers *) +(** * Properties of multiplication on binary integer numbers *) Theorem Zpos_mult_morphism : - forall p q:positive, Zpos (p*q) = Zpos p * Zpos q. + forall p q:positive, Zpos (p*q) = Zpos p * Zpos q. Proof. -auto. + auto. Qed. -(** One is neutral for multiplication *) +(** ** One is neutral for multiplication *) Theorem Zmult_1_l : forall n:Z, Zpos 1 * n = n. Proof. -intro x; destruct x; reflexivity. + intro x; destruct x; reflexivity. Qed. Theorem Zmult_1_r : forall n:Z, n * Zpos 1 = n. Proof. -intro x; destruct x; simpl in |- *; try rewrite Pmult_1_r; reflexivity. + intro x; destruct x; simpl in |- *; try rewrite Pmult_1_r; reflexivity. Qed. -(** Zero property of multiplication *) +(** ** Zero property of multiplication *) Theorem Zmult_0_l : forall n:Z, Z0 * n = Z0. Proof. -intro x; destruct x; reflexivity. + intro x; destruct x; reflexivity. Qed. Theorem Zmult_0_r : forall n:Z, n * Z0 = Z0. Proof. -intro x; destruct x; reflexivity. + intro x; destruct x; reflexivity. Qed. Hint Local Resolve Zmult_0_l Zmult_0_r. Lemma Zmult_0_r_reverse : forall n:Z, Z0 = n * Z0. Proof. -intro x; destruct x; reflexivity. + intro x; destruct x; reflexivity. Qed. -(** Commutativity of multiplication *) +(** ** Commutativity of multiplication *) Theorem Zmult_comm : forall n m:Z, n * m = m * n. Proof. -intros x y; destruct x as [| p| p]; destruct y as [| q| q]; simpl in |- *; - try rewrite (Pmult_comm p q); reflexivity. + intros x y; destruct x as [| p| p]; destruct y as [| q| q]; simpl in |- *; + try rewrite (Pmult_comm p q); reflexivity. Qed. -(** Associativity of multiplication *) +(** ** Associativity of multiplication *) Theorem Zmult_assoc : forall n m p:Z, n * (m * p) = n * m * p. Proof. -intros x y z; destruct x; destruct y; destruct z; simpl in |- *; - try rewrite Pmult_assoc; reflexivity. + intros x y z; destruct x; destruct y; destruct z; simpl in |- *; + try rewrite Pmult_assoc; reflexivity. Qed. Lemma Zmult_assoc_reverse : forall n m p:Z, n * m * p = n * (m * p). Proof. -intros n m p; rewrite Zmult_assoc; trivial with arith. + intros n m p; rewrite Zmult_assoc; trivial with arith. Qed. -(** Associativity mixed with commutativity *) +(** ** Associativity mixed with commutativity *) Theorem Zmult_permute : forall n m p:Z, n * (m * p) = m * (n * p). Proof. -intros x y z; rewrite (Zmult_assoc y x z); rewrite (Zmult_comm y x). -apply Zmult_assoc. + intros x y z; rewrite (Zmult_assoc y x z); rewrite (Zmult_comm y x). + apply Zmult_assoc. Qed. -(** Z is integral *) +(** ** Z is integral *) Theorem Zmult_integral_l : forall n m:Z, n <> Z0 -> m * n = Z0 -> m = Z0. Proof. -intros x y; destruct x as [| p| p]. + 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. @@ -782,214 +791,220 @@ Qed. Theorem Zmult_integral : forall n m:Z, n * m = Z0 -> n = Z0 \/ m = Z0. Proof. -intros x y; destruct x; destruct y; auto; simpl in |- *; intro H; - discriminate H. + intros x y; destruct x; destruct y; auto; simpl in |- *; intro H; + discriminate H. Qed. Lemma Zmult_1_inversion_l : - forall n m:Z, n * m = Zpos 1 -> n = Zpos 1 \/ n = Zneg 1. + forall n m:Z, n * m = Zpos 1 -> n = Zpos 1 \/ n = Zneg 1. Proof. -intros x y; destruct x as [| p| p]; intro; [ discriminate | left | right ]; - (destruct y as [| q| q]; try discriminate; simpl in H; injection H; clear H; - intro H; rewrite Pmult_1_inversion_l with (1 := H); - reflexivity). + intros x y; destruct x as [| p| p]; intro; [ discriminate | left | right ]; + (destruct y as [| q| q]; try discriminate; simpl in H; injection H; clear H; + intro H; rewrite Pmult_1_inversion_l with (1 := H); + reflexivity). Qed. -(** Multiplication and Opposite *) +(** ** Multiplication and Opposite *) Theorem Zopp_mult_distr_l : forall n m:Z, - (n * m) = - n * m. Proof. -intros x y; destruct x; destruct y; reflexivity. + intros x y; destruct x; destruct y; reflexivity. Qed. Theorem Zopp_mult_distr_r : forall n m:Z, - (n * m) = n * - m. -intros x y; rewrite (Zmult_comm x y); rewrite Zopp_mult_distr_l; - apply Zmult_comm. +Proof. + intros x y; rewrite (Zmult_comm x y); rewrite Zopp_mult_distr_l; + apply Zmult_comm. Qed. Lemma Zopp_mult_distr_l_reverse : forall n m:Z, - n * m = - (n * m). Proof. -intros x y; symmetry in |- *; apply Zopp_mult_distr_l. + intros x y; symmetry in |- *; apply Zopp_mult_distr_l. Qed. Theorem Zmult_opp_comm : forall n m:Z, - n * m = n * - m. -intros x y; rewrite Zopp_mult_distr_l_reverse; rewrite Zopp_mult_distr_r; - trivial with arith. +Proof. + intros x y; rewrite Zopp_mult_distr_l_reverse; rewrite Zopp_mult_distr_r; + trivial with arith. Qed. Theorem Zmult_opp_opp : forall n m:Z, - n * - m = n * m. Proof. -intros x y; destruct x; destruct y; reflexivity. + intros x y; destruct x; destruct y; reflexivity. Qed. Theorem Zopp_eq_mult_neg_1 : forall n:Z, - n = n * Zneg 1. -intro x; induction x; intros; rewrite Zmult_comm; auto with arith. +Proof. + intro x; induction x; intros; rewrite Zmult_comm; auto with arith. Qed. -(** Distributivity of multiplication over addition *) +(** ** Distributivity of multiplication over addition *) Lemma weak_Zmult_plus_distr_r : - forall (p:positive) (n m:Z), Zpos p * (n + m) = Zpos p * n + Zpos p * m. -Proof. -intros x y' z'; case y'; case z'; auto with arith; intros y z; - (simpl in |- *; rewrite Pmult_plus_distr_l; trivial with arith) || - (simpl in |- *; ElimPcompare z y; intros E0; rewrite E0; - [ rewrite (Pcompare_Eq_eq z y E0); rewrite (Pcompare_refl (x * y)); - trivial with arith - | cut ((x * z ?= x * y)%positive Eq = Lt); - [ intros E; rewrite E; rewrite Pmult_minus_distr_l; - [ trivial with arith | apply ZC2; assumption ] - | apply nat_of_P_lt_Lt_compare_complement_morphism; - do 2 rewrite nat_of_P_mult_morphism; elim (ZL4 x); - intros h H1; rewrite H1; apply mult_S_lt_compat_l; - exact (nat_of_P_lt_Lt_compare_morphism z y E0) ] - | cut ((x * z ?= x * y)%positive Eq = Gt); - [ intros E; rewrite E; rewrite Pmult_minus_distr_l; auto with arith - | apply nat_of_P_gt_Gt_compare_complement_morphism; unfold gt in |- *; - do 2 rewrite nat_of_P_mult_morphism; elim (ZL4 x); - intros h H1; rewrite H1; apply mult_S_lt_compat_l; - exact (nat_of_P_gt_Gt_compare_morphism z y E0) ] ]). + forall (p:positive) (n m:Z), Zpos p * (n + m) = Zpos p * n + Zpos p * m. +Proof. + intros x y' z'; case y'; case z'; auto with arith; intros y z; + (simpl in |- *; rewrite Pmult_plus_distr_l; trivial with arith) || + (simpl in |- *; ElimPcompare z y; intros E0; rewrite E0; + [ rewrite (Pcompare_Eq_eq z y E0); rewrite (Pcompare_refl (x * y)); + trivial with arith + | cut ((x * z ?= x * y)%positive Eq = Lt); + [ intros E; rewrite E; rewrite Pmult_minus_distr_l; + [ trivial with arith | apply ZC2; assumption ] + | apply nat_of_P_lt_Lt_compare_complement_morphism; + do 2 rewrite nat_of_P_mult_morphism; elim (ZL4 x); + intros h H1; rewrite H1; apply mult_S_lt_compat_l; + exact (nat_of_P_lt_Lt_compare_morphism z y E0) ] + | cut ((x * z ?= x * y)%positive Eq = Gt); + [ intros E; rewrite E; rewrite Pmult_minus_distr_l; auto with arith + | apply nat_of_P_gt_Gt_compare_complement_morphism; unfold gt in |- *; + do 2 rewrite nat_of_P_mult_morphism; elim (ZL4 x); + intros h H1; rewrite H1; apply mult_S_lt_compat_l; + exact (nat_of_P_gt_Gt_compare_morphism z y E0) ] ]). Qed. Theorem Zmult_plus_distr_r : forall n m p:Z, n * (m + p) = n * m + n * p. Proof. -intros x y z; case x; - [ auto with arith - | intros x'; apply weak_Zmult_plus_distr_r - | intros p; apply Zopp_inj; rewrite Zopp_plus_distr; - do 3 rewrite <- Zopp_mult_distr_l_reverse; rewrite Zopp_neg; - apply weak_Zmult_plus_distr_r ]. + intros x y z; case x; + [ auto with arith + | intros x'; apply weak_Zmult_plus_distr_r + | intros p; apply Zopp_inj; rewrite Zopp_plus_distr; + do 3 rewrite <- Zopp_mult_distr_l_reverse; rewrite Zopp_neg; + apply weak_Zmult_plus_distr_r ]. Qed. Theorem Zmult_plus_distr_l : forall n m p:Z, (n + m) * p = n * p + m * p. Proof. -intros n m p; rewrite Zmult_comm; rewrite Zmult_plus_distr_r; - do 2 rewrite (Zmult_comm p); trivial with arith. + intros n m p; rewrite Zmult_comm; rewrite Zmult_plus_distr_r; + do 2 rewrite (Zmult_comm p); trivial with arith. Qed. -(** Distributivity of multiplication over subtraction *) +(** ** Distributivity of multiplication over subtraction *) Lemma Zmult_minus_distr_r : forall n m p:Z, (n - m) * p = n * p - m * p. Proof. -intros x y z; unfold Zminus in |- *. -rewrite <- Zopp_mult_distr_l_reverse. -apply Zmult_plus_distr_l. + intros x y z; unfold Zminus in |- *. + rewrite <- Zopp_mult_distr_l_reverse. + apply Zmult_plus_distr_l. Qed. Lemma Zmult_minus_distr_l : forall n m p:Z, p * (n - m) = p * n - p * m. Proof. -intros x y z; rewrite (Zmult_comm z (x - y)). -rewrite (Zmult_comm z x). -rewrite (Zmult_comm z y). -apply Zmult_minus_distr_r. + intros x y z; rewrite (Zmult_comm z (x - y)). + rewrite (Zmult_comm z x). + rewrite (Zmult_comm z y). + apply Zmult_minus_distr_r. Qed. -(** Simplification of multiplication for non-zero integers *) +(** ** Simplification of multiplication for non-zero integers *) Lemma Zmult_reg_l : forall n m p:Z, p <> Z0 -> p * n = p * m -> n = m. Proof. -intros x y z H H0. -generalize (Zeq_minus _ _ H0). -intro. -apply Zminus_eq. -rewrite <- Zmult_minus_distr_l in H1. -clear H0; destruct (Zmult_integral _ _ H1). -contradiction. -trivial. + intros x y z H H0. + generalize (Zeq_minus _ _ H0). + intro. + apply Zminus_eq. + rewrite <- Zmult_minus_distr_l in H1. + clear H0; destruct (Zmult_integral _ _ H1). + contradiction. + trivial. Qed. Lemma Zmult_reg_r : forall n m p:Z, p <> Z0 -> n * p = m * p -> n = m. Proof. -intros x y z Hz. -rewrite (Zmult_comm x z). -rewrite (Zmult_comm y z). -intro; apply Zmult_reg_l with z; assumption. + intros x y z Hz. + rewrite (Zmult_comm x z). + rewrite (Zmult_comm y z). + intro; apply Zmult_reg_l with z; assumption. Qed. -(** Addition and multiplication by 2 *) +(** ** Addition and multiplication by 2 *) Lemma Zplus_diag_eq_mult_2 : forall n:Z, n + n = n * Zpos 2. Proof. -intros x; pattern x at 1 2 in |- *; rewrite <- (Zmult_1_r x); - rewrite <- Zmult_plus_distr_r; reflexivity. + intros x; pattern x at 1 2 in |- *; rewrite <- (Zmult_1_r x); + rewrite <- Zmult_plus_distr_r; reflexivity. Qed. -(** Multiplication and successor *) +(** ** Multiplication and successor *) Lemma Zmult_succ_r : forall n m:Z, n * Zsucc m = n * m + n. Proof. -intros n m; unfold Zsucc in |- *; rewrite Zmult_plus_distr_r; - rewrite (Zmult_comm n (Zpos 1)); rewrite Zmult_1_l; - trivial with arith. + intros n m; unfold Zsucc in |- *; rewrite Zmult_plus_distr_r; + rewrite (Zmult_comm n (Zpos 1)); rewrite Zmult_1_l; + trivial with arith. Qed. Lemma Zmult_succ_r_reverse : forall n m:Z, n * m + n = n * Zsucc m. Proof. -intros; symmetry in |- *; apply Zmult_succ_r. + intros; symmetry in |- *; apply Zmult_succ_r. Qed. Lemma Zmult_succ_l : forall n m:Z, Zsucc n * m = n * m + m. Proof. -intros n m; unfold Zsucc in |- *; rewrite Zmult_plus_distr_l; - rewrite Zmult_1_l; trivial with arith. + intros n m; unfold Zsucc in |- *; rewrite Zmult_plus_distr_l; + rewrite Zmult_1_l; trivial with arith. Qed. Lemma Zmult_succ_l_reverse : forall n m:Z, n * m + m = Zsucc n * m. Proof. -intros; symmetry in |- *; apply Zmult_succ_l. + intros; symmetry in |- *; apply Zmult_succ_l. Qed. -(** Misc redundant properties *) +(** ** Misc redundant properties *) Lemma Z_eq_mult : forall n m:Z, m = Z0 -> m * n = Z0. -intros x y H; rewrite H; auto with arith. +Proof. + intros x y H; rewrite H; auto with arith. Qed. + + (**********************************************************************) -(** Relating binary positive numbers and binary integers *) +(** * Relating binary positive numbers and binary integers *) Lemma Zpos_xI : forall p:positive, Zpos (xI p) = Zpos 2 * Zpos p + Zpos 1. Proof. -intro; apply refl_equal. + intro; apply refl_equal. Qed. Lemma Zpos_xO : forall p:positive, Zpos (xO p) = Zpos 2 * Zpos p. Proof. -intro; apply refl_equal. + intro; apply refl_equal. Qed. Lemma Zneg_xI : forall p:positive, Zneg (xI p) = Zpos 2 * Zneg p - Zpos 1. Proof. -intro; apply refl_equal. + intro; apply refl_equal. Qed. Lemma Zneg_xO : forall p:positive, Zneg (xO p) = Zpos 2 * Zneg p. Proof. -reflexivity. + reflexivity. Qed. Lemma Zpos_plus_distr : forall p q:positive, Zpos (p + q) = Zpos p + Zpos q. Proof. -intros p p'; destruct p; - [ destruct p' as [p0| p0| ] - | destruct p' as [p0| p0| ] - | destruct p' as [p| p| ] ]; reflexivity. + intros p p'; destruct p; + [ destruct p' as [p0| p0| ] + | destruct p' as [p0| p0| ] + | destruct p' as [p| p| ] ]; reflexivity. Qed. Lemma Zneg_plus_distr : forall p q:positive, Zneg (p + q) = Zneg p + Zneg q. Proof. -intros p p'; destruct p; - [ destruct p' as [p0| p0| ] - | destruct p' as [p0| p0| ] - | destruct p' as [p| p| ] ]; reflexivity. + intros p p'; destruct p; + [ destruct p' as [p0| p0| ] + | destruct p' as [p0| p0| ] + | destruct p' as [p| p| ] ]; reflexivity. Qed. (**********************************************************************) -(** Order relations *) +(** * Order relations *) Definition Zlt (x y:Z) := (x ?= y) = Lt. Definition Zgt (x y:Z) := (x ?= y) = Gt. @@ -1008,41 +1023,41 @@ Notation "x < y < z" := (x < y /\ y < z) : Z_scope. Notation "x < y <= z" := (x < y /\ y <= z) : Z_scope. (**********************************************************************) -(** Absolute value on integers *) +(** * 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 + | 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 + | Z0 => Z0 + | Zpos p => Zpos p + | Zneg p => Zpos p end. (**********************************************************************) -(** From [nat] to [Z] *) +(** * From [nat] to [Z] *) Definition Z_of_nat (x:nat) := match x with - | O => Z0 - | S y => Zpos (P_of_succ_nat y) + | 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 + | 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 + | N0 => Z0 + | Npos p => Zpos p end. |