Library Coq.Classes.Morphisms_Relations
Morphism instances for relations.
Author: Matthieu Sozeau Institution: LRI, CNRS UMR 8623 - University Paris Sud
Require
Import
Relation_Definitions
.
Require
Import
Coq.Classes.Morphisms
.
Require
Import
Coq.Program.Program
.
Morphisms for relations
Instance
relation_conjunction_morphism
:
Proper
(
relation_equivalence
(
A
:=
A
)
==>
relation_equivalence
==>
relation_equivalence
)
relation_conjunction
.
Instance
relation_disjunction_morphism
:
Proper
(
relation_equivalence
(
A
:=
A
)
==>
relation_equivalence
==>
relation_equivalence
)
relation_disjunction
.
Lemma
predicate_equivalence_pointwise
(
l
:
Tlist
) :
Proper
(@
predicate_equivalence
l
==>
pointwise_lifting
iff
l
)
id
.
Lemma
predicate_implication_pointwise
(
l
:
Tlist
) :
Proper
(@
predicate_implication
l
==>
pointwise_lifting
impl
l
)
id
.
The instantiation at relation allows rewriting applications of relations
R
x
y
to
R'
x
y
when
R
and
R'
are in
relation_equivalence
.
Instance
relation_equivalence_pointwise
:
Proper
(
relation_equivalence
==>
pointwise_relation
A
(
pointwise_relation
A
iff
))
id
.
Instance
subrelation_pointwise
:
Proper
(
subrelation
==>
pointwise_relation
A
(
pointwise_relation
A
impl
))
id
.
Lemma
flip_pointwise_relation
A
(
R
:
relation
A
) :
relation_equivalence
(
pointwise_relation
A
(
flip
R
)) (
flip
(
pointwise_relation
A
R
)).