Library Coq.ZArith.Zcompare



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.

Transitivity of comparison


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).