diff options
Diffstat (limited to 'theories/Classes/RelationClasses.v')
| -rw-r--r-- | theories/Classes/RelationClasses.v | 193 |
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. |