(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(*i $Id: BinInt.v 8883 2006-05-31 21:56:37Z letouzey $ i*)

(***********************************************************)
(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
(***********************************************************)

Require Export BinPos.
Require Export Pnat.
Require Import BinNat.
Require Import Plus.
Require Import Mult.

Unset Boxed Definitions.
(**********************************************************************)
(** Binary integer numbers *)

Inductive Z : Set :=
  | Z0 : Z
  | Zpos : positive -> Z
  | Zneg : positive -> Z.

(** Declare Scope Z_scope with Key Z *)
Delimit Scope Z_scope with Z.

(** Automatically open scope positive_scope for the constructors of Z *)
Bind Scope Z_scope with Z.
Arguments Scope Zpos [positive_scope].
Arguments Scope Zneg [positive_scope].

(** Subtraction of positive into Z *)

Definition Zdouble_plus_one (x:Z) :=
  match x with
  | Z0 => Zpos 1
  | Zpos p => Zpos (xI p)
  | Zneg p => Zneg (Pdouble_minus_one p)
  end.

Definition Zdouble_minus_one (x:Z) :=
  match x with
  | Z0 => Zneg 1
  | Zneg p => Zneg (xI p)
  | Zpos p => Zpos (Pdouble_minus_one p)
  end.

Definition Zdouble (x:Z) :=
  match x with
  | Z0 => Z0
  | Zpos p => Zpos (xO p)
  | Zneg p => Zneg (xO p)
  end.

Fixpoint ZPminus (x y:positive) {struct y} : Z :=
  match x, y with
  | xI x', xI y' => Zdouble (ZPminus x' y')
  | xI x', xO y' => Zdouble_plus_one (ZPminus x' y')
  | xI x', xH => Zpos (xO x')
  | xO x', xI y' => Zdouble_minus_one (ZPminus x' y')
  | xO x', xO y' => Zdouble (ZPminus x' y')
  | xO x', xH => Zpos (Pdouble_minus_one x')
  | xH, xI y' => Zneg (xO y')
  | xH, xO y' => Zneg (Pdouble_minus_one y')
  | xH, xH => Z0
  end.

(** Addition on integers *)

Definition Zplus (x y:Z) :=
  match x, y with
  | Z0, y => y
  | x, Z0 => x
  | Zpos x', Zpos y' => Zpos (x' + y')
  | Zpos x', Zneg y' =>
      match (x' ?= y')%positive Eq with
      | Eq => Z0
      | Lt => Zneg (y' - x')
      | Gt => Zpos (x' - y')
      end
  | Zneg x', Zpos y' =>
      match (x' ?= y')%positive Eq with
      | Eq => Z0
      | Lt => Zpos (y' - x')
      | Gt => Zneg (x' - y')
      end
  | Zneg x', Zneg y' => Zneg (x' + y')
  end.

Infix "+" := Zplus : Z_scope.

(** Opposite *)

Definition Zopp (x:Z) :=
  match x with
  | Z0 => Z0
  | Zpos x => Zneg x
  | Zneg x => Zpos x
  end.

Notation "- x" := (Zopp x) : Z_scope.

(** Successor on integers *)

Definition Zsucc (x:Z) := (x + Zpos 1)%Z.

(** Predecessor on integers *)

Definition Zpred (x:Z) := (x + Zneg 1)%Z.

(** Subtraction on integers *)

Definition Zminus (m n:Z) := (m + - n)%Z.

Infix "-" := Zminus : Z_scope.

(** Multiplication on integers *)

Definition Zmult (x y:Z) :=
  match x, y with
  | Z0, _ => Z0
  | _, Z0 => Z0
  | Zpos x', Zpos y' => Zpos (x' * y')
  | Zpos x', Zneg y' => Zneg (x' * y')
  | Zneg x', Zpos y' => Zneg (x' * y')
  | Zneg x', Zneg y' => Zpos (x' * y')
  end.

Infix "*" := Zmult : Z_scope.

(** Comparison of integers *)

