Library Coq.Structures.EqualitiesFacts
In a BooleanEqualityType, eqb is compatible with eq
Module BoolEqualityFacts (Import E : BooleanEqualityType).
Instance eqb_compat : Proper (E.eq ==> E.eq ==> Logic.eq) eqb.
End BoolEqualityFacts.
Module KeyDecidableType(Import D:DecidableType).
Section Elt.
Variable elt : Type.
Notation key:=t.
Local Open Scope signature_scope.
Definition eqk : relation (key*elt) := eq @@1.
Definition eqke : relation (key*elt) := eq * Logic.eq.
Hint Unfold eqk eqke.
Global Instance eqke_eqk : subrelation eqke eqk.
Global Instance eqk_equiv : Equivalence eqk.
Global Instance eqke_equiv : Equivalence eqke.
Lemma InA_eqke_eqk :
forall x m, InA eqke x m -> InA eqk x m.
Hint Resolve InA_eqke_eqk.
Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m.
Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
Definition In k m := exists e:elt, MapsTo k e m.
Hint Unfold MapsTo In.
Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l.
Lemma In_alt2 : forall k l, In k l <-> Exists (fun p => eq k (fst p)) l.
Lemma In_nil : forall k, In k nil <-> False.
Lemma In_cons : forall k p l,
In k (p::l) <-> eq k (fst p) \/ In k l.
Global Instance MapsTo_compat :
Proper (eq==>Logic.eq==>equivlistA eqke==>iff) MapsTo.
Global Instance In_compat : Proper (eq==>equivlistA eqk==>iff) In.
Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.
Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l.
Lemma In_inv_2 : forall k k' e e' l,
InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l.
Lemma In_inv_3 : forall x x' l,
InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l.
End Elt.
Hint Unfold eqk eqke.
Hint Extern 2 (eqke ?a ?b) => split.
Hint Resolve InA_eqke_eqk.
Hint Unfold MapsTo In.
Hint Resolve In_inv_2 In_inv_3.
End KeyDecidableType.
Section Elt.
Variable elt : Type.
Notation key:=t.
Local Open Scope signature_scope.
Definition eqk : relation (key*elt) := eq @@1.
Definition eqke : relation (key*elt) := eq * Logic.eq.
Hint Unfold eqk eqke.
Global Instance eqke_eqk : subrelation eqke eqk.
Global Instance eqk_equiv : Equivalence eqk.
Global Instance eqke_equiv : Equivalence eqke.
Lemma InA_eqke_eqk :
forall x m, InA eqke x m -> InA eqk x m.
Hint Resolve InA_eqke_eqk.
Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m.
Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
Definition In k m := exists e:elt, MapsTo k e m.
Hint Unfold MapsTo In.
Lemma In_alt : forall k l, In k l <-> exists e, InA eqk (k,e) l.
Lemma In_alt2 : forall k l, In k l <-> Exists (fun p => eq k (fst p)) l.
Lemma In_nil : forall k, In k nil <-> False.
Lemma In_cons : forall k p l,
In k (p::l) <-> eq k (fst p) \/ In k l.
Global Instance MapsTo_compat :
Proper (eq==>Logic.eq==>equivlistA eqke==>iff) MapsTo.
Global Instance In_compat : Proper (eq==>equivlistA eqk==>iff) In.
Lemma MapsTo_eq : forall l x y e, eq x y -> MapsTo x e l -> MapsTo y e l.
Lemma In_eq : forall l x y, eq x y -> In x l -> In y l.
Lemma In_inv : forall k k' e l, In k ((k',e) :: l) -> eq k k' \/ In k l.
Lemma In_inv_2 : forall k k' e e' l,
InA eqk (k, e) ((k', e') :: l) -> ~ eq k k' -> InA eqk (k, e) l.
Lemma In_inv_3 : forall x x' l,
InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l.
End Elt.
Hint Unfold eqk eqke.
Hint Extern 2 (eqke ?a ?b) => split.
Hint Resolve InA_eqke_eqk.
Hint Unfold MapsTo In.
Hint Resolve In_inv_2 In_inv_3.
End KeyDecidableType.
PairDecidableType
From two decidable types, we can build a new DecidableType over their cartesian product.
Module PairDecidableType(D1 D2:DecidableType) <: DecidableType.
Definition t := (D1.t * D2.t)%type.
Definition eq := (D1.eq * D2.eq)%signature.
Instance eq_equiv : Equivalence eq.
Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }.
End PairDecidableType.
Similarly for pairs of UsualDecidableType
Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType.
Definition t := (D1.t * D2.t)%type.
Definition eq := @eq t.
Program Instance eq_equiv : Equivalence eq.
Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }.
End PairUsualDecidableType.