Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(* -*- coding: utf-8 -*- *)
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

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. (* Useless now, for compatibility only *)

Local Open Scope Z_scope.

(***************************)

Comparison on integers

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

Lemma Zcompare_antisym n m : CompOpp (n ?= m) = (m ?= n).n, m:Z
CompOpp (n ?= m) = (m ?= n)
Proof eq_sym (Z.compare_antisym n m).

Transitivity of comparison

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

Lemma Zcompare_Gt_trans :
  forall n m p:Z, (n ?= m) = Gt -> (m ?= p) = Gt -> (n ?= p) = Gt.forall n m p : Z,
(n ?= m) = Gt -> (m ?= p) = Gt -> (n ?= p) = Gt
Proof.forall n m p : Z,
(n ?= m) = Gt -> (m ?= p) = Gt -> (n ?= p) = Gt
 intros n m p.n, m, p:Z
(n ?= m) = Gt -> (m ?= p) = Gt -> (n ?= p) = Gt change (n > m -> m > p -> n > p).n, m, p:Z
n > m -> m > p -> n > p
 Z.swap_greater.n, m, p:Z
m < n -> p < m -> p < n intros.n, m, p:Z
H:m < n
H0:p < m
p < n now transitivity m.
Qed.

Comparison and opposite

Lemma Zcompare_opp n m : (n ?= m) = (- m ?= - n).n, m:Z
(n ?= m) = (- m ?= - n)
Proof.n, m:Z
(n ?= m) = (- m ?= - n)
 symmetry.n, m:Z
(- m ?= - n) = (n ?= m) apply Z.compare_opp.
Qed.

Comparison first-order specification

Lemma Zcompare_Gt_spec n m : (n ?= m) = Gt ->  exists h, n + - m = Zpos h.n, m:Z
(n ?= m) = Gt ->
exists h : positive, n + - m = Z.pos h
Proof.n, m:Z
(n ?= m) = Gt ->
exists h : positive, n + - m = Z.pos h
 rewrite Z.compare_sub.n, m:Z
(n - m ?= 0) = Gt ->
exists h : positive, n + - m = Z.pos h unfold Z.sub.n, m:Z
(n + - m ?= 0) = Gt ->
exists h : positive, n + - m = Z.pos h
 destruct (n+-m) as [|p|p]; try discriminate.n, m:Z
p:positive
(Z.pos p ?= 0) = Gt ->
exists h : positive, Z.pos p = Z.pos h now exists p.
Qed.

Comparison and addition

Lemma Zcompare_plus_compat n m p : (p + n ?= p + m) = (n ?= m).n, m, p:Z
(p + n ?= p + m) = (n ?= m)
Proof.n, m, p:Z
(p + n ?= p + m) = (n ?= m)
 apply Z.add_compare_mono_l.
Qed.

Lemma Zplus_compare_compat (r:comparison) (n m p q:Z) :
  (n ?= m) = r -> (p ?= q) = r -> (n + p ?= m + q) = r.r:comparison
n, m, p, q:Z
(n ?= m) = r -> (p ?= q) = r -> (n + p ?= m + q) = r
Proof.r:comparison
n, m, p, q:Z
(n ?= m) = r -> (p ?= q) = r -> (n + p ?= m + q) = r
 rewrite (Z.compare_sub n), (Z.compare_sub p), (Z.compare_sub (n+p)).r:comparison
n, m, p, q:Z
(n - m ?= 0) = r ->
(p - q ?= 0) = r -> (n + p - (m + q) ?= 0) = r
 unfold Z.sub.r:comparison
n, m, p, q:Z
(n + - m ?= 0) = r ->
(p + - q ?= 0) = r -> (n + p + - (m + q) ?= 0) = r rewrite Z.opp_add_distr.r:comparison
n, m, p, q:Z
(n + - m ?= 0) = r ->
(p + - q ?= 0) = r -> (n + p + (- m + - q) ?= 0) = r rewrite Z.add_shuffle1.r:comparison
n, m, p, q:Z
(n + - m ?= 0) = r ->
(p + - q ?= 0) = r -> (n + - m + (p + - q) ?= 0) = r
 destruct (n+-m), (p+-q); simpl; intros; now subst.
Qed.

Lemma Zcompare_succ_Gt n : (Z.succ n ?= n) = Gt.n:Z
(Z.succ n ?= n) = Gt
Proof.n:Z
(Z.succ n ?= n) = Gt
 apply Z.lt_gt.n:Z
n < Z.succ n apply Z.lt_succ_diag_r.
Qed.

Lemma Zcompare_Gt_not_Lt n m : (n ?= m) = Gt <-> (n ?= m+1) <> Lt.n, m:Z
(n ?= m) = Gt <-> (n ?= m + 1) <> Lt
Proof.n, m:Z
(n ?= m) = Gt <-> (n ?= m + 1) <> Lt
 change (n > m <-> n >= m+1).n, m:Z
n > m <-> n >= m + 1 Z.swap_greater.n, m:Z
m < n <-> m + 1 <= n symmetry.n, m:Z
m + 1 <= n <-> m < n apply Z.le_succ_l.
Qed.

Successor and comparison

Lemma Zcompare_succ_compat n m : (Z.succ n ?= Z.succ m) = (n ?= m).n, m:Z
(Z.succ n ?= Z.succ m) = (n ?= m)
Proof.n, m:Z
(Z.succ n ?= Z.succ m) = (n ?= m)
 rewrite <- 2 Z.add_1_l.n, m:Z
