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.

(************************************************************************)
(*         *   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)         *)
(************************************************************************)

Require Import Sumbool.

Require Import BinInt.
Require Import Zorder.
Require Import Zcompare.
Local Open Scope Z_scope.

(* begin hide *)
(* Trivial, to deprecate? *)
Lemma Dcompare_inf : forall r:comparison, {r = Eq} + {r = Lt} + {r = Gt}.forall r : comparison, {r = Eq} + {r = Lt} + {r = Gt}
Proof.forall r : comparison, {r = Eq} + {r = Lt} + {r = Gt}
  induction r; auto.
Defined.
(* end hide *)

Lemma Zcompare_rect (P:Type) (n m:Z) :
  ((n ?= m) = Eq -> P) -> ((n ?= m) = Lt -> P) -> ((n ?= m) = Gt -> P) -> P.P:Type
n, m:Z
((n ?= m) = Eq -> P) ->
((n ?= m) = Lt -> P) -> ((n ?= m) = Gt -> P) -> P
Proof.P:Type
n, m:Z
((n ?= m) = Eq -> P) ->
((n ?= m) = Lt -> P) -> ((n ?= m) = Gt -> P) -> P
  intros H1 H2 H3.P:Type
n, m:Z
H1:(n ?= m) = Eq -> P
H2:(n ?= m) = Lt -> P
H3:(n ?= m) = Gt -> P
P
  destruct (n ?= m); auto.
Defined.

Lemma Zcompare_rec (P:Set) (n m:Z) :
  ((n ?= m) = Eq -> P) -> ((n ?= m) = Lt -> P) -> ((n ?= m) = Gt -> P) -> P.P:Set
n, m:Z
((n ?= m) = Eq -> P) ->
((n ?= m) = Lt -> P) -> ((n ?= m) = Gt -> P) -> P
Proof.P:Set
n, m:Z
((n ?= m) = Eq -> P) ->
((n ?= m) = Lt -> P) -> ((n ?= m) = Gt -> P) -> P apply Zcompare_rect. Defined.

Section decidability.

  Variables x y : Z.

Decidability of order on binary integers

  Definition Z_lt_dec : {x < y} + {~ x < y}.x, y:Z
{x < y} + {~ x < y}
  Proof.x, y:Z
{x < y} + {~ x < y}
    unfold Z.lt; case Z.compare; (now left) || (now right).
  Defined.

  Definition Z_le_dec : {x <= y} + {~ x <= y}.x, y:Z
{x <= y} + {~ x <= y}
  Proof.x, y:Z
{x <= y} + {~ x <= y}
    unfold Z.le; case Z.compare; (now left) || (right; tauto).
  Defined.

  Definition Z_gt_dec : {x > y} + {~ x > y}.x, y:Z
{x > y} + {~ x > y}
  Proof.x, y:Z
{x > y} + {~ x > y}
    unfold Z.gt; case Z.compare; (now left) || (now right).
  Defined.

  Definition Z_ge_dec : {x >= y} + {~ x >= y}.x, y:Z
{x >= y} + {~ x >= y}
  Proof.x, y:Z
{x >= y} + {~ x >= y}
    unfold Z.ge; case Z.compare; (now left) || (right; tauto).
  Defined.

  Definition Z_lt_ge_dec : {x < y} + {x >= y}.x, y:Z
{x < y} + {x >= y}
  Proof.x, y:Z
{x < y} + {x >= y}
    exact Z_lt_dec.
  Defined.

  Lemma Z_lt_le_dec : {x < y} + {y <= x}.x, y:Z
{x < y} + {y <= x}
  Proof.x, y:Z
{x < y} + {y <= x}
    elim Z_lt_ge_dec.x, y:Z
x < y -> {x < y} + {y <= x}
x, y:Z
x >= y -> {x < y} + {y <= x}
    *x, y:Z
x < y -> {x < y} + {y <= x} now left.
    *x, y:Z
x >= y -> {x < y} + {y <= x} right; now apply Z.ge_le.
  Defined.

  Definition Z_le_gt_dec : {x <= y} + {x > y}.x, y:Z
{x <= y} + {x > y}
  Proof.x, y:Z
{x <= y} + {x > y}
    elim Z_le_dec; auto with arith.x, y:Z
~ x <= y -> {x <= y} + {x > y}
    intro.x, y:Z
