Library Coq.Classes.CRelationClasses
Typeclass-based relations, tactics and standard instances
This is the basic theory needed to formalize morphisms and setoids.
Author: Matthieu Sozeau
Institution: LRI, CNRS UMR 8623 - University Paris Sud
We allow to unfold the crelation definition while doing morphism search.
Section Defs.
Context {
A :
Type}.
We rebind crelational properties in separate classes to be able to overload each proof.
Opaque for proof-search.
Typeclasses Opaque complement iffT.
These are convertible.
Various combinations of reflexivity, symmetry and transitivity.
A
PreOrder is both Reflexive and Transitive.
A StrictOrder is both Irreflexive and Transitive.
By definition, a strict order is also asymmetric
A partial equivalence crelation is Symmetric and Transitive.
Equivalence crelations.
An Equivalence is a PER plus reflexivity.
We can now define antisymmetry w.r.t. an equivalence crelation on the carrier.
Any symmetric crelation is equal to its inverse.
Inversing the larger structures
Rewrite crelation on a given support: declares a crelation as a rewrite
crelation for use by the generalized rewriting tactic.
It helps choosing if a rewrite should be handled
by the generalized or the regular rewriting tactic using leibniz equality.
Users can declare an RewriteRelation A RA anywhere to declare default
crelations. This is also done automatically by the Declare Relation A RA
commands.
Any Equivalence declared in the context is automatically considered
a rewrite crelation.
Leibniz equality.
Leibinz equality eq is an equivalence crelation.
The instance has low priority as it is always applicable
if only the type is constrained.
Default rewrite crelations handled by setoid_rewrite.
Hints to drive the typeclass resolution avoiding loops
due to the use of full unification.
A HintDb for crelations.
Ltac solve_crelation :=
match goal with
| [ |- ?R ?x ?x ] => reflexivity
| [ H : ?R ?x ?y |- ?R ?y ?x ] => symmetry ; exact H
end.
Hint Extern 4 => solve_crelation : crelations.
We can already dualize all these properties.
Standard instances.
Ltac reduce_hyp H :=
match type of H with
|
context [
_ <-> _ ] =>
fail 1
|
_ =>
red in H ;
try reduce_hyp H
end.
Ltac reduce_goal :=
match goal with
| [ |-
_ <-> _ ] =>
fail 1
|
_ =>
red ;
intros ;
try reduce_goal
end.
Tactic Notation "reduce" "in"
hyp(
Hid) :=
reduce_hyp Hid.
Ltac reduce :=
reduce_goal.
Tactic Notation "apply" "*"
constr(
t) :=
first [
refine t |
refine (
t _) |
refine (
t _ _) |
refine (
t _ _ _) |
refine (
t _ _ _ _) |
refine (
t _ _ _ _ _) |
refine (
t _ _ _ _ _ _) |
refine (
t _ _ _ _ _ _ _) ].
Ltac simpl_crelation :=
unfold flip,
impl,
arrow ;
try reduce ;
program_simpl ;
try (
solve [
dintuition ]).
Logical implication.
Logical equivalence.
Logical equivalence iff is an equivalence crelation.
We now develop a generalization of results on crelations for arbitrary predicates.
The resulting theory can be applied to homogeneous binary crelations but also to
arbitrary n-ary predicates.
Local Open Scope list_scope.
A compact representation of non-dependent arities, with the codomain singled-out.
We define the various operations which define the algebra on binary crelations
Relation equivalence is an equivalence, and subrelation defines a partial order.
Partial Order.
A partial order is a preorder which is additionally antisymmetric.
We give an equivalent definition, up-to an equivalence crelation
on the carrier.
The equivalence proof is sufficient for proving that R must be a
morphism for equivalence (see Morphisms). It is also sufficient to
show that R is antisymmetric w.r.t. eqA
The partial order defined by subrelation and crelation equivalence.
Typeclasses Opaque relation_equivalence.