Library Coq.Classes.CMorphisms
Typeclass-based morphism definition and standard, minimal instances
Author: Matthieu Sozeau
Institution: LRI, CNRS UMR 8623 - University Paris Sud
Morphisms.
We now turn to the definition of
Proper and declare standard instances.
These will be used by the
setoid_rewrite tactic later.
A morphism for a relation
R is a proper element of the relation.
The relation
R will be instantiated by
respectful and
A by an arrow
type for usual morphisms.
Every element in the carrier of a reflexive relation is a morphism
for this relation. We use a proxy class for this case which is used
internally to discharge reflexivity constraints. The Reflexive
instance will almost always be used, but it won't apply in general to
any kind of Proper (A -> B) _ _ goal, making proof-search much
slower. A cleaner solution would be to be able to set different
priorities in different hint bases and select a particular hint
database for resolution of a type class constraint.
Respectful morphisms.
The fully dependent version, not used yet.
The non-dependent version is an instance where we forget dependencies.
We favor the use of Leibniz equality or a declared reflexive crelation
when resolving ProperProxy, otherwise, if the crelation is given (not an evar),
we fall back to Proper.
Notations reminiscent of the old syntax for declaring morphisms.
Delimit Scope signature_scope with signature.
Module ProperNotations.
Notation " R ++> R' " := (@
respectful _ _ (
R%
signature) (
R'%
signature))
(
right associativity,
at level 55) :
signature_scope.
Notation " R ==> R' " := (@
respectful _ _ (
R%
signature) (
R'%
signature))
(
right associativity,
at level 55) :
signature_scope.
Notation " R --> R' " := (@
respectful _ _ (
flip (
R%
signature)) (
R'%
signature))
(
right associativity,
at level 55) :
signature_scope.
End ProperNotations.
Export ProperNotations.
Local Open Scope signature_scope.
solve_proper try to solve the goal Proper (?==> ... ==>?) f
by repeated introductions and setoid rewrites. It should work
fine when f is a combination of already known morphisms and
quantifiers.
Ltac solve_respectful t :=
match goal with
| |-
respectful _ _ _ _ =>
let H :=
fresh "H"
in
intros ? ?
H;
solve_respectful ltac:(
setoid_rewrite H;
t)
|
_ =>
t;
reflexivity
end.
Ltac solve_proper :=
unfold Proper;
solve_respectful ltac:(
idtac).
f_equiv is a clone of f_equal that handles setoid equivalences.
For example, if we know that f is a morphism for E1==>E2==>E,
then the goal E (f x y) (f x' y') will be transformed by f_equiv
into the subgoals E1 x x' and E2 y y'.
Ltac f_equiv :=
match goal with
| |- ?
R (?
f ?
x) (?
f' _) =>
let T :=
type of x in
let Rx :=
fresh "R"
in
evar (
Rx :
crelation T);
let H :=
fresh in
assert (
H : (
Rx==>R)%
signature f f');
unfold Rx in *;
clear Rx; [
f_equiv |
apply H;
clear H;
try reflexivity ]
| |- ?
R ?
f ?
f' =>
solve [
change (
Proper R f);
eauto with typeclass_instances |
reflexivity ]
|
_ =>
idtac
end.
Section Relations.
Context {
A :
Type}.
forall_def reifies the dependent product as a definition.
Dependent pointwise lifting of a crelation on the range.
Non-dependent pointwise lifting
Subcrelations induce a morphism on the identity.
The subrelation property goes through products as usual.
And of course it is reflexive.
Proper is itself a covariant morphism for subrelation.
We use an unconvertible premise to avoid looping.
For dependent function types.
Resolution with subrelation: favor decomposing products over applying reflexivity
for unconstrained goals.
Essential subrelation instances for iff, impl and pointwise_relation.
Essential subrelation instances for iffT and arrow.
We use an extern hint to help unification.
We can build a PER on the Coq function space if we have PERs on the domain and
codomain.
The complement of a crelation conserves its proper elements.
The
flip too, actually the
flip instance is a bit more general.
Every Transitive crelation gives rise to a binary morphism on impl,
contravariant in the first argument, covariant in the second.
Proper declarations for partial applications.
Every Transitive crelation induces a morphism by "pushing" an R x y on the left of an R x z proof to get an R y z goal.
Every Symmetric and Transitive crelation gives rise to an equivariant morphism.
Coq functions are morphisms for Leibniz equality,
applied only if really needed.
respectful is a morphism for crelation equivalence .
R is Reflexive, hence we can build the needed proof.
Treating flip: can't make them direct instances as we
need at least a flip present in the goal.
That's if and only if
Once we have normalized, we will apply this instance to simplify the problem.
Every reflexive crelation gives rise to a morphism,
only for immediately solving goals without variables.
Bootstrap !!!
Special-purpose class to do normalization of signatures w.r.t. flip.
Current strategy: add flip everywhere and reduce using subrelation
afterwards.
When the crelation on the domain is symmetric, we can
flip the crelation on the codomain. Same for binary functions.
When the crelation on the domain is symmetric, a predicate is
compatible with iff as soon as it is compatible with impl.
Same with a binary crelation.
A PartialOrder is compatible with its underlying equivalence.
From a PartialOrder to the corresponding StrictOrder:
lt = le /\ ~eq.
If the order is total, we could also say gt = ~le.
From a StrictOrder to the corresponding PartialOrder:
le = lt \/ eq.
If the order is total, we could also say ge = ~lt.