b:~ x <= y
{x <= y} + {x > y} right.x, y:Z
b:~ x <= y
x > y Z.swap_greater.x, y:Z
b:~ x <= y
y < x now apply Z.nle_gt.
  Defined.

  Definition Z_gt_le_dec : {x > y} + {x <= y}.x, y:Z
{x > y} + {x <= y}
  Proof.x, y:Z
{x > y} + {x <= y}
    exact Z_gt_dec.
  Defined.

  Definition Z_ge_lt_dec : {x >= y} + {x < y}.x, y:Z
{x >= y} + {x < y}
  Proof.x, y:Z
{x >= y} + {x < y}
    elim Z_ge_dec; auto with arith.x, y:Z
~ x >= y -> {x >= y} + {x < y}
    intro.x, y:Z
b:~ x >= y
{x >= y} + {x < y} right.x, y:Z
b:~ x >= y
x < y Z.swap_greater.x, y:Z
b:~ y <= x
x < y now apply Z.lt_nge.
  Defined.

  Definition Z_le_lt_eq_dec : x <= y -> {x < y} + {x = y}.x, y:Z
x <= y -> {x < y} + {x = y}
  Proof.x, y:Z
x <= y -> {x < y} + {x = y}
    intro H.x, y:Z
H:x <= y
{x < y} + {x = y}
    apply Zcompare_rec with (n := x) (m := y).x, y:Z
H:x <= y
(x ?= y) = Eq -> {x < y} + {x = y}
x, y:Z
H:x <= y
(x ?= y) = Lt -> {x < y} + {x = y}
x, y:Z
H:x <= y
(x ?= y) = Gt -> {x < y} + {x = y}
    intro.x, y:Z
H:x <= y
H0:(x ?= y) = Eq
{x < y} + {x = y}
x, y:Z
H:x <= y
(x ?= y) = Lt -> {x < y} + {x = y}
x, y:Z
H:x <= y
(x ?= y) = Gt -> {x < y} + {x = y} right.x, y:Z
H:x <= y
H0:(x ?= y) = Eq
x = y
x, y:Z
H:x <= y
(x ?= y) = Lt -> {x < y} + {x = y}
x, y:Z
H:x <= y
(x ?= y) = Gt -> {x < y} + {x = y} elim (Z.compare_eq_iff x y); auto with arith.x, y:Z
H:x <= y
(x ?= y) = Lt -> {x < y} + {x = y}
x, y:Z
H:x <= y
(x ?= y) = Gt -> {x < y} + {x = y}
    intro.x, y:Z
H:x <= y
H0:(x ?= y) = Lt
{x < y} + {x = y}
x, y:Z
H:x <= y
(x ?= y) = Gt -> {x < y} + {x = y} left.x, y:Z
H:x <= y
H0:(x ?= y) = Lt
x < y
x, y:Z
H:x <= y
(x ?= y) = Gt -> {x < y} + {x = y} elim (Z.compare_eq_iff x y); auto with arith.x, y:Z
H:x <= y
(x ?= y) = Gt -> {x < y} + {x = y}
    intro H1.x, y:Z
H:x <= y
H1:(x ?= y) = Gt
{x < y} + {x = y} absurd (x > y); auto with arith.
  Defined.

End decidability.

Cotransitivity of order on binary integers

Lemma Zlt_cotrans : forall n m:Z, n < m -> forall p:Z, {n < p} + {p < m}.forall n m : Z,
n < m -> forall p : Z, {n < p} + {p < m}
Proof.forall n m : Z,
n < m -> forall p : Z, {n < p} + {p < m}
  intros x y H z.x, y:Z
H:x < y
z:Z
{x < z} + {z < y}
  case (Z_lt_ge_dec x z).x, y:Z
H:x < y
z:Z
x < z -> {x < z} + {z < y}
x, y:Z
H:x < y
z:Z
x >= z -> {x < z} + {z < y}
  intro.x, y:Z
H:x < y
z:Z
l:x < z
{x < z} + {z < y}
x, y:Z
H:x < y
z:Z
x >= z -> {x < z} + {z < y}
  left.x, y:Z
H:x < y
z:Z
l:x < z
x < z
x, y:Z
H:x < y
z:Z
x >= z -> {x < z} + {z < y}
  assumption.x, y:Z
H:x < y
z:Z
x >= z -> {x < z} + {z < y}
  intro.x, y:Z
H:x < y
z:Z
g:x >= z
{x < z} + {z < y}
  right.x, y:Z
H:x < y
z:Z
g:x >= z
z < y
  apply Z.le_lt_trans with (m := x).x, y:Z
