Library Coq.ZArith.Zcompare


Binary Integers : results about Z.compare Initial author: Pierre Crégut (CNET, Lannion, France
THIS FILE IS DEPRECATED. It is now almost entirely made of compatibility formulations for results already present in BinInt.Z.

Require Export BinPos BinInt.
Require Import Lt Gt Plus Mult.
Local Open Scope Z_scope.

Comparison on integers


Lemma Zcompare_Gt_Lt_antisym : forall n m:Z, (n ?= m) = Gt <-> (m ?= n) = Lt.

Lemma Zcompare_antisym n m : CompOpp (n ?= m) = (m ?= n).

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 n m : (n ?= m) = (- m ?= - n).

Comparison first-order specification


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

Comparison and addition


Lemma Zcompare_plus_compat n m p : (p + n ?= p + m) = (n ?= m).

Lemma Zplus_compare_compat (r:comparison) (n m p q:Z) :
  (n ?= m) = r -> (p ?= q) = r -> (n + p ?= m + q) = r.

Lemma Zcompare_succ_Gt n : (Z.succ n ?= n) = Gt.

Lemma Zcompare_Gt_not_Lt n m : (n ?= m) = Gt <-> (n ?= m+1) <> Lt.

Successor and comparison

Multiplication and comparison


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

Lemma Zmult_compare_compat_l n m p:
  p > 0 -> (n ?= m) = (p * n ?= p * m).

Lemma Zmult_compare_compat_r n m p :
  p > 0 -> (n ?= m) = (n * p ?= m * p).

Relating x ?= y to =, <=, <, >= or >


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.

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.

Compatibility notations

Notation Zcompare_refl := Z.compare_refl (compat "8.3").
Notation Zcompare_Eq_eq := Z.compare_eq (compat "8.3").
Notation Zcompare_Eq_iff_eq := Z.compare_eq_iff (compat "8.3").
Notation Zcompare_spec := Z.compare_spec (compat "8.3").
Notation Zmin_l := Z.min_l (compat "8.3").
Notation Zmin_r := Z.min_r (compat "8.3").
Notation Zmax_l := Z.max_l (compat "8.3").
Notation Zmax_r := Z.max_r (compat "8.3").
Notation Zabs_eq := Z.abs_eq (compat "8.3").
Notation Zabs_non_eq := Z.abs_neq (compat "8.3").
Notation Zsgn_0 := Z.sgn_null (compat "8.3").
Notation Zsgn_1 := Z.sgn_pos (compat "8.3").
Notation Zsgn_m1 := Z.sgn_neg (compat "8.3").

Not kept: Zcompare_egal_dec