diff options
Diffstat (limited to 'theories/Classes/RelationClasses.v')
| -rw-r--r-- | theories/Classes/RelationClasses.v | 116 |
1 files changed, 60 insertions, 56 deletions
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 9a43a1ba..f95894be 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -1,4 +1,3 @@ -(* -*- coq-prog-name: "coqtop.byte"; coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.RelationClasses") -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -14,7 +13,7 @@ Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud 91405 Orsay, France *) -(* $Id: RelationClasses.v 11282 2008-07-28 11:51:53Z msozeau $ *) +(* $Id: RelationClasses.v 11800 2009-01-18 18:34:15Z msozeau $ *) Require Export Coq.Classes.Init. Require Import Coq.Program.Basics. @@ -23,12 +22,13 @@ Require Export Coq.Relations.Relation_Definitions. (** We allow to unfold the [relation] definition while doing morphism search. *) -Typeclasses unfold relation. - Notation inverse R := (flip (R:relation _) : relation _). Definition complement {A} (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 : forall A (R : relation A), complement (inverse R) = inverse (complement R). @@ -39,64 +39,65 @@ Proof. reflexivity. Qed. Set Implicit Arguments. Unset Strict Implicit. -Class Reflexive A (R : relation A) := +Class Reflexive {A} (R : relation A) := reflexivity : forall x, R x x. -Class Irreflexive A (R : relation A) := +Class Irreflexive {A} (R : relation A) := irreflexivity :> Reflexive (complement R). -Class Symmetric A (R : relation A) := +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. Unset Implicit Arguments. +(** 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. *) -Program Instance flip_Reflexive [ Reflexive A R ] : Reflexive (flip R) := - reflexivity := reflexivity (R:=R). +Program Instance flip_Reflexive `(Reflexive A R) : Reflexive (flip R) := + reflexivity (R:=R). -Program Instance flip_Irreflexive [ Irreflexive A R ] : Irreflexive (flip R) := - irreflexivity := irreflexivity (R:=R). +Program Instance flip_Irreflexive `(Irreflexive A R) : Irreflexive (flip R) := + irreflexivity (R:=R). -Program Instance flip_Symmetric [ Symmetric A R ] : Symmetric (flip R). +Program Instance flip_Symmetric `(Symmetric A R) : Symmetric (flip R). - Solve Obligations using unfold flip ; program_simpl ; clapply Symmetric. + Solve Obligations using unfold flip ; intros ; tcapp symmetry ; assumption. -Program Instance flip_Asymmetric [ Asymmetric A R ] : Asymmetric (flip R). +Program Instance flip_Asymmetric `(Asymmetric A R) : Asymmetric (flip R). - Solve Obligations using program_simpl ; unfold flip in * ; intros ; clapply asymmetry. + Solve Obligations using program_simpl ; unfold flip in * ; intros ; typeclass_app asymmetry ; eauto. -Program Instance flip_Transitive [ Transitive A R ] : Transitive (flip R). +Program Instance flip_Transitive `(Transitive A R) : Transitive (flip R). - Solve Obligations using unfold flip ; program_simpl ; clapply transitivity. + Solve Obligations using unfold flip ; program_simpl ; typeclass_app transitivity ; eauto. -Program Instance Reflexive_complement_Irreflexive [ Reflexive A (R : relation A) ] +Program Instance Reflexive_complement_Irreflexive `(Reflexive A (R : relation A)) : Irreflexive (complement R). Next Obligation. - Proof. - unfold complement. - red. intros H. - intros H' ; apply H'. - apply reflexivity. - Qed. - + Proof. firstorder. Qed. -Program Instance complement_Symmetric [ Symmetric A (R : relation A) ] : Symmetric (complement R). +Program Instance complement_Symmetric `(Symmetric A (R : relation A)) : Symmetric (complement R). Next Obligation. - Proof. - red ; intros H'. - apply (H (symmetry H')). - Qed. + Proof. firstorder. Qed. (** * Standard instances. *) @@ -147,52 +148,52 @@ Program Instance eq_Transitive : Transitive (@eq A). (** A [PreOrder] is both Reflexive and Transitive. *) -Class PreOrder A (R : relation A) : Prop := +Class PreOrder {A} (R : relation A) : Prop := { PreOrder_Reflexive :> Reflexive R ; - PreOrder_Transitive :> Transitive R. + PreOrder_Transitive :> Transitive R }. (** A partial equivalence relation is Symmetric and Transitive. *) -Class PER (carrier : Type) (pequiv : relation carrier) : Prop := - PER_Symmetric :> Symmetric pequiv ; - PER_Transitive :> Transitive pequiv. +Class PER {A} (R : relation A) : Prop := { + PER_Symmetric :> Symmetric R ; + PER_Transitive :> Transitive R }. (** Equivalence relations. *) -Class Equivalence (carrier : Type) (equiv : relation carrier) : Prop := - Equivalence_Reflexive :> Reflexive equiv ; - Equivalence_Symmetric :> Symmetric equiv ; - Equivalence_Transitive :> Transitive equiv. +Class Equivalence {A} (R : relation A) : Prop := { + Equivalence_Reflexive :> Reflexive R ; + Equivalence_Symmetric :> Symmetric R ; + Equivalence_Transitive :> Transitive R }. (** An Equivalence is a PER plus reflexivity. *) -Instance Equivalence_PER [ Equivalence A R ] : PER A R | 10 := - PER_Symmetric := Equivalence_Symmetric ; - PER_Transitive := Equivalence_Transitive. +Instance Equivalence_PER `(Equivalence A R) : PER R | 10 := + { PER_Symmetric := Equivalence_Symmetric ; + PER_Transitive := Equivalence_Transitive }. (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *) -Class Antisymmetric ((equ : Equivalence A eqA)) (R : relation A) := +Class Antisymmetric A eqA `{equ : Equivalence A eqA} (R : relation A) := antisymmetry : forall x y, R x y -> R y x -> eqA x y. -Program Instance flip_antiSymmetric {{Antisymmetric A eqA R}} : +Program Instance flip_antiSymmetric `(Antisymmetric A eqA R) : ! Antisymmetric A eqA (flip R). (** Leibinz equality [eq] is an equivalence relation. The instance has low priority as it is always applicable if only the type is constrained. *) -Program Instance eq_equivalence : Equivalence A (@eq A) | 10. +Program Instance eq_equivalence : Equivalence (@eq A) | 10. (** Logical equivalence [iff] is an equivalence relation. *) -Program Instance iff_equivalence : Equivalence Prop iff. +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. *) -Require Import List. +Require Import Coq.Lists.List. (* Notation " [ ] " := nil : list_scope. *) (* Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) (at level 1) : list_scope. *) @@ -273,7 +274,7 @@ Definition predicate_implication {l : list Type} := (** Notations for pointwise equivalence and implication of predicates. *) Infix "<∙>" := predicate_equivalence (at level 95, no associativity) : predicate_scope. -Infix "-∙>" := predicate_implication (at level 70) : predicate_scope. +Infix "-∙>" := predicate_implication (at level 70, right associativity) : predicate_scope. Open Local Scope predicate_scope. @@ -306,7 +307,7 @@ Notation "∙⊥∙" := false_predicate : predicate_scope. (** Predicate equivalence is an equivalence, and predicate implication defines a preorder. *) Program Instance predicate_equivalence_equivalence : - Equivalence (predicate l) predicate_equivalence. + Equivalence (@predicate_equivalence l). Next Obligation. induction l ; firstorder. @@ -324,7 +325,7 @@ Program Instance predicate_equivalence_equivalence : Qed. Program Instance predicate_implication_preorder : - PreOrder (predicate l) predicate_implication. + PreOrder (@predicate_implication l). Next Obligation. induction l ; firstorder. @@ -356,10 +357,10 @@ Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relatio (** Relation equivalence is an equivalence, and subrelation defines a partial order. *) Instance relation_equivalence_equivalence (A : Type) : - Equivalence (relation A) relation_equivalence. + Equivalence (@relation_equivalence A). Proof. intro A. exact (@predicate_equivalence_equivalence (cons A (cons A nil))). Qed. -Instance relation_implication_preorder : PreOrder (relation A) subrelation. +Instance relation_implication_preorder : PreOrder (@subrelation A). Proof. intro A. exact (@predicate_implication_preorder (cons A (cons A nil))). Qed. (** *** Partial Order. @@ -367,14 +368,14 @@ Proof. intro A. exact (@predicate_implication_preorder (cons A (cons A nil))). Q We give an equivalent definition, up-to an equivalence relation on the carrier. *) -Class [ equ : Equivalence A eqA, preo : PreOrder A R ] => PartialOrder := +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 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. +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. apply <- poe. firstorder. @@ -389,3 +390,6 @@ Program Instance subrelation_partial_order : Proof. unfold relation_equivalence in *. firstorder. Qed. + +Typeclasses Opaque arrows predicate_implication predicate_equivalence + relation_equivalence pointwise_lifting. |