Compare_dec.v

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 Le Lt Gt Decidable PeanoNat.

Local Open Scope nat_scope.

Implicit Types m n x y : nat.

Definition zerop n : {n = 0} + {0 < n}.n:nat
{n = 0} + {0 < n}
Proof.n:nat
{n = 0} + {0 < n}
  destruct n; auto with arith.
Defined.

Definition lt_eq_lt_dec n m : {n < m} + {n = m} + {m < n}.n, m:nat
{n < m} + {n = m} + {m < n}
Proof.n, m:nat
{n < m} + {n = m} + {m < n}
  induction n in m |- *; destruct m; auto with arith.n, m:nat
IHn:forall m0 : nat, {n < m0} + {n = m0} + {m0 < n}
{S n < S m} + {S n = S m} + {S m < S n}
  destruct (IHn m) as [H|H]; auto with arith.n, m:nat
IHn:forall m0 : nat, {n < m0} + {n = m0} + {m0 < n}
H:{n < m} + {n = m}
{S n < S m} + {S n = S m} + {S m < S n}
  destruct H; auto with arith.
Defined.

Definition gt_eq_gt_dec n m : {m > n} + {n = m} + {n > m}.n, m:nat
{m > n} + {n = m} + {n > m}
Proof.n, m:nat
{m > n} + {n = m} + {n > m}
  now apply lt_eq_lt_dec.
Defined.

Definition le_lt_dec n m : {n <= m} + {m < n}.n, m:nat
{n <= m} + {m < n}
Proof.n, m:nat
{n <= m} + {m < n}
  induction n in m |- *.m:nat
{0 <= m} + {m < 0}
n, m:nat
IHn:forall m0 : nat, {n <= m0} + {m0 < n}
{S n <= m} + {m < S n}
  -m:nat
{0 <= m} + {m < 0} left; auto with arith.
  -n, m:nat
IHn:forall m0 : nat, {n <= m0} + {m0 < n}
{S n <= m} + {m < S n} destruct m.n:nat
IHn:forall m : nat, {n <= m} + {m < n}
{S n <= 0} + {0 < S n}
n, m:nat
IHn:forall m0 : nat, {n <= m0} + {m0 < n}
{S n <= S m} + {S m < S n}
    +n:nat
IHn:forall m : nat, {n <= m} + {m < n}
{S n <= 0} + {0 < S n} right; auto with arith.
    +n, m:nat
IHn:forall m0 : nat, {n <= m0} + {m0 < n}
{S n <= S m} + {S m < S n} elim (IHn m); [left|right]; auto with arith.
Defined.

Definition le_le_S_dec n m : {n <= m} + {S m <= n}.n, m:nat
{n <= m} + {S m <= n}
Proof.n, m:nat
{n <= m} + {S m <= n}
  exact (le_lt_dec n m).
Defined.

Definition le_ge_dec n m : {n <= m} + {n >= m}.n, m:nat
{n <= m} + {n >= m}
Proof.n, m:nat
{n <= m} + {n >= m}
  elim (le_lt_dec n m); auto with arith.
Defined.

Definition le_gt_dec n m : {n <= m} + {n > m}.n, m:nat
{n <= m} + {n > m}
Proof.n, m:nat
{n <= m} + {n > m}
  exact (le_lt_dec n m).
Defined.

Definition le_lt_eq_dec n m : n <= m -> {n < m} + {n = m}.n, m:nat
n <= m -> {n < m} + {n = m}
Proof.n, m:nat
n <= m -> {n < m} + {n = m}
  intros; destruct (lt_eq_lt_dec n m); auto with arith.n, m:nat
H:n <= m
l:m < n
{n < m} + {n = m}
  intros; absurd (m < n); auto with arith.
Defined.

Theorem le_dec n m : {n <= m} + {~ n <= m}.n, m:nat
{n <= m} + {~ n <= m}
Proof.n, m:nat
{n <= m} + {~ n <= m}
  destruct (le_gt_dec n m).n, m:nat
l:n <= m
{n <= m} + {~ n <= m}
n, m:nat
g:n > m
{n <= m} + {~ n <= m}
  -n, m:nat
l:n <= m
{n <= m} + {~ n <= m} now left.
  -n, m:nat
g:n > m
{n <= m} + {~ n <= m} right.n, m:nat
g:n > m
~ n <= m now apply gt_not_le.
Defined.

