1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
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.
|
