diff options
Diffstat (limited to 'theories/Bool/BoolOrder.v')
| -rw-r--r-- | theories/Bool/BoolOrder.v | 42 |
1 files changed, 19 insertions, 23 deletions
diff --git a/theories/Bool/BoolOrder.v b/theories/Bool/BoolOrder.v index 61aab607a9..aaa7321bfc 100644 --- a/theories/Bool/BoolOrder.v +++ b/theories/Bool/BoolOrder.v @@ -14,69 +14,65 @@ 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. +Import BoolNotations. (** * Order [le] *) -Lemma le_refl : forall b, le b b. +Lemma le_refl : forall b, b <= b. Proof. destr_bool. Qed. Lemma le_trans : forall b1 b2 b3, - le b1 b2 -> le b2 b3 -> le b1 b3. + b1 <= b2 -> b2 <= b3 -> b1 <= b3. Proof. destr_bool. Qed. -Lemma le_true : forall b, le b true. +Lemma le_true : forall b, b <= true. Proof. destr_bool. Qed. -Lemma false_le : forall b, le false b. +Lemma false_le : forall b, false <= b. Proof. intros; constructor. Qed. -Instance le_compat : Proper (eq ==> eq ==> iff) le. +Instance le_compat : Proper (eq ==> eq ==> iff) Bool.le. Proof. intuition. Qed. (** * Strict order [lt] *) -Lemma lt_irrefl : forall b, ~ lt b b. +Lemma lt_irrefl : forall b, ~ b < b. Proof. destr_bool; auto. Qed. Lemma lt_trans : forall b1 b2 b3, - lt b1 b2 -> lt b2 b3 -> lt b1 b3. + b1 < b2 -> b2 < b3 -> b1 < b3. Proof. destr_bool; auto. Qed. -Instance lt_compat : Proper (eq ==> eq ==> iff) lt. +Instance lt_compat : Proper (eq ==> eq ==> iff) Bool.lt. Proof. intuition. Qed. -Lemma lt_trichotomy : forall b1 b2, { lt b1 b2 } + { b1 = b2 } + { lt b2 b1 }. +Lemma lt_trichotomy : forall b1 b2, { b1 < b2 } + { b1 = b2 } + { b2 < b1 }. Proof. destr_bool; auto. Qed. -Lemma lt_total : forall b1 b2, lt b1 b2 \/ b1 = b2 \/ lt b2 b1. +Lemma lt_total : forall b1 b2, b1 < b2 \/ b1 = b2 \/ b2 < b1. Proof. destr_bool; auto. Qed. -Lemma lt_le_incl : forall b1 b2, lt b1 b2 -> le b1 b2. +Lemma lt_le_incl : forall b1 b2, b1 < b2 -> b1 <= b2. Proof. destr_bool; auto. Qed. -Lemma le_lteq_dec : forall b1 b2, le b1 b2 -> { lt b1 b2 } + { b1 = b2 }. +Lemma le_lteq_dec : forall b1 b2, b1 <= b2 -> { b1 < b2 } + { b1 = b2 }. Proof. destr_bool; auto. Qed. -Lemma le_lteq : forall b1 b2, le b1 b2 <-> lt b1 b2 \/ b1 = b2. +Lemma le_lteq : forall b1 b2, b1 <= b2 <-> b1 < b2 \/ b1 = b2. Proof. destr_bool; intuition. Qed. (** * Order structures *) (* Class structure *) -Instance le_preorder : PreOrder le. +Instance le_preorder : PreOrder Bool.le. Proof. split. - intros b; apply le_refl. - intros b1 b2 b3; apply le_trans. Qed. -Instance lt_strorder : StrictOrder lt. +Instance lt_strorder : StrictOrder Bool.lt. Proof. split. - intros b; apply lt_irrefl. @@ -88,13 +84,13 @@ Module BoolOrd <: UsualDecidableTypeFull <: OrderedTypeFull <: TotalOrder. Definition t := bool. Definition eq := @eq bool. Definition eq_equiv := @eq_equivalence bool. - Definition lt := lt. + Definition lt := Bool.lt. Definition lt_strorder := lt_strorder. Definition lt_compat := lt_compat. - Definition le := le. + Definition le := Bool.le. Definition le_lteq := le_lteq. Definition lt_total := lt_total. - Definition compare := compare. + Definition compare := Bool.compare. Definition compare_spec := compare_spec. Definition eq_dec := bool_dec. Definition eq_refl := @eq_Reflexive bool. |