H:x < y
z:Z
g:x >= z
z <= x
x, y:Z
H:x < y
z:Z
g:x >= z
x < y
  apply Z.ge_le.x, y:Z
H:x < y
z:Z
g:x >= z
x >= z
x, y:Z
H:x < y
z:Z
g:x >= z
x < y
  assumption.x, y:Z
H:x < y
z:Z
g:x >= z
x < y
  assumption.
Defined.

Lemma Zlt_cotrans_pos : forall n m:Z, 0 < n + m -> {0 < n} + {0 < m}.forall n m : Z, 0 < n + m -> {0 < n} + {0 < m}
Proof.forall n m : Z, 0 < n + m -> {0 < n} + {0 < m}
  intros x y H.x, y:Z
H:0 < x + y
{0 < x} + {0 < y}
  case (Zlt_cotrans 0 (x + y) H x).x, y:Z
H:0 < x + y
0 < x -> {0 < x} + {0 < y}
x, y:Z
H:0 < x + y
x < x + y -> {0 < x} + {0 < y}
  -x, y:Z
H:0 < x + y
0 < x -> {0 < x} + {0 < y} now left.
  -x, y:Z
H:0 < x + y
x < x + y -> {0 < x} + {0 < y} right.x, y:Z
H:0 < x + y
l:x < x + y
0 < y
    apply Z.add_lt_mono_l with (p := x).x, y:Z
H:0 < x + y
l:x < x + y
x + 0 < x + y
    now rewrite Z.add_0_r.
Defined.

Lemma Zlt_cotrans_neg : forall n m:Z, n + m < 0 -> {n < 0} + {m < 0}.forall n m : Z, n + m < 0 -> {n < 0} + {m < 0}
Proof.forall n m : Z, n + m < 0 -> {n < 0} + {m < 0}
  intros x y H; case (Zlt_cotrans (x + y) 0 H x); intro Hxy;
    [ right; apply Z.add_lt_mono_l with (p := x); rewrite Z.add_0_r | left ];
    assumption.
Defined.

Lemma not_Zeq_inf : forall n m:Z, n <> m -> {n < m} + {m < n}.forall n m : Z, n <> m -> {n < m} + {m < n}
Proof.forall n m : Z, n <> m -> {n < m} + {m < n}
  intros x y H.x, y:Z
H:x <> y
{x < y} + {y < x}
  case Z_lt_ge_dec with x y.x, y:Z
H:x <> y
x < y -> {x < y} + {y < x}
x, y:Z
H:x <> y
x >= y -> {x < y} + {y < x}
  intro.x, y:Z
H:x <> y
l:x < y
{x < y} + {y < x}
x, y:Z
H:x <> y
x >= y -> {x < y} + {y < x}
  left.x, y:Z
H:x <> y
l:x < y
x < y
x, y:Z
H:x <> y
x >= y -> {x < y} + {y < x}
  assumption.x, y:Z
H:x <> y
x >= y -> {x < y} + {y < x}
  intro H0.x, y:Z
H:x <> y
H0:x >= y
{x < y} + {y < x}
  generalize (Z.ge_le _ _ H0).x, y:Z
H:x <> y
H0:x >= y
y <= x -> {x < y} + {y < x}
  intro.x, y:Z
H:x <> y
H0:x >= y
H1:y <= x
{x < y} + {y < x}
  case (Z_le_lt_eq_dec _ _ H1).x, y:Z
H:x <> y
H0:x >= y
H1:y <= x
y < x -> {x < y} + {y < x}
x, y:Z
H:x <> y
H0:x >= y
H1:y <= x
y = x -> {x < y} + {y < x}
  intro.x, y:Z
H:x <> y
H0:x >= y
H1:y <= x
l:y < x
{x < y} + {y < x}
x, y:Z
H:x <> y
H0:x >= y
H1:y <= x
y = x -> {x < y} + {y < x}
  right.x, y:Z
H:x <> y
H0:x >= y
H1:y <= x
l:y < x
y < x
x, y:Z
H:x <> y
H0:x >= y
H1:y <= x
y = x -> {x < y} + {y < x}
  assumption.x, y:Z
H:x <> y
H0:x >= y
H1:y <= x
y = x -> {x < y} + {y < x}
  intro.x, y:Z
H:x <> y
H0:x >= y
H1:y <= x
e:y = x
{x < y} + {y < x}
  apply False_rec.x, y:Z
H:x <> y
H0:x >= y
H1:y <= x
e:y = x
False
  apply H.x, y:Z
