Library Coq.Arith.Compare_dec
Require Import PeanoNat Decidable.
Local Open Scope nat_scope.
Implicit Types m n x y : nat.
Definition zerop n : {n = 0} + {0 < n}.
Definition lt_eq_lt_dec n m : {n < m} + {n = m} + {m < n}.
Definition gt_eq_gt_dec n m : {m > n} + {n = m} + {n > m}.
Definition le_lt_dec n m : {n <= m} + {m < n}.
Definition le_le_S_dec n m : {n <= m} + {S m <= n}.
Definition le_ge_dec n m : {n <= m} + {n >= m}.
Definition le_gt_dec n m : {n <= m} + {n > m}.
Definition le_lt_eq_dec n m : n <= m -> {n < m} + {n = m}.
Theorem le_dec n m : {n <= m} + {~ n <= m}.
Theorem lt_dec n m : {n < m} + {~ n < m}.
Theorem gt_dec n m : {n > m} + {~ n > m}.
Theorem ge_dec n m : {n >= m} + {~ n >= m}.
Register le_gt_dec as num.nat.le_gt_dec.
Proofs of decidability
Theorem dec_le n m : decidable (n <= m).
Theorem dec_lt n m : decidable (n < m).
Theorem dec_gt n m : decidable (n > m).
Theorem dec_ge n m : decidable (n >= m).
Theorem not_eq n m : n <> m -> n < m \/ m < n.
Theorem not_le n m : ~ n <= m -> n > m.
Theorem not_gt n m : ~ n > m -> n <= m.
Theorem not_ge n m : ~ n >= m -> n < m.
Theorem not_lt n m : ~ n < m -> n >= m.
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.
Lemma nat_compare_gt n m : n>m <-> (n ?= m) = Gt.
Lemma nat_compare_le n m : n<=m <-> (n ?= m) <> Gt.
Lemma nat_compare_ge n m : n>=m <-> (n ?= m) <> Lt.
Some projections of the above equivalences.
Lemma nat_compare_eq n m : (n ?= m) = Eq -> n = m.
Lemma nat_compare_Lt_lt n m : (n ?= m) = Lt -> n<m.
Lemma nat_compare_Gt_gt n m : (n ?= m) = Gt -> n>m.
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.
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.
Lemma leb_correct m n : m <= n -> (m <=? n) = true.
Lemma leb_complete m n : (m <=? n) = true -> m <= n.
Lemma leb_correct_conv m n : m < n -> (n <=? m) = false.
Lemma leb_complete_conv m n : (n <=? m) = false -> m < n.
Lemma leb_compare n m : (n <=? m) = true <-> (n ?= m) <> Gt.
Require Import Le Lt Gt.