diff options
Diffstat (limited to 'theories/Structures/Equalities.v')
-rw-r--r-- | theories/Structures/Equalities.v | 56 |
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. |