Definition Zcompare (x y:Z) :=
  match x, y with
  | Z0, Z0 => Eq
  | Z0, Zpos y' => Lt
  | Z0, Zneg y' => Gt
  | Zpos x', Z0 => Gt
  | Zpos x', Zpos y' => (x' ?= y')%positive Eq
  | Zpos x', Zneg y' => Gt
  | Zneg x', Z0 => Lt
  | Zneg x', Zpos y' => Lt
  | Zneg x', Zneg y' => CompOpp ((x' ?= y')%positive Eq)
  end.

Infix "?=" := Zcompare (at level 70, no associativity) : Z_scope.

Ltac elim_compare com1 com2 :=
  case (Dcompare (com1 ?= com2)%Z);
   [ idtac | let x := fresh "H" in
             (intro x; case x; clear x) ].

(** Sign function *)

Definition Zsgn (z:Z) : Z :=
  match z with
  | Z0 => Z0
  | Zpos p => Zpos 1
  | Zneg p => Zneg 1
  end.

(** Direct, easier to handle variants of successor and addition *)

Definition Zsucc' (x:Z) :=
  match x with
  | Z0 => Zpos 1
  | Zpos x' => Zpos (Psucc x')
  | Zneg x' => ZPminus 1 x'
  end.

Definition Zpred' (x:Z) :=
  match x with
  | Z0 => Zneg 1
  | Zpos x' => ZPminus x' 1
  | Zneg x' => Zneg (Psucc x')
  end.

Definition Zplus' (x y:Z) :=
  match x, y with
  | Z0, y => y
  | x, Z0 => x
  | Zpos x', Zpos y' => Zpos (x' + y')
  | Zpos x', Zneg y' => ZPminus x' y'
  | Zneg x', Zpos y' => ZPminus y' x'
  | Zneg x', Zneg y' => Zneg (x' + y')
  end.

Open Local Scope Z_scope.

(**********************************************************************)
(** Inductive specification of Z *)

