aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures/Equalities.v
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-06-20 17:18:39 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-06-20 17:18:39 +0000
commitca96d3477993d102d6cc42166eab52516630d181 (patch)
tree073b17efe149637da819caf527b23cf09f15865d /theories/Structures/Equalities.v
parentca1848177a50e51bde0736e51f506e06efc81b1d (diff)
Arithemtic: more concerning compare, eqb, leb, ltb
Start of a uniform treatment of compare, eqb, leb, ltb: - We now ensure that they are provided by N,Z,BigZ,BigN,Nat and Pos - Some generic properties are derived in OrdersFacts.BoolOrderFacts In BinPos, more work about sub_mask with nice implications on compare (e.g. simplier proof of lt_trans). In BinNat/BinPos, for uniformity, compare_antisym is now (y ?= x) = CompOpp (x ?=y) instead of the symmetrical result. In BigN / BigZ, eq_bool is now eqb In BinIntDef, gtb and geb are kept for the moment, but a comment advise to rather use ltb and leb. Z.div now uses Z.ltb and Z.leb. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14227 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Structures/Equalities.v')
-rw-r--r--theories/Structures/Equalities.v56
1 files changed, 49 insertions, 7 deletions
diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v
index 2fbdff624..933c4ea0e 100644
--- a/theories/Structures/Equalities.v
+++ b/theories/Structures/Equalities.v
@@ -66,10 +66,19 @@ End HasEqDec.
(** Having [eq_dec] is the same as having a boolean equality plus
a correctness proof. *)
-Module Type HasEqBool (Import E:Eq').
+Module Type HasEqb (Import T:Typ).
Parameter Inline eqb : t -> t -> bool.
- Parameter eqb_eq : forall x y, eqb x y = true <-> x==y.
-End HasEqBool.
+End HasEqb.
+
+Module Type EqbSpec (T:Typ)(X:HasEq T)(Y:HasEqb T).
+ Parameter eqb_eq : forall x y, Y.eqb x y = true <-> X.eq x y.
+End EqbSpec.
+
+Module Type EqbNotation (T:Typ)(E:HasEqb T).
+ Infix "=?" := E.eqb (at level 70, no associativity).
+End EqbNotation.
+
+Module Type HasEqBool (E:Eq) := HasEqb E <+ EqbSpec E E.
(** From these basic blocks, we can build many combinations
of static standalone module types. *)
@@ -107,8 +116,10 @@ Module Type EqualityTypeBoth' := EqualityTypeBoth <+ EqNotation.
Module Type DecidableType' := DecidableType <+ EqNotation.
Module Type DecidableTypeOrig' := DecidableTypeOrig <+ EqNotation.
Module Type DecidableTypeBoth' := DecidableTypeBoth <+ EqNotation.
-Module Type BooleanEqualityType' := BooleanEqualityType <+ EqNotation.
-Module Type BooleanDecidableType' := BooleanDecidableType <+ EqNotation.
+Module Type BooleanEqualityType' :=
+ BooleanEqualityType <+ EqNotation <+ EqbNotation.
+Module Type BooleanDecidableType' :=
+ BooleanDecidableType <+ EqNotation <+ EqbNotation.
Module Type DecidableTypeFull' := DecidableTypeFull <+ EqNotation.
(** * Compatibility wrapper from/to the old version of
@@ -166,9 +177,12 @@ Module Dec2Bool (E:DecidableType) <: BooleanDecidableType
Module Bool2Dec (E:BooleanEqualityType) <: BooleanDecidableType
:= E <+ HasEqBool2Dec.
-(** In a BooleanEqualityType, [eqb] is compatible with [eq] *)
-Module BoolEqualityFacts (Import E : BooleanEqualityType).
+(** Some properties of boolean equality *)
+
+Module BoolEqualityFacts (Import E : BooleanEqualityType').
+
+(** [eqb] is compatible with [eq] *)
Instance eqb_compat : Proper (E.eq ==> E.eq ==> Logic.eq) eqb.
Proof.
@@ -177,6 +191,34 @@ apply eq_true_iff_eq.
now rewrite 2 eqb_eq, Exx', Eyy'.
Qed.
+(** Alternative specification of [eqb] based on [reflect]. *)
+
+Lemma eqb_spec x y : reflect (x==y) (x =? y).
+Proof.
+apply iff_reflect. symmetry. apply eqb_eq.
+Qed.
+
+(** Negated form of [eqb_eq] *)
+
+Lemma eqb_neq x y : (x =? y) = false <-> x ~= y.
+Proof.
+now rewrite <- not_true_iff_false, eqb_eq.
+Qed.
+
+(** Basic equality laws for [eqb] *)
+
+Lemma eqb_refl x : (x =? x) = true.
+Proof.
+now apply eqb_eq.
+Qed.
+
+Lemma eqb_sym x y : (x =? y) = (y =? x).
+Proof.
+apply eq_true_iff_eq. now rewrite 2 eqb_eq.
+Qed.
+
+(** Transitivity is a particular case of [eqb_compat] *)
+
End BoolEqualityFacts.