# 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

Require Export Coq.Classes.Init.
Require Import Coq.Program.Basics.
Require Import Coq.Program.Tactics.
Require Import Coq.Relations.Relation_Definitions.

Generalizable Variables A B C D R S T U l eqA eqB eqC eqD.

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.

Class Reflexive (R : relation A) :=
reflexivity : forall x : A, R x x.

Definition complement (R : relation A) : relation A := fun x y => R x y -> False.

Opaque for proof-search.
Typeclasses Opaque complement.

These are convertible.
Lemma complement_inverse R : complement (flip R) = flip (complement R).

Class Irreflexive (R : relation A) :=
irreflexivity : Reflexive (complement R).

Class Symmetric (R : relation A) :=
symmetry : forall {x y}, R x y -> R y x.

Class Asymmetric (R : relation A) :=
asymmetry : forall {x y}, R x y -> R y x -> False.

Class Transitive (R : relation A) :=
transitivity : forall {x y z}, R x y -> R y z -> R x z.

Various combinations of reflexivity, symmetry and transitivity.
A PreOrder is both Reflexive and Transitive.

Class PreOrder (R : relation A) : Prop := {
#[global] PreOrder_Reflexive :: Reflexive R | 2 ;
#[global] PreOrder_Transitive :: Transitive R | 2 }.

A StrictOrder is both Irreflexive and Transitive.

Class StrictOrder (R : relation A) : Prop := {
#[global] StrictOrder_Irreflexive :: Irreflexive R ;
#[global] StrictOrder_Transitive :: Transitive R }.

By definition, a strict order is also asymmetric
Global Instance StrictOrder_Asymmetric `(StrictOrder R) : Asymmetric R.

A partial equivalence relation is Symmetric and Transitive.

Class PER (R : relation A) : Prop := {
#[global] PER_Symmetric :: Symmetric R | 3 ;
#[global] PER_Transitive :: Transitive R | 3 }.

Equivalence relations.

Class Equivalence (R : relation A) : Prop := {
#[global] Equivalence_Reflexive :: Reflexive R ;
#[global] Equivalence_Symmetric :: Symmetric R ;
#[global] Equivalence_Transitive :: Transitive R }.

An Equivalence is a PER plus reflexivity.

Global Instance Equivalence_PER {R} `(E:Equivalence R) : PER R | 10 :=
{ }.

An Equivalence is a PreOrder plus symmetry.

Global Instance Equivalence_PreOrder {R} `(E:Equivalence R) : PreOrder R | 10 :=
{ }.

We can now define antisymmetry w.r.t. an equivalence relation on the carrier.

Class Antisymmetric eqA `{equ : Equivalence eqA} (R : relation A) :=
antisymmetry : forall {x y}, R x y -> R y x -> eqA x y.

Class subrelation (R R' : relation A) : Prop :=
is_subrelation : forall {x y}, R x y -> R' x y.

Any symmetric relation is equal to its inverse.

Lemma subrelation_symmetric R `(Symmetric R) : subrelation (flip R) R.

Section flip.

Lemma flip_Reflexive `{Reflexive R} : Reflexive (flip R).

Program Definition flip_Irreflexive `(Irreflexive R) : Irreflexive (flip R) :=
irreflexivity (R:=R).

Program Definition flip_Symmetric `(Symmetric R) : Symmetric (flip R) :=
fun x y H => symmetry (R:=R) H.

Program Definition flip_Asymmetric `(Asymmetric R) : Asymmetric (flip R) :=
fun x y H H' => asymmetry (R:=R) H H'.

Program Definition flip_Transitive `(Transitive R) : Transitive (flip R) :=
fun x y z H H' => transitivity (R:=R) H' H.

Program Definition flip_Antisymmetric `(Antisymmetric eqA R) :
Antisymmetric eqA (flip R).

Inversing the larger structures

Lemma flip_PreOrder `(PreOrder R) : PreOrder (flip R).

Lemma flip_StrictOrder `(StrictOrder R) : StrictOrder (flip R).

Lemma flip_PER `(PER R) : PER (flip R).

Lemma flip_Equivalence `(Equivalence R) : Equivalence (flip R).

End flip.

Section complement.

Definition complement_Irreflexive `(Reflexive R)
: Irreflexive (complement R).

Definition complement_Symmetric `(Symmetric R) : Symmetric (complement R).
End complement.

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 on a given type `A`. This is also done automatically by the Declare Relation A RA commands. It has no mode declaration: it will assign `?A := Prop, ?R := iff` on an entirely unspecified query `RewriteRelation ?A ?R`, or any prefered rewrite relation of priority < 2.

Class RewriteRelation (RA : relation A).

Leibniz equality.
Section Leibniz.
Global Instance eq_Reflexive : Reflexive (@eq A) := @eq_refl A.
Global Instance eq_Symmetric : Symmetric (@eq A) := @eq_sym A.
Global Instance eq_Transitive : Transitive (@eq A) := @eq_trans A.

Leibinz equality eq is an equivalence relation. The instance has low priority as it is always applicable if only the type is constrained.

Global Program Instance eq_equivalence : Equivalence (@eq A) | 10.
End Leibniz.

Leibniz disequality.
Section LeibnizNot.
Disequality is symmetric.
Global Instance neq_Symmetric : Symmetric (fun x y : A => x <> y) := (@not_eq_sym A).
End LeibnizNot.
End Defs.

Default rewrite relations handled by setoid_rewrite on Prop.
#[global]
Instance inverse_impl_rewrite_relation : RewriteRelation (flip impl) | 3 := {}.
#[global]
Instance impl_rewrite_relation : RewriteRelation impl | 3 := {}.
#[global]
Instance iff_rewrite_relation : RewriteRelation iff | 2 := {}.

Any Equivalence declared in the context is automatically considered a rewrite relation. This only applies if the relation is at least partially defined: setoid_rewrite won't try to infer arbitrary user rewrite relations.

Definition equivalence_rewrite_relation `(eqa : Equivalence A eqA) : RewriteRelation eqA :=
Build_RewriteRelation _.

Ltac equiv_rewrite_relation R :=
tryif is_evar R then fail
else class_apply equivalence_rewrite_relation.

#[global]
Hint Extern 10 (@RewriteRelation ?A ?R) => equiv_rewrite_relation R : typeclass_instances.

Hints to drive the typeclass resolution avoiding loops due to the use of full unification.
#[global]
Hint Extern 1 (Reflexive (complement _)) => class_apply @irreflexivity : typeclass_instances.
#[global]
Hint Extern 3 (Symmetric (complement _)) => class_apply complement_Symmetric : typeclass_instances.
#[global]
Hint Extern 3 (Irreflexive (complement _)) => class_apply complement_Irreflexive : typeclass_instances.

#[global]
Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances.
#[global]
Hint Extern 3 (Irreflexive (flip _)) => class_apply flip_Irreflexive : typeclass_instances.
#[global]
Hint Extern 3 (Symmetric (flip _)) => class_apply flip_Symmetric : typeclass_instances.
#[global]
Hint Extern 3 (Asymmetric (flip _)) => class_apply flip_Asymmetric : typeclass_instances.
#[global]
Hint Extern 3 (Antisymmetric (flip _)) => class_apply flip_Antisymmetric : typeclass_instances.
#[global]
Hint Extern 3 (Transitive (flip _)) => class_apply flip_Transitive : typeclass_instances.
#[global]
Hint Extern 3 (StrictOrder (flip _)) => class_apply flip_StrictOrder : typeclass_instances.
#[global]
Hint Extern 3 (PreOrder (flip _)) => class_apply flip_PreOrder : typeclass_instances.

#[global]
Hint Extern 4 (subrelation (flip _) _) =>
class_apply @subrelation_symmetric : typeclass_instances.

Arguments irreflexivity {A R Irreflexive} [x] _ : rename.
Arguments symmetry {A} {R} {_} [x] [y] _.
Arguments asymmetry {A} {R} {_} [x] [y] _ _.
Arguments transitivity {A} {R} {_} [x] [y] [z] _ _.
Arguments Antisymmetric A eqA {_} _.

#[global]
Hint Resolve irreflexivity : ord.

Unset Implicit Arguments.

Ltac solve_relation :=
match goal with
| [ |- ?R ?x ?x ] => reflexivity
| [ H : ?R ?x ?y |- ?R ?y ?x ] => symmetry ; exact H
end.

#[global]
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 auto with relations ]).

Local Obligation Tactic := try solve [ simpl_relation ].

Logical implication.

#[global]
Program Instance impl_Reflexive : Reflexive impl.
#[global]
Program Instance impl_Transitive : Transitive impl.

Logical equivalence.

#[global]
Instance iff_Reflexive : Reflexive iff := iff_refl.
#[global]
Instance iff_Symmetric : Symmetric iff := iff_sym.
#[global]
Instance iff_Transitive : Transitive iff := iff_trans.

Logical equivalence iff is an equivalence relation.

#[global]
Program Instance iff_equivalence : Equivalence iff.

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.

Inductive Tlist : Type := Tnil : Tlist | Tcons : Type -> Tlist -> Tlist.
Local Infix "::" := Tcons.

Fixpoint arrows (l : Tlist) (r : Type) : Type :=
match l with
| Tnil => 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.

Notation predicate l := (arrows l Prop).

Unary predicates, or sets.

Definition unary_predicate A := predicate (A::Tnil).

Homogeneous binary relations, equivalent to relation A.
We can close a predicate by universal or existential quantification.

Fixpoint predicate_all (l : Tlist) : predicate l -> Prop :=
match l with
| Tnil => fun f => f
| A :: tl => fun f => forall x : A, predicate_all tl (f x)
end.

Fixpoint predicate_exists (l : Tlist) : predicate l -> Prop :=
match l with
| Tnil => fun f => f
| A :: tl => fun f => exists x : A, predicate_exists tl (f x)
end.

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.

Fixpoint pointwise_extension {T : Type} (op : binary_operation T)
(l : Tlist) : binary_operation (arrows l T) :=
match l with
| Tnil => fun R R' => op R R'
| A :: tl => fun R R' =>
fun x => pointwise_extension op tl (R x) (R' x)
end.

Pointwise lifting, equivalent to doing pointwise_extension and closing using predicate_all.

Fixpoint pointwise_lifting (op : binary_relation Prop) (l : Tlist) : binary_relation (predicate l) :=
match l with
| Tnil => fun R R' => op R R'
| A :: tl => fun R R' =>
forall x, pointwise_lifting op tl (R x) (R' x)
end.

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.

Declare Scope predicate_scope.

Infix "<∙>" := predicate_equivalence (at level 95, no associativity) : predicate_scope.
Infix "-∙>" := predicate_implication (at level 70, right associativity) : predicate_scope.

Local Open Scope predicate_scope.

The pointwise liftings of conjunction and disjunctions. Note that these are binary_operations, building new relations out of old ones.

Definition predicate_intersection := pointwise_extension and.
Definition predicate_union := pointwise_extension or.

Infix "/∙\" := predicate_intersection (at level 80, right associativity) : predicate_scope.
Infix "\∙/" := predicate_union (at level 85, right associativity) : predicate_scope.

The always True and always False predicates.

Fixpoint true_predicate {l : Tlist} : predicate l :=
match l with
| Tnil => True
| A :: tl => fun _ => @true_predicate tl
end.

Fixpoint false_predicate {l : Tlist} : predicate l :=
match l with
| Tnil => False
| A :: tl => fun _ => @false_predicate tl
end.

Notation "∙⊤∙" := true_predicate : predicate_scope.
Notation "∙⊥∙" := false_predicate : predicate_scope.

Predicate equivalence is an equivalence, and predicate implication defines a preorder.

#[global]
Program Instance predicate_equivalence_equivalence {l} :
Equivalence (@predicate_equivalence l).

#[global]
Program Instance predicate_implication_preorder {l} :
PreOrder (@predicate_implication l).

We define the various operations which define the algebra on binary relations, from the general ones.

Section Binary.
Context {A : Type}.

Definition relation_equivalence : relation (relation A) :=
@predicate_equivalence (_::_::Tnil).

Global Instance relation_equivalence_rewrite_relation: RewriteRelation relation_equivalence := {}.

Definition relation_conjunction (R : relation A) (R' : relation A) : relation A :=
@predicate_intersection (A::A::Tnil) R R'.

Definition relation_disjunction (R : relation A) (R' : relation A) : relation A :=
@predicate_union (A::A::Tnil) R R'.

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

Global Instance partial_order_antisym `(PartialOrder eqA R) : Antisymmetric A eqA R.

Lemma PartialOrder_inverse `(PartialOrder eqA R) : PartialOrder eqA (flip R).
End Binary.

#[global]
Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : typeclass_instances.

The partial order defined by subrelation and relation equivalence.

#[global]
Program Instance subrelation_partial_order {A} :
PartialOrder (@relation_equivalence A) subrelation.

Global Typeclasses Opaque arrows predicate_implication predicate_equivalence
relation_equivalence pointwise_lifting.