(* Contribution to the Coq Library   V6.3 (July 1999)                    *)

(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA                        ENS-CNRS                *)
(*              Rocquencourt                        Lyon                    *)
(*                                                                          *)
(*                                Coq V5.10                                 *)
(*                              Nov 25th 1994                               *)
(*                                                                          *)
(****************************************************************************)
(*                                 Zbase.v                                  *)
(****************************************************************************)

(* Basic definitions on type Z *)

(*************)
Inductive Z : Set :=
  | OZ : Z
  | pos : nat -> Z
  | neg : nat -> Z.

(***********)
Definition IZ := pos 0.

(****************)
(* was
Fixpoint is_posn [x,z :Z] : Prop :=
Cases x z of 
  OZ       y => False
| (pos n) OZ => False 
| (pos n) (pos m) => (eq nat n m)
| (pos n) (neg m) => False
| (neg n) y => False
end .
*)

Definition is_posn (x z : Z) :=
  match x, z with
  | pos n, pos m => n = m :>nat
  | _, _ => False
  end.



(**********************)
Lemma tech_pos_not_posZ : forall n m : nat, n <> m -> pos n <> pos m.


(* Goal: forall (n m : nat) (_ : not (@eq nat n m)), not (@eq Z (pos n) (pos m)) *)
unfold not in |- *; intros.
(* Goal: False *)
cut (is_posn (pos n) (pos m)).
(* Goal: forall _ : is_posn (pos n) (pos m), False *)
(* Goal: is_posn (pos n) (pos m) *)
simpl in |- *; exact H. rewrite H0; simpl in |- *; reflexivity.
Qed.

(**************)
Lemma eq_OZ_dec : forall x : Z, {x = OZ} + {x <> OZ}.


(* Goal: forall x : Z, sumbool (@eq Z x OZ) (not (@eq Z x OZ)) *)
intros; elim x.
(* Goal: sumbool (@eq Z OZ OZ) (not (@eq Z OZ OZ)) *)
(* Goal: forall n : nat, sumbool (@eq Z (pos n) OZ) (not (@eq Z (pos n) OZ)) *)
(* Goal: forall n : nat, sumbool (@eq Z (neg n) OZ) (not (@eq Z (neg n) OZ)) *)
left; reflexivity.
(* Goal: forall n : nat, sumbool (@eq Z (neg n) OZ) (not (@eq Z (neg n) OZ)) *)
intros; right; discriminate.
(* Goal: forall n : nat, sumbool (@eq Z (neg n) OZ) (not (@eq Z (neg n) OZ)) *)
intros; right; discriminate.
Qed.

(**************)
Definition posOZ (n : nat) :=
  match n return Z with
  | O =>
      (* O *)  OZ
      (* S n' *) 
  | S n' => pos n'
  end.

(**************)
Definition negOZ (n : nat) :=
  match n return Z with
  | O =>
      (* O *)  OZ
      (* S n' *) 
  | S n' => neg n'
  end.

(*************)
Definition absZ (x : Z) :=
  match x return Z with
  | OZ =>
      (* OZ *)  OZ 
      (* pos n *) 
  | pos n => pos n
      (* neg n *) 
  | neg n => pos n
  end.

(*************)
Definition sgnZ (x : Z) :=
  match x return Z with
  | OZ =>
      (* OZ *)  OZ
      (* pos n *) 
  | pos n => pos 0
      (* neg n *) 
  | neg n => neg 0
  end.
