| Binary Integers (Pierre Crégut, CNET, Lannion, France) |
Require Export BinPos.
Require Export Pnat.
Require Import BinNat.
Require Import Plus.
Require Import Mult.
| Binary integer numbers |
Inductive Z : Set :=
| Z0 : Z
| Zpos : positive -> Z
| Zneg : positive -> Z.
| Declare Scope Z_scope with Key Z |
Delimit Scope Z_scope with Z.
| Automatically open scope positive_scope for the constructors of Z |
Bind Scope Z_scope with Z.
Arguments Scope Zpos [positive_scope].
Arguments Scope Zneg [positive_scope].
| Subtraction of positive into Z |
Definition Zdouble_plus_one (x:Z) :=
match x with
| Z0 => Zpos 1
| Zpos p => Zpos (xI p)
| Zneg p => Zneg (Pdouble_minus_one p)
end.
Definition Zdouble_minus_one (x:Z) :=
match x with
| Z0 => Zneg 1
| Zneg p => Zneg (xI p)
| Zpos p => Zpos (Pdouble_minus_one p)
end.
Definition Zdouble (x:Z) :=
match x with
| Z0 => Z0
| Zpos p => Zpos (xO p)
| Zneg p => Zneg (xO p)
end.
Fixpoint ZPminus (x y:positive) {struct y} : Z :=
match x, y with
| xI x', xI y' => Zdouble (ZPminus x' y')
| xI x', xO y' => Zdouble_plus_one (ZPminus x' y')
| xI x', xH => Zpos (xO x')
| xO x', xI y' => Zdouble_minus_one (ZPminus x' y')
| xO x', xO y' => Zdouble (ZPminus x' y')
| xO x', xH => Zpos (Pdouble_minus_one x')
| xH, xI y' => Zneg (xO y')
| xH, xO y' => Zneg (Pdouble_minus_one y')
| xH, xH => Z0
end.
| Addition on integers |
Definition Zplus (x y:Z) :=
match x, y with
| Z0, y => y
| x, Z0 => x
| Zpos x', Zpos y' => Zpos (x' + y')
| Zpos x', Zneg y' =>
match (x' ?= y')%positive Eq with
| Eq => Z0
| Lt => Zneg (y' - x')
| Gt => Zpos (x' - y')
end
| Zneg x', Zpos y' =>
match (x' ?= y')%positive Eq with
| Eq => Z0
| Lt => Zpos (y' - x')
| Gt => Zneg (x' - y')
end
| Zneg x', Zneg y' => Zneg (x' + y')
end.
Infix "+" := Zplus : Z_scope.
| Opposite |
Definition Zopp (x:Z) :=
match x with
| Z0 => Z0
| Zpos x => Zneg x
| Zneg x => Zpos x
end.
Notation "- x" := (Zopp x) : Z_scope.
| Successor on integers |
Definition Zsucc (x:Z) := (x + Zpos 1)%Z.
| Predecessor on integers |
Definition Zpred (x:Z) := (x + Zneg 1)%Z.
| Subtraction on integers |
Definition Zminus (m n:Z) := (m + - n)%Z.
Infix "-" := Zminus : Z_scope.
| Multiplication on integers |
Definition Zmult (x y:Z) :=
match x, y with
| Z0, _ => Z0
| _, Z0 => Z0
| Zpos x', Zpos y' => Zpos (x' * y')
| Zpos x', Zneg y' => Zneg (x' * y')
| Zneg x', Zpos y' => Zneg (x' * y')
| Zneg x', Zneg y' => Zpos (x' * y')
end.
Infix "*" := Zmult : Z_scope.
| Comparison of integers |
Definition Zcompare (x y:Z) :=
match x, y with
| Z0, Z0 => Eq
| Z0, Zpos y' => Lt
| Z0, Zneg y' => Gt
| Zpos x', Z0 => Gt
| Zpos x', Zpos y' => (x' ?= y')%positive Eq
| Zpos x', Zneg y' => Gt
| Zneg x', Z0 => Lt
| Zneg x', Zpos y' => Lt
| Zneg x', Zneg y' => CompOpp ((x' ?= y')%positive Eq)
end.
Infix "?=" := Zcompare (at level 70, no associativity) : Z_scope.
Ltac elim_compare com1 com2 :=
case (Dcompare (com1 ?= com2)%Z);
[ idtac | let x := fresh "H" in
(intro x; case x; clear x) ].
| Sign function |
Definition Zsgn (z:Z) : Z :=
match z with
| Z0 => Z0
| Zpos p => Zpos 1
| Zneg p => Zneg 1
end.
| Direct, easier to handle variants of successor and addition |
Definition Zsucc' (x:Z) :=
match x with
| Z0 => Zpos 1
| Zpos x' => Zpos (Psucc x')
| Zneg x' => ZPminus 1 x'
end.
Definition Zpred' (x:Z) :=
match x with
| Z0 => Zneg 1
| Zpos x' => ZPminus x' 1
| Zneg x' => Zneg (Psucc x')
end.
Definition Zplus' (x y:Z) :=
match x, y with
| Z0, y => y
| x, Z0 => x
| Zpos x', Zpos y' => Zpos (x' + y')
| Zpos x', Zneg y' => ZPminus x' y'
| Zneg x', Zpos y' => ZPminus y' x'
| Zneg x', Zneg y' => Zneg (x' + y')
end.
Open Local Scope Z_scope.
| Inductive specification of Z |
Theorem Zind :
forall P:Z -> Prop,
P Z0 ->
(forall x:Z, P x -> P (Zsucc' x)) ->
(forall x:Z, P x -> P (Zpred' x)) -> forall n:Z, P n.
Proof.
intros P H0 Hs Hp z; destruct z.
assumption.
apply Pind with (P:= fun p => P (Zpos p)).
change (P (Zsucc' Z0)) in |- *; apply Hs; apply H0.
intro n; exact (Hs (Zpos n)).
apply Pind with (P:= fun p => P (Zneg p)).
change (P (Zpred' Z0)) in |- *; apply Hp; apply H0.
intro n; exact (Hp (Zneg n)).
Qed.
| Properties of opposite on binary integer numbers |
Theorem Zopp_neg : forall p:positive, - Zneg p = Zpos p.
Proof.
reflexivity.
Qed.
opp is involutive
|
Theorem Zopp_involutive : forall n:Z, - - n = n.
Proof.
intro x; destruct x; reflexivity.
Qed.
| Injectivity of the opposite |
Theorem Zopp_inj : forall n m:Z, - n = - m -> n = m.
Proof.
intros x y; case x; case y; simpl in |- *; intros;
[ trivial
| discriminate H
| discriminate H
| discriminate H
| simplify_eq H; intro E; rewrite E; trivial
| discriminate H
| discriminate H
| discriminate H
| simplify_eq H; intro E; rewrite E; trivial ].
Qed.
Lemma Zpred'_succ' : forall n:Z, Zpred' (Zsucc' n) = n.
Proof.
intro x; destruct x; simpl in |- *.
reflexivity.
destruct p; simpl in |- *; try rewrite Pdouble_minus_one_o_succ_eq_xI;
reflexivity.
destruct p; simpl in |- *; try rewrite Psucc_o_double_minus_one_eq_xO;
reflexivity.
Qed.
Lemma Zsucc'_discr : forall n:Z, n <> Zsucc' n.
Proof.
intro x; destruct x; simpl in |- *.
discriminate.
injection; apply Psucc_discr.
destruct p; simpl in |- *.
discriminate.
intro H; symmetry in H; injection H; apply double_moins_un_xO_discr.
discriminate.
Qed.
| Other properties of binary integer numbers |
Lemma ZL0 : 2%nat = (1 + 1)%nat.
Proof.
reflexivity.
Qed.
| Properties of the addition on integers |
| zero is left neutral for addition |
Theorem Zplus_0_l : forall n:Z, Z0 + n = n.
Proof.
intro x; destruct x; reflexivity.
Qed.
| zero is right neutral for addition |
Theorem Zplus_0_r : forall n:Z, n + Z0 = n.
Proof.
intro x; destruct x; reflexivity.
Qed.
| addition is commutative |
Theorem Zplus_comm : forall n m:Z, n + m = m + n.
Proof.
intro x; induction x as [| p| p]; intro y; destruct y as [| q| q];
simpl in |- *; try reflexivity.
rewrite Pplus_comm; reflexivity.
rewrite ZC4; destruct ((q ?= p)%positive Eq); reflexivity.
rewrite ZC4; destruct ((q ?= p)%positive Eq); reflexivity.
rewrite Pplus_comm; reflexivity.
Qed.
| opposite distributes over addition |
Theorem Zopp_plus_distr : forall n m:Z, - (n + m) = - n + - m.
Proof.
intro x; destruct x as [| p| p]; intro y; destruct y as [| q| q];
simpl in |- *; reflexivity || destruct ((p ?= q)%positive Eq);
reflexivity.
Qed.
| opposite is inverse for addition |
Theorem Zplus_opp_r : forall n:Z, n + - n = Z0.
Proof.
intro x; destruct x as [| p| p]; simpl in |- *;
[ reflexivity
| rewrite (Pcompare_refl p); reflexivity
| rewrite (Pcompare_refl p); reflexivity ].
Qed.
Theorem Zplus_opp_l : forall n:Z, - n + n = Z0.
Proof.
intro; rewrite Zplus_comm; apply Zplus_opp_r.
Qed.
Hint Local Resolve Zplus_0_l Zplus_0_r.
| addition is associative |
Lemma weak_assoc :
forall (p q:positive) (n:Z), Zpos p + (Zpos q + n) = Zpos p + Zpos q + n.
Proof.
intros x y z'; case z';
[ auto with arith
| intros z; simpl in |- *; rewrite Pplus_assoc; auto with arith
| intros z; simpl in |- *; ElimPcompare y z; intros E0; rewrite E0;
ElimPcompare (x + y)%positive z; intros E1; rewrite E1;
[ absurd ((x + y ?= z)%positive Eq = Eq);
[ 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);
[ 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);
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);
[ 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);
[ 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);
[ 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);
[ 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);
[ 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;
elim Pminus_mask_Gt with (1 := E1); intros i H2;
elim H1; intros H3 H4; elim H4; intros H5 H6;
elim H2; intros H7 H8; elim H8; intros H9 H10;
unfold Pminus in |- *; rewrite H3; rewrite H7;
cut ((x + k)%positive = i);
[ intros E; rewrite E; auto with arith
| apply (Pplus_reg_l z); rewrite (Pplus_comm x k); rewrite Pplus_assoc;
rewrite H5; rewrite H9; rewrite Pplus_comm;
trivial with arith ] ] ].
Qed.
Hint Local Resolve weak_assoc.
Theorem Zplus_assoc : forall n m p:Z, n + (m + p) = n + m + p.
Proof.
intros x y z; case x; case y; case z; auto with arith; intros;
[ rewrite (Zplus_comm (Zneg p0)); rewrite weak_assoc;
rewrite (Zplus_comm (Zpos p1 + Zneg p0)); rewrite weak_assoc;
rewrite (Zplus_comm (Zpos p1)); trivial with arith
| apply Zopp_inj; do 4 rewrite Zopp_plus_distr; do 2 rewrite Zopp_neg;
rewrite Zplus_comm; rewrite <- weak_assoc;
rewrite (Zplus_comm (- Zpos p1));
rewrite (Zplus_comm (Zpos p0 + - Zpos p1)); rewrite (weak_assoc p);
rewrite weak_assoc; rewrite (Zplus_comm (Zpos p0));
trivial with arith
| rewrite Zplus_comm; rewrite (Zplus_comm (Zpos p0) (Zpos p));
rewrite <- weak_assoc; rewrite Zplus_comm; rewrite (Zplus_comm (Zpos p0));
trivial with arith
| apply Zopp_inj; do 4 rewrite Zopp_plus_distr; do 2 rewrite Zopp_neg;
rewrite (Zplus_comm (- Zpos p0)); rewrite weak_assoc;
rewrite (Zplus_comm (Zpos p1 + - Zpos p0)); rewrite weak_assoc;
rewrite (Zplus_comm (Zpos p)); trivial with arith
| apply Zopp_inj; do 4 rewrite Zopp_plus_distr; do 2 rewrite Zopp_neg;
apply weak_assoc
| apply Zopp_inj; do 4 rewrite Zopp_plus_distr; do 2 rewrite Zopp_neg;
apply weak_assoc ].
Qed.
Lemma Zplus_assoc_reverse : forall n m p:Z, n + m + p = n + (m + p).
Proof.
intros; symmetry in |- *; apply Zplus_assoc.
Qed.
| Associativity mixed with commutativity |
Theorem Zplus_permute : forall n m p:Z, n + (m + p) = m + (n + p).
Proof.
intros n m p; rewrite Zplus_comm; rewrite <- Zplus_assoc;
rewrite (Zplus_comm p n); trivial with arith.
Qed.
| addition simplifies |
Theorem Zplus_reg_l : forall n m p:Z, n + m = n + p -> m = p.
intros n m p H; cut (- n + (n + m) = - n + (n + p));
[ do 2 rewrite Zplus_assoc; rewrite (Zplus_comm (- n) n);
rewrite Zplus_opp_r; simpl in |- *; trivial with arith
| rewrite H; trivial with arith ].
Qed.
| addition and successor permutes |
Lemma Zplus_succ_l : forall n m:Z, Zsucc n + m = Zsucc (n + m).
Proof.
intros x y; unfold Zsucc in |- *; rewrite (Zplus_comm (x + y));
rewrite Zplus_assoc; rewrite (Zplus_comm (Zpos 1));
trivial with arith.
Qed.
Lemma Zplus_succ_r : forall n m:Z, Zsucc (n + m) = n + Zsucc m.
Proof.
intros n m; unfold Zsucc in |- *; rewrite Zplus_assoc; trivial with arith.
Qed.
Lemma Zplus_succ_comm : forall n m:Z, Zsucc n + m = n + Zsucc m.
Proof.
unfold Zsucc in |- *; intros n m; rewrite <- Zplus_assoc;
rewrite (Zplus_comm (Zpos 1)); trivial with arith.
Qed.
| Misc properties, usually redundant or non natural |
Lemma Zplus_0_r_reverse : forall n:Z, n = n + Z0.
Proof.
symmetry in |- *; apply Zplus_0_r.
Qed.
Lemma Zplus_0_simpl_l : forall n m:Z, n + Z0 = m -> n = m.
Proof.
intros n m; rewrite Zplus_0_r; intro; assumption.
Qed.
Lemma Zplus_0_simpl_l_reverse : forall n m:Z, n = m + Z0 -> n = m.
Proof.
intros n m; rewrite Zplus_0_r; intro; assumption.
Qed.
Lemma Zplus_eq_compat : forall n m p q:Z, n = m -> p = q -> n + p = m + q.
Proof.
intros; rewrite H; rewrite H0; reflexivity.
Qed.
Lemma Zplus_opp_expand : forall n m p:Z, n + - m = n + - p + (p + - m).
Proof.
intros x y z.
rewrite <- (Zplus_assoc x).
rewrite (Zplus_assoc (- z)).
rewrite Zplus_opp_l.
reflexivity.
Qed.
| Properties of successor and predecessor on binary integer numbers |
Theorem Zsucc_discr : forall n:Z, n <> Zsucc n.
Proof.
intros n; cut (Z0 <> Zpos 1);
[ unfold not in |- *; intros H1 H2; apply H1; apply (Zplus_reg_l n);
rewrite Zplus_0_r; exact H2
| discriminate ].
Qed.
Theorem Zpos_succ_morphism :
forall p:positive, Zpos (Psucc p) = Zsucc (Zpos p).
Proof.
intro; rewrite Pplus_one_succ_r; unfold Zsucc in |- *; simpl in |- *;
trivial with arith.
Qed.
| successor and predecessor are inverse functions |
Theorem Zsucc_pred : forall n:Z, n = Zsucc (Zpred n).
Proof.
intros n; unfold Zsucc, Zpred in |- *; rewrite <- Zplus_assoc; simpl in |- *;
rewrite Zplus_0_r; trivial with arith.
Qed.
Hint Immediate Zsucc_pred: zarith.
Theorem Zpred_succ : forall n:Z, n = Zpred (Zsucc n).
Proof.
intros m; unfold Zpred, Zsucc in |- *; rewrite <- Zplus_assoc; simpl in |- *;
rewrite Zplus_comm; auto with arith.
Qed.
Theorem Zsucc_inj : forall n m:Z, Zsucc n = Zsucc m -> n = m.
Proof.
intros n m H.
change (Zneg 1 + Zpos 1 + n = Zneg 1 + Zpos 1 + m) in |- *;
do 2 rewrite <- Zplus_assoc; do 2 rewrite (Zplus_comm (Zpos 1));
unfold Zsucc in H; rewrite H; trivial with arith.
Qed.
| Misc properties, usually redundant or non natural |
Lemma Zsucc_eq_compat : forall n m:Z, n = m -> Zsucc n = Zsucc m.
Proof.
intros n m H; rewrite H; reflexivity.
Qed.
Lemma Zsucc_inj_contrapositive : forall n m:Z, n <> m -> Zsucc n <> Zsucc m.
Proof.
unfold not in |- *; intros n m H1 H2; apply H1; apply Zsucc_inj; assumption.
Qed.
| Properties of subtraction on binary integer numbers |
Lemma Zminus_0_r : forall n:Z, n - Z0 = n.
Proof.
intro; unfold Zminus in |- *; simpl in |- *; rewrite Zplus_0_r;
trivial with arith.
Qed.
Lemma Zminus_0_l_reverse : forall n:Z, n = n - Z0.
Proof.
intro; symmetry in |- *; apply Zminus_0_r.
Qed.
Lemma Zminus_diag : forall n:Z, n - n = Z0.
Proof.
intro; unfold Zminus in |- *; rewrite Zplus_opp_r; trivial with arith.
Qed.
Lemma Zminus_diag_reverse : forall n:Z, Z0 = n - n.
Proof.
intro; symmetry in |- *; apply Zminus_diag.
Qed.
Lemma Zplus_minus_eq : forall n m p:Z, n = m + p -> p = n - m.
Proof.
intros n m p H; unfold Zminus in |- *; apply (Zplus_reg_l m);
rewrite (Zplus_comm m (n + - m)); rewrite <- Zplus_assoc;
rewrite Zplus_opp_l; rewrite Zplus_0_r; rewrite H;
trivial with arith.
Qed.
Lemma Zminus_plus : forall n m:Z, n + m - n = m.
Proof.
intros n m; unfold Zminus in |- *; rewrite (Zplus_comm n m);
rewrite <- Zplus_assoc; rewrite Zplus_opp_r; apply Zplus_0_r.
Qed.
Lemma Zplus_minus : forall n m:Z, n + (m - n) = m.
Proof.
unfold Zminus in |- *; intros n m; rewrite Zplus_permute; rewrite Zplus_opp_r;
apply Zplus_0_r.
Qed.
Lemma Zminus_succ_l : forall n m:Z, Zsucc (n - m) = Zsucc n - m.
Proof.
intros n m; unfold Zminus, Zsucc in |- *; rewrite (Zplus_comm n (- m));
rewrite <- Zplus_assoc; apply Zplus_comm.
Qed.
Lemma Zminus_plus_simpl_l : forall n m p:Z, p + n - (p + m) = n - m.
Proof.
intros n m p; unfold Zminus in |- *; rewrite Zopp_plus_distr;
rewrite Zplus_assoc; rewrite (Zplus_comm p); rewrite <- (Zplus_assoc n p);
rewrite Zplus_opp_r; rewrite Zplus_0_r; trivial with arith.
Qed.
Lemma Zminus_plus_simpl_l_reverse : forall n m p:Z, n - m = p + n - (p + m).
Proof.
intros; symmetry in |- *; apply Zminus_plus_simpl_l.
Qed.
Lemma Zminus_plus_simpl_r : forall n m p:Z, n + p - (m + p) = n - m.
intros x y n.
unfold Zminus in |- *.
rewrite Zopp_plus_distr.
rewrite (Zplus_comm (- y) (- n)).
rewrite Zplus_assoc.
rewrite <- (Zplus_assoc x n (- n)).
rewrite (Zplus_opp_r n).
rewrite <- Zplus_0_r_reverse.
reflexivity.
Qed.
| Misc redundant properties |
Lemma Zeq_minus : forall n m:Z, n = m -> n - m = Z0.
Proof.
intros x y H; rewrite H; symmetry in |- *; apply Zminus_diag_reverse.
Qed.
Lemma Zminus_eq : forall n m:Z, n - m = Z0 -> n = m.
Proof.
intros x y H; rewrite <- (Zplus_minus y x); rewrite H; apply Zplus_0_r.
Qed.
| Properties of multiplication on binary integer numbers |
| One is neutral for multiplication |
Theorem Zmult_1_l : forall n:Z, Zpos 1 * n = n.
Proof.
intro x; destruct x; reflexivity.
Qed.
Theorem Zmult_1_r : forall n:Z, n * Zpos 1 = n.
Proof.
intro x; destruct x; simpl in |- *; try rewrite Pmult_1_r; reflexivity.
Qed.
| Zero property of multiplication |
Theorem Zmult_0_l : forall n:Z, Z0 * n = Z0.
Proof.
intro x; destruct x; reflexivity.
Qed.
Theorem Zmult_0_r : forall n:Z, n * Z0 = Z0.
Proof.
intro x; destruct x; reflexivity.
Qed.
Hint Local Resolve Zmult_0_l Zmult_0_r.
Lemma Zmult_0_r_reverse : forall n:Z, Z0 = n * Z0.
Proof.
intro x; destruct x; reflexivity.
Qed.
| Commutativity of multiplication |
Theorem Zmult_comm : forall n m:Z, n * m = m * n.
Proof.
intros x y; destruct x as [| p| p]; destruct y as [| q| q]; simpl in |- *;
try rewrite (Pmult_comm p q); reflexivity.
Qed.
| Associativity of multiplication |
Theorem Zmult_assoc : forall n m p:Z, n * (m * p) = n * m * p.
Proof.
intros x y z; destruct x; destruct y; destruct z; simpl in |- *;
try rewrite Pmult_assoc; reflexivity.
Qed.
Lemma Zmult_assoc_reverse : forall n m p:Z, n * m * p = n * (m * p).
Proof.
intros n m p; rewrite Zmult_assoc; trivial with arith.
Qed.
| Associativity mixed with commutativity |
Theorem Zmult_permute : forall n m p:Z, n * (m * p) = m * (n * p).
Proof.
intros x y z; rewrite (Zmult_assoc y x z); rewrite (Zmult_comm y x).
apply Zmult_assoc.
Qed.
| Z is integral |
Theorem Zmult_integral_l : forall n m:Z, n <> Z0 -> m * n = Z0 -> m = Z0.
Proof.
intros x y; destruct x as [| p| p].
intro H; absurd (Z0 = Z0); trivial.
intros _ H; destruct y as [| q| q]; reflexivity || discriminate.
intros _ H; destruct y as [| q| q]; reflexivity || discriminate.
Qed.
Theorem Zmult_integral : forall n m:Z, n * m = Z0 -> n = Z0 \/ m = Z0.
Proof.
intros x y; destruct x; destruct y; auto; simpl in |- *; intro H;
discriminate H.
Qed.
Lemma Zmult_1_inversion_l :
forall n m:Z, n * m = Zpos 1 -> n = Zpos 1 \/ n = Zneg 1.
Proof.
intros x y; destruct x as [| p| p]; intro; [ discriminate | left | right ];
(destruct y as [| q| q]; try discriminate; simpl in H; injection H; clear H;
intro H; rewrite Pmult_1_inversion_l with (1 := H);
reflexivity).
Qed.
| Multiplication and Opposite |
Theorem Zopp_mult_distr_l : forall n m:Z, - (n * m) = - n * m.
Proof.
intros x y; destruct x; destruct y; reflexivity.
Qed.
Theorem Zopp_mult_distr_r : forall n m:Z, - (n * m) = n * - m.
intros x y; rewrite (Zmult_comm x y); rewrite Zopp_mult_distr_l;
apply Zmult_comm.
Qed.
Lemma Zopp_mult_distr_l_reverse : forall n m:Z, - n * m = - (n * m).
Proof.
intros x y; symmetry in |- *; apply Zopp_mult_distr_l.
Qed.
Theorem Zmult_opp_comm : forall n m:Z, - n * m = n * - m.
intros x y; rewrite Zopp_mult_distr_l_reverse; rewrite Zopp_mult_distr_r;
trivial with arith.
Qed.
Theorem Zmult_opp_opp : forall n m:Z, - n * - m = n * m.
Proof.
intros x y; destruct x; destruct y; reflexivity.
Qed.
Theorem Zopp_eq_mult_neg_1 : forall n:Z, - n = n * Zneg 1.
intro x; induction x; intros; rewrite Zmult_comm; auto with arith.
Qed.
| Distributivity of multiplication over addition |
Lemma weak_Zmult_plus_distr_r :
forall (p:positive) (n m:Z), Zpos p * (n + m) = Zpos p * n + Zpos p * m.
Proof.
intros x y' z'; case y'; case z'; auto with arith; intros y z;
(simpl in |- *; rewrite Pmult_plus_distr_l; trivial with arith) ||
(simpl in |- *; ElimPcompare z y; intros E0; rewrite E0;
[ rewrite (Pcompare_Eq_eq z y E0); rewrite (Pcompare_refl (x * y));
trivial with arith
| cut ((x * z ?= x * y)%positive Eq = Lt);
[ intros E; rewrite E; rewrite Pmult_minus_distr_l;
[ trivial with arith | apply ZC2; assumption ]
| apply nat_of_P_lt_Lt_compare_complement_morphism;
do 2 rewrite nat_of_P_mult_morphism; elim (ZL4 x);
intros h H1; rewrite H1; apply mult_S_lt_compat_l;
exact (nat_of_P_lt_Lt_compare_morphism z y E0) ]
| cut ((x * z ?= x * y)%positive Eq = Gt);
[ intros E; rewrite E; rewrite Pmult_minus_distr_l; auto with arith
| apply nat_of_P_gt_Gt_compare_complement_morphism; unfold gt in |- *;
do 2 rewrite nat_of_P_mult_morphism; elim (ZL4 x);
intros h H1; rewrite H1; apply mult_S_lt_compat_l;
exact (nat_of_P_gt_Gt_compare_morphism z y E0) ] ]).
Qed.
Theorem Zmult_plus_distr_r : forall n m p:Z, n * (m + p) = n * m + n * p.
Proof.
intros x y z; case x;
[ auto with arith
| intros x'; apply weak_Zmult_plus_distr_r
| intros p; apply Zopp_inj; rewrite Zopp_plus_distr;
do 3 rewrite <- Zopp_mult_distr_l_reverse; rewrite Zopp_neg;
apply weak_Zmult_plus_distr_r ].
Qed.
Theorem Zmult_plus_distr_l : forall n m p:Z, (n + m) * p = n * p + m * p.
Proof.
intros n m p; rewrite Zmult_comm; rewrite Zmult_plus_distr_r;
do 2 rewrite (Zmult_comm p); trivial with arith.
Qed.
| Distributivity of multiplication over subtraction |
Lemma Zmult_minus_distr_r : forall n m p:Z, (n - m) * p = n * p - m * p.
Proof.
intros x y z; unfold Zminus in |- *.
rewrite <- Zopp_mult_distr_l_reverse.
apply Zmult_plus_distr_l.
Qed.
Lemma Zmult_minus_distr_l : forall n m p:Z, p * (n - m) = p * n - p * m.
Proof.
intros x y z; rewrite (Zmult_comm z (x - y)).
rewrite (Zmult_comm z x).
rewrite (Zmult_comm z y).
apply Zmult_minus_distr_r.
Qed.
| Simplification of multiplication for non-zero integers |
Lemma Zmult_reg_l : forall n m p:Z, p <> Z0 -> p * n = p * m -> n = m.
Proof.
intros x y z H H0.
generalize (Zeq_minus _ _ H0).
intro.
apply Zminus_eq.
rewrite <- Zmult_minus_distr_l in H1.
clear H0; destruct (Zmult_integral _ _ H1).
contradiction.
trivial.
Qed.
Lemma Zmult_reg_r : forall n m p:Z, p <> Z0 -> n * p = m * p -> n = m.
Proof.
intros x y z Hz.
rewrite (Zmult_comm x z).
rewrite (Zmult_comm y z).
intro; apply Zmult_reg_l with z; assumption.
Qed.
| Addition and multiplication by 2 |
Lemma Zplus_diag_eq_mult_2 : forall n:Z, n + n = n * Zpos 2.
Proof.
intros x; pattern x at 1 2 in |- *; rewrite <- (Zmult_1_r x);
rewrite <- Zmult_plus_distr_r; reflexivity.
Qed.
| Multiplication and successor |
Lemma Zmult_succ_r : forall n m:Z, n * Zsucc m = n * m + n.
Proof.
intros n m; unfold Zsucc in |- *; rewrite Zmult_plus_distr_r;
rewrite (Zmult_comm n (Zpos 1)); rewrite Zmult_1_l;
trivial with arith.
Qed.
Lemma Zmult_succ_r_reverse : forall n m:Z, n * m + n = n * Zsucc m.
Proof.
intros; symmetry in |- *; apply Zmult_succ_r.
Qed.
Lemma Zmult_succ_l : forall n m:Z, Zsucc n * m = n * m + m.
Proof.
intros n m; unfold Zsucc in |- *; rewrite Zmult_plus_distr_l;
rewrite Zmult_1_l; trivial with arith.
Qed.
Lemma Zmult_succ_l_reverse : forall n m:Z, n * m + m = Zsucc n * m.
Proof.
intros; symmetry in |- *; apply Zmult_succ_l.
Qed.
| Misc redundant properties |
Lemma Z_eq_mult : forall n m:Z, m = Z0 -> m * n = Z0.
intros x y H; rewrite H; auto with arith.
Qed.
| Relating binary positive numbers and binary integers |
Lemma Zpos_xI : forall p:positive, Zpos (xI p) = Zpos 2 * Zpos p + Zpos 1.
Proof.
intro; apply refl_equal.
Qed.
Lemma Zpos_xO : forall p:positive, Zpos (xO p) = Zpos 2 * Zpos p.
Proof.
intro; apply refl_equal.
Qed.
Lemma Zneg_xI : forall p:positive, Zneg (xI p) = Zpos 2 * Zneg p - Zpos 1.
Proof.
intro; apply refl_equal.
Qed.
Lemma Zneg_xO : forall p:positive, Zneg (xO p) = Zpos 2 * Zneg p.
Proof.
reflexivity.
Qed.
Lemma Zpos_plus_distr : forall p q:positive, Zpos (p + q) = Zpos p + Zpos q.
Proof.
intros p p'; destruct p;
[ destruct p' as [p0| p0| ]
| destruct p' as [p0| p0| ]
| destruct p' as [p| p| ] ]; reflexivity.
Qed.
Lemma Zneg_plus_distr : forall p q:positive, Zneg (p + q) = Zneg p + Zneg q.
Proof.
intros p p'; destruct p;
[ destruct p' as [p0| p0| ]
| destruct p' as [p0| p0| ]
| destruct p' as [p| p| ] ]; reflexivity.
Qed.
| Order relations |
Definition Zlt (x y:Z) := (x ?= y) = Lt.
Definition Zgt (x y:Z) := (x ?= y) = Gt.
Definition Zle (x y:Z) := (x ?= y) <> Gt.
Definition Zge (x y:Z) := (x ?= y) <> Lt.
Definition Zne (x y:Z) := x <> y.
Infix "<=" := Zle : Z_scope.
Infix "<" := Zlt : Z_scope.
Infix ">=" := Zge : Z_scope.
Infix ">" := Zgt : Z_scope.
Notation "x <= y <= z" := (x <= y /\ y <= z) : Z_scope.
Notation "x <= y < z" := (x <= y /\ y < z) : Z_scope.
Notation "x < y < z" := (x < y /\ y < z) : Z_scope.
Notation "x < y <= z" := (x < y /\ y <= z) : Z_scope.
| Absolute value on integers |
Definition Zabs_nat (x:Z) : nat :=
match x with
| Z0 => 0%nat
| Zpos p => nat_of_P p
| Zneg p => nat_of_P p
end.
Definition Zabs (z:Z) : Z :=
match z with
| Z0 => Z0
| Zpos p => Zpos p
| Zneg p => Zpos p
end.
From nat to Z
|
Definition Z_of_nat (x:nat) :=
match x with
| O => Z0
| S y => Zpos (P_of_succ_nat y)
end.
Require Import BinNat.
Definition Zabs_N (z:Z) :=
match z with
| Z0 => 0%N
| Zpos p => Npos p
| Zneg p => Npos p
end.
Definition Z_of_N (x:N) := match x with
| N0 => Z0
| Npos p => Zpos p
end.