(1 + n ?= 1 + m) = (n ?= m) apply Z.add_compare_mono_l.
Qed.

Multiplication and comparison

Lemma Zcompare_mult_compat :
  forall (p:positive) (n m:Z), (Zpos p * n ?= Zpos p * m) = (n ?= m).forall (p : positive) (n m : Z),
(Z.pos p * n ?= Z.pos p * m) = (n ?= m)
Proof.forall (p : positive) (n m : Z),
(Z.pos p * n ?= Z.pos p * m) = (n ?= m)
 intros p [|n|n] [|m|m]; simpl; trivial; now rewrite Pos.mul_compare_mono_l.
Qed.

Lemma Zmult_compare_compat_l n m p:
  p > 0 -> (n ?= m) = (p * n ?= p * m).n, m, p:Z
p > 0 -> (n ?= m) = (p * n ?= p * m)
Proof.n, m, p:Z
p > 0 -> (n ?= m) = (p * n ?= p * m)
 intros; destruct p; try discriminate.n, m:Z
p:positive
H:Z.pos p > 0
(n ?= m) = (Z.pos p * n ?= Z.pos p * m)
 symmetry.n, m:Z
p:positive
H:Z.pos p > 0
(Z.pos p * n ?= Z.pos p * m) = (n ?= m) apply Zcompare_mult_compat.
Qed.

Lemma Zmult_compare_compat_r n m p :
  p > 0 -> (n ?= m) = (n * p ?= m * p).n, m, p:Z
p > 0 -> (n ?= m) = (n * p ?= m * p)
Proof.n, m, p:Z
p > 0 -> (n ?= m) = (n * p ?= m * p)
 intros; rewrite 2 (Z.mul_comm _ p); now apply Zmult_compare_compat_l.
Qed.

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.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
Proof.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
 intros.c1, c2, c3:Prop
n, m:Z
H:n = m -> c1
H0:n < m -> c2
H1:n > m -> c3
match n ?= m with
| Eq => c1
| Lt => c2
| Gt => c3
end case Z.compare_spec; trivial.c1, c2, c3:Prop
n, m:Z
H:n = m -> c1
H0:n < m -> c2
H1:n > m -> c3
m < n -> c3 now Z.swap_greater.
Qed.

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.forall (c1 c2 c3 : Prop) (n m : Z),
c1 ->
n = m ->
match n ?= m with
| Eq => c1
| Lt => c2
| Gt => c3
end
Proof.forall (c1 c2 c3 : Prop) (n m : Z),
c1 ->
n = m ->
match n ?= m with
| Eq => c1
| Lt => c2
| Gt => c3
end
 intros.c1, c2, c3:Prop
n, m:Z
H:c1
H0:n = m
match n ?= m with
| Eq => c1
| Lt => c2
| Gt => c3
end subst.c1, c2, c3:Prop
m:Z
H:c1
match m ?= m with
| Eq => c1
| Lt => c2
| Gt => c3
end now rewrite Z.compare_refl.
Qed.

Lemma Zle_compare :
  forall n m:Z,
    n <= m -> match n ?= m with
		| Eq => True
		| Lt => True
		| Gt => False
              end.forall n m : Z,
n <= m ->
match n ?= m with
| Gt => False
| _ => True
end
Proof.forall n m : Z,
n <= m ->
match n ?= m with
| Gt => False
| _ => True
end
  intros.n, m:Z
H:n <= m
match n ?= m with
| Gt => False
| _ => True
end case Z.compare_spec; trivial; Z.order.
Qed.

Lemma Zlt_compare :
  forall n m:Z,
   n < m -> match n ?= m with
              | Eq => False
              | Lt => True
              | Gt => False
            end.forall n m : Z,
n < m ->
match n ?= m with
| Lt => True
| _ => False
end
Proof.forall n m : Z,
n < m ->
match n ?= m with
| Lt => True
| _ => False
end
  intros x y H; now rewrite H.
Qed.

Lemma Zge_compare :
  forall n m:Z,
    n >= m -> match n ?= m with
		| Eq => True
		| Lt => False
		| Gt => True
              end.forall n m : Z,
n >= m ->
match n ?= m with
| Lt => False
| _ => True
end
Proof.forall n m : Z,
n >= m ->
match n ?= m with
| Lt => False
| _ => True
end
  intros.n, m:Z
H:n >= m
match n ?= m with
| Lt => False
| _ => True
end now case Z.compare_spec.
Qed.

Lemma Zgt_compare :
  forall n m:Z,
    n > m -> match n ?= m with
               | Eq => False
               | Lt => False
               | Gt => True
             end.forall n m : Z,
n > m ->
match n ?= m with
| Gt => True
| _ => False
end
Proof.forall n m : Z,
n > m ->
match n ?= m with
| Gt => True
| _ => False
end
  intros x y H; now rewrite H.
Qed.

Compatibility notations

Notation Zcompare_Eq_eq := Z.compare_eq (only parsing).
Notation Zcompare_Eq_iff_eq := Z.compare_eq_iff (only parsing).
Notation Zabs_non_eq := Z.abs_neq (only parsing).
Notation Zsgn_0 := Z.sgn_null (only parsing).
Notation Zsgn_1 := Z.sgn_pos (only parsing).
Notation Zsgn_m1 := Z.sgn_neg (only parsing).

Not kept: Zcompare_egal_dec