Theorem Zind :
 forall P:Z -> Prop,
   P Z0 ->
   (forall x:Z, P x -> P (Zsucc' x)) ->
   (forall x:Z, P x -> P (Zpred' x)) -> forall n:Z, P n.
Proof.
intros P H0 Hs Hp z; destruct z.
  assumption.
  apply Pind with (P := fun p => P (Zpos p)).
    change (P (Zsucc' Z0)) in |- *; apply Hs; apply H0.
    intro n; exact (Hs (Zpos n)).
  apply Pind with (P := fun p => P (Zneg p)).
    change (P (Zpred' Z0)) in |- *; apply Hp; apply H0.
    intro n; exact (Hp (Zneg n)).
Qed.

(**********************************************************************)
(** Properties of opposite on binary integer numbers *)

Theorem Zopp_neg : forall p:positive, - Zneg p = Zpos p.
Proof.
reflexivity.
Qed.

(** [opp] is involutive *)

Theorem Zopp_involutive : forall n:Z, - - n = n.
Proof.
intro x; destruct x; reflexivity.
Qed.

(** Injectivity of the opposite *)

Theorem Zopp_inj : forall n m:Z, - n = - m -> n = m.
Proof.
intros x y; case x; case y; simpl in |- *; intros;
 [ trivial
 | discriminate H
 | discriminate H
 | discriminate H
 | simplify_eq H; intro E; rewrite E; trivial
 | discriminate H
 | discriminate H
 | discriminate H
 | simplify_eq H; intro E; rewrite E; trivial ].
Qed.

(**********************************************************************)
(* Properties of the direct definition of successor and predecessor *)

Lemma Zpred'_succ' : forall n:Z, Zpred' (Zsucc' n) = n.
Proof.
intro x; destruct x; simpl in |- *.
  reflexivity.
destruct p; simpl in |- *; try rewrite Pdouble_minus_one_o_succ_eq_xI;
 reflexivity.
destruct p; simpl in |- *; try rewrite Psucc_o_double_minus_one_eq_xO;
 reflexivity.
Qed.

Lemma Zsucc'_discr : forall n:Z, n <> Zsucc' n.
Proof.
intro x; destruct x; simpl in |- *.
  discriminate.
  injection; apply Psucc_discr.
  destruct p; simpl in |- *.
    discriminate.
    intro H; symmetry  in H; injection H; apply double_moins_un_xO_discr.
    discriminate.
Qed.

(**********************************************************************)
(** Other properties of binary integer numbers *)

Lemma ZL0 : 2%nat = (1 + 1)%nat.
Proof.
reflexivity.
Qed.

(**********************************************************************)
(** Properties of the addition on integers *)

(** zero is left neutral for addition *)

Theorem Zplus_0_l : forall n:Z, Z0 + n = n.
Proof.
intro x; destruct x; reflexivity.
Qed.

(** zero is right neutral for addition *)

Theorem Zplus_0_r : forall n:Z, n + Z0 = n.
Proof.
intro x; destruct x; reflexivity.
Qed.

(** addition is commutative *)

Theorem Zplus_comm : forall n m:Z, n + m = m + n.
Proof.
intro x; induction x as [| p| p]; intro y; destruct y as [| q| q];
 simpl in |- *; try reflexivity.
  rewrite Pplus_comm; reflexivity.
  rewrite ZC4; destruct ((q ?= p)%positive Eq); reflexivity.
  rewrite ZC4; destruct ((q ?= p)%positive Eq); reflexivity.
  rewrite Pplus_comm; reflexivity.
Qed.

(** opposite distributes over addition *)

Theorem Zopp_plus_distr : forall n m:Z, - (n + m) = - n + - m.
Proof.
intro x; destruct x as [| p| p]; intro y; destruct y as [| q| q];
 simpl in |- *; reflexivity || destruct ((p ?= q)%positive Eq); 
 reflexivity.
Qed.

(** opposite is inverse for addition *)

Theorem Zplus_opp_r : forall n:Z, n + - n = Z0.
Proof.
intro x; destruct x as [| p| p]; simpl in |- *;
 [ reflexivity
 | rewrite (Pcompare_refl p); reflexivity
 | rewrite (Pcompare_refl p); reflexivity ].
Qed.

Theorem Zplus_opp_l : forall n:Z, - n + n = Z0.
Proof.
intro; rewrite Zplus_comm; apply Zplus_opp_r.
Qed.

Hint Local Resolve Zplus_0_l Zplus_0_r.

(** addition is associative *)

Lemma weak_assoc :
 forall (p q:positive) (n:Z), Zpos p + (Zpos q + n) = Zpos p + Zpos q + n.
Proof.
intros x y z'; case z';
 [ auto with arith
 | intros z; simpl in |- *; rewrite Pplus_assoc; auto with arith
 | intros z; simpl in |- *; ElimPcompare y z; intros E0; rewrite E0;
    ElimPcompare (x + y)%positive z; intros E1; rewrite E1;
    [ absurd ((x + y ?= z)%positive Eq = Eq);
       [  (* Case 1 *)
          rewrite nat_of_P_gt_Gt_compare_complement_morphism;
          [ discriminate
          | rewrite nat_of_P_plus_morphism; rewrite (Pcompare_Eq_eq y z E0);
             elim (ZL4 x); intros k E2; rewrite E2; 
             simpl in |- *; unfold gt, lt in |- *; 
             apply le_n_S; apply le_plus_r ]
       | assumption ]
    | absurd ((x + y ?= z)%positive Eq = Lt);
       [  (* Case 2 *)
          rewrite nat_of_P_gt_Gt_compare_complement_morphism;
          [ discriminate
          | rewrite nat_of_P_plus_morphism; rewrite (Pcompare_Eq_eq y z E0);
             elim (ZL4 x); intros k E2; rewrite E2; 
             simpl in |- *; unfold gt, lt in |- *; 
             apply le_n_S; apply le_plus_r ]
       | assumption ]
    | rewrite (Pcompare_Eq_eq y z E0);
        (* Case 3 *)
       elim (Pminus_mask_Gt (x + z) z);
       [ intros t H; elim H; intros H1 H2; elim H2; intros H3 H4;
          unfold Pminus in |- *; rewrite H1; cut (x = t);
          [ intros E; rewrite E; auto with arith
          | apply Pplus_reg_r with (r := z); rewrite <- H3;
             rewrite Pplus_comm; trivial with arith ]
       | pattern z at 1 in |- *; rewrite <- (Pcompare_Eq_eq y z E0);
          assumption ]
    | elim (Pminus_mask_Gt z y);
       [  (* Case 4 *)
          intros k H; elim H; intros H1 H2; elim H2; intros H3 H4;
          unfold Pminus at 1 in |- *; rewrite H1; cut (x = k);
          [ intros E; rewrite E; rewrite (Pcompare_refl k);
             trivial with arith
          | apply Pplus_reg_r with (r := y); rewrite (Pplus_comm k y);
             rewrite H3; apply Pcompare_Eq_eq; assumption ]
       | apply ZC2; assumption ]
    | elim (Pminus_mask_Gt z y);
       [  (* Case 5 *)
          intros k H; elim H; intros H1 H2; elim H2; intros H3 H4;
          unfold Pminus at 1 3 5 in |- *; rewrite H1;
          cut ((x ?= k)%positive Eq = Lt);
          [ intros E2; rewrite E2; elim (Pminus_mask_Gt k x);
             [ intros i H5; elim H5; intros H6 H7; elim H7; intros H8 H9;
                elim (Pminus_mask_Gt z (x + y));
                [ intros j H10; elim H10; intros H11 H12; elim H12;
                   intros H13 H14; unfold Pminus in |- *; 
                   rewrite H6; rewrite H11; cut (i = j);
                   [ intros E; rewrite E; auto with arith
                   | apply (Pplus_reg_l (x + y)); rewrite H13;
                      rewrite (Pplus_comm x y); rewrite <- Pplus_assoc;
                      rewrite H8; assumption ]
                | apply ZC2; assumption ]
             | apply ZC2; assumption ]
          | apply nat_of_P_lt_Lt_compare_complement_morphism;
             apply plus_lt_reg_l with (p := nat_of_P y);
             do 2 rewrite <- nat_of_P_plus_morphism;
             apply nat_of_P_lt_Lt_compare_morphism; 
             rewrite H3; rewrite Pplus_comm; assumption ]
       | apply ZC2; assumption ]
    | elim (Pminus_mask_Gt z y);
       [  (* Case 6 *)
          intros k H; elim H; intros H1 H2; elim H2; intros H3 H4;
          elim (Pminus_mask_Gt (x + y) z);
          [ intros i H5; elim H5; intros H6 H7; elim H7; intros H8 H9;
             unfold Pminus in |- *; rewrite H1; rewrite H6;
             cut ((x ?= k)%positive Eq = Gt);
             [ intros H10; elim (Pminus_mask_Gt x k H10); intros j H11;
                elim H11; intros H12 H13; elim H13; 
                intros H14 H15; rewrite H10; rewrite H12; 
                cut (i = j);
                [ intros H16; rewrite H16; auto with arith
                | apply (Pplus_reg_l (z + k)); rewrite <- (Pplus_assoc z k j);
                   rewrite H14; rewrite (Pplus_comm z k);
                   rewrite <- Pplus_assoc; rewrite H8;
                   rewrite (Pplus_comm x y); rewrite Pplus_assoc;
                   rewrite (Pplus_comm k y); rewrite H3; 
                   trivial with arith ]
             | apply nat_of_P_gt_Gt_compare_complement_morphism;
                unfold lt, gt in |- *;
                apply plus_lt_reg_l with (p := nat_of_P y);
                do 2 rewrite <- nat_of_P_plus_morphism;
                apply nat_of_P_lt_Lt_compare_morphism; 
                rewrite H3; rewrite Pplus_comm; apply ZC1; 
                assumption ]
          | assumption ]
       | apply ZC2; assumption ]
    | absurd ((x + y ?= z)%positive Eq = Eq);
       [  (* Case 7 *)
          rewrite nat_of_P_gt_Gt_compare_complement_morphism;
          [ discriminate
          | rewrite nat_of_P_plus_morphism; unfold gt in |- *;
             apply lt_le_trans with (m := nat_of_P y);
             [ apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; assumption
             | apply le_plus_r ] ]
       | assumption ]
    | absurd ((x + y ?= z)%positive Eq = Lt);
       [  (* Case 8 *)
          rewrite nat_of_P_gt_Gt_compare_complement_morphism;
          [ discriminate
          | unfold gt in |- *; apply lt_le_trans with (m := nat_of_P y);
             [ exact (nat_of_P_gt_Gt_compare_morphism y z E0)
             | rewrite nat_of_P_plus_morphism; apply le_plus_r ] ]
       | assumption ]
    | elim Pminus_mask_Gt with (1 := E0); intros k H1;
        (* Case 9 *)
       elim Pminus_mask_Gt with (1 := E1); intros i H2; 
       elim H1; intros H3 H4; elim H4; intros H5 H6; 
       elim H2; intros H7 H8; elim H8; intros H9 H10; 
       unfold Pminus in |- *; rewrite H3; rewrite H7;
       cut ((x + k)%positive = i);
       [ intros E; rewrite E; auto with arith
       | apply (Pplus_reg_l z); rewrite (Pplus_comm x k); rewrite Pplus_assoc;
          rewrite H5; rewrite H9; rewrite Pplus_comm; 
          trivial with arith ] ] ].
Qed.

Hint Local Resolve weak_assoc.

Theorem Zplus_assoc : forall n m p:Z, n + (m + p) = n + m + p.
Proof.
intros x y z; case x; case y; case z; auto with arith; intros;
 [ rewrite (Zplus_comm (Zneg p0)); rewrite weak_assoc;
    rewrite (Zplus_comm (Zpos p1 + Zneg p0)); rewrite weak_assoc;
    rewrite (Zplus_comm (Zpos p1)); trivial with arith
 | apply Zopp_inj; do 4 rewrite Zopp_plus_distr; do 2 rewrite Zopp_neg;
    rewrite Zplus_comm; rewrite <- weak_assoc;
    rewrite (Zplus_comm (- Zpos p1));
    rewrite (Zplus_comm (Zpos p0 + - Zpos p1)); rewrite (weak_assoc p);
    rewrite weak_assoc; rewrite (Zplus_comm (Zpos p0)); 
    trivial with arith
 | rewrite Zplus_comm; rewrite (Zplus_comm (Zpos p0) (Zpos p));
    rewrite <- weak_assoc; rewrite Zplus_comm; rewrite (Zplus_comm (Zpos p0));
    trivial with arith
 | apply Zopp_inj; do 4 rewrite Zopp_plus_distr; do 2 rewrite Zopp_neg;
    rewrite (Zplus_comm (- Zpos p0)); rewrite weak_assoc;
    rewrite (Zplus_comm (Zpos p1 + - Zpos p0)); rewrite weak_assoc;
    rewrite (Zplus_comm (Zpos p)); trivial with arith
 | apply Zopp_inj; do 4 rewrite Zopp_plus_distr; do 2 rewrite Zopp_neg;
    apply weak_assoc
 | apply Zopp_inj; do 4 rewrite Zopp_plus_distr; do 2 rewrite Zopp_neg;
    apply weak_assoc ].
Qed.


Lemma Zplus_assoc_reverse : forall n m p:Z, n + m + p = n + (m + p).
Proof.
intros; symmetry  in |- *; apply Zplus_assoc.
Qed.

(** Associativity mixed with commutativity *)

Theorem Zplus_permute : forall n m p:Z, n + (m + p) = m + (n + p).
Proof.
intros n m p; rewrite Zplus_comm; rewrite <- Zplus_assoc;
 rewrite (Zplus_comm p n); trivial with arith.
Qed.

(** addition simplifies *)

Theorem Zplus_reg_l : forall n m p:Z, n + m = n + p -> m = p.
intros n m p H; cut (- n + (n + m) = - n + (n + p));
 [ do 2 rewrite Zplus_assoc; rewrite (Zplus_comm (- n) n);
    rewrite Zplus_opp_r; simpl in |- *; trivial with arith
 | rewrite H; trivial with arith ].
Qed.

(** addition and successor permutes *)

Lemma Zplus_succ_l : forall n m:Z, Zsucc n + m = Zsucc (n + m).
Proof.
intros x y; unfold Zsucc in |- *; rewrite (Zplus_comm (x + y));
 rewrite Zplus_assoc; rewrite (Zplus_comm (Zpos 1)); 
 trivial with arith.
Qed.

Lemma Zplus_succ_r : forall n m:Z, Zsucc (n + m) = n + Zsucc m.
Proof.
intros n m; unfold Zsucc in |- *; rewrite Zplus_assoc; trivial with arith.
Qed.

Lemma Zplus_succ_comm : forall n m:Z, Zsucc n + m = n + Zsucc m.
Proof.
unfold Zsucc in |- *; intros n m; rewrite <- Zplus_assoc;
 rewrite (Zplus_comm (Zpos 1)); trivial with arith.
Qed.

(** Misc properties, usually redundant or non natural *)

Lemma Zplus_0_r_reverse : forall n:Z, n = n + Z0.
Proof.
symmetry  in |- *; apply Zplus_0_r.
Qed.

Lemma Zplus_0_simpl_l : forall n m:Z, n + Z0 = m -> n = m.
Proof.
intros n m; rewrite Zplus_0_r; intro; assumption.
Qed.

Lemma Zplus_0_simpl_l_reverse : forall n m:Z, n = m + Z0 -> n = m.
Proof.
intros n m; rewrite Zplus_0_r; intro; assumption.
Qed.

Lemma Zplus_eq_compat : forall n m p q:Z, n = m -> p = q -> n + p = m + q.
Proof.
intros; rewrite H; rewrite H0; reflexivity.
Qed.

Lemma Zplus_opp_expand : forall n m p:Z, n + - m = n + - p + (p + - m).
Proof.
intros x y z.
rewrite <- (Zplus_assoc x).
rewrite (Zplus_assoc (- z)).
rewrite Zplus_opp_l.
reflexivity.
Qed.

(**********************************************************************)
(** Properties of successor and predecessor on binary integer numbers *)

Theorem Zsucc_discr : forall n:Z, n <> Zsucc n.
Proof.
intros n; cut (Z0 <> Zpos 1);
 [ unfold not in |- *; intros H1 H2; apply H1; apply (Zplus_reg_l n);
    rewrite Zplus_0_r; exact H2
 | discriminate ].
Qed.

Theorem Zpos_succ_morphism :
 forall p:positive, Zpos (Psucc p) = Zsucc (Zpos p).
Proof.
intro; rewrite Pplus_one_succ_r; unfold Zsucc in |- *; simpl in |- *;
 trivial with arith.
Qed.

(** successor and predecessor are inverse functions *)

Theorem Zsucc_pred : forall n:Z, n = Zsucc (Zpred n).
Proof.
intros n; unfold Zsucc, Zpred in |- *; rewrite <- Zplus_assoc; simpl in |- *;
 rewrite Zplus_0_r; trivial with arith.
Qed. 

Hint Immediate Zsucc_pred: zarith.
 
Theorem Zpred_succ : forall n:Z, n = Zpred (Zsucc n).
Proof.
intros m; unfold Zpred, Zsucc in |- *; rewrite <- Zplus_assoc; simpl in |- *;
 rewrite Zplus_comm; auto with arith.
Qed.

Theorem Zsucc_inj : forall n m:Z, Zsucc n = Zsucc m -> n = m.
Proof.
intros n m H.
change (Zneg 1 + Zpos 1 + n = Zneg 1 + Zpos 1 + m) in |- *;
 do 2 rewrite <- Zplus_assoc; do 2 rewrite (Zplus_comm (Zpos 1));
 unfold Zsucc in H; rewrite H; trivial with arith.
Qed.
 
(** Misc properties, usually redundant or non natural *)

Lemma Zsucc_eq_compat : forall n m:Z, n = m -> Zsucc n = Zsucc m.
Proof.
intros n m H; rewrite H; reflexivity.
Qed.

Lemma Zsucc_inj_contrapositive : forall n m:Z, n <> m -> Zsucc n <> Zsucc m.
Proof.
unfold not in |- *; intros n m H1 H2; apply H1; apply Zsucc_inj; assumption.
Qed.

(**********************************************************************)
(** Properties of subtraction on binary integer numbers *)

Lemma Zminus_0_r : forall n:Z, n - Z0 = n.
Proof.
intro; unfold Zminus in |- *; simpl in |- *; rewrite Zplus_0_r;
 trivial with arith.
Qed.

Lemma Zminus_0_l_reverse : forall n:Z, n = n - Z0.
Proof.
intro; symmetry  in |- *; apply Zminus_0_r.
Qed.

Lemma Zminus_diag : forall n:Z, n - n = Z0.
Proof.
intro; unfold Zminus in |- *; rewrite Zplus_opp_r; trivial with arith.
Qed.

Lemma Zminus_diag_reverse : forall n:Z, Z0 = n - n.
Proof.
intro; symmetry  in |- *; apply Zminus_diag.
Qed.

Lemma Zplus_minus_eq : forall n m p:Z, n = m + p -> p = n - m.
Proof.
intros n m p H; unfold Zminus in |- *; apply (Zplus_reg_l m);
 rewrite (Zplus_comm m (n + - m)); rewrite <- Zplus_assoc;
 rewrite Zplus_opp_l; rewrite Zplus_0_r; rewrite H; 
 trivial with arith.
Qed.

Lemma Zminus_plus : forall n m:Z, n + m - n = m.
Proof.
intros n m; unfold Zminus in |- *; rewrite (Zplus_comm n m);
 rewrite <- Zplus_assoc; rewrite Zplus_opp_r; apply Zplus_0_r.
Qed.

Lemma Zplus_minus : forall n m:Z, n + (m - n) = m.
Proof.
unfold Zminus in |- *; intros n m; rewrite Zplus_permute; rewrite Zplus_opp_r;
 apply Zplus_0_r.
Qed.

Lemma Zminus_succ_l : forall n m:Z, Zsucc (n - m) = Zsucc n - m.
Proof.
intros n m; unfold Zminus, Zsucc in |- *; rewrite (Zplus_comm n (- m));
 rewrite <- Zplus_assoc; apply Zplus_comm.
Qed.

Lemma Zminus_plus_simpl_l : forall n m p:Z, p + n - (p + m) = n - m.
Proof.
intros n m p; unfold Zminus in |- *; rewrite Zopp_plus_distr;
 rewrite Zplus_assoc; rewrite (Zplus_comm p); rewrite <- (Zplus_assoc n p);
 rewrite Zplus_opp_r; rewrite Zplus_0_r; trivial with arith.
Qed.

Lemma Zminus_plus_simpl_l_reverse : forall n m p:Z, n - m = p + n - (p + m).
Proof.
intros; symmetry  in |- *; apply Zminus_plus_simpl_l.
Qed.

Lemma Zminus_plus_simpl_r : forall n m p:Z, n + p - (m + p) = n - m.
intros x y n.
unfold Zminus in |- *.
rewrite Zopp_plus_distr.
rewrite (Zplus_comm (- y) (- n)).
rewrite Zplus_assoc.
rewrite <- (Zplus_assoc x n (- n)).
rewrite (Zplus_opp_r n).
rewrite <- Zplus_0_r_reverse.
reflexivity.
Qed.

(** Misc redundant properties *)


Lemma Zeq_minus : forall n m:Z, n = m -> n - m = Z0.
Proof.
intros x y H; rewrite H; symmetry  in |- *; apply Zminus_diag_reverse.
Qed.

Lemma Zminus_eq : forall n m:Z, n - m = Z0 -> n = m.
Proof.
intros x y H; rewrite <- (Zplus_minus y x); rewrite H; apply Zplus_0_r.
Qed.


(**********************************************************************)
(** Properties of multiplication on binary integer numbers *)

Theorem Zpos_mult_morphism : 
 forall p q:positive, Zpos (p*q) = Zpos p * Zpos q.
Proof.
auto.
Qed.

(** 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.