Theorem lt_dec n m : {n < m} + {~ n < m}.n, m:nat
{n < m} + {~ n < m}
Proof.n, m:nat
{n < m} + {~ n < m}
  apply le_dec.
Defined.

Theorem gt_dec n m : {n > m} + {~ n > m}.n, m:nat
{n > m} + {~ n > m}
Proof.n, m:nat
{n > m} + {~ n > m}
  apply lt_dec.
Defined.

Theorem ge_dec n m : {n >= m} + {~ n >= m}.n, m:nat
{n >= m} + {~ n >= m}
Proof.n, m:nat
{n >= m} + {~ n >= m}
  apply le_dec.
Defined.

Register le_gt_dec as num.nat.le_gt_dec.

Proofs of decidability

Theorem dec_le n m : decidable (n <= m).n, m:nat
decidable (n <= m)
Proof.n, m:nat
decidable (n <= m)
  apply Nat.le_decidable.
Qed.

Theorem dec_lt n m : decidable (n < m).n, m:nat
decidable (n < m)
Proof.n, m:nat
decidable (n < m)
  apply Nat.lt_decidable.
Qed.

Theorem dec_gt n m : decidable (n > m).n, m:nat
decidable (n > m)
Proof.n, m:nat
decidable (n > m)
  apply Nat.lt_decidable.
Qed.

Theorem dec_ge n m : decidable (n >= m).n, m:nat
decidable (n >= m)
Proof.n, m:nat
decidable (n >= m)
  apply Nat.le_decidable.
Qed.

Theorem not_eq n m : n <> m -> n < m \/ m < n.n, m:nat
n <> m -> n < m \/ m < n
Proof.n, m:nat
n <> m -> n < m \/ m < n
  apply Nat.lt_gt_cases.
Qed.

Theorem not_le n m : ~ n <= m -> n > m.n, m:nat
~ n <= m -> n > m
Proof.n, m:nat
~ n <= m -> n > m
  apply Nat.nle_gt.
Qed.

Theorem not_gt n m : ~ n > m -> n <= m.n, m:nat
~ n > m -> n <= m
Proof.n, m:nat
~ n > m -> n <= m
  apply Nat.nlt_ge.
Qed.

Theorem not_ge n m : ~ n >= m -> n < m.n, m:nat
~ n >= m -> n < m
Proof.n, m:nat
~ n >= m -> n < m
  apply Nat.nle_gt.
Qed.

Theorem not_lt n m : ~ n < m -> n >= m.n, m:nat
~ n < m -> n >= m
Proof.n, m:nat
~ n < m -> n >= m
  apply Nat.nlt_ge.
Qed.

Register dec_le as num.nat.dec_le.
Register dec_lt as num.nat.dec_lt.
Register dec_ge as num.nat.dec_ge.
Register dec_gt as num.nat.dec_gt.
Register not_eq as num.nat.not_eq.
Register not_le as num.nat.not_le.
Register not_lt as num.nat.not_lt.
Register not_ge as num.nat.not_ge.
Register not_gt as num.nat.not_gt.

A ternary comparison function in the spirit of Z.compare. See now Nat.compare and its properties. In scope nat_scope, the notation for Nat.compare is "?="

Notation nat_compare_S := Nat.compare_succ (only parsing).

Lemma nat_compare_lt n m : n<m <-> (n ?= m) = Lt.n, m:nat
n < m <-> (n ?= m) = Lt
Proof.n, m:nat
n < m <-> (n ?= m) = Lt
 symmetry.n, m:nat
(n ?= m) = Lt <-> n < m apply Nat.compare_lt_iff.
Qed.

Lemma nat_compare_gt n m : n>m <-> (n ?= m) = Gt.n, m:nat
n > m <-> (n ?= m) = Gt
Proof.n, m:nat
n > m <-> (n ?= m) = Gt
 symmetry.n, m:nat
(n ?= m) = Gt <-> n > m apply Nat.compare_gt_iff.
Qed.

Lemma nat_compare_le n m : n<=m <-> (n ?= m) <> Gt.n, m:nat
n <= m <-> (n ?= m) <> Gt
Proof.n, m:nat
n <= m <-> (n ?= m) <> Gt
 symmetry.n, m:nat
(n ?= m) <> Gt <-> n <= m apply Nat.compare_le_iff.
Qed.

