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 Bool Basics OrdersTac.
Require Export Orders.

Set Implicit Arguments.
Unset Strict Implicit.

Properties of compare

Module Type CompareFacts (Import O:DecStrOrder').

 Local Infix "?=" := compare (at level 70, no associativity).

 Lemma compare_eq_iff x y : (x ?= y) = Eq <-> x==y.x, y:t
(x ?= y) = Eq <-> x == y
 Proof.x, y:t
(x ?= y) = Eq <-> x == y
 case compare_spec; intro H; split; try easy; intro EQ;
  contradict H; rewrite EQ; apply irreflexivity.
 Qed.

 Lemma compare_eq x y : (x ?= y) = Eq -> x==y.x, y:t
(x ?= y) = Eq -> x == y
 Proof.x, y:t
(x ?= y) = Eq -> x == y
 apply compare_eq_iff.
 Qed.

 Lemma compare_lt_iff x y : (x ?= y) = Lt <-> x<y.x, y:t
(x ?= y) = Lt <-> x < y
 Proof.x, y:t
(x ?= y) = Lt <-> x < y
  case compare_spec; intro H; split; try easy; intro LT;
  contradict LT; rewrite H; apply irreflexivity.
 Qed.

 Lemma compare_gt_iff x y : (x ?= y) = Gt <-> y<x.x, y:t
(x ?= y) = Gt <-> y < x
 Proof.x, y:t
(x ?= y) = Gt <-> y < x
 case compare_spec; intro H; split; try easy; intro LT;
  contradict LT; rewrite H; apply irreflexivity.
 Qed.

 Lemma compare_nlt_iff x y : (x ?= y) <> Lt <-> ~(x<y).x, y:t
(x ?= y) <> Lt <-> ~ x < y
 Proof.x, y:t
(x ?= y) <> Lt <-> ~ x < y
 rewrite compare_lt_iff; intuition.
 Qed.

 Lemma compare_ngt_iff x y : (x ?= y) <> Gt <-> ~(y<x).x, y:t
(x ?= y) <> Gt <-> ~ y < x
 Proof.x, y:t
(x ?= y) <> Gt <-> ~ y < x
 rewrite compare_gt_iff; intuition.
 Qed.

 Hint Rewrite compare_eq_iff compare_lt_iff compare_gt_iff : order.

 Instance compare_compat : Proper (eq==>eq==>Logic.eq) compare.Proper (eq ==> eq ==> Logic.eq) compare
 Proof.Proper (eq ==> eq ==> Logic.eq) compare
 intros x x' Hxx' y y' Hyy'.x, x':t
Hxx':x == x'
y, y':t
Hyy':y == y'
(x ?= y) = (x' ?= y')
 case (compare_spec x' y'); autorewrite with order; now rewrite Hxx', Hyy'.
 Qed.

 Lemma compare_refl x : (x ?= x) = Eq.x:t
(x ?= x) = Eq
 Proof.x:t
(x ?= x) = Eq
 case compare_spec; intros; trivial; now elim irreflexivity with x.
 Qed.

 Lemma compare_antisym x y : (y ?= x) = CompOpp (x ?= y).x, y:t
(y ?= x) = CompOpp (x ?= y)
 Proof.x, y:t
(y ?= x) = CompOpp (x ?= y)
 case (compare_spec x y); simpl; autorewrite with order;
  trivial; now symmetry.
 Qed.

End CompareFacts.

Properties of OrderedTypeFull

Module OrderedTypeFullFacts (Import O:OrderedTypeFull').

 Module OrderTac := OTF_to_OrderTac O.
 Ltac order := OrderTac.order.
 Ltac iorder := intuition order.

 Instance le_compat : Proper (eq==>eq==>iff) le.Proper (eq ==> eq ==> iff) le
 Proof.Proper (eq ==> eq ==> iff) le repeat red; iorder. Qed.

 Instance le_preorder : PreOrder le.PreOrder le
 Proof.PreOrder le split; red; order. Qed.

 Instance le_order : PartialOrder eq le.PartialOrder eq le
 Proof.PartialOrder eq le compute; iorder. Qed.

 Instance le_antisym : Antisymmetric _ eq le.Antisymmetric t eq le
 Proof.Antisymmetric t eq le apply partial_order_antisym; auto with *. Qed.

 Lemma le_not_gt_iff : forall x y, x<=y <-> ~y<x.forall x y : t, x <= y <-> ~ y < x
 Proof.forall x y : t, x <= y <-> ~ y < x iorder. Qed.

 Lemma lt_not_ge_iff : forall x y, x<y <-> ~y<=x.forall x y : t, x < y <-> ~ y <= x
 Proof.forall x y : t, x < y <-> ~ y <= x iorder. Qed.

 Lemma le_or_gt : forall x y, x<=y \/ y<x.forall x y : t, x <= y \/ y < x
 Proof.forall x y : t, x <= y \/ y < x intros.x, y:t
x <= y \/ y < x rewrite le_lteq; destruct (O.compare_spec x y); auto. Qed.

 Lemma lt_or_ge : forall x y, x<y \/ y<=x.forall x y : t, x < y \/ y <= x
 Proof.forall x y : t, x < y \/ y <= x intros.x, y:t
x < y \/ y <= x rewrite le_lteq; destruct (O.compare_spec x y); iorder. Qed.

 Lemma eq_is_le_ge : forall x y, x==y <-> x<=y /\ y<=x.forall x y : t, x == y <-> x <= y <= x
 Proof.forall x y : t, x == y <-> x <= y <= x iorder. Qed.

 Include CompareFacts O.

 Lemma compare_le_iff x y : compare x y <> Gt <-> x<=y.x, y:t
(x ?= y) <> Gt <-> x <= y
 Proof.x, y:t
(x ?= y) <> Gt <-> x <= y
 rewrite le_not_gt_iff.x, y:t
(x ?= y) <> Gt <-> ~ y < x apply compare_ngt_iff.
 Qed.

 Lemma compare_ge_iff x y : compare x y <> Lt <-> y<=x.x, y:t
(x ?= y) <> Lt <-> y <= x
 Proof.x, y:t
(x ?= y) <> Lt <-> y <= x
 rewrite le_not_gt_iff.x, y:t
(x ?= y) <> Lt <-> ~ x < y apply compare_nlt_iff.
 Qed.

End OrderedTypeFullFacts.

Properties of OrderedType

Module OrderedTypeFacts (Import O: OrderedType').

  Module OrderTac := OT_to_OrderTac O.
  Ltac order := OrderTac.order.

  Declare Scope order.
  Notation "x <= y" := (~lt y x) : order.
  Infix "?=" := compare (at level 70, no associativity) : order.

  Local Open Scope order.

  Tactic Notation "elim_compare" constr(x) constr(y) :=
   destruct (compare_spec x y).

  Tactic Notation "elim_compare" constr(x) constr(y) "as" ident(h) :=
   destruct (compare_spec x y) as [h|h|h].

The following lemmas are either re-phrasing of eq_equiv and lt_strorder or immediately provable by order. Interest: compatibility, test of order, etc

  Definition eq_refl (x:t) : x==x := Equivalence_Reflexive x.

  Definition eq_sym (x y:t) : x==y -> y==x := Equivalence_Symmetric x y.

  Definition eq_trans (x y z:t) : x==y -> y==z -> x==z :=
   Equivalence_Transitive x y z.

  Definition lt_trans (x y z:t) : x<y -> y<z -> x<z :=
   StrictOrder_Transitive x y z.

  Definition lt_irrefl (x:t) : ~x<x := StrictOrder_Irreflexive x.

  Include CompareFacts O.
  Notation compare_le_iff := compare_ngt_iff (only parsing).
  Notation compare_ge_iff := compare_nlt_iff (only parsing).

For compatibility reasons

  Definition eq_dec := eq_dec.

  Lemma lt_dec : forall x y : t, {lt x y} + {~ lt x y}.forall x y : t, {x < y} + {y <= x}
  Proof.forall x y : t, {x < y} + {y <= x}
   intros x y; destruct (CompSpec2Type (compare_spec x y));
    [ right | left | right ]; order.
  Defined.

  Definition eqb x y : bool := if eq_dec x y then true else false.

  Lemma if_eq_dec : forall x y (B:Type)(b b':B),
    (if eq_dec x y then b else b') =
    (match compare x y with Eq => b | _ => b' end).forall (x y : t) (B : Type) (b b' : B),
(if eq_dec x y then b else b') =
match x ?= y with
| Eq => b
| _ => b'
end
  Proof.forall (x y : t) (B : Type) (b b' : B),
(if eq_dec x y then b else b') =
match x ?= y with
| Eq => b
| _ => b'
end
  intros; destruct eq_dec; elim_compare x y; auto; order.
  Qed.

  Lemma eqb_alt :
    forall x y, eqb x y = match compare x y with Eq => true | _ => false end.forall x y : t,
eqb x y =
match x ?= y with
| Eq => true
| _ => false
end
  Proof.forall x y : t,
eqb x y =
match x ?= y with
| Eq => true
| _ => false
end
  unfold eqb; intros; apply if_eq_dec.
  Qed.

  Instance eqb_compat : Proper (eq==>eq==>Logic.eq) eqb.Proper (eq ==> eq ==> Logic.eq) eqb
  Proof.Proper (eq ==> eq ==> Logic.eq) eqb
  intros x x' Hxx' y y' Hyy'.x, x':t
Hxx':x == x'
y, y':t
Hyy':y == y'
eqb x y = eqb x' y'
  rewrite 2 eqb_alt, Hxx', Hyy'; auto.
  Qed.

End OrderedTypeFacts.

Tests of the order tactic

Is it at least capable of proving some basic properties ?

Module OrderedTypeTest (Import O:OrderedType').
  Module Import MO := OrderedTypeFacts O.
  Local Open Scope order.
  Lemma lt_not_eq x y : x<y -> ~x==y.x, y:t
x < y -> x ~= y  Proof.x, y:t
x < y -> x ~= y order. Qed.
  Lemma lt_eq x y z : x<y -> y==z -> x<z.x, y, z:t
x < y -> y == z -> x < z Proof.x, y, z:t
x < y -> y == z -> x < z order. Qed.
  Lemma eq_lt x y z : x==y -> y<z -> x<z.x, y, z:t
x == y -> y < z -> x < z Proof.x, y, z:t
x == y -> y < z -> x < z order. Qed.
  Lemma le_eq x y z : x<=y -> y==z -> x<=z.x, y, z:t
x <= y -> y == z -> x <= z Proof.x, y, z:t
x <= y -> y == z -> x <= z order. Qed.
  Lemma eq_le x y z : x==y -> y<=z -> x<=z.x, y, z:t
x == y -> y <= z -> x <= z Proof.x, y, z:t
x == y -> y <= z -> x <= z order. Qed.
  Lemma neq_eq x y z : ~x==y -> y==z -> ~x==z.x, y, z:t
x ~= y -> y == z -> x ~= z Proof.x, y, z:t
x ~= y -> y == z -> x ~= z order. Qed.
  Lemma eq_neq x y z : x==y -> ~y==z -> ~x==z.x, y, z:t
x == y -> y ~= z -> x ~= z Proof.x, y, z:t
x == y -> y ~= z -> x ~= z order. Qed.
  Lemma le_lt_trans x y z : x<=y -> y<z -> x<z.x, y, z:t
x <= y -> y < z -> x < z Proof.x, y, z:t
x <= y -> y < z -> x < z order. Qed.
  Lemma lt_le_trans x y z : x<y -> y<=z -> x<z.x, y, z:t
x < y -> y <= z -> x < z Proof.x, y, z:t
x < y -> y <= z -> x < z order. Qed.
  Lemma le_trans x y z : x<=y -> y<=z -> x<=z.x, y, z:t
x <= y -> y <= z -> x <= z Proof.x, y, z:t
x <= y -> y <= z -> x <= z order. Qed.
  Lemma le_antisym x y : x<=y -> y<=x -> x==y.x, y:t
x <= y -> y <= x -> x == y Proof.x, y:t
x <= y -> y <= x -> x == y order. Qed.
  Lemma le_neq x y : x<=y -> ~x==y -> x<y.x, y:t
x <= y -> x ~= y -> x < y Proof.x, y:t
x <= y -> x ~= y -> x < y order. Qed.
  Lemma neq_sym x y : ~x==y -> ~y==x.x, y:t
x ~= y -> y ~= x Proof.x, y:t
x ~= y -> y ~= x order. Qed.
  Lemma lt_le x y : x<y -> x<=y.x, y:t
x < y -> x <= y Proof.x, y:t
x < y -> x <= y order. Qed.
  Lemma gt_not_eq x y : y<x -> ~x==y.x, y:t
y < x -> x ~= y Proof.x, y:t
y < x -> x ~= y order. Qed.
  Lemma eq_not_lt x y : x==y -> ~x<y.x, y:t
x == y -> y <= x Proof.x, y:t
x == y -> y <= x order. Qed.
  Lemma eq_not_gt x y : x==y -> ~ y<x.x, y:t
x == y -> x <= y Proof.x, y:t
x == y -> x <= y order. Qed.
  Lemma lt_not_gt x y : x<y -> ~ y<x.x, y:t
x < y -> x <= y Proof.x, y:t
x < y -> x <= y order. Qed.
  Lemma eq_is_nlt_ngt x y : x==y <-> ~x<y /\ ~y<x.x, y:t
x == y <-> y <= x /\ x <= y
  Proof.x, y:t
x == y <-> y <= x /\ x <= y intuition; order. Qed.
End OrderedTypeTest.

Reversed OrderedTypeFull.

we can switch the orientation of the order. This is used for example when deriving properties of min out of the ones of max (see GenericMinMax).

Module OrderedTypeRev (O:OrderedTypeFull) <: OrderedTypeFull.

Definition t := O.t.
Definition eq := O.eq.
Instance eq_equiv : Equivalence eq.
Definition eq_dec := O.eq_dec.

Definition lt := flip O.lt.
Definition le := flip O.le.

Instance lt_strorder: StrictOrder lt.StrictOrder lt
Proof.StrictOrder lt unfold lt; auto with *. Qed.
Instance lt_compat : Proper (eq==>eq==>iff) lt.Proper (eq ==> eq ==> iff) lt
Proof.Proper (eq ==> eq ==> iff) lt unfold lt; auto with *. Qed.

Lemma le_lteq : forall x y, le x y <-> lt x y \/ eq x y.forall x y : O.t, le x y <-> lt x y \/ eq x y
Proof.forall x y : O.t, le x y <-> lt x y \/ eq x y intros; unfold le, lt, flip.x, y:O.t
O.le y x <-> O.lt y x \/ eq x y rewrite O.le_lteq; intuition. Qed.

Definition compare := flip O.compare.

Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).forall x y : O.t, CompSpec eq lt x y (compare x y)
Proof.forall x y : O.t, CompSpec eq lt x y (compare x y)
intros; unfold compare, eq, lt, flip.x, y:O.t
CompSpec O.eq (fun x0 y0 : O.t => O.lt y0 x0) x y
  (O.compare y x)
destruct (O.compare_spec y x); auto with relations.
Qed.

End OrderedTypeRev.

Unset Implicit Arguments.

Order relations derived from a compare function.

We factorize here some common properties for ZArith, NArith and co, where lt and le are defined in terms of compare. Note that we do not require anything here concerning compatibility of compare w.r.t eq, nor anything concerning transitivity.

Module Type CompareBasedOrder (Import E:EqLtLe')(Import C:HasCmp E).
 Include CmpNotation E C.
 Include IsEq E.
 Axiom compare_eq_iff : forall x y, (x ?= y) = Eq <-> x == y.
 Axiom compare_lt_iff : forall x y, (x ?= y) = Lt <-> x < y.
 Axiom compare_le_iff : forall x y, (x ?= y) <> Gt <-> x <= y.
 Axiom compare_antisym : forall x y, (y ?= x) = CompOpp (x ?= y).
End CompareBasedOrder.

Module Type CompareBasedOrderFacts
 (Import E:EqLtLe')
 (Import C:HasCmp E)
 (Import O:CompareBasedOrder E C).

 Lemma compare_spec x y : CompareSpec (x==y) (x<y) (y<x) (x?=y).x, y:t
CompareSpec (x == y) (x < y) (y < x) (x ?= y)
 Proof.x, y:t
CompareSpec (x == y) (x < y) (y < x) (x ?= y)
  case_eq (compare x y); intros H; constructor.x, y:t
H:(x ?= y) = Eq
x == y
x, y:t
H:(x ?= y) = Lt
x < y
x, y:t
H:(x ?= y) = Gt
y < x
  -x, y:t
H:(x ?= y) = Eq
x == y now apply compare_eq_iff.
  -x, y:t
H:(x ?= y) = Lt
x < y now apply compare_lt_iff.
  -x, y:t
H:(x ?= y) = Gt
y < x rewrite compare_antisym, CompOpp_iff in H.x, y:t
H:(y ?= x) = CompOpp Gt
y < x now apply compare_lt_iff.
 Qed.

 Lemma compare_eq x y : (x ?= y) = Eq -> x==y.x, y:t
(x ?= y) = Eq -> x == y
 Proof.x, y:t
(x ?= y) = Eq -> x == y
 apply compare_eq_iff.
 Qed.

 Lemma compare_refl x : (x ?= x) = Eq.x:t
(x ?= x) = Eq
 Proof.x:t
(x ?= x) = Eq
 now apply compare_eq_iff.
 Qed.

 Lemma compare_gt_iff x y : (x ?= y) = Gt <-> y<x.x, y:t
(x ?= y) = Gt <-> y < x
 Proof.x, y:t
(x ?= y) = Gt <-> y < x
 now rewrite <- compare_lt_iff, compare_antisym, CompOpp_iff.
 Qed.

 Lemma compare_ge_iff x y : (x ?= y) <> Lt <-> y<=x.x, y:t
(x ?= y) <> Lt <-> y <= x
 Proof.x, y:t
(x ?= y) <> Lt <-> y <= x
 now rewrite <- compare_le_iff, compare_antisym, CompOpp_iff.
 Qed.

 Lemma compare_ngt_iff x y : (x ?= y) <> Gt <-> ~(y<x).x, y:t
(x ?= y) <> Gt <-> ~ y < x
 Proof.x, y:t
(x ?= y) <> Gt <-> ~ y < x
 rewrite compare_gt_iff; intuition.
 Qed.

 Lemma compare_nlt_iff x y : (x ?= y) <> Lt <-> ~(x<y).x, y:t
(x ?= y) <> Lt <-> ~ x < y
 Proof.x, y:t
(x ?= y) <> Lt <-> ~ x < y
 rewrite compare_lt_iff; intuition.
 Qed.

 Lemma compare_nle_iff x y : (x ?= y) = Gt <-> ~(x<=y).x, y:t
(x ?= y) = Gt <-> ~ x <= y
 Proof.x, y:t
(x ?= y) = Gt <-> ~ x <= y
 rewrite <- compare_le_iff.x, y:t
(x ?= y) = Gt <-> ~ (x ?= y) <> Gt
 destruct compare; split; easy || now destruct 1.
 Qed.

 Lemma compare_nge_iff x y : (x ?= y) = Lt <-> ~(y<=x).x, y:t
(x ?= y) = Lt <-> ~ y <= x
 Proof.x, y:t
(x ?= y) = Lt <-> ~ y <= x
 now rewrite <- compare_nle_iff, compare_antisym, CompOpp_iff.
 Qed.

 Lemma lt_irrefl x : ~ (x<x).x:t
~ x < x
 Proof.x:t
~ x < x
 now rewrite <- compare_lt_iff, compare_refl.
 Qed.

 Lemma lt_eq_cases n m : n <= m <-> n < m \/ n==m.n, m:t
n <= m <-> n < m \/ n == m
 Proof.n, m:t
n <= m <-> n < m \/ n == m
 rewrite <- compare_lt_iff, <- compare_le_iff, <- compare_eq_iff.n, m:t
(n ?= m) <> Gt <-> (n ?= m) = Lt \/ (n ?= m) = Eq
 destruct (n ?= m); now intuition.
 Qed.

End CompareBasedOrderFacts.

Basic facts about boolean comparisons

Module Type BoolOrderFacts
 (Import E:EqLtLe')
 (Import C:HasCmp E)
 (Import F:HasBoolOrdFuns' E)
 (Import O:CompareBasedOrder E C)
 (Import S:BoolOrdSpecs E F).

Include CompareBasedOrderFacts E C O.

Nota : apart from eqb_compare below, facts about eqb are in BoolEqualityFacts

Alternate specifications based on BoolSpec and reflect

Lemma leb_spec0 x y : reflect (x<=y) (x<=?y).x, y:t
reflect (x <= y) (x <=? y)
Proof.x, y:t
reflect (x <= y) (x <=? y)
 apply iff_reflect.x, y:t
x <= y <-> x <=? y = true symmetry.x, y:t
x <=? y = true <-> x <= y apply leb_le.
Defined.

Lemma leb_spec x y : BoolSpec (x<=y) (y<x) (x<=?y).x, y:t
BoolSpec (x <= y) (y < x) (x <=? y)
Proof.x, y:t
BoolSpec (x <= y) (y < x) (x <=? y)
 case leb_spec0; constructor; trivial.x, y:t
n:~ x <= y
y < x
 now rewrite <- compare_lt_iff, compare_nge_iff.
Qed.

Lemma ltb_spec0 x y : reflect (x<y) (x<?y).x, y:t
reflect (x < y) (x <? y)
Proof.x, y:t
reflect (x < y) (x <? y)
 apply iff_reflect.x, y:t
x < y <-> x <? y = true symmetry.x, y:t
x <? y = true <-> x < y apply ltb_lt.
Defined.

Lemma ltb_spec x y : BoolSpec (x<y) (y<=x) (x<?y).x, y:t
BoolSpec (x < y) (y <= x) (x <? y)
Proof.x, y:t
BoolSpec (x < y) (y <= x) (x <? y)
 case ltb_spec0; constructor; trivial.x, y:t
n:~ x < y
y <= x
 now rewrite <- compare_le_iff, compare_ngt_iff.
Qed.

Negated variants of the specifications

Lemma leb_nle x y : x <=? y = false <-> ~ (x <= y).x, y:t
x <=? y = false <-> ~ x <= y
Proof.x, y:t
x <=? y = false <-> ~ x <= y
now rewrite <- not_true_iff_false, leb_le.
Qed.

Lemma leb_gt x y : x <=? y = false <-> y < x.x, y:t
x <=? y = false <-> y < x
Proof.x, y:t
x <=? y = false <-> y < x
now rewrite leb_nle, <- compare_lt_iff, compare_nge_iff.
Qed.

Lemma ltb_nlt x y : x <? y = false <-> ~ (x < y).x, y:t
x <? y = false <-> ~ x < y
Proof.x, y:t
x <? y = false <-> ~ x < y
now rewrite <- not_true_iff_false, ltb_lt.
Qed.

Lemma ltb_ge x y : x <? y = false <-> y <= x.x, y:t
x <? y = false <-> y <= x
Proof.x, y:t
x <? y = false <-> y <= x
now rewrite ltb_nlt, <- compare_le_iff, compare_ngt_iff.
Qed.

Basic equality laws for boolean tests

Lemma leb_refl x : x <=? x = true.x:t
x <=? x = true
Proof.x:t
x <=? x = true
apply leb_le.x:t
x <= x apply lt_eq_cases.x:t
x < x \/ x == x now right.
Qed.

Lemma leb_antisym x y : y <=? x = negb (x <? y).x, y:t
y <=? x = negb (x <? y)
Proof.x, y:t
y <=? x = negb (x <? y)
apply eq_true_iff_eq.x, y:t
y <=? x = true <-> negb (x <? y) = true now rewrite negb_true_iff, leb_le, ltb_ge.
Qed.

Lemma ltb_irrefl x : x <? x = false.x:t
x <? x = false
Proof.x:t
x <? x = false
apply ltb_ge.x:t
x <= x apply lt_eq_cases.x:t
x < x \/ x == x now right.
Qed.

Lemma ltb_antisym x y : y <? x = negb (x <=? y).x, y:t
y <? x = negb (x <=? y)
Proof.x, y:t
y <? x = negb (x <=? y)
apply eq_true_iff_eq.x, y:t
y <? x = true <-> negb (x <=? y) = true now rewrite negb_true_iff, ltb_lt, leb_gt.
Qed.

Relation between compare and the boolean comparisons

Lemma eqb_compare x y :
 (x =? y) = match compare x y with Eq => true | _ => false end.x, y:t
(x =? y) =
match x ?= y with
| Eq => true
| _ => false
end
Proof.x, y:t
(x =? y) =
match x ?= y with
| Eq => true
| _ => false
end
apply eq_true_iff_eq.x, y:t
(x =? y) = true <->
match x ?= y with
| Eq => true
| _ => false
end = true rewrite eqb_eq, <- compare_eq_iff.x, y:t
(x ?= y) = Eq <->
match x ?= y with
| Eq => true
| _ => false
end = true
now destruct compare.
Qed.

Lemma ltb_compare x y :
 (x <? y) = match compare x y with Lt => true | _ => false end.x, y:t
x <? y =
match x ?= y with
| Lt => true
| _ => false
end
Proof.x, y:t
x <? y =
match x ?= y with
| Lt => true
| _ => false
end
apply eq_true_iff_eq.x, y:t
x <? y = true <->
match x ?= y with
| Lt => true
| _ => false
end = true rewrite ltb_lt, <- compare_lt_iff.x, y:t
(x ?= y) = Lt <->
match x ?= y with
| Lt => true
| _ => false
end = true
now destruct compare.
Qed.

Lemma leb_compare x y :
 (x <=? y) = match compare x y with Gt => false | _ => true end.x, y:t
x <=? y =
match x ?= y with
| Gt => false
| _ => true
end
Proof.x, y:t
x <=? y =
match x ?= y with
| Gt => false
| _ => true
end
apply eq_true_iff_eq.x, y:t
x <=? y = true <->
match x ?= y with
| Gt => false
| _ => true
end = true rewrite leb_le, <- compare_le_iff.x, y:t
(x ?= y) <> Gt <->
match x ?= y with
| Gt => false
| _ => true
end = true
now destruct compare.
Qed.

End BoolOrderFacts.