Merge PR #12008: [stdlib] Add order properties about bool

Reviewed-by: anton-trunov
Reviewed-by: herbelin

6 files changed, 143 insertions, 5 deletions

diff --git a/doc/changelog/10-standard-library/12008-ollibs-bool.rst b/doc/changelog/10-standard-library/12008-ollibs-bool.rst
new file mode 100644
index 0000000000..7c10d261a7
--- /dev/null
+++ b/doc/changelog/10-standard-library/12008-ollibs-bool.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  Order relations ``ltb`` and ``compareb`` added in ``Bool.Bool``.
+  Order properties for ``bool`` added in ``Bool.BoolOrder`` as well as two modules ``Bool_as_OT`` and ``Bool_as_DT`` in ``Structures.OrdersEx``
+  (`#12008 <https://github.com/coq/coq/pull/12008>`_,
+  by Olivier Laurent).
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index b2c9c936c9..4a62888552 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -99,6 +99,7 @@ through the <tt>Require Import</tt> command.</p>
   <dd>
     theories/Bool/Bool.v
     theories/Bool/BoolEq.v
+    theories/Bool/BoolOrder.v
     theories/Bool/DecBool.v
     theories/Bool/IfProp.v
     theories/Bool/Sumbool.v
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 8708f5a2bf..57cc8c4e90 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -94,7 +94,24 @@ Proof.
   destr_bool; intuition.
 Qed.
 
-(* Infix "<=" := leb : bool_scope. *)
+Definition ltb (b1 b2:bool) :=
+  match b1 with
+    | true => False
+    | false => b2 = true
+  end.
+Hint Unfold ltb: bool.
+
+Definition compareb (b1 b2 : bool) :=
+  match b1, b2 with
+   | false, true => Lt
+   | true, false => Gt
+   | _, _ => Eq
+  end.
+
+Lemma compareb_spec : forall b1 b2,
+  CompareSpec (b1 = b2) (ltb b1 b2) (ltb b2 b1) (compareb b1 b2).
+Proof. destr_bool; auto. Qed.
+
 
 (***************)
 (** * Equality *)
@@ -915,3 +932,11 @@ Lemma eqb_spec (b b' : bool) : reflect (b = b') (eqb b b').
 Proof.
  destruct b, b'; now constructor.
 Defined.
+
+(** Notations *)
+Module BoolNotations.
+Infix "<=" := leb : bool_scope.
+Infix "<" := ltb : bool_scope.
+Infix "?=" := compareb (at level 70) : bool_scope.
+Infix "=?" := eqb (at level 70) : bool_scope.
+End BoolNotations.
diff --git a/theories/Bool/BoolOrder.v b/theories/Bool/BoolOrder.v
new file mode 100644
index 0000000000..61aab607a9
--- /dev/null
+++ b/theories/Bool/BoolOrder.v
@@ -0,0 +1,105 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \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)         *)
+(************************************************************************)
+
+(** The order relations [le] [lt] and [compare] are defined in [Bool.v] *)
+
+(** Order properties of [bool]  *)
+
+Require Export Bool.
+Require Import Orders.
+
+Local Notation le := Bool.leb.
+Local Notation lt := Bool.ltb.
+Local Notation compare := Bool.compareb.
+Local Notation compare_spec := Bool.compareb_spec.
+
+(** * Order [le] *)
+
+Lemma le_refl : forall b, le b b.
+Proof. destr_bool. Qed.
+
+Lemma le_trans : forall b1 b2 b3,
+  le b1 b2 -> le b2 b3 -> le b1 b3.
+Proof. destr_bool. Qed.
+
+Lemma le_true : forall b, le b true.
+Proof. destr_bool. Qed.
+
+Lemma false_le : forall b, le false b.
+Proof. intros; constructor. Qed.
+
+Instance le_compat : Proper (eq ==> eq ==> iff) le.
+Proof. intuition. Qed.
+
+(** * Strict order [lt] *)
+
+Lemma lt_irrefl : forall b, ~ lt b b.
+Proof. destr_bool; auto. Qed.
+
+Lemma lt_trans : forall b1 b2 b3,
+  lt b1 b2 -> lt b2 b3 -> lt b1 b3.
+Proof. destr_bool; auto. Qed.
+
+Instance lt_compat : Proper (eq ==> eq ==> iff) lt.
+Proof. intuition. Qed.
+
+Lemma lt_trichotomy : forall b1 b2, { lt b1 b2 } + { b1 = b2 } + { lt b2 b1 }.
+Proof. destr_bool; auto. Qed.
+
+Lemma lt_total : forall b1 b2, lt b1 b2 \/ b1 = b2 \/ lt b2 b1.
+Proof. destr_bool; auto. Qed.
+
+Lemma lt_le_incl : forall b1 b2, lt b1 b2 -> le b1 b2.
+Proof. destr_bool; auto. Qed.
+
+Lemma le_lteq_dec : forall b1 b2, le b1 b2 -> { lt b1 b2 } + { b1 = b2 }.
+Proof. destr_bool; auto. Qed.
+
+Lemma le_lteq : forall b1 b2, le b1 b2 <-> lt b1 b2 \/ b1 = b2.
+Proof. destr_bool; intuition. Qed.
+
+
+(** * Order structures *)
+
+(* Class structure *)
+Instance le_preorder : PreOrder le.
+Proof.
+split.
+- intros b; apply le_refl.
+- intros b1 b2 b3; apply le_trans.
+Qed.
+
+Instance lt_strorder : StrictOrder lt.
+Proof.
+split.
+- intros b; apply lt_irrefl.
+- intros b1 b2 b3; apply lt_trans.
+Qed.
+
+(* Module structure *)
+Module BoolOrd <: UsualDecidableTypeFull <: OrderedTypeFull <: TotalOrder.
+  Definition t := bool.
+  Definition eq := @eq bool.
+  Definition eq_equiv := @eq_equivalence bool.
+  Definition lt := lt.
+  Definition lt_strorder := lt_strorder.
+  Definition lt_compat := lt_compat.
+  Definition le := le.
+  Definition le_lteq := le_lteq.
+  Definition lt_total := lt_total.
+  Definition compare := 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.
diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v
index bacc4a7650..b65cb294aa 100644
--- a/theories/Numbers/Cyclic/Int63/Int63.v
+++ b/theories/Numbers/Cyclic/Int63/Int63.v
@@ -978,7 +978,7 @@ Proof.
    case (leb_spec digits j); rewrite H; auto with zarith.
    intros _ HH; generalize (HH H1); discriminate.
  clear H.
