# Library Coq.Structures.Equalities

Require Export RelationClasses.

# Structure with just a base type t

Module Type Typ.
Parameter Inline t : Type.
End Typ.

# Structure with an equality relation eq

Module Type HasEq (Import T:Typ).
Parameter Inline eq : t -> t -> Prop.
End HasEq.

Module Type Eq := Typ <+ HasEq.

Module Type EqNotation (Import E:Eq).
Infix "==" := eq (at level 70, no associativity).
Notation "x ~= y" := (~eq x y) (at level 70, no associativity).
End EqNotation.

Module Type Eq' := Eq <+ EqNotation.

# Specification of the equality via the Equivalence type class

Module Type IsEq (Import E:Eq).
Declare Instance eq_equiv : Equivalence eq.
End IsEq.

# Earlier specification of equality by three separate lemmas.

Module Type IsEqOrig (Import E:Eq').
Axiom eq_refl : forall x : t, x==x.
Axiom eq_sym : forall x y : t, x==y -> y==x.
Axiom eq_trans : forall x y z : t, x==y -> y==z -> x==z.
Hint Immediate eq_sym.
Hint Resolve eq_refl eq_trans.
End IsEqOrig.

# Types with decidable equality

Module Type HasEqDec (Import E:Eq').
Parameter eq_dec : forall x y : t, { x==y } + { ~ x==y }.
End HasEqDec.

# Boolean Equality

Having eq_dec is the same as having a boolean equality plus a correctness proof.

Module Type HasEqBool (Import E:Eq').
Parameter Inline eqb : t -> t -> bool.
Parameter eqb_eq : forall x y, eqb x y = true <-> x==y.
End HasEqBool.

From these basic blocks, we can build many combinations of static standalone module types.
Same, with notation for eq

# Compatibility wrapper from/to the old version of

EqualityType and DecidableType

# Having eq_dec is equivalent to having eqb and its spec.

Module HasEqDec2Bool (E:Eq)(F:HasEqDec E) <: HasEqBool E.
Definition eqb x y := if F.eq_dec x y then true else false.
Lemma eqb_eq : forall x y, eqb x y = true <-> E.eq x y.
End HasEqDec2Bool.

Module HasEqBool2Dec (E:Eq)(F:HasEqBool E) <: HasEqDec E.
Lemma eq_dec : forall x y, {E.eq x y}+{~E.eq x y}.
End HasEqBool2Dec.

Module Dec2Bool (E:DecidableType) <: BooleanDecidableType
:= E <+ HasEqDec2Bool.

Module Bool2Dec (E:BooleanEqualityType) <: BooleanDecidableType
:= E <+ HasEqBool2Dec.

# UsualDecidableType

A particular case of DecidableType where the equality is the usual one of Coq.

Module Type HasUsualEq (Import T:Typ) <: HasEq T.
Definition eq := @Logic.eq t.
End HasUsualEq.

Module Type UsualEq <: Eq := Typ <+ HasUsualEq.

Module Type UsualIsEq (E:UsualEq) <: IsEq E.
Definition eq_equiv : Equivalence E.eq := eq_equivalence.
End UsualIsEq.

Module Type UsualIsEqOrig (E:UsualEq) <: IsEqOrig E.
Definition eq_refl := @Logic.eq_refl E.t.
Definition eq_sym := @Logic.eq_sym E.t.
Definition eq_trans := @Logic.eq_trans E.t.
End UsualIsEqOrig.

Module Type UsualEqualityType <: EqualityType
:= UsualEq <+ UsualIsEq.

Module Type UsualDecidableType <: DecidableType
:= UsualEq <+ UsualIsEq <+ HasEqDec.

Module Type UsualDecidableTypeOrig <: DecidableTypeOrig
:= UsualEq <+ UsualIsEqOrig <+ HasEqDec.

Module Type UsualDecidableTypeBoth <: DecidableTypeBoth
:= UsualEq <+ UsualIsEq <+ UsualIsEqOrig <+ HasEqDec.

Module Type UsualBoolEq := UsualEq <+ HasEqBool.

Module Type UsualDecidableTypeFull <: DecidableTypeFull
:= UsualEq <+ UsualIsEq <+ UsualIsEqOrig <+ HasEqDec <+ HasEqBool.

Some shortcuts for easily building a UsualDecidableType

Module Type MiniDecidableType.
Include Typ.
Parameter eq_dec : forall x y : t, {x=y}+{~x=y}.
End MiniDecidableType.

Module Make_UDT (M:MiniDecidableType) <: UsualDecidableTypeBoth
:= M <+ HasUsualEq <+ UsualIsEq <+ UsualIsEqOrig.

Module Make_UDTF (M:UsualBoolEq) <: UsualDecidableTypeFull
:= M <+ UsualIsEq <+ UsualIsEqOrig <+ HasEqBool2Dec.