# Library Coq.ZArith.Zcompare

i
Binary Integers (Pierre Crégut, CNET, Lannion, France)
Require Export BinPos.
Require Export BinInt.
Require Import Lt.
Require Import Gt.
Require Import Plus.
Require Import Mult.
Open Local Scope Z_scope.

# Comparison on integers

Lemma Zcompare_refl : forall n:Z, ( n ?= n ) = Eq.
Lemma Zcompare_Eq_eq : forall n m:Z, ( n ?= m ) = Eq -> n = m.
Ltac destr_zcompare :=
match goal with |- context [Zcompare ?x ?y] =>
let H := fresh "H" in
case_eq (Zcompare x y); intro H;
[generalize (Zcompare_Eq_eq _ _ H); clear H; intro H |
change (x < y)%Z in H |
change (x > y)%Z in H ]
end.
Lemma Zcompare_Eq_iff_eq : forall n m:Z, ( n ?= m ) = Eq <-> n = m.
Lemma Zcompare_antisym : forall n m:Z, CompOpp (n ?= m) = ( m ?= n ).
Lemma Zcompare_Gt_Lt_antisym : forall n m:Z, ( n ?= m ) = Gt <-> ( m ?= n ) = Lt.
Lemma Zcompare_spec : forall n m, CompSpec eq Zlt n m (n ?= m).

# Transitivity of comparison

Lemma Zcompare_Lt_trans :
forall n m p:Z, ( n ?= m ) = Lt -> ( m ?= p ) = Lt -> ( n ?= p ) = Lt.
Lemma Zcompare_Gt_trans :
forall n m p:Z, ( n ?= m ) = Gt -> ( m ?= p ) = Gt -> ( n ?= p ) = Gt.

# Comparison and opposite

Lemma Zcompare_opp : forall n m:Z, ( n ?= m ) = ( - m ?= - n ).
Hint Local Resolve Pcompare_refl.

# Comparison first-order specification

Lemma Zcompare_Gt_spec :
forall n m:Z, ( n ?= m ) = Gt -> exists h : positive , n + - m = Zpos h.

# Comparison and addition

Lemma weaken_Zcompare_Zplus_compatible :
(forall (n m:Z) (p:positive), ( Zpos p + n ?= Zpos p + m ) = ( n ?= m )) ->
forall n m p:Z, ( p + n ?= p + m ) = ( n ?= m ).
Hint Local Resolve ZC4.
Lemma weak_Zcompare_Zplus_compatible :
forall (n m:Z) (p:positive), ( Zpos p + n ?= Zpos p + m ) = ( n ?= m ).
Lemma Zcompare_plus_compat : forall n m p:Z, ( p + n ?= p + m ) = ( n ?= m ).
Lemma Zplus_compare_compat :
forall (r:comparison) (n m p q:Z),
( n ?= m ) = r -> ( p ?= q ) = r -> ( n + p ?= m + q ) = r.
Lemma Zcompare_succ_Gt : forall n:Z, ( Zsucc n ?= n ) = Gt.
Lemma Zcompare_Gt_not_Lt : forall n m:Z, ( n ?= m ) = Gt <-> ( n ?= m + 1) <> Lt.

# Successor and comparison

Lemma Zcompare_succ_compat : forall n m:Z, ( Zsucc n ?= Zsucc m ) = ( n ?= m ).

# Multiplication and comparison

Lemma Zcompare_mult_compat :
forall (p:positive) (n m:Z), ( Zpos p * n ?= Zpos p * m ) = ( n ?= m ).

# Reverting x ?= y to trichotomy

Lemma rename :
forall (A:Type) (P:A -> Prop) (x:A), (forall y:A, x = y -> P y) -> P x.
Lemma Zcompare_elim :
forall (c1 c2 c3:Prop) (n m:Z),
(n = m -> c1) ->
(n < m -> c2) ->
(n > m -> c3) -> match n ?= m with
| Eq => c1
| Lt => c2
| Gt => c3
end.
Lemma Zcompare_eq_case :
forall (c1 c2 c3:Prop) (n m:Z),
c1 -> n = m -> match n ?= m with
| Eq => c1
| Lt => c2
| Gt => c3
end.

# Decompose an egality between two ?= relations into 3 implications

Lemma Zcompare_egal_dec :
forall n m p q:Z,
(n < m -> p < q) ->
(( n ?= m ) = Eq -> ( p ?= q ) = Eq) ->
(n > m -> p > q) -> ( n ?= m ) = ( p ?= q ).

# Relating x ?= y to Zle, Zlt, Zge or Zgt

Lemma Zle_compare :
forall n m:Z,
n <= m -> match n ?= m with
| Eq => True
| Lt => True
| Gt => False
end.
Lemma Zlt_compare :
forall n m:Z,
n < m -> match n ?= m with
| Eq => False
| Lt => True
| Gt => False
end.
Lemma Zge_compare :
forall n m:Z,
n >= m -> match n ?= m with
| Eq => True
| Lt => False
| Gt => True
end.
Lemma Zgt_compare :
forall n m:Z,
n > m -> match n ?= m with
| Eq => False
| Lt => False
| Gt => True
end.

# Other properties

Lemma Zmult_compare_compat_l :
forall n m p:Z, p > 0 -> ( n ?= m ) = ( p * n ?= p * m ).
Lemma Zmult_compare_compat_r :
forall n m p:Z, p > 0 -> ( n ?= m ) = ( n * p ?= m * p ).