(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

(* This includes a lot of copied code from arithmetics/Z.ma, so some of the
   comments may no longer be applicable. *)

(*include "arithmetics/compare.ma".*)
include "utilities/binary/positive.ma".

inductive Z : Type[0] ≝
  OZ  : Z
| pos : Pos → Z
| neg : Pos → Z.

(*interpretation "Integers" 'D = Z.*)

definition Z_of_nat ≝
λn. match n with
[ O ⇒ OZ 
| S n ⇒ pos (succ_pos_of_nat n)].

coercion Z_of_nat : ∀n:nat.Z ≝ Z_of_nat on _n:nat to Z.

definition neg_Z_of_nat \def
λn. match n with
[ O ⇒ OZ 
| S n ⇒ neg (succ_pos_of_nat n)].

definition abs ≝
λz.match z with 
[ OZ ⇒ O
| pos n ⇒ nat_of_pos n
| neg n ⇒ nat_of_pos n].

definition OZ_test ≝
λz.match z with 
[ OZ ⇒ true
| pos _ ⇒ false
| neg _ ⇒ false].

theorem OZ_test_to_Prop : ∀z:Z.
  match OZ_test z with
  [true ⇒ z=OZ 
  |false ⇒ z ≠ OZ].
#z cases z
[ @refl
|*:#z1 @nmk #H destruct]
qed.

(* discrimination *)
theorem injective_pos: injective Pos Z pos.
#n #m #H destruct //
qed.

(* variant inj_pos : \forall n,m:nat. pos n = pos m \to n = m
\def injective_pos. *)

theorem injective_neg: injective Pos Z neg.
#n #m #H destruct //
qed.

(* variant inj_neg : \forall n,m:nat. neg n = neg m \to n = m
\def injective_neg. *)

theorem not_eq_OZ_pos: ∀n:Pos. OZ ≠ pos n.
#n @nmk #H destruct;
qed.

theorem not_eq_OZ_neg :∀n:Pos. OZ ≠ neg n.
#n @nmk #H destruct;
qed.

theorem not_eq_pos_neg : ∀n,m:Pos. pos n ≠ neg m.
#n #m @nmk #H destruct;
qed.

theorem decidable_eq_Z : ∀x,y:Z. decidable (x=y).
#x #y cases x;
[cases y;
   [% //
   |*:#n %2 @nmk #H destruct]
|#n cases y;
   [%2 @nmk #H destruct;
   |#m cases (decidable_eq_pos n m) #H
      [>H % //
      |%2 @(not_to_not … H) #E destruct @refl
      ]
   |#m %2 @nmk #H destruct]
|#n cases y;
   [%2 @nmk #H destruct;
   |#m %2 @nmk #H destruct
   |#m cases (decidable_eq_pos n m);#H
      [>H % //
      |%2 @(not_to_not … H) #E destruct @refl
]]]
qed.

definition Zsucc ≝
λz. match z with
[ OZ ⇒ pos one
| pos n ⇒ pos (succ n)
| neg n ⇒
          match n with
          [ one ⇒ OZ
          | _ ⇒ neg (pred n)]].

definition Zpred ≝
λz. match z with
[ OZ ⇒ neg one
| pos n ⇒
          match n with
          [ one ⇒ OZ
          | _ ⇒ pos (pred n)]
| neg n ⇒ neg (succ n)].

lemma pred_succ_unfold_hack: ∀p. Zpred (Zsucc (neg (p0 p))) = neg (succ (pred (p0 p))).
//; qed.

theorem Zpred_Zsucc: ∀z:Z. Zpred (Zsucc z) = z.
#z cases z;
[ //
| #n normalize; cases n; /2/;
| #n cases n; //; #n'
    >(pred_succ_unfold_hack …) <(succ_pred_n …) //;
    % #H destruct;
qed.

lemma succ_pred_unfold_hack: ∀p. Zsucc (Zpred (pos (p0 p))) = pos (succ (pred (p0 p))).
//; qed.

theorem Zsucc_Zpred: ∀z:Z. Zsucc (Zpred z) = z.
#z cases z
[ //
| #n cases n;//; #n'
    >(succ_pred_unfold_hack …) <(succ_pred_n …) //;
    % #H destruct;
| #n cases n;/3/;
]
qed.

let rec Zle (x:Z) (y:Z) on x : Prop ≝
  match x with
  [ OZ ⇒ 
    match y with 
    [ OZ ⇒ True
    | pos m ⇒ True
    | neg m ⇒ False ]
  | pos n ⇒
    match y with 
    [ OZ ⇒ False
    | pos m ⇒ n ≤ m
    | neg m ⇒ False ]
  | neg n ⇒
    match y with 
    [ OZ ⇒ True
    | pos m ⇒ True
    | neg m ⇒ m ≤ n ]].

interpretation "integer 'less or equal to'" 'leq x y = (Zle x y).
interpretation "integer 'neither less nor equal to'" 'nleq x y = (Not (Zle x y)).

let rec Zlt (x:Z) (y:Z) on x : Prop ≝
  match x with
  [ OZ ⇒
    match y with 
    [ OZ ⇒ False
    | pos m ⇒ True
    | neg m ⇒ False ]
  | pos n ⇒
    match y with 
    [ OZ ⇒ False
    | pos m ⇒ n<m
    | neg m ⇒ False ]
  | neg n ⇒
    match y with 
    [ OZ ⇒ True
    | pos m ⇒ True
    | neg m ⇒ m<n ]].
    
interpretation "integer 'less than'" 'lt x y = (Zlt x y).
interpretation "integer 'not less than'" 'nless x y = (Not (Zlt x y)).

theorem irreflexive_Zlt: irreflexive Z Zlt.
#x cases x
[@nmk //
|*:#n @(not_le_succ_n n) (* XXX: auto?? *)]
qed.

(* transitivity *)
theorem transitive_Zle : transitive Z Zle.
#x #y #z cases x
[cases y
   [//
   |*:#n cases z;//]
|#n cases y
   [#H cases H
   |(**:#m #Hl cases z;//;*)
      #m #Hl cases z;//;#p #Hr
      @(transitive_le n m p) //; (* XXX: auto??? *)
   |#m #Hl cases Hl]
|#n cases y
   [#Hl cases z
      [1,2://
      |#m #Hr cases Hr]
   |#m #Hl cases z;
      [1,2://
      |#p #Hr cases Hr]
   |#m #Hl cases z;//;#p #Hr
      @(transitive_le p m n) //; (* XXX: auto??? *) ]
qed.

(* variant trans_Zle: transitive Z Zle
\def transitive_Zle.*)

theorem transitive_Zlt: transitive Z Zlt.
#x #y #z cases x
[cases y
   [//
   |#n cases z
      [#_ #Hr cases Hr
      |//
      |#m #_ #Hr cases Hr]
   |#n #Hl cases Hl]
|#n cases y
   [#Hl cases Hl
   |#m cases z
      [//
      |#p @transitive_lt (* XXX: auto??? *) 
      |//]
   |#m #Hl cases Hl]
|#n cases y
   [cases z;
      [1,2://
      |#m #_ #Hr cases Hr]
   |#m cases z;
      [1,2://
      |#p #_ #Hr cases Hr]
   |#m cases z
      [1,2://
      |#p #Hl #Hr @(transitive_lt … Hr Hl)]
   ]
]
qed.     

(* variant trans_Zlt: transitive Z Zlt
\def transitive_Zlt.
theorem irrefl_Zlt: irreflexive Z Zlt
\def irreflexive_Zlt.*)

theorem Zlt_neg_neg_to_lt: 
  ∀n,m:Pos. neg n < neg m → m < n.
//;
qed.

theorem lt_to_Zlt_neg_neg: ∀n,m:Pos.m < n → neg n < neg m. 
//;
qed.

theorem Zlt_pos_pos_to_lt: 
  ∀n,m:Pos. pos n < pos m → n < m.
//;
qed.

theorem lt_to_Zlt_pos_pos: ∀n,m:Pos.n < m → pos n < pos m. 
//;
qed.

lemma Zsucc_neg_succ: ∀n:Pos. Zsucc (neg (succ n)) = neg n.
#n normalize; <(pred_succ_n n) cases n; //; qed.

theorem Zlt_to_Zle: ∀x,y:Z. x < y → Zsucc x ≤ y.
#x #y cases x
[cases y
   [#H cases H
   |//;
   |#p #H cases H]
|#n cases y
   [#H cases H
   |#p normalize;//
   |#p #H cases H]
|#n cases y
   [1,2:cases n;//
   |#p @(pos_cases … n)
      [#H elim (not_le_succ_one p);#H2 @H2 @H (*// *) (* XXX: auto? *)
      |#m >(Zsucc_neg_succ m) @le_S_S_to_le (* XXX: auto? *)
      ]
   ]
]
qed.

(*** COMPARE ***)

(* boolean equality *)
let rec eqZb (x:Z) (y:Z) on x : bool ≝
  match x with
  [ OZ ⇒
      match y with
        [ OZ ⇒ true
        | pos q ⇒ false
        | neg q ⇒ false]
  | pos p ⇒
      match y with
        [ OZ ⇒ false
        | pos q ⇒ eqb p q
        | neg q ⇒ false]     
  | neg p ⇒
      match y with
        [ OZ ⇒ false
        | pos q ⇒ false
        | neg q ⇒ eqb p q]].

theorem eqZb_to_Prop: 
  ∀x,y:Z. 
    match eqZb x y with
    [ true ⇒ x=y
    | false ⇒ x ≠ y].
#x #y cases x
[cases y;
   [//
   |@not_eq_OZ_pos (* XXX: auto? *)
   |@not_eq_OZ_neg (* XXX: auto? *)]
|#n cases y;
   [@nmk #H elim (not_eq_OZ_pos n);#H2 /2/;
   |#m normalize @eqb_elim
      [//
      | * #H % #H' @H @(match H' return λx.λ_.n=match x with [pos m ⇒ m | neg m ⇒ m | OZ ⇒ one ] with [refl ⇒ ?]) //
      ]
   |#m @not_eq_pos_neg]
|#n cases y
   [@nmk #H elim (not_eq_OZ_neg n);#H /2/;
   |#m @nmk #H destruct
   |#m normalize @eqb_elim
      [//
      | * #H % #H' @H @(match H' return λx.λ_.n=match x with [pos m ⇒ m | neg m ⇒ m | OZ ⇒ one ] with [refl ⇒ ?]) //
   ]
]
qed.

theorem eqZb_elim: ∀x,y:Z.∀P:bool → Prop.
  (x=y → P true) → (x ≠ y → P false) → P (eqZb x y).
#x #y #P #HP1 #HP2
cut 
(match (eqZb x y) with
[ true ⇒ x=y
| false ⇒ x ≠ y] → P (eqZb x y))
[cases (eqZb x y);normalize; (* XXX: auto?? *)
   [@HP1
   |@HP2]
|#Hcut @Hcut @eqZb_to_Prop]
qed.

let rec Z_compare (x:Z) (y:Z) : compare ≝
  match x with
  [ OZ ⇒
    match y with 
    [ OZ ⇒ EQ
    | pos m ⇒ LT
    | neg m ⇒ GT ]
  | pos n ⇒
    match y with 
    [ OZ ⇒ GT
    | pos m ⇒ pos_compare n m
    | neg m ⇒ GT]
  | neg n ⇒ 
    match y with 
    [ OZ ⇒ LT
    | pos m ⇒ LT
    | neg m ⇒ pos_compare m n ]].

theorem Z_compare_to_Prop : 
∀x,y:Z. match (Z_compare x y) with
[ LT ⇒ x < y
| EQ ⇒ x=y
| GT ⇒ y < x]. 
#x #y elim x
[elim y;//;
|elim y
   [1,3://
   |#n #m normalize;
      cut (match (pos_compare m n) with
      [ LT ⇒ m < n
      | EQ ⇒ m = n
      | GT ⇒ n < m ] →
      match (pos_compare m n) with
      [ LT ⇒ (succ m)  ≤ n
      | EQ ⇒ pos m = pos n
      | GT ⇒ (succ n)  ≤ m])
      [cases (pos_compare m n);//
      |#Hcut @Hcut @pos_compare_to_Prop]
   ]
|elim y
   [#n //
   |normalize;//
   |normalize;#n #m
      cut (match (pos_compare n m) with
        [ LT ⇒ n < m
        | EQ ⇒ n = m
        | GT ⇒ m < n] →
      match (pos_compare n m) with
      [ LT ⇒ (succ n) ≤ m
      | EQ ⇒ neg m = neg n
      | GT ⇒ (succ m) ≤ n])
      [cases (pos_compare n m);//
      |#Hcut @Hcut @pos_compare_to_Prop]
   ]
]
qed.

let rec Zplus (x:Z) (y:Z) on x : Z ≝
  match x with
    [ OZ ⇒ y
    | pos m ⇒
        match y with
         [ OZ ⇒ x
         | pos n ⇒ (pos (m + n))
         | neg n ⇒ 
              match pos_compare m n with
                [ LT ⇒ (neg (n-m))
                | EQ ⇒ OZ
                | GT ⇒ (pos (m-n))] ]
    | neg m ⇒
        match y with
         [ OZ ⇒ x
         | pos n ⇒
              match pos_compare m n with
                [ LT ⇒ (pos (n-m))
                | EQ ⇒ OZ
                | GT ⇒ (neg (m-n))]     
         | neg n ⇒ (neg (m + n))] ].

interpretation "integer plus" 'plus x y = (Zplus x y).

theorem eq_plus_Zplus: ∀n,m:nat. Z_of_nat (n+m) = Z_of_nat n + Z_of_nat m.
#n #m cases n
[//
|#p cases m
   [normalize;//
   |#m' normalize;>(nat_plus_pos_plus …) >(succ_nat_pos ?) /2/]
qed.

theorem eq_pplus_Zplus: ∀n,m:Pos. pos (n+m) = pos n + pos m.
//; qed.

theorem Zplus_z_OZ: ∀z:Z. z+OZ = z.
#z cases z;//;
qed.

theorem sym_Zplus : ∀x,y:Z. x+y = y+x.
#x #y cases x
[>Zplus_z_OZ //
|#p cases y
   [//
   |//
   |#q whd in ⊢ (??%%); >pos_compare_n_m_m_n
      cases (pos_compare q p);//]
|#p cases y
   [//;
   |#q whd in ⊢ (??%%); >pos_compare_n_m_m_n
      cases (pos_compare q p);//
   |normalize;//]
]
qed.

theorem Zpred_Zplus_neg_O : ∀z. Zpred z = (neg one)+z.
#z cases z
[//
|*:#n cases n;//]
qed.

theorem Zsucc_Zplus_pos_O : ∀z. Zsucc z = (pos one)+z.
#z cases z
[//
|*:#n cases n;//]
qed.

lemma Zpred_pos_succ: ∀n. Zpred (pos (succ n)) = pos n.
#n normalize; cases n; /2/; qed.

theorem Zplus_pos_pos:
  ∀n,m. (pos n)+(pos m) = (Zsucc (pos n))+(Zpred (pos m)).
#n #m @(pos_cases … n)
[ @(pos_cases … m) //;
|#p @(pos_cases … m)
   [normalize; <(succ_plus_one …) //;
   |#q >(Zsucc_Zplus_pos_O …) >(Zpred_pos_succ ?)
      normalize; /2/;
   ]
]
qed.

theorem Zplus_pos_neg:
  ∀n,m. (pos n)+(neg m) = (Zsucc (pos n))+(Zpred (neg m)).
#n #m
whd in ⊢ (??%%);
<(pos_compare_S_S …)
>(minus_S_S …)
>(minus_S_S …) //;
qed.

lemma pos_nonzero: ∀A.∀P:Pos→A.∀Q,n. match succ n with [ one ⇒ Q | p0 p ⇒ P n | p1 p ⇒ P n ] = P n.
#A #P #Q #n @succ_elim //; qed.

lemma partial_minus_S_one: ∀n. partial_minus (succ n) one = MinusPos n.
#n cases n; //;
#n' whd in ⊢ (??%?); normalize; <(pred_succ_n …)
@succ_elim //; qed.

theorem Zplus_neg_pos :
  ∀n,m. (neg n)+(pos m) = (Zsucc (neg n))+(Zpred (pos m)).
#n #m @(pos_cases … n) @(pos_cases … m)
[ //;
| #m' >Zpred_pos_succ
    change with (Zsucc (pos m')) in ⊢ (??(??%)?);
    <Zpred_Zplus_neg_O >Zpred_Zsucc @refl
| #m' whd in ⊢ (??%%); >pos_compare_S_one normalize;
    >partial_minus_S_one normalize; >pos_nonzero
    <pred_succ_n //
| #m' #n' whd in ⊢ (??%%); <pos_compare_S_S
    >minus_S_S
    >minus_S_S normalize
    >pos_nonzero
    >pos_nonzero
    <pred_succ_n
    <pred_succ_n
    normalize; //;
] qed. 

theorem Zplus_neg_neg:
  ∀n,m. (neg n)+(neg m) = (Zsucc (neg n))+(Zpred (neg m)).
#n #m @(pos_cases … n) @(pos_cases … m)
[ 1,2: //;
| #n' normalize in ⊢ (???(?%?));
    >(pos_nonzero …)
    <(pred_succ_n …) normalize; //;
| #m' #n' normalize; >(pos_nonzero …)
    <(pred_succ_n …) normalize; //;
] qed.

theorem Zplus_Zsucc_Zpred: ∀x,y. x+y = (Zsucc x)+(Zpred y).
#x #y cases x
[cases y
   [//
   |#n <(Zsucc_Zplus_pos_O ?) >(Zsucc_Zpred ?) //
   |#p <(Zsucc_Zplus_pos_O …) //]
|cases y;/2/; #p >(sym_Zplus ? (Zpred OZ))
   <Zpred_Zplus_neg_O //;
|cases y
   [#n <(sym_Zplus ??) <(sym_Zplus (Zpred OZ) ?)
      <(Zpred_Zplus_neg_O ?) >(Zpred_Zsucc ?) //
   |*:/2/]
qed.

theorem Zplus_Zsucc_pos_pos : 
  ∀n,m. (Zsucc (pos n))+(pos m) = Zsucc ((pos n)+(pos m)).
#n #m >(Zsucc_Zplus_pos_O ?) >(Zsucc_Zplus_pos_O ?) //;
qed.

theorem Zplus_Zsucc_pos_neg: 
  ∀n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))).
#n #m
@(pos_elim2 (λn,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m)))))
[#n1 elim n1
   [//
   |*:#n2 #IH elim n2;//]
|#n' >(sym_Zplus …) <(Zpred_Zplus_neg_O ?)
   >(sym_Zplus …) <(Zpred_Zplus_neg_O ?)
   >(Zpred_Zsucc …)  /2/
|#n1 #m1 #IH <(Zplus_pos_neg ? m1) >IH
<(Zplus_pos_neg …) //]
qed.

theorem Zplus_Zsucc_neg_neg : 
  ∀n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m).
#n #m
@(pos_elim2 (λ n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m)))
[@pos_elim
   [//
   |#n2 #IH normalize;<(pred_succ_n …) >(pos_nonzero …) //]
| #n' normalize;
   >(pos_nonzero …)
   <(pred_succ_n …) normalize;
   <(succ_plus_one …)
   <(succ_plus_one …) >(pos_nonzero …) //;
| #n' #m' #IH normalize;
   >(pos_nonzero …) normalize;
   <(pluss_succn_m …)
   >(pos_nonzero …) //;
]
qed.

lemma neg_pos_succ: ∀n,m:Pos. neg (succ n) + pos (succ m) = neg n + pos m.
#n #m whd in ⊢ (??%%); <pos_compare_S_S
>minus_S_S >minus_S_S
 //; qed.


theorem Zplus_Zsucc_neg_pos: 
  ∀n,m. Zsucc (neg n)+(pos m) = Zsucc ((neg n)+(pos m)).
#n #m
@(pos_elim2 (λn,m. (Zsucc (neg n)) + (pos m) = Zsucc (neg n + pos m)))
[@pos_elim
   [//
   |#n2 #IH normalize; >(pos_nonzero …) normalize;
      >(partial_minus_S_one …) //]
| #n'
    >(sym_Zplus …)
    <(Zsucc_Zplus_pos_O …)
    >(sym_Zplus …)
    <(Zsucc_Zplus_pos_O …) //;
|#n' #m' #IH
   >(neg_pos_succ …) //;
] qed.

theorem Zplus_Zsucc : ∀x,y:Z. (Zsucc x)+y = Zsucc (x+y).
#x #y cases x
[cases y;//;(*#n normalize;cases n;//;*)
|*:#n cases y;//;#m @Zplus_Zsucc_neg_pos(* XXX: // didn't work! *)]
qed.

theorem Zplus_Zpred: ∀x,y:Z. (Zpred x)+y = Zpred (x+y).
#x #y cut (Zpred (x+y) = Zpred ((Zsucc (Zpred x))+y))
[>(Zsucc_Zpred ?) //
|#Hcut >Hcut >(Zplus_Zsucc ??) //]
qed.

theorem associative_Zplus: associative Z Zplus.
(* nchange with (\forall x,y,z:Z. (x + y) + z = x + (y + z));*)
#x #y #z cases x
[//
|@pos_elim
   [<(Zsucc_Zplus_pos_O ?) <(Zsucc_Zplus_pos_O ?) //;
   |#n1 #IH
      >(Zplus_Zsucc (pos n1) ?) >(Zplus_Zsucc (pos n1) ?)
      >(Zplus_Zsucc ((pos n1)+y) ?) //]
|@pos_elim
   [<(Zpred_Zplus_neg_O (y+z)) <(Zpred_Zplus_neg_O y) //;
   |#n1 #IH
      >(Zplus_Zpred (neg n1) ?) >(Zplus_Zpred (neg n1) ?)
      >(Zplus_Zpred ((neg n1)+y) ?) //]
]
qed.

(* variant assoc_Zplus : \forall x,y,z:Z.  (x+y)+z = x+(y+z)
\def associative_Zplus. *)

(* Zopp *)
definition Zopp : Z → Z ≝
  λx:Z. match x with
  [ OZ ⇒ OZ
  | pos n ⇒ neg n
  | neg n ⇒ pos n ].

interpretation "integer unary minus" 'uminus x = (Zopp x).

theorem eq_OZ_Zopp_OZ : OZ = (- OZ).
//;
qed.

theorem Zopp_Zplus: ∀x,y:Z. -(x+y) = -x + -y.
#x #y cases x
[cases y;//
|*:#n cases y;//;#m whd in ⊢ (??(?%)%); @pos_compare_elim normalize;//]
qed.

theorem Zopp_Zopp: ∀x:Z. --x = x.
#x cases x;//;
qed.

theorem Zplus_Zopp: ∀ x:Z. x+ -x = OZ.
#x cases x
[//
|*:#n whd in ⊢ (??%?); >pos_compare_n_n //]
qed.

theorem injective_Zplus_l: ∀x:Z.injective Z Z (λy.y+x).
#x #z #y #H
<(Zplus_z_OZ z) <(Zplus_z_OZ y)
<(Zplus_Zopp x)
<(associative_Zplus ???) <(associative_Zplus ???)
//;
qed.

theorem injective_Zplus_r: ∀x:Z.injective Z Z (λy.x+y).
#x #z #y #H
@(injective_Zplus_l x)
<(sym_Zplus ??)
//;
qed.

(* minus *)
definition Zminus : Z → Z → Z ≝ λx,y:Z. x + (-y).

interpretation "integer minus" 'minus x y = (Zminus x y).



definition Z_two_power_nat : nat → Z ≝ λn. pos (two_power_nat n).
definition Z_two_power_pos : Pos → Z ≝ λn. pos (two_power_pos n).
definition two_p : Z → Z ≝
λz.match z with
[ OZ ⇒ pos one
| pos p ⇒ pos (two_power_pos p)
| neg _ ⇒ OZ  (* same fib as Coq *)
].



lemma eqZb_z_z : ∀z.eqZb z z = true.
#z cases z;normalize;//;
qed.



lemma injective_Z_of_nat : injective ? ? Z_of_nat.
normalize;
#n #m cases n;cases m;normalize;//;
[ 1,2: #n' #H destruct
| #n' #m' #H destruct; >(succ_pos_of_nat_inj … e0) //
] qed.

lemma reflexive_Zle : reflexive ? Zle.
#x cases x; //; qed.

lemma Zsucc_pos : ∀n. Z_of_nat (S n) = Zsucc (Z_of_nat n).
#n cases n;normalize;//;qed.

lemma Zsucc_le : ∀x:Z. x ≤ Zsucc x.
#x cases x; //;
#n cases n; //; qed.

lemma Zplus_le_pos : ∀x,y:Z.∀n. x ≤ y → x ≤ y+pos n.
#x #y
@pos_elim
 [ 2: #n' #IH ]
>(Zplus_Zsucc_Zpred y ?)
[ >(Zpred_Zsucc (pos n'))
 #H @(transitive_Zle ??? (IH H)) >(Zplus_Zsucc ??)
    @Zsucc_le
| #H @(transitive_Zle ??? H) >(Zplus_z_OZ ?) @Zsucc_le
] qed.

theorem Zle_to_Zlt: ∀x,y:Z. x ≤ y → Zpred x < y.
#x #y cases x;
[ cases y;
  [ 1,2: //
  | #n @False_ind
  ]
| #n cases y;
  [ normalize; @False_ind
  | #m @(pos_cases … n) /2/;
  | #m normalize; @False_ind
  ]
| #n cases y; /2/;
] qed.
    
theorem Zlt_to_Zle_to_Zlt: ∀n,m,p:Z. n < m → m ≤ p → n < p.
#n #m #p #Hlt #Hle <(Zpred_Zsucc n) @Zle_to_Zlt
@(transitive_Zle … Hle) /2/;
qed.

include "basics/types.ma".

definition decidable_eq_Z_Type : ∀z1,z2:Z. (z1 = z2) + (z1 ≠ z2).
#z1 #z2 lapply (eqZb_to_Prop z1 z2);cases (eqZb z1 z2);normalize;#H
[% //
|%2 //]
qed.

lemma eqZb_false : ∀z1,z2. z1≠z2 → eqZb z1 z2 = false.
#z1 #z2 lapply (eqZb_to_Prop z1 z2); cases (eqZb z1 z2); //;
#H #H' @False_ind @(absurd ? H H')
qed.

(* Z.ma *)

definition Zge: Z → Z → Prop ≝
λn,m:Z.m ≤ n.

interpretation "integer 'greater or equal to'" 'geq x y = (Zge x y).

definition Zgt: Z → Z → Prop ≝
λn,m:Z.m<n.

interpretation "integer 'greater than'" 'gt x y = (Zgt x y).

interpretation "integer 'not greater than'" 'ngtr x y = (Not (Zgt x y)).

let rec Zleb (x:Z) (y:Z) : bool ≝
  match x with
  [ OZ ⇒ 
    match y with 
    [ OZ ⇒ true
    | pos m ⇒ true
    | neg m ⇒ false ]
  | pos n ⇒
    match y with 
    [ OZ ⇒ false
    | pos m ⇒ leb n m
    | neg m ⇒ false ]
  | neg n ⇒
    match y with 
    [ OZ ⇒ true
    | pos m ⇒ true
    | neg m ⇒ leb m n ]].
    
let rec Zltb (x:Z) (y:Z) : bool ≝
  match x with
  [ OZ ⇒
    match y with 
    [ OZ ⇒ false
    | pos m ⇒ true
    | neg m ⇒ false ]
  | pos n ⇒
    match y with 
    [ OZ ⇒ false
    | pos m ⇒ leb (succ n) m
    | neg m ⇒ false ]
  | neg n ⇒
    match y with 
    [ OZ ⇒ true
    | pos m ⇒ true
    | neg m ⇒ leb (succ m) n ]].



theorem Zle_to_Zleb_true: ∀n,m. n ≤ m → Zleb n m = true.
#n #m cases n;cases m; //;
[ 1,2: #m' normalize; #H @(False_ind ? H)
| 3,5: #n' #m' normalize; @le_to_leb_true
| 4: #n' #m' normalize; #H @(False_ind ? H)
] qed.

theorem Zleb_true_to_Zle: ∀n,m.Zleb n m = true → n ≤ m.
#n #m cases n;cases m; //;
[ 1,2: #m' normalize; #H destruct
| 3,5: #n' #m' normalize; @leb_true_to_le
| 4: #n' #m' normalize; #H destruct
] qed.

theorem Zleb_false_to_not_Zle: ∀n,m.Zleb n m = false → n ≰ m.
#n #m #H % #H' >(Zle_to_Zleb_true … H') in H; #H destruct;
qed.

theorem Zlt_to_Zltb_true: ∀n,m. n < m → Zltb n m = true.
#n #m cases n;cases m; //;
[ normalize; #H @(False_ind ? H)
| 2,3: #m' normalize; #H @(False_ind ? H)
| 4,6: #n' #m' normalize; @le_to_leb_true
| #n' #m' normalize; #H @(False_ind ? H)
] qed.

theorem Zltb_true_to_Zlt: ∀n,m. Zltb n m = true → n < m.
#n #m cases n;cases m; //;
[ normalize; #H destruct
| 2,3: #m' normalize; #H destruct
| 4,6: #n' #m' @leb_true_to_le
| #n' #m' normalize; #H destruct
] qed.

theorem Zltb_false_to_not_Zlt: ∀n,m.Zltb n m = false → n ≮ m.
#n #m #H % #H' >(Zlt_to_Zltb_true … H') in H; #H destruct;
qed.

theorem Zleb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0]. 
(n ≤ m → P true) → (n ≰ m → P false) → P (Zleb n m).
#n #m #P #Hle #Hnle
lapply (refl ? (Zleb n m));
elim (Zleb n m) in ⊢ ((???%)→%);
#Hb
[ @Hle @(Zleb_true_to_Zle … Hb)
| @Hnle @(Zleb_false_to_not_Zle … Hb) 
] qed.

theorem Zltb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0]. 
(n < m → P true) → (n ≮ m → P false) → P (Zltb n m).
#n #m #P #Hlt #Hnlt
lapply (refl ? (Zltb n m));
elim (Zltb n m) in ⊢ ((???%)→%);
#Hb
[ @Hlt @(Zltb_true_to_Zlt … Hb)
| @Hnlt @(Zltb_false_to_not_Zlt … Hb) 
] qed.

lemma monotonic_Zle_Zsucc: monotonic Z Zle Zsucc.
#x #y cases x; cases y; /2/;
#n #m @(pos_cases … n) @(pos_cases … m)
[ //;
| #n' /2/;
| #m' #H @False_ind normalize in H; @(absurd … (not_le_succ_one m')) /2/;
| #n' #m' #H normalize in H;
    >(Zsucc_neg_succ n') >(Zsucc_neg_succ m') /2/;
] qed.

lemma monotonic_Zle_Zpred: monotonic Z Zle Zpred.
#x #y cases x; cases y;
[ 1,2,7,8,9: /2/;
| 3,4: #m normalize; *;
| #m #n @(pos_cases … n) @(pos_cases … m)
  [ 1,2: /2/;
  | #n' normalize; #H @False_ind @(absurd … (not_le_succ_one n')) /2/;
  | #n' #m' >(Zpred_pos_succ n') >(Zpred_pos_succ m') /2/;
  ]
| #m #n normalize; *;
] qed.

lemma monotonic_Zle_Zplus_r: ∀n.monotonic Z Zle (λm.n + m).
#n cases n; //; #n' #a #b #H
[ @(pos_elim … n')
  [ <(Zsucc_Zplus_pos_O a) <(Zsucc_Zplus_pos_O b) /2/;
  | #n'' #H >(?:pos (succ n'') = Zsucc (pos n'')) //;
      >(Zplus_Zsucc …) >(Zplus_Zsucc …) /2/;
  ]
| @(pos_elim … n')
  [ <(Zpred_Zplus_neg_O a) <(Zpred_Zplus_neg_O b) /2/;
  | #n'' #H >(?:neg (succ n'') = Zpred (neg n'')) //;
      >(Zplus_Zpred …) >(Zplus_Zpred …) /2/;
  ]
] qed.

lemma monotonic_Zle_Zplus_l: ∀n.monotonic Z Zle (λm.m + n).
/2/; qed.

let rec Z_times (x:Z) (y:Z) : Z ≝
match x with
[ OZ ⇒ OZ
| pos n ⇒
  match y with
  [ OZ ⇒ OZ
  | pos m ⇒ pos (n*m)
  | neg m ⇒ neg (n*m)
  ]
| neg n ⇒
  match y with
  [ OZ ⇒ OZ
  | pos m ⇒ neg (n*m)
  | neg m ⇒ pos (n*m)
  ]
].
interpretation "integer multiplication" 'times x y = (Z_times x y).



definition Zmax : Z → Z → Z ≝ 
  λx,y.match Z_compare x y with
  [ LT ⇒ y
  | _ ⇒ x ].

lemma Zmax_l: ∀x,y. x ≤ Zmax x y.
#x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y) cases (Z_compare x y)
/3/ qed.

lemma Zmax_r: ∀x,y. y ≤ Zmax x y.
#x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y) cases (Z_compare x y)
whd in ⊢ (% → ??%); /3/ qed.


lemma Zminus_Zlt: ∀x,y:Z. y>0 → x-y < x.
#x #y cases y;
[ #H @(False_ind … H)
| #m #_ cases x; //; #n
    whd in ⊢ (?%?);
    lapply (pos_compare_to_Prop n m);
    cases (pos_compare n m); /2/
    #lt whd <(minus_Sn_m … lt) /2/;
| #m #H @(False_ind … H)
] qed.