1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* Typeclass-based relations, tactics and standard instances.
10
This is the basic theory needed to formalize morphisms and setoids.
12
Author: Matthieu Sozeau
13
Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
14
91405 Orsay, France *)
16
(* $Id: RelationClasses.v 12187 2009-06-13 19:36:59Z msozeau $ *)
18
Require Export Coq.Classes.Init.
19
Require Import Coq.Program.Basics.
20
Require Import Coq.Program.Tactics.
21
Require Import Coq.Relations.Relation_Definitions.
23
(** We allow to unfold the [relation] definition while doing morphism search. *)
25
Notation inverse R := (flip (R:relation _) : relation _).
27
Definition complement {A} (R : relation A) : relation A := fun x y => R x y -> False.
29
(** Opaque for proof-search. *)
30
Typeclasses Opaque complement.
32
(** These are convertible. *)
34
Lemma complement_inverse : forall A (R : relation A), complement (inverse R) = inverse (complement R).
35
Proof. reflexivity. Qed.
37
(** We rebind relations in separate classes to be able to overload each proof. *)
39
Set Implicit Arguments.
40
Unset Strict Implicit.
42
Class Reflexive {A} (R : relation A) :=
43
reflexivity : forall x, R x x.
45
Class Irreflexive {A} (R : relation A) :=
46
irreflexivity :> Reflexive (complement R).
48
Class Symmetric {A} (R : relation A) :=
49
symmetry : forall x y, R x y -> R y x.
51
Class Asymmetric {A} (R : relation A) :=
52
asymmetry : forall x y, R x y -> R y x -> False.
54
Class Transitive {A} (R : relation A) :=
55
transitivity : forall x y z, R x y -> R y z -> R x z.
57
Hint Resolve @irreflexivity : ord.
59
Unset Implicit Arguments.
61
(** A HintDb for relations. *)
63
Ltac solve_relation :=
65
| [ |- ?R ?x ?x ] => reflexivity
66
| [ H : ?R ?x ?y |- ?R ?y ?x ] => symmetry ; exact H
69
Hint Extern 4 => solve_relation : relations.
71
(** We can already dualize all these properties. *)
73
Program Instance flip_Reflexive `(Reflexive A R) : Reflexive (flip R) :=
76
Program Instance flip_Irreflexive `(Irreflexive A R) : Irreflexive (flip R) :=
79
Program Instance flip_Symmetric `(Symmetric A R) : Symmetric (flip R).
81
Solve Obligations using unfold flip ; intros ; tcapp symmetry ; assumption.
83
Program Instance flip_Asymmetric `(Asymmetric A R) : Asymmetric (flip R).
85
Solve Obligations using program_simpl ; unfold flip in * ; intros ; typeclass_app asymmetry ; eauto.
87
Program Instance flip_Transitive `(Transitive A R) : Transitive (flip R).
89
Solve Obligations using unfold flip ; program_simpl ; typeclass_app transitivity ; eauto.
91
Program Instance Reflexive_complement_Irreflexive `(Reflexive A (R : relation A))
92
: Irreflexive (complement R).
95
Proof. firstorder. Qed.
97
Program Instance complement_Symmetric `(Symmetric A (R : relation A)) : Symmetric (complement R).
100
Proof. firstorder. Qed.
102
(** * Standard instances. *)
106
| context [ _ <-> _ ] => fail 1
107
| _ => red in H ; try reduce_hyp H
112
| [ |- _ <-> _ ] => fail 1
113
| _ => red ; intros ; try reduce_goal
116
Tactic Notation "reduce" "in" hyp(Hid) := reduce_hyp Hid.
118
Ltac reduce := reduce_goal.
120
Tactic Notation "apply" "*" constr(t) :=
121
first [ refine t | refine (t _) | refine (t _ _) | refine (t _ _ _) | refine (t _ _ _ _) |
122
refine (t _ _ _ _ _) | refine (t _ _ _ _ _ _) | refine (t _ _ _ _ _ _ _) ].
124
Ltac simpl_relation :=
125
unfold flip, impl, arrow ; try reduce ; program_simpl ;
126
try ( solve [ intuition ]).
128
Ltac obligation_tactic ::= simpl_relation.
130
(** Logical implication. *)
132
Program Instance impl_Reflexive : Reflexive impl.
133
Program Instance impl_Transitive : Transitive impl.
135
(** Logical equivalence. *)
137
Program Instance iff_Reflexive : Reflexive iff.
138
Program Instance iff_Symmetric : Symmetric iff.
139
Program Instance iff_Transitive : Transitive iff.
141
(** Leibniz equality. *)
143
Program Instance eq_Reflexive : Reflexive (@eq A).
144
Program Instance eq_Symmetric : Symmetric (@eq A).
145
Program Instance eq_Transitive : Transitive (@eq A).
147
(** Various combinations of reflexivity, symmetry and transitivity. *)
149
(** A [PreOrder] is both Reflexive and Transitive. *)
151
Class PreOrder {A} (R : relation A) : Prop := {
152
PreOrder_Reflexive :> Reflexive R ;
153
PreOrder_Transitive :> Transitive R }.
155
(** A partial equivalence relation is Symmetric and Transitive. *)
157
Class PER {A} (R : relation A) : Prop := {
158
PER_Symmetric :> Symmetric R ;
159
PER_Transitive :> Transitive R }.
161
(** Equivalence relations. *)
163
Class Equivalence {A} (R : relation A) : Prop := {
164
Equivalence_Reflexive :> Reflexive R ;
165
Equivalence_Symmetric :> Symmetric R ;
166
Equivalence_Transitive :> Transitive R }.
168
(** An Equivalence is a PER plus reflexivity. *)
170
Instance Equivalence_PER `(Equivalence A R) : PER R | 10 :=
171
{ PER_Symmetric := Equivalence_Symmetric ;
172
PER_Transitive := Equivalence_Transitive }.
174
(** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *)
176
Class Antisymmetric A eqA `{equ : Equivalence A eqA} (R : relation A) :=
177
antisymmetry : forall x y, R x y -> R y x -> eqA x y.
179
Program Instance flip_antiSymmetric `(Antisymmetric A eqA R) :
180
! Antisymmetric A eqA (flip R).
182
(** Leibinz equality [eq] is an equivalence relation.
183
The instance has low priority as it is always applicable
184
if only the type is constrained. *)
186
Program Instance eq_equivalence : Equivalence (@eq A) | 10.
188
(** Logical equivalence [iff] is an equivalence relation. *)
190
Program Instance iff_equivalence : Equivalence iff.
192
(** We now develop a generalization of results on relations for arbitrary predicates.
193
The resulting theory can be applied to homogeneous binary relations but also to
194
arbitrary n-ary predicates. *)
196
Require Import Coq.Lists.List.
198
(* Notation " [ ] " := nil : list_scope. *)
199
(* Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) (at level 1) : list_scope. *)
201
(* Open Local Scope list_scope. *)
203
(** A compact representation of non-dependent arities, with the codomain singled-out. *)
205
Fixpoint arrows (l : list Type) (r : Type) : Type :=
208
| A :: l' => A -> arrows l' r
211
(** We can define abbreviations for operation and relation types based on [arrows]. *)
213
Definition unary_operation A := arrows (cons A nil) A.
214
Definition binary_operation A := arrows (cons A (cons A nil)) A.
215
Definition ternary_operation A := arrows (cons A (cons A (cons A nil))) A.
217
(** We define n-ary [predicate]s as functions into [Prop]. *)
219
Notation predicate l := (arrows l Prop).
221
(** Unary predicates, or sets. *)
223
Definition unary_predicate A := predicate (cons A nil).
225
(** Homogeneous binary relations, equivalent to [relation A]. *)
227
Definition binary_relation A := predicate (cons A (cons A nil)).
229
(** We can close a predicate by universal or existential quantification. *)
231
Fixpoint predicate_all (l : list Type) : predicate l -> Prop :=
234
| A :: tl => fun f => forall x : A, predicate_all tl (f x)
237
Fixpoint predicate_exists (l : list Type) : predicate l -> Prop :=
240
| A :: tl => fun f => exists x : A, predicate_exists tl (f x)
243
(** Pointwise extension of a binary operation on [T] to a binary operation
244
on functions whose codomain is [T].
245
For an operator on [Prop] this lifts the operator to a binary operation. *)
247
Fixpoint pointwise_extension {T : Type} (op : binary_operation T)
248
(l : list Type) : binary_operation (arrows l T) :=
250
| nil => fun R R' => op R R'
251
| A :: tl => fun R R' =>
252
fun x => pointwise_extension op tl (R x) (R' x)
255
(** Pointwise lifting, equivalent to doing [pointwise_extension] and closing using [predicate_all]. *)
257
Fixpoint pointwise_lifting (op : binary_relation Prop) (l : list Type) : binary_relation (predicate l) :=
259
| nil => fun R R' => op R R'
260
| A :: tl => fun R R' =>
261
forall x, pointwise_lifting op tl (R x) (R' x)
264
(** The n-ary equivalence relation, defined by lifting the 0-ary [iff] relation. *)
266
Definition predicate_equivalence {l : list Type} : binary_relation (predicate l) :=
267
pointwise_lifting iff l.
269
(** The n-ary implication relation, defined by lifting the 0-ary [impl] relation. *)
271
Definition predicate_implication {l : list Type} :=
272
pointwise_lifting impl l.
274
(** Notations for pointwise equivalence and implication of predicates. *)
276
Infix "<∙>" := predicate_equivalence (at level 95, no associativity) : predicate_scope.
277
Infix "-∙>" := predicate_implication (at level 70, right associativity) : predicate_scope.
279
Open Local Scope predicate_scope.
281
(** The pointwise liftings of conjunction and disjunctions.
282
Note that these are [binary_operation]s, building new relations out of old ones. *)
284
Definition predicate_intersection := pointwise_extension and.
285
Definition predicate_union := pointwise_extension or.
287
Infix "/∙\" := predicate_intersection (at level 80, right associativity) : predicate_scope.
288
Infix "\∙/" := predicate_union (at level 85, right associativity) : predicate_scope.
290
(** The always [True] and always [False] predicates. *)
292
Fixpoint true_predicate {l : list Type} : predicate l :=
295
| A :: tl => fun _ => @true_predicate tl
298
Fixpoint false_predicate {l : list Type} : predicate l :=
301
| A :: tl => fun _ => @false_predicate tl
304
Notation "∙⊤∙" := true_predicate : predicate_scope.
305
Notation "∙⊥∙" := false_predicate : predicate_scope.
307
(** Predicate equivalence is an equivalence, and predicate implication defines a preorder. *)
309
Program Instance predicate_equivalence_equivalence :
310
Equivalence (@predicate_equivalence l).
313
induction l ; firstorder.
317
induction l ; firstorder.
321
fold pointwise_lifting.
322
induction l. firstorder.
323
intros. simpl in *. pose (IHl (x x0) (y x0) (z x0)).
327
Program Instance predicate_implication_preorder :
328
PreOrder (@predicate_implication l).
331
induction l ; firstorder.
335
induction l. firstorder.
336
unfold predicate_implication in *. simpl in *.
337
intro. pose (IHl (x x0) (y x0) (z x0)). firstorder.
340
(** We define the various operations which define the algebra on binary relations,
341
from the general ones. *)
343
Definition relation_equivalence {A : Type} : relation (relation A) :=
344
@predicate_equivalence (cons _ (cons _ nil)).
346
Class subrelation {A:Type} (R R' : relation A) : Prop :=
347
is_subrelation : @predicate_implication (cons A (cons A nil)) R R'.
349
Implicit Arguments subrelation [[A]].
351
Definition relation_conjunction {A} (R : relation A) (R' : relation A) : relation A :=
352
@predicate_intersection (cons A (cons A nil)) R R'.
354
Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relation A :=
355
@predicate_union (cons A (cons A nil)) R R'.
357
(** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
359
Instance relation_equivalence_equivalence (A : Type) :
360
Equivalence (@relation_equivalence A).
361
Proof. intro A. exact (@predicate_equivalence_equivalence (cons A (cons A nil))). Qed.
363
Instance relation_implication_preorder : PreOrder (@subrelation A).
364
Proof. intro A. exact (@predicate_implication_preorder (cons A (cons A nil))). Qed.
366
(** *** Partial Order.
367
A partial order is a preorder which is additionally antisymmetric.
368
We give an equivalent definition, up-to an equivalence relation
371
Class PartialOrder {A} eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} :=
372
partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (inverse R)).
374
(** The equivalence proof is sufficient for proving that [R] must be a morphism
375
for equivalence (see Morphisms).
376
It is also sufficient to show that [R] is antisymmetric w.r.t. [eqA] *)
378
Instance partial_order_antisym `(PartialOrder A eqA R) : ! Antisymmetric A eqA R.
381
pose proof partial_order_equivalence as poe. do 3 red in poe.
382
apply <- poe. firstorder.
385
(** The partial order defined by subrelation and relation equivalence. *)
387
Program Instance subrelation_partial_order :
388
! PartialOrder (relation A) relation_equivalence subrelation.
392
unfold relation_equivalence in *. firstorder.
395
Typeclasses Opaque arrows predicate_implication predicate_equivalence
396
relation_equivalence pointwise_lifting.
added
removed
theories/Classes/RelationClasses.v
