summaryrefslogtreecommitdiff
path: root/theories/Classes/RelationClasses.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /theories/Classes/RelationClasses.v
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'theories/Classes/RelationClasses.v')
-rw-r--r--theories/Classes/RelationClasses.v193
1 files changed, 122 insertions, 71 deletions
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index e1de9ee9..9b848551 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -6,14 +7,15 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* Typeclass-based relations, tactics and standard instances.
+(** * 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 - UniversitÃcopyright Paris Sud
- 91405 Orsay, France *)
+ Institution: LRI, CNRS UMR 8623 - University Paris Sud
+*)
-(* $Id: RelationClasses.v 12187 2009-06-13 19:36:59Z msozeau $ *)
+(* $Id$ *)
Require Export Coq.Classes.Init.
Require Import Coq.Program.Basics.
@@ -42,16 +44,18 @@ Unset Strict Implicit.
Class Reflexive {A} (R : relation A) :=
reflexivity : forall x, R x x.
-Class Irreflexive {A} (R : relation A) :=
- irreflexivity :> Reflexive (complement R).
+Class Irreflexive {A} (R : relation A) :=
+ irreflexivity : Reflexive (complement R).
-Class Symmetric {A} (R : relation A) :=
+Hint Extern 1 (Reflexive (complement _)) => class_apply @irreflexivity : typeclass_instances.
+
+Class Symmetric {A} (R : relation A) :=
symmetry : forall x y, R x y -> R y x.
-Class Asymmetric {A} (R : relation A) :=
+Class Asymmetric {A} (R : relation A) :=
asymmetry : forall x y, R x y -> R y x -> False.
-Class Transitive {A} (R : relation A) :=
+Class Transitive {A} (R : relation A) :=
transitivity : forall x y z, R x y -> R y z -> R x z.
Hint Resolve @irreflexivity : ord.
@@ -61,7 +65,7 @@ Unset Implicit Arguments.
(** A HintDb for relations. *)
Ltac solve_relation :=
- match goal with
+ match goal with
| [ |- ?R ?x ?x ] => reflexivity
| [ H : ?R ?x ?y |- ?R ?y ?x ] => symmetry ; exact H
end.
@@ -70,34 +74,39 @@ Hint Extern 4 => solve_relation : relations.
(** We can already dualize all these properties. *)
-Program Instance flip_Reflexive `(Reflexive A R) : Reflexive (flip R) :=
- reflexivity (R:=R).
+Generalizable Variables A B C D R S T U l eqA eqB eqC eqD.
-Program Instance flip_Irreflexive `(Irreflexive A R) : Irreflexive (flip R) :=
- irreflexivity (R:=R).
+Program Lemma flip_Reflexive `(Reflexive A R) : Reflexive (flip R).
+Proof. tauto. Qed.
+
+Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances.
-Program Instance flip_Symmetric `(Symmetric A R) : Symmetric (flip R).
+Program Definition flip_Irreflexive `(Irreflexive A R) : Irreflexive (flip R) :=
+ irreflexivity (R:=R).
- Solve Obligations using unfold flip ; intros ; tcapp symmetry ; assumption.
+Program Definition flip_Symmetric `(Symmetric A R) : Symmetric (flip R) :=
+ fun x y H => symmetry (R:=R) H.
-Program Instance flip_Asymmetric `(Asymmetric A R) : Asymmetric (flip R).
-
- Solve Obligations using program_simpl ; unfold flip in * ; intros ; typeclass_app asymmetry ; eauto.
+Program Definition flip_Asymmetric `(Asymmetric A R) : Asymmetric (flip R) :=
+ fun x y H H' => asymmetry (R:=R) H H'.
-Program Instance flip_Transitive `(Transitive A R) : Transitive (flip R).
+Program Definition flip_Transitive `(Transitive A R) : Transitive (flip R) :=
+ fun x y z H H' => transitivity (R:=R) H' H.
- Solve Obligations using unfold flip ; program_simpl ; typeclass_app transitivity ; eauto.
+Hint Extern 3 (Irreflexive (flip _)) => class_apply flip_Irreflexive : typeclass_instances.
+Hint Extern 3 (Symmetric (flip _)) => class_apply flip_Symmetric : typeclass_instances.
+Hint Extern 3 (Asymmetric (flip _)) => class_apply flip_Asymmetric : typeclass_instances.
+Hint Extern 3 (Transitive (flip _)) => class_apply flip_Transitive : typeclass_instances.
-Program Instance Reflexive_complement_Irreflexive `(Reflexive A (R : relation A))
+Definition Reflexive_complement_Irreflexive `(Reflexive A (R : relation A))
: Irreflexive (complement R).
+Proof. firstorder. Qed.
- Next Obligation.
- Proof. firstorder. Qed.
-
-Program Instance complement_Symmetric `(Symmetric A (R : relation A)) : Symmetric (complement R).
+Definition complement_Symmetric `(Symmetric A (R : relation A)) : Symmetric (complement R).
+Proof. firstorder. Qed.
- Next Obligation.
- Proof. firstorder. Qed.
+Hint Extern 3 (Symmetric (complement _)) => class_apply complement_Symmetric : typeclass_instances.
+Hint Extern 3 (Irreflexive (complement _)) => class_apply Reflexive_complement_Irreflexive : typeclass_instances.
(** * Standard instances. *)
@@ -117,7 +126,7 @@ Tactic Notation "reduce" "in" hyp(Hid) := reduce_hyp Hid.
Ltac reduce := reduce_goal.
-Tactic Notation "apply" "*" constr(t) :=
+Tactic Notation "apply" "*" constr(t) :=
first [ refine t | refine (t _) | refine (t _ _) | refine (t _ _ _) | refine (t _ _ _ _) |
refine (t _ _ _ _ _) | refine (t _ _ _ _ _ _) | refine (t _ _ _ _ _ _ _) ].
@@ -125,7 +134,7 @@ Ltac simpl_relation :=
unfold flip, impl, arrow ; try reduce ; program_simpl ;
try ( solve [ intuition ]).
-Ltac obligation_tactic ::= simpl_relation.
+Local Obligation Tactic := simpl_relation.
(** Logical implication. *)
@@ -174,13 +183,14 @@ Instance Equivalence_PER `(Equivalence A R) : PER R | 10 :=
(** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *)
Class Antisymmetric A eqA `{equ : Equivalence A eqA} (R : relation A) :=
- antisymmetry : forall x y, R x y -> R y x -> eqA x y.
+ antisymmetry : forall {x y}, R x y -> R y x -> eqA x y.
-Program Instance flip_antiSymmetric `(Antisymmetric A eqA R) :
- ! Antisymmetric A eqA (flip R).
+Program Definition flip_antiSymmetric `(Antisymmetric A eqA R) :
+ Antisymmetric A eqA (flip R).
+Proof. firstorder. Qed.
(** Leibinz equality [eq] is an equivalence relation.
- The instance has low priority as it is always applicable
+ The instance has low priority as it is always applicable
if only the type is constrained. *)
Program Instance eq_equivalence : Equivalence (@eq A) | 10.
@@ -193,26 +203,24 @@ Program Instance iff_equivalence : Equivalence iff.
The resulting theory can be applied to homogeneous binary relations but also to
arbitrary n-ary predicates. *)
-Require Import Coq.Lists.List.
+Local Open Scope list_scope.
(* Notation " [ ] " := nil : list_scope. *)
(* Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) (at level 1) : list_scope. *)
-(* Open Local Scope list_scope. *)
-
(** A compact representation of non-dependent arities, with the codomain singled-out. *)
-Fixpoint arrows (l : list Type) (r : Type) : Type :=
- match l with
+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]. *)
-Definition unary_operation A := arrows (cons A nil) A.
-Definition binary_operation A := arrows (cons A (cons A nil)) A.
-Definition ternary_operation A := arrows (cons A (cons A (cons A nil))) A.
+Definition unary_operation A := arrows (A::nil) A.
+Definition binary_operation A := arrows (A::A::nil) A.
+Definition ternary_operation A := arrows (A::A::A::nil) A.
(** We define n-ary [predicate]s as functions into [Prop]. *)
@@ -220,13 +228,13 @@ Notation predicate l := (arrows l Prop).
(** Unary predicates, or sets. *)
-Definition unary_predicate A := predicate (cons A nil).
+Definition unary_predicate A := predicate (A::nil).
(** Homogeneous binary relations, equivalent to [relation A]. *)
-Definition binary_relation A := predicate (cons A (cons A nil)).
+Definition binary_relation A := predicate (A::A::nil).
-(** We can close a predicate by universal or existential quantification. *)
+(** We can close a predicate by universal or existential quantification. *)
Fixpoint predicate_all (l : list Type) : predicate l -> Prop :=
match l with
@@ -240,7 +248,7 @@ Fixpoint predicate_exists (l : list Type) : predicate l -> Prop :=
| 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
+(** 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. *)
@@ -248,7 +256,7 @@ Fixpoint pointwise_extension {T : Type} (op : binary_operation T)
(l : list Type) : binary_operation (arrows l T) :=
match l with
| nil => fun R R' => op R R'
- | A :: tl => fun R R' =>
+ | A :: tl => fun R R' =>
fun x => pointwise_extension op tl (R x) (R' x)
end.
@@ -257,7 +265,7 @@ Fixpoint pointwise_extension {T : Type} (op : binary_operation T)
Fixpoint pointwise_lifting (op : binary_relation Prop) (l : list Type) : binary_relation (predicate l) :=
match l with
| nil => fun R R' => op R R'
- | A :: tl => fun R R' =>
+ | A :: tl => fun R R' =>
forall x, pointwise_lifting op tl (R x) (R' x)
end.
@@ -289,7 +297,7 @@ Infix "\∙/" := predicate_union (at level 85, right associativity) : predicate_
(** The always [True] and always [False] predicates. *)
-Fixpoint true_predicate {l : list Type} : predicate l :=
+Fixpoint true_predicate {l : list Type} : predicate l :=
match l with
| nil => True
| A :: tl => fun _ => @true_predicate tl
@@ -306,17 +314,13 @@ Notation "∙⊥∙" := false_predicate : predicate_scope.
(** Predicate equivalence is an equivalence, and predicate implication defines a preorder. *)
-Program Instance predicate_equivalence_equivalence :
- Equivalence (@predicate_equivalence l).
-
+Program Instance predicate_equivalence_equivalence : Equivalence (@predicate_equivalence l).
Next Obligation.
induction l ; firstorder.
Qed.
-
Next Obligation.
induction l ; firstorder.
Qed.
-
Next Obligation.
fold pointwise_lifting.
induction l. firstorder.
@@ -326,59 +330,59 @@ Program Instance predicate_equivalence_equivalence :
Program Instance predicate_implication_preorder :
PreOrder (@predicate_implication l).
-
Next Obligation.
induction l ; firstorder.
Qed.
-
Next Obligation.
induction l. firstorder.
- unfold predicate_implication in *. simpl in *.
+ unfold predicate_implication in *. simpl in *.
intro. pose (IHl (x x0) (y x0) (z x0)). firstorder.
Qed.
-(** We define the various operations which define the algebra on binary relations,
+(** We define the various operations which define the algebra on binary relations,
from the general ones. *)
Definition relation_equivalence {A : Type} : relation (relation A) :=
- @predicate_equivalence (cons _ (cons _ nil)).
+ @predicate_equivalence (_::_::nil).
Class subrelation {A:Type} (R R' : relation A) : Prop :=
- is_subrelation : @predicate_implication (cons A (cons A nil)) R R'.
+ is_subrelation : @predicate_implication (A::A::nil) R R'.
Implicit Arguments subrelation [[A]].
Definition relation_conjunction {A} (R : relation A) (R' : relation A) : relation A :=
- @predicate_intersection (cons A (cons A nil)) R R'.
+ @predicate_intersection (A::A::nil) R R'.
Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relation A :=
- @predicate_union (cons A (cons A nil)) R R'.
+ @predicate_union (A::A::nil) R R'.
(** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
+Set Automatic Introduction.
+
Instance relation_equivalence_equivalence (A : Type) :
Equivalence (@relation_equivalence A).
-Proof. intro A. exact (@predicate_equivalence_equivalence (cons A (cons A nil))). Qed.
+Proof. exact (@predicate_equivalence_equivalence (A::A::nil)). Qed.
-Instance relation_implication_preorder : PreOrder (@subrelation A).
-Proof. intro A. exact (@predicate_implication_preorder (cons A (cons A nil))). Qed.
+Instance relation_implication_preorder A : PreOrder (@subrelation A).
+Proof. exact (@predicate_implication_preorder (A::A::nil)). Qed.
(** *** Partial Order.
A partial order is a preorder which is additionally antisymmetric.
- We give an equivalent definition, up-to an equivalence relation
+ We give an equivalent definition, up-to an equivalence relation
on the carrier. *)
Class PartialOrder {A} eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} :=
partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (inverse R)).
-(** The equivalence proof is sufficient for proving that [R] must be a morphism
+(** 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] *)
Instance partial_order_antisym `(PartialOrder A eqA R) : ! Antisymmetric A eqA R.
Proof with auto.
- reduce_goal.
- pose proof partial_order_equivalence as poe. do 3 red in poe.
+ reduce_goal.
+ pose proof partial_order_equivalence as poe. do 3 red in poe.
apply <- poe. firstorder.
Qed.
@@ -392,5 +396,52 @@ Program Instance subrelation_partial_order :
unfold relation_equivalence in *. firstorder.
Qed.
-Typeclasses Opaque arrows predicate_implication predicate_equivalence
+Typeclasses Opaque arrows predicate_implication predicate_equivalence
relation_equivalence pointwise_lifting.
+
+(** 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. *)
+
+Class RewriteRelation {A : Type} (RA : relation A).
+
+Instance: RewriteRelation impl.
+Instance: RewriteRelation iff.
+Instance: RewriteRelation (@relation_equivalence A).
+
+(** Any [Equivalence] declared in the context is automatically considered
+ a rewrite relation. *)
+
+Instance equivalence_rewrite_relation `(Equivalence A eqA) : RewriteRelation eqA.
+
+(** Strict Order *)
+
+Class StrictOrder {A : Type} (R : relation A) := {
+ StrictOrder_Irreflexive :> Irreflexive R ;
+ StrictOrder_Transitive :> Transitive R
+}.
+
+Instance StrictOrder_Asymmetric `(StrictOrder A R) : Asymmetric R.
+Proof. firstorder. Qed.
+
+(** Inversing a [StrictOrder] gives another [StrictOrder] *)
+
+Lemma StrictOrder_inverse `(StrictOrder A R) : StrictOrder (inverse R).
+Proof. firstorder. Qed.
+
+(** Same for [PartialOrder]. *)
+
+Lemma PreOrder_inverse `(PreOrder A R) : PreOrder (inverse R).
+Proof. firstorder. Qed.
+
+Hint Extern 3 (StrictOrder (inverse _)) => class_apply StrictOrder_inverse : typeclass_instances.
+Hint Extern 3 (PreOrder (inverse _)) => class_apply PreOrder_inverse : typeclass_instances.
+
+Lemma PartialOrder_inverse `(PartialOrder A eqA R) : PartialOrder eqA (inverse R).
+Proof. firstorder. Qed.
+
+Hint Extern 3 (PartialOrder (inverse _)) => class_apply PartialOrder_inverse : typeclass_instances.