The Coq Proof Assistant

# Library Coq.Bool.BoolOrder

The order relations le lt and compare are defined in Bool.v
Order properties of bool
Require Export Bool.
Require Import Orders.
Import BoolNotations.
Local Ltac Tauto.intuition_solver ::= auto with typeclass_instances relations.

# Order le

Lemma le_refl : forall b, b <= b.
Lemma le_trans : forall b1 b2 b3,
b1 <= b2 -> b2 <= b3 -> b1 <= b3.
Lemma le_true : forall b, b <= true.
Lemma false_le : forall b, false <= b.
#[global]
Instance le_compat : Proper (eq ==> eq ==> iff) Bool.le.

# Strict order lt

Lemma lt_irrefl : forall b, ~ b < b.
Lemma lt_trans : forall b1 b2 b3,
b1 < b2 -> b2 < b3 -> b1 < b3.
#[global]
Instance lt_compat : Proper (eq ==> eq ==> iff) Bool.lt.
Lemma lt_trichotomy : forall b1 b2, { b1 < b2 } + { b1 = b2 } + { b2 < b1 }.
Lemma lt_total : forall b1 b2, b1 < b2 \/ b1 = b2 \/ b2 < b1.
Lemma lt_le_incl : forall b1 b2, b1 < b2 -> b1 <= b2.
Lemma le_lteq_dec : forall b1 b2, b1 <= b2 -> { b1 < b2 } + { b1 = b2 }.
Lemma le_lteq : forall b1 b2, b1 <= b2 <-> b1 < b2 \/ b1 = b2.

# Order structures

#[global]
Instance le_preorder : PreOrder Bool.le.
#[global]
Instance lt_strorder : StrictOrder Bool.lt.
Module BoolOrd <: UsualDecidableTypeFull <: OrderedTypeFull <: TotalOrder.
Definition t := bool.
Definition eq := @eq bool.
Definition eq_equiv := @eq_equivalence bool.
Definition lt := Bool.lt.
Definition lt_strorder := lt_strorder.
Definition lt_compat := lt_compat.
Definition le := Bool.le.
Definition le_lteq := le_lteq.
Definition lt_total := lt_total.
Definition compare := Bool.compare.
Definition compare_spec := compare_spec.
Definition eq_dec := bool_dec.
Definition eq_refl := @eq_Reflexive bool.
Definition eq_sym := @eq_Symmetric bool.
Definition eq_trans := @eq_Transitive bool.
Definition eqb := eqb.
Definition eqb_eq := eqb_true_iff.
End BoolOrd.