Library Coq.Classes.RelationClasses
We allow to unfold the relation definition while doing morphism search.
Opaque for proof-search.
These are convertible.
We rebind relations in separate classes to be able to overload each proof.
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.
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 [ intuition ]).
Ltac obligation_tactic ::= simpl_relation.
Logical implication.
Logical equivalence.
Leibniz equality.
Various combinations of reflexivity, symmetry and transitivity.
A PreOrder is both Reflexive and Transitive.
A partial equivalence relation is Symmetric and Transitive.
Equivalence relations.
An Equivalence is a PER plus reflexivity.
We can now define antisymmetry w.r.t. an equivalence relation on the carrier.
Leibinz equality eq is an equivalence relation.
The instance has low priority as it is always applicable
if only the type is constrained.
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.
A compact representation of non-dependent arities, with the codomain singled-out.
Fixpoint arrows (
l :
list Type) (
r :
Type) :
Type :=
match l with
|
nil =>
r
|
A ::
l' =>
A ->
arrows l' r
end.
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.
Infix "<∙>" :=
predicate_equivalence (
at level 95,
no associativity) :
predicate_scope.
Infix "-∙>" :=
predicate_implication (
at level 70,
right associativity) :
predicate_scope.
Open Local Scope predicate_scope.
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.