Library Coq.Classes.Morphisms_Prop
Require
Import
Coq.Classes.Morphisms
.
Require
Import
Coq.Program.Basics
.
Require
Import
Coq.Program.Tactics
.
Standard instances for
not
,
iff
and
impl
.
Logical negation.
Program Instance
not_impl_morphism
:
Morphism
(
impl
-->
impl
)
not
.
Program Instance
not_iff_morphism
:
Morphism
(
iff
++>
iff
)
not
.
Logical conjunction.
Program Instance
and_impl_morphism
:
Morphism
(
impl
==>
impl
==>
impl
)
and
.
Program Instance
and_iff_morphism
:
Morphism
(
iff
==>
iff
==>
iff
)
and
.
Logical disjunction.
Program Instance
or_impl_morphism
:
Morphism
(
impl
==>
impl
==>
impl
)
or
.
Program Instance
or_iff_morphism
:
Morphism
(
iff
==>
iff
==>
iff
)
or
.
Logical implication
impl
is a morphism for logical equivalence.
Program Instance
iff_iff_iff_impl_morphism
:
Morphism
(
iff
==>
iff
==>
iff
)
impl
.
Morphisms for quantifiers
Program Instance
ex_iff_morphism
{
A
:
Type
} :
Morphism
(
pointwise_relation
A
iff
==>
iff
) (@
ex
A
).
Program Instance
ex_impl_morphism
{
A
:
Type
} :
Morphism
(
pointwise_relation
A
impl
==>
impl
) (@
ex
A
).
Program Instance
ex_inverse_impl_morphism
{
A
:
Type
} :
Morphism
(
pointwise_relation
A
(
inverse
impl
) ==>
inverse
impl
) (@
ex
A
).
Program Instance
all_iff_morphism
{
A
:
Type
} :
Morphism
(
pointwise_relation
A
iff
==>
iff
) (@
all
A
).
Program Instance
all_impl_morphism
{
A
:
Type
} :
Morphism
(
pointwise_relation
A
impl
==>
impl
) (@
all
A
).
Program Instance
all_inverse_impl_morphism
{
A
:
Type
} :
Morphism
(
pointwise_relation
A
(
inverse
impl
) ==>
inverse
impl
) (@
all
A
).