- generalize (ltb_spec j i); case ltb; intros H2; unfold bit; simpl.
+ generalize (ltb_spec j i); case Int63.ltb; intros H2; unfold bit; simpl.
    assert (F2: (φ j < φ i)%Z) by (case H2; auto); clear H2.
    replace (is_zero (((x << i) >> j) << (digits - 1))) with true; auto.
    case (to_Z_bounded j); intros  H1j H2j.
diff --git a/theories/Structures/OrdersEx.v b/theories/Structures/OrdersEx.v
index 0ad79825d2..adffa1ded4 100644
--- a/theories/Structures/OrdersEx.v
+++ b/theories/Structures/OrdersEx.v
@@ -13,14 +13,15 @@
  * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
  *              91405 Orsay, France *)
 
-Require Import Orders PeanoNat POrderedType BinNat BinInt
+Require Import Orders BoolOrder PeanoNat POrderedType BinNat BinInt
  RelationPairs EqualitiesFacts.
 
 (** * Examples of Ordered Type structures. *)
 
 
-(** Ordered Type for [nat], [Positive], [N], [Z] with the usual order. *)
+(** Ordered Type for [bool], [nat], [Positive], [N], [Z] with the usual order. *)
 
+Module Bool_as_OT := BoolOrder.BoolOrd.
 Module Nat_as_OT := PeanoNat.Nat.
 Module Positive_as_OT := BinPos.Pos.
 Module N_as_OT := BinNat.N.
@@ -30,8 +31,9 @@ Module Z_as_OT := BinInt.Z.
 
 Module OT_as_DT (O:OrderedType) <: DecidableType := O.
 
-(** (Usual) Decidable Type for [nat], [positive], [N], [Z] *)
+(** (Usual) Decidable Type for [bool], [nat], [positive], [N], [Z] *)
 
+Module Bool_as_DT <: UsualDecidableType := Bool_as_OT.
 Module Nat_as_DT <: UsualDecidableType := Nat_as_OT.
 Module Positive_as_DT <: UsualDecidableType := Positive_as_OT.
 Module N_as_DT <: UsualDecidableType := N_as_OT.