Library Coq.Classes.RelationClasses
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 relation definition while doing morphism search.
Section Defs.
Context {
A :
Type}.
We rebind relational properties in separate classes to be able to overload each proof.
Opaque for proof-search.
Typeclasses Opaque complement.
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 relation is Symmetric and Transitive.
Equivalence relations.
An Equivalence is a PER plus reflexivity.
An Equivalence is a PreOrder plus symmetry.
We can now define antisymmetry w.r.t. an equivalence relation on the carrier.
Any symmetric relation is equal to its inverse.
Inversing the larger structures
Rewrite relation on a given support: declares a relation as a rewrite
relation 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
relations. This is also done automatically by the Declare Relation A RA
commands.
Any Equivalence declared in the context is automatically considered
a rewrite relation.
Leibniz equality.
Leibinz equality eq is an equivalence relation.
The instance has low priority as it is always applicable
if only the type is constrained.
Default rewrite relations handled by setoid_rewrite.
Hints to drive the typeclass resolution avoiding loops
due to the use of full unification.
A HintDb for relations.
Ltac solve_relation :=
match goal with
| [ |- ?R ?x ?x ] => reflexivity
| [ H : ?R ?x ?y |- ?R ?y ?x ] => symmetry ; exact H
end.
Hint Extern 4 => solve_relation : relations.
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_relation :=
unfold flip,
impl,
arrow ;
try reduce ;
program_simpl ;
try (
solve [
dintuition ]).
Logical implication.
Logical equivalence.
Logical equivalence iff is an equivalence relation.
We now develop a generalization of results on relations for arbitrary predicates.
The resulting theory can be applied to homogeneous binary relations 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 can define abbreviations for operation and relation types based on arrows.
We define n-ary predicates as functions into Prop.
Unary predicates, or sets.
Homogeneous binary relations, equivalent to relation A.
We can close a predicate by universal or existential quantification.
Pointwise extension of a binary operation on T to a binary operation
on functions whose codomain is T.
For an operator on Prop this lifts the operator to a binary operation.
Pointwise lifting, equivalent to doing pointwise_extension and closing using predicate_all.
The n-ary equivalence relation, defined by lifting the 0-ary iff relation.
The n-ary implication relation, defined by lifting the 0-ary impl relation.
Notations for pointwise equivalence and implication of predicates.
The pointwise liftings of conjunction and disjunctions.
Note that these are binary_operations, building new relations out of old ones.
The always True and always False predicates.
Predicate equivalence is an equivalence, and predicate implication defines a preorder.
We define the various operations which define the algebra on binary relations,
from the general ones.
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 relation
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 relation equivalence.