Lemma nat_compare_ge n m : n>=m <-> (n ?= m) <> Lt.n, m:nat
n >= m <-> (n ?= m) <> Lt
Proof.n, m:nat
n >= m <-> (n ?= m) <> Lt
 symmetry.n, m:nat
(n ?= m) <> Lt <-> n >= m apply Nat.compare_ge_iff.
Qed.

Some projections of the above equivalences.

Lemma nat_compare_eq n m : (n ?= m) = Eq -> n = m.n, m:nat
(n ?= m) = Eq -> n = m
Proof.n, m:nat
(n ?= m) = Eq -> n = m
  apply Nat.compare_eq_iff.
Qed.

Lemma nat_compare_Lt_lt n m : (n ?= m) = Lt -> n<m.n, m:nat
(n ?= m) = Lt -> n < m
Proof.n, m:nat
(n ?= m) = Lt -> n < m
  apply Nat.compare_lt_iff.
Qed.

Lemma nat_compare_Gt_gt n m : (n ?= m) = Gt -> n>m.n, m:nat
(n ?= m) = Gt -> n > m
Proof.n, m:nat
(n ?= m) = Gt -> n > m
  apply Nat.compare_gt_iff.
Qed.

A previous definition of nat_compare in terms of lt_eq_lt_dec. The new version avoids the creation of proof parts.

Definition nat_compare_alt (n m:nat) :=
  match lt_eq_lt_dec n m with
    | inleft (left _) => Lt
    | inleft (right _) => Eq
    | inright _ => Gt
  end.

Lemma nat_compare_equiv n m : (n ?= m) = nat_compare_alt n m.n, m:nat
(n ?= m) = nat_compare_alt n m
Proof.n, m:nat
(n ?= m) = nat_compare_alt n m
  unfold nat_compare_alt; destruct lt_eq_lt_dec as [[|]|].n, m:nat
l:n < m
(n ?= m) = Lt
n, m:nat
e:n = m
(n ?= m) = Eq
n, m:nat
l:m < n
(n ?= m) = Gt
  -n, m:nat
l:n < m
(n ?= m) = Lt now apply Nat.compare_lt_iff.
  -n, m:nat
e:n = m
(n ?= m) = Eq now apply Nat.compare_eq_iff.
  -n, m:nat
l:m < n
(n ?= m) = Gt now apply Nat.compare_gt_iff.
Qed.

A boolean version of le over nat. See now Nat.leb and its properties. In scope nat_scope, the notation for Nat.leb is "<=?"

Notation leb := Nat.leb (only parsing).

Notation leb_iff := Nat.leb_le (only parsing).

Lemma leb_iff_conv m n : (n <=? m) = false <-> m < n.m, n:nat
(n <=? m) = false <-> m < n
Proof.m, n:nat
(n <=? m) = false <-> m < n
 rewrite Nat.leb_nle.m, n:nat
~ n <= m <-> m < n apply Nat.nle_gt.
Qed.

Lemma leb_correct m n : m <= n -> (m <=? n) = true.m, n:nat
m <= n -> (m <=? n) = true
Proof.m, n:nat
m <= n -> (m <=? n) = true
 apply Nat.leb_le.
Qed.

Lemma leb_complete m n : (m <=? n) = true -> m <= n.m, n:nat
(m <=? n) = true -> m <= n
Proof.m, n:nat
(m <=? n) = true -> m <= n
 apply Nat.leb_le.
Qed.

Lemma leb_correct_conv m n : m < n -> (n <=? m) = false.m, n:nat
m < n -> (n <=? m) = false
Proof.m, n:nat
m < n -> (n <=? m) = false
 apply leb_iff_conv.
Qed.

Lemma leb_complete_conv m n : (n <=? m) = false -> m < n.m, n:nat
(n <=? m) = false -> m < n
Proof.m, n:nat
(n <=? m) = false -> m < n
 apply leb_iff_conv.
Qed.

Lemma leb_compare n m : (n <=? m) = true <-> (n ?= m) <> Gt.n, m:nat
(n <=? m) = true <-> (n ?= m) <> Gt
Proof.n, m:nat
(n <=? m) = true <-> (n ?= m) <> Gt
 rewrite Nat.compare_le_iff.n, m:nat
(n <=? m) = true <-> n <= m apply Nat.leb_le.
Qed.