H:x <> y
H0:x >= y
H1:y <= x
e:y = x
x = y
  symmetry .x, y:Z
H:x <> y
H0:x >= y
H1:y <= x
e:y = x
y = x
  assumption.
Defined.

Lemma Z_dec : forall n m:Z, {n < m} + {n > m} + {n = m}.forall n m : Z, {n < m} + {n > m} + {n = m}
Proof.forall n m : Z, {n < m} + {n > m} + {n = m}
  intros x y.x, y:Z
{x < y} + {x > y} + {x = y}
  case (Z_lt_ge_dec x y).x, y:Z
x < y -> {x < y} + {x > y} + {x = y}
x, y:Z
x >= y -> {x < y} + {x > y} + {x = y}
  intro H.x, y:Z
H:x < y
{x < y} + {x > y} + {x = y}
x, y:Z
x >= y -> {x < y} + {x > y} + {x = y}
  left.x, y:Z
H:x < y
{x < y} + {x > y}
x, y:Z
x >= y -> {x < y} + {x > y} + {x = y}
  left.x, y:Z
H:x < y
x < y
x, y:Z
x >= y -> {x < y} + {x > y} + {x = y}
  assumption.x, y:Z
x >= y -> {x < y} + {x > y} + {x = y}
  intro H.x, y:Z
H:x >= y
{x < y} + {x > y} + {x = y}
  generalize (Z.ge_le _ _ H).x, y:Z
H:x >= y
y <= x -> {x < y} + {x > y} + {x = y}
  intro H0.x, y:Z
H:x >= y
H0:y <= x
{x < y} + {x > y} + {x = y}
  case (Z_le_lt_eq_dec y x H0).x, y:Z
H:x >= y
H0:y <= x
y < x -> {x < y} + {x > y} + {x = y}
x, y:Z
H:x >= y
H0:y <= x
y = x -> {x < y} + {x > y} + {x = y}
  intro H1.x, y:Z
H:x >= y
H0:y <= x
H1:y < x
{x < y} + {x > y} + {x = y}
x, y:Z
H:x >= y
H0:y <= x
y = x -> {x < y} + {x > y} + {x = y}
  left.x, y:Z
H:x >= y
H0:y <= x
H1:y < x
{x < y} + {x > y}
x, y:Z
H:x >= y
H0:y <= x
y = x -> {x < y} + {x > y} + {x = y}
  right.x, y:Z
H:x >= y
H0:y <= x
H1:y < x
x > y
x, y:Z
H:x >= y
H0:y <= x
y = x -> {x < y} + {x > y} + {x = y}
  apply Z.lt_gt.x, y:Z
H:x >= y
H0:y <= x
H1:y < x
y < x
x, y:Z
H:x >= y
H0:y <= x
y = x -> {x < y} + {x > y} + {x = y}
  assumption.x, y:Z
H:x >= y
H0:y <= x
y = x -> {x < y} + {x > y} + {x = y}
  intro.x, y:Z
H:x >= y
H0:y <= x
e:y = x
{x < y} + {x > y} + {x = y}
  right.x, y:Z
H:x >= y
H0:y <= x
e:y = x
x = y
  symmetry .x, y:Z
H:x >= y
H0:y <= x
e:y = x
y = x
  assumption.
Defined.


Lemma Z_dec' : forall n m:Z, {n < m} + {m < n} + {n = m}.forall n m : Z, {n < m} + {m < n} + {n = m}
Proof.forall n m : Z, {n < m} + {m < n} + {n = m}
  intros x y.x, y:Z
{x < y} + {y < x} + {x = y}
  case (Z.eq_dec x y); intro H;
    [ right; assumption | left; apply (not_Zeq_inf _ _ H) ].
Defined.

(* begin hide *)
(* To deprecate ? *)
Corollary Z_zerop : forall x:Z, {x = 0} + {x <> 0}.forall x : Z, {x = 0} + {x <> 0}
Proof.forall x : Z, {x = 0} + {x <> 0}
  exact (fun x:Z => Z.eq_dec x 0).
Defined.

Corollary Z_notzerop : forall (x:Z), {x <> 0} + {x = 0}.forall x : Z, {x <> 0} + {x = 0}
Proof (fun x => sumbool_not _ _ (Z_zerop x)).

Corollary Z_noteq_dec : forall (x y:Z), {x <> y} + {x = y}.forall x y : Z, {x <> y} + {x = y}
Proof (fun x y => sumbool_not _ _ (Z.eq_dec x y)).
(* end hide *)