diff options
Diffstat (limited to 'theories/Classes')
| -rw-r--r-- | theories/Classes/CEquivalence.v | 139 | ||||
| -rw-r--r-- | theories/Classes/CMorphisms.v | 701 | ||||
| -rw-r--r-- | theories/Classes/CRelationClasses.v | 359 | ||||
| -rw-r--r-- | theories/Classes/DecidableClass.v | 92 | ||||
| -rw-r--r-- | theories/Classes/EquivDec.v | 13 | ||||
| -rw-r--r-- | theories/Classes/Equivalence.v | 38 | ||||
| -rw-r--r-- | theories/Classes/Init.v | 2 | ||||
| -rw-r--r-- | theories/Classes/Morphisms.v | 577 | ||||
| -rw-r--r-- | theories/Classes/Morphisms_Prop.v | 59 | ||||
| -rw-r--r-- | theories/Classes/Morphisms_Relations.v | 10 | ||||
| -rw-r--r-- | theories/Classes/RelationClasses.v | 432 | ||||
| -rw-r--r-- | theories/Classes/RelationPairs.v | 116 | ||||
| -rw-r--r-- | theories/Classes/SetoidClass.v | 2 | ||||
| -rw-r--r-- | theories/Classes/SetoidDec.v | 6 | ||||
| -rw-r--r-- | theories/Classes/SetoidTactics.v | 3 | ||||
| -rw-r--r-- | theories/Classes/vo.itarget | 4 |
16 files changed, 1939 insertions, 614 deletions
diff --git a/theories/Classes/CEquivalence.v b/theories/Classes/CEquivalence.v new file mode 100644 index 00000000..65353ed2 --- /dev/null +++ b/theories/Classes/CEquivalence.v @@ -0,0 +1,139 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** * Typeclass-based setoids. Definitions on [Equivalence]. + + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) + +Require Import Coq.Program.Basics. +Require Import Coq.Program.Tactics. + +Require Import Coq.Classes.Init. +Require Import Relation_Definitions. +Require Export Coq.Classes.CRelationClasses. +Require Import Coq.Classes.CMorphisms. + +Set Implicit Arguments. +Unset Strict Implicit. + +Generalizable Variables A R eqA B S eqB. +Local Obligation Tactic := try solve [simpl_crelation]. + +Local Open Scope signature_scope. + +Definition equiv `{Equivalence A R} : crelation A := R. + +(** Overloaded notations for setoid equivalence and inequivalence. + Not to be confused with [eq] and [=]. *) + +Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scope. + +Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : equiv_scope. + +Local Open Scope equiv_scope. + +(** Overloading for [PER]. *) + +Definition pequiv `{PER A R} : crelation A := R. + +(** Overloaded notation for partial equivalence. *) + +Infix "=~=" := pequiv (at level 70, no associativity) : equiv_scope. + +(** Shortcuts to make proof search easier. *) + +Program Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv. + +Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv. + +Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv. + + Next Obligation. + Proof. intros A R sa x y z Hxy Hyz. + now transitivity y. + Qed. + +(** Use the [substitute] command which substitutes an equivalence in every hypothesis. *) + +Ltac setoid_subst H := + match type of H with + ?x === ?y => substitute H ; clear H x + end. + +Ltac setoid_subst_nofail := + match goal with + | [ H : ?x === ?y |- _ ] => setoid_subst H ; setoid_subst_nofail + | _ => idtac + end. + +(** [subst*] will try its best at substituting every equality in the goal. *) + +Tactic Notation "subst" "*" := subst_no_fail ; setoid_subst_nofail. + +(** Simplify the goal w.r.t. equivalence. *) + +Ltac equiv_simplify_one := + match goal with + | [ H : ?x === ?x |- _ ] => clear H + | [ H : ?x === ?y |- _ ] => setoid_subst H + | [ |- ?x =/= ?y ] => let name:=fresh "Hneq" in intro name + | [ |- ~ ?x === ?y ] => let name:=fresh "Hneq" in intro name + end. + +Ltac equiv_simplify := repeat equiv_simplify_one. + +(** "reify" relations which are equivalences to applications of the overloaded [equiv] method + for easy recognition in tactics. *) + +Ltac equivify_tac := + match goal with + | [ s : Equivalence ?A ?R, H : ?R ?x ?y |- _ ] => change R with (@equiv A R s) in H + | [ s : Equivalence ?A ?R |- context C [ ?R ?x ?y ] ] => change (R x y) with (@equiv A R s x y) + end. + +Ltac equivify := repeat equivify_tac. + +Section Respecting. + + (** Here we build an equivalence instance for functions which relates respectful ones only, + we do not export it. *) + + Definition respecting `(eqa : Equivalence A (R : crelation A), + eqb : Equivalence B (R' : crelation B)) : Type := + { morph : A -> B & respectful R R' morph morph }. + + Program Instance respecting_equiv `(eqa : Equivalence A R, eqb : Equivalence B R') : + Equivalence (fun (f g : respecting eqa eqb) => + forall (x y : A), R x y -> R' (projT1 f x) (projT1 g y)). + + Solve Obligations with unfold respecting in * ; simpl_crelation ; program_simpl. + + Next Obligation. + Proof. + intros. intros f g h H H' x y Rxy. + unfold respecting in *. program_simpl. transitivity (g y); auto. firstorder. + Qed. + +End Respecting. + +(** The default equivalence on function spaces, with higher-priority than [eq]. *) + +Instance pointwise_reflexive {A} `(reflb : Reflexive B eqB) : + Reflexive (pointwise_relation A eqB) | 9. +Proof. firstorder. Qed. +Instance pointwise_symmetric {A} `(symb : Symmetric B eqB) : + Symmetric (pointwise_relation A eqB) | 9. +Proof. firstorder. Qed. +Instance pointwise_transitive {A} `(transb : Transitive B eqB) : + Transitive (pointwise_relation A eqB) | 9. +Proof. firstorder. Qed. +Instance pointwise_equivalence {A} `(eqb : Equivalence B eqB) : + Equivalence (pointwise_relation A eqB) | 9. +Proof. split; apply _. Qed. diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v new file mode 100644 index 00000000..073cd5e9 --- /dev/null +++ b/theories/Classes/CMorphisms.v @@ -0,0 +1,701 @@ +(* -*- coding: utf-8 -*- *) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** * Typeclass-based morphism definition and standard, minimal instances + + Author: Matthieu Sozeau + Institution: LRI, CNRS UMR 8623 - University Paris Sud +*) + +Require Import Coq.Program.Basics. +Require Import Coq.Program.Tactics. +Require Export Coq.Classes.CRelationClasses. + +Generalizable Variables A eqA B C D R RA RB RC m f x y. +Local Obligation Tactic := simpl_crelation. + +Set Universe Polymorphism. + +(** * Morphisms. + + We now turn to the definition of [Proper] and declare standard instances. + These will be used by the [setoid_rewrite] tactic later. *) + +(** A morphism for a relation [R] is a proper element of the relation. + The relation [R] will be instantiated by [respectful] and [A] by an arrow + type for usual morphisms. *) +Section Proper. + Context {A B : Type}. + + Class Proper (R : crelation A) (m : A) := + proper_prf : R m m. + + (** Every element in the carrier of a reflexive relation is a morphism + for this relation. We use a proxy class for this case which is used + internally to discharge reflexivity constraints. The [Reflexive] + instance will almost always be used, but it won't apply in general to + any kind of [Proper (A -> B) _ _] goal, making proof-search much + slower. A cleaner solution would be to be able to set different + priorities in different hint bases and select a particular hint + database for resolution of a type class constraint. *) + + Class ProperProxy (R : crelation A) (m : A) := + proper_proxy : R m m. + + Lemma eq_proper_proxy (x : A) : ProperProxy (@eq A) x. + Proof. firstorder. Qed. + + Lemma reflexive_proper_proxy `(Reflexive A R) (x : A) : ProperProxy R x. + Proof. firstorder. Qed. + + Lemma proper_proper_proxy x `(Proper R x) : ProperProxy R x. + Proof. firstorder. Qed. + + (** Respectful morphisms. *) + + (** The fully dependent version, not used yet. *) + + Definition respectful_hetero + (A B : Type) + (C : A -> Type) (D : B -> Type) + (R : A -> B -> Type) + (R' : forall (x : A) (y : B), C x -> D y -> Type) : + (forall x : A, C x) -> (forall x : B, D x) -> Type := + fun f g => forall x y, R x y -> R' x y (f x) (g y). + + (** The non-dependent version is an instance where we forget dependencies. *) + + Definition respectful (R : crelation A) (R' : crelation B) : crelation (A -> B) := + Eval compute in @respectful_hetero A A (fun _ => B) (fun _ => B) R (fun _ _ => R'). +End Proper. + +(** We favor the use of Leibniz equality or a declared reflexive crelation + when resolving [ProperProxy], otherwise, if the crelation is given (not an evar), + we fall back to [Proper]. *) +Hint Extern 1 (ProperProxy _ _) => + class_apply @eq_proper_proxy || class_apply @reflexive_proper_proxy : typeclass_instances. + +Hint Extern 2 (ProperProxy ?R _) => + not_evar R; class_apply @proper_proper_proxy : typeclass_instances. + +(** Notations reminiscent of the old syntax for declaring morphisms. *) +Delimit Scope signature_scope with signature. + +Module ProperNotations. + + Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature)) + (right associativity, at level 55) : signature_scope. + + Notation " R ==> R' " := (@respectful _ _ (R%signature) (R'%signature)) + (right associativity, at level 55) : signature_scope. + + Notation " R --> R' " := (@respectful _ _ (flip (R%signature)) (R'%signature)) + (right associativity, at level 55) : signature_scope. + +End ProperNotations. + +Arguments Proper {A}%type R%signature m. +Arguments respectful {A B}%type (R R')%signature _ _. + +Export ProperNotations. + +Local Open Scope signature_scope. + +(** [solve_proper] try to solve the goal [Proper (?==> ... ==>?) f] + by repeated introductions and setoid rewrites. It should work + fine when [f] is a combination of already known morphisms and + quantifiers. *) + +Ltac solve_respectful t := + match goal with + | |- respectful _ _ _ _ => + let H := fresh "H" in + intros ? ? H; solve_respectful ltac:(setoid_rewrite H; t) + | _ => t; reflexivity + end. + +Ltac solve_proper := unfold Proper; solve_respectful ltac:(idtac). + +(** [f_equiv] is a clone of [f_equal] that handles setoid equivalences. + For example, if we know that [f] is a morphism for [E1==>E2==>E], + then the goal [E (f x y) (f x' y')] will be transformed by [f_equiv] + into the subgoals [E1 x x'] and [E2 y y']. +*) + +Ltac f_equiv := + match goal with + | |- ?R (?f ?x) (?f' _) => + let T := type of x in + let Rx := fresh "R" in + evar (Rx : crelation T); + let H := fresh in + assert (H : (Rx==>R)%signature f f'); + unfold Rx in *; clear Rx; [ f_equiv | apply H; clear H; try reflexivity ] + | |- ?R ?f ?f' => + solve [change (Proper R f); eauto with typeclass_instances | reflexivity ] + | _ => idtac + end. + +Section Relations. + Context {A B : Type}. + + (** [forall_def] reifies the dependent product as a definition. *) + + Definition forall_def (P : A -> Type) : Type := forall x : A, P x. + + (** Dependent pointwise lifting of a crelation on the range. *) + + Definition forall_relation (P : A -> Type) + (sig : forall a, crelation (P a)) : crelation (forall x, P x) := + fun f g => forall a, sig a (f a) (g a). + + (** Non-dependent pointwise lifting *) + Definition pointwise_relation (R : crelation B) : crelation (A -> B) := + fun f g => forall a, R (f a) (g a). + + Lemma pointwise_pointwise (R : crelation B) : + relation_equivalence (pointwise_relation R) (@eq A ==> R). + Proof. intros. split. simpl_crelation. firstorder. Qed. + + (** Subcrelations induce a morphism on the identity. *) + + Global Instance subrelation_id_proper `(subrelation A RA RA') : Proper (RA ==> RA') id. + Proof. firstorder. Qed. + + (** The subrelation property goes through products as usual. *) + + Lemma subrelation_respectful `(subl : subrelation A RA' RA, subr : subrelation B RB RB') : + subrelation (RA ==> RB) (RA' ==> RB'). + Proof. simpl_crelation. Qed. + + (** And of course it is reflexive. *) + + Lemma subrelation_refl R : @subrelation A R R. + Proof. simpl_crelation. Qed. + + (** [Proper] is itself a covariant morphism for [subrelation]. + We use an unconvertible premise to avoid looping. + *) + + Lemma subrelation_proper `(mor : Proper A R' m) + `(unc : Unconvertible (crelation A) R R') + `(sub : subrelation A R' R) : Proper R m. + Proof. + intros. apply sub. apply mor. + Qed. + + Global Instance proper_subrelation_proper_arrow : + Proper (subrelation ++> eq ==> arrow) (@Proper A). + Proof. reduce. subst. firstorder. Qed. + + Global Instance pointwise_subrelation `(sub : subrelation B R R') : + subrelation (pointwise_relation R) (pointwise_relation R') | 4. + Proof. reduce. unfold pointwise_relation in *. apply sub. auto. Qed. + + (** For dependent function types. *) + Lemma forall_subrelation (P : A -> Type) (R S : forall x : A, crelation (P x)) : + (forall a, subrelation (R a) (S a)) -> + subrelation (forall_relation P R) (forall_relation P S). + Proof. reduce. firstorder. Qed. +End Relations. +Typeclasses Opaque respectful pointwise_relation forall_relation. +Arguments forall_relation {A P}%type sig%signature _ _. +Arguments pointwise_relation A%type {B}%type R%signature _ _. + +Hint Unfold Reflexive : core. +Hint Unfold Symmetric : core. +Hint Unfold Transitive : core. + +(** Resolution with subrelation: favor decomposing products over applying reflexivity + for unconstrained goals. *) +Ltac subrelation_tac T U := + (is_ground T ; is_ground U ; class_apply @subrelation_refl) || + class_apply @subrelation_respectful || class_apply @subrelation_refl. + +Hint Extern 3 (@subrelation _ ?T ?U) => subrelation_tac T U : typeclass_instances. + +CoInductive apply_subrelation : Prop := do_subrelation. + +Ltac proper_subrelation := + match goal with + [ H : apply_subrelation |- _ ] => clear H ; class_apply @subrelation_proper + end. + +Hint Extern 5 (@Proper _ ?H _) => proper_subrelation : typeclass_instances. + +(** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *) + +Instance iff_impl_subrelation : subrelation iff impl | 2. +Proof. firstorder. Qed. + +Instance iff_flip_impl_subrelation : subrelation iff (flip impl) | 2. +Proof. firstorder. Qed. + +(** Essential subrelation instances for [iffT] and [arrow]. *) + +Instance iffT_arrow_subrelation : subrelation iffT arrow | 2. +Proof. firstorder. Qed. + +Instance iffT_flip_arrow_subrelation : subrelation iffT (flip arrow) | 2. +Proof. firstorder. Qed. + +(** We use an extern hint to help unification. *) + +Hint Extern 4 (subrelation (@forall_relation ?A ?B ?R) (@forall_relation _ _ ?S)) => + apply (@forall_subrelation A B R S) ; intro : typeclass_instances. + +Section GenericInstances. + (* Share universes *) + Context {A B C : Type}. + + (** We can build a PER on the Coq function space if we have PERs on the domain and + codomain. *) + + Program Instance respectful_per `(PER A R, PER B R') : PER (R ==> R'). + + Next Obligation. + Proof with auto. + assert(R x0 x0). + transitivity y0... symmetry... + transitivity (y x0)... + Qed. + + (** The complement of a crelation conserves its proper elements. *) + + Program Definition complement_proper + `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) : + Proper (RA ==> RA ==> iff) (complement R) := _. + + Next Obligation. + Proof. + unfold complement. + pose (mR x y X x0 y0 X0). + intuition. + Qed. + + (** The [flip] too, actually the [flip] instance is a bit more general. *) + + Program Definition flip_proper + `(mor : Proper (A -> B -> C) (RA ==> RB ==> RC) f) : + Proper (RB ==> RA ==> RC) (flip f) := _. + + Next Obligation. + Proof. + apply mor ; auto. + Qed. + + + (** Every Transitive crelation gives rise to a binary morphism on [impl], + contravariant in the first argument, covariant in the second. *) + + Global Program + Instance trans_contra_co_type_morphism + `(Transitive A R) : Proper (R --> R ++> arrow) R. + + Next Obligation. + Proof with auto. + transitivity x... + transitivity x0... + Qed. + + (** Proper declarations for partial applications. *) + + Global Program + Instance trans_contra_inv_impl_type_morphism + `(Transitive A R) : Proper (R --> flip arrow) (R x) | 3. + + Next Obligation. + Proof with auto. + transitivity y... + Qed. + + Global Program + Instance trans_co_impl_type_morphism + `(Transitive A R) : Proper (R ++> arrow) (R x) | 3. + + Next Obligation. + Proof with auto. + transitivity x0... + Qed. + + Global Program + Instance trans_sym_co_inv_impl_type_morphism + `(PER A R) : Proper (R ++> flip arrow) (R x) | 3. + + Next Obligation. + Proof with auto. + transitivity y... symmetry... + Qed. + + Global Program Instance trans_sym_contra_arrow_morphism + `(PER A R) : Proper (R --> arrow) (R x) | 3. + + Next Obligation. + Proof with auto. + transitivity x0... symmetry... + Qed. + + Global Program Instance per_partial_app_type_morphism + `(PER A R) : Proper (R ==> iffT) (R x) | 2. + + Next Obligation. + Proof with auto. + split. intros ; transitivity x0... + intros. + transitivity y... + symmetry... + Qed. + + (** Every Transitive crelation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof to get an [R y z] goal. *) + + Global Program + Instance trans_co_eq_inv_arrow_morphism + `(Transitive A R) : Proper (R ==> (@eq A) ==> flip arrow) R | 2. + + Next Obligation. + Proof with auto. + transitivity y... + Qed. + + (** Every Symmetric and Transitive crelation gives rise to an equivariant morphism. *) + + Global Program + Instance PER_type_morphism `(PER A R) : Proper (R ==> R ==> iffT) R | 1. + + Next Obligation. + Proof with auto. + split ; intros. + transitivity x0... transitivity x... symmetry... + + transitivity y... transitivity y0... symmetry... + Qed. + + Lemma symmetric_equiv_flip `(Symmetric A R) : relation_equivalence R (flip R). + Proof. firstorder. Qed. + + Global Program Instance compose_proper RA RB RC : + Proper ((RB ==> RC) ==> (RA ==> RB) ==> (RA ==> RC)) (@compose A B C). + + Next Obligation. + Proof. + simpl_crelation. + unfold compose. firstorder. + Qed. + + (** Coq functions are morphisms for Leibniz equality, + applied only if really needed. *) + + Global Instance reflexive_eq_dom_reflexive `(Reflexive B R') : + Reflexive (@Logic.eq A ==> R'). + Proof. simpl_crelation. Qed. + + (** [respectful] is a morphism for crelation equivalence . *) + Set Printing All. Set Printing Universes. + Global Instance respectful_morphism : + Proper (relation_equivalence ++> relation_equivalence ++> relation_equivalence) + (@respectful A B). + Proof. + intros R R' HRR' S S' HSS' f g. + unfold respectful , relation_equivalence in *; simpl in *. + split ; intros H x y Hxy. + apply (fst (HSS' _ _)). apply H. now apply (snd (HRR' _ _)). + apply (snd (HSS' _ _)). apply H. now apply (fst (HRR' _ _)). + Qed. + + (** [R] is Reflexive, hence we can build the needed proof. *) + + Lemma Reflexive_partial_app_morphism `(Proper (A -> B) (R ==> R') m, ProperProxy A R x) : + Proper R' (m x). + Proof. simpl_crelation. Qed. + + Class Params (of : A) (arity : nat). + + Lemma flip_respectful (R : crelation A) (R' : crelation B) : + relation_equivalence (flip (R ==> R')) (flip R ==> flip R'). + Proof. + intros. + unfold flip, respectful. + split ; intros ; intuition. + Qed. + + + (** Treating flip: can't make them direct instances as we + need at least a [flip] present in the goal. *) + + Lemma flip1 `(subrelation A R' R) : subrelation (flip (flip R')) R. + Proof. firstorder. Qed. + + Lemma flip2 `(subrelation A R R') : subrelation R (flip (flip R')). + Proof. firstorder. Qed. + + (** That's if and only if *) + + Lemma eq_subrelation `(Reflexive A R) : subrelation (@eq A) R. + Proof. simpl_crelation. Qed. + + (** Once we have normalized, we will apply this instance to simplify the problem. *) + + Definition proper_flip_proper `(mor : Proper A R m) : Proper (flip R) m := mor. + + (** Every reflexive crelation gives rise to a morphism, + only for immediately solving goals without variables. *) + + Lemma reflexive_proper `{Reflexive A R} (x : A) : Proper R x. + Proof. firstorder. Qed. + + Lemma proper_eq (x : A) : Proper (@eq A) x. + Proof. intros. apply reflexive_proper. Qed. + +End GenericInstances. + +Class PartialApplication. + +CoInductive normalization_done : Prop := did_normalization. + +Ltac partial_application_tactic := + let rec do_partial_apps H m cont := + match m with + | ?m' ?x => class_apply @Reflexive_partial_app_morphism ; + [(do_partial_apps H m' ltac:idtac)|clear H] + | _ => cont + end + in + let rec do_partial H ar m := + match ar with + | 0%nat => do_partial_apps H m ltac:(fail 1) + | S ?n' => + match m with + ?m' ?x => do_partial H n' m' + end + end + in + let params m sk fk := + (let m' := fresh in head_of_constr m' m ; + let n := fresh in evar (n:nat) ; + let v := eval compute in n in clear n ; + let H := fresh in + assert(H:Params m' v) by typeclasses eauto ; + let v' := eval compute in v in subst m'; + (sk H v' || fail 1)) + || fk + in + let on_morphism m cont := + params m ltac:(fun H n => do_partial H n m) + ltac:(cont) + in + match goal with + | [ _ : normalization_done |- _ ] => fail 1 + | [ _ : @Params _ _ _ |- _ ] => fail 1 + | [ |- @Proper ?T _ (?m ?x) ] => + match goal with + | [ H : PartialApplication |- _ ] => + class_apply @Reflexive_partial_app_morphism; [|clear H] + | _ => on_morphism (m x) + ltac:(class_apply @Reflexive_partial_app_morphism) + end + end. + +(** Bootstrap !!! *) + +Instance proper_proper : Proper (relation_equivalence ==> eq ==> iffT) (@Proper A). +Proof. + intros A R R' HRR' x y <-. red in HRR'. + split ; red ; intros. + now apply (fst (HRR' _ _)). + now apply (snd (HRR' _ _)). +Qed. + +Ltac proper_reflexive := + match goal with + | [ _ : normalization_done |- _ ] => fail 1 + | _ => class_apply proper_eq || class_apply @reflexive_proper + end. + + +Hint Extern 1 (subrelation (flip _) _) => class_apply @flip1 : typeclass_instances. +Hint Extern 1 (subrelation _ (flip _)) => class_apply @flip2 : typeclass_instances. + +Hint Extern 1 (Proper _ (complement _)) => apply @complement_proper + : typeclass_instances. +Hint Extern 1 (Proper _ (flip _)) => apply @flip_proper + : typeclass_instances. +Hint Extern 2 (@Proper _ (flip _) _) => class_apply @proper_flip_proper + : typeclass_instances. +Hint Extern 4 (@Proper _ _ _) => partial_application_tactic + : typeclass_instances. +Hint Extern 7 (@Proper _ _ _) => proper_reflexive + : typeclass_instances. + +(** Special-purpose class to do normalization of signatures w.r.t. flip. *) + +Section Normalize. + Context (A : Type). + + Class Normalizes (m : crelation A) (m' : crelation A) : Prop := + normalizes : relation_equivalence m m'. + + (** Current strategy: add [flip] everywhere and reduce using [subrelation] + afterwards. *) + + Lemma proper_normalizes_proper `(Normalizes R0 R1, Proper A R1 m) : Proper R0 m. + Proof. + red in H, H0. red in H. + apply (snd (H _ _)). + assumption. + Qed. + + Lemma flip_atom R : Normalizes R (flip (flip R)). + Proof. + firstorder. + Qed. + +End Normalize. + +Lemma flip_arrow `(NA : Normalizes A R (flip R'''), NB : Normalizes B R' (flip R'')) : + Normalizes (A -> B) (R ==> R') (flip (R''' ==> R'')%signature). +Proof. + unfold Normalizes in *. intros. + rewrite NA, NB. firstorder. +Qed. + +Ltac normalizes := + match goal with + | [ |- Normalizes _ (respectful _ _) _ ] => class_apply @flip_arrow + | _ => class_apply @flip_atom + end. + +Ltac proper_normalization := + match goal with + | [ _ : normalization_done |- _ ] => fail 1 + | [ _ : apply_subrelation |- @Proper _ ?R _ ] => + let H := fresh "H" in + set(H:=did_normalization) ; class_apply @proper_normalizes_proper + end. + +Hint Extern 1 (Normalizes _ _ _) => normalizes : typeclass_instances. +Hint Extern 6 (@Proper _ _ _) => proper_normalization + : typeclass_instances. + +(** When the crelation on the domain is symmetric, we can + flip the crelation on the codomain. Same for binary functions. *) + +Lemma proper_sym_flip : + forall `(Symmetric A R1)`(Proper (A->B) (R1==>R2) f), + Proper (R1==>flip R2) f. +Proof. +intros A R1 Sym B R2 f Hf. +intros x x' Hxx'. apply Hf, Sym, Hxx'. +Qed. + +Lemma proper_sym_flip_2 : + forall `(Symmetric A R1)`(Symmetric B R2)`(Proper (A->B->C) (R1==>R2==>R3) f), + Proper (R1==>R2==>flip R3) f. +Proof. +intros A R1 Sym1 B R2 Sym2 C R3 f Hf. +intros x x' Hxx' y y' Hyy'. apply Hf; auto. +Qed. + +(** When the crelation on the domain is symmetric, a predicate is + compatible with [iff] as soon as it is compatible with [impl]. + Same with a binary crelation. *) + +Lemma proper_sym_impl_iff : forall `(Symmetric A R)`(Proper _ (R==>impl) f), + Proper (R==>iff) f. +Proof. +intros A R Sym f Hf x x' Hxx'. repeat red in Hf. split; eauto. +Qed. + +Lemma proper_sym_arrow_iffT : forall `(Symmetric A R)`(Proper _ (R==>arrow) f), + Proper (R==>iffT) f. +Proof. +intros A R Sym f Hf x x' Hxx'. repeat red in Hf. split; eauto. +Qed. + +Lemma proper_sym_impl_iff_2 : + forall `(Symmetric A R)`(Symmetric B R')`(Proper _ (R==>R'==>impl) f), + Proper (R==>R'==>iff) f. +Proof. +intros A R Sym B R' Sym' f Hf x x' Hxx' y y' Hyy'. +repeat red in Hf. split; eauto. +Qed. + +Lemma proper_sym_arrow_iffT_2 : + forall `(Symmetric A R)`(Symmetric B R')`(Proper _ (R==>R'==>arrow) f), + Proper (R==>R'==>iffT) f. +Proof. +intros A R Sym B R' Sym' f Hf x x' Hxx' y y' Hyy'. +repeat red in Hf. split; eauto. +Qed. + +(** A [PartialOrder] is compatible with its underlying equivalence. *) +Require Import Relation_Definitions. + +Instance PartialOrder_proper_type `(PartialOrder A eqA R) : + Proper (eqA==>eqA==>iffT) R. +Proof. +intros. +apply proper_sym_arrow_iffT_2; auto with *. +intros x x' Hx y y' Hy Hr. +transitivity x. +generalize (partial_order_equivalence x x'); compute; intuition. +transitivity y; auto. +generalize (partial_order_equivalence y y'); compute; intuition. +Qed. + +(** From a [PartialOrder] to the corresponding [StrictOrder]: + [lt = le /\ ~eq]. + If the order is total, we could also say [gt = ~le]. *) + +Lemma PartialOrder_StrictOrder `(PartialOrder A eqA R) : + StrictOrder (relation_conjunction R (complement eqA)). +Proof. +split; compute. +intros x (_,Hx). apply Hx, Equivalence_Reflexive. +intros x y z (Hxy,Hxy') (Hyz,Hyz'). split. +apply PreOrder_Transitive with y; assumption. +intro Hxz. +apply Hxy'. +apply partial_order_antisym; auto. +rewrite Hxz. auto. +Qed. + +(** From a [StrictOrder] to the corresponding [PartialOrder]: + [le = lt \/ eq]. + If the order is total, we could also say [ge = ~lt]. *) + +Lemma StrictOrder_PreOrder + `(Equivalence A eqA, StrictOrder A R, Proper _ (eqA==>eqA==>iffT) R) : + PreOrder (relation_disjunction R eqA). +Proof. +split. +intros x. right. reflexivity. +intros x y z [Hxy|Hxy] [Hyz|Hyz]. +left. transitivity y; auto. +left. rewrite <- Hyz; auto. +left. rewrite Hxy; auto. +right. transitivity y; auto. +Qed. + +Hint Extern 4 (PreOrder (relation_disjunction _ _)) => + class_apply StrictOrder_PreOrder : typeclass_instances. + +Lemma StrictOrder_PartialOrder + `(Equivalence A eqA, StrictOrder A R, Proper _ (eqA==>eqA==>iffT) R) : + PartialOrder eqA (relation_disjunction R eqA). +Proof. +intros. intros x y. compute. intuition. +elim (StrictOrder_Irreflexive x). +transitivity y; auto. +Qed. + +Hint Extern 4 (StrictOrder (relation_conjunction _ _)) => + class_apply PartialOrder_StrictOrder : typeclass_instances. + +Hint Extern 4 (PartialOrder _ (relation_disjunction _ _)) => + class_apply StrictOrder_PartialOrder : typeclass_instances. diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v new file mode 100644 index 00000000..35b2b8a3 --- /dev/null +++ b/theories/Classes/CRelationClasses.v @@ -0,0 +1,359 @@ +(* -*- coding: utf-8 -*- *) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** * 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. + +Generalizable Variables A B C D R S T U l eqA eqB eqC eqD. + +Set Universe Polymorphism. + +Definition crelation (A : Type) := A -> A -> Type. + +Definition arrow (A B : Type) := A -> B. + +Definition flip {A B C : Type} (f : A -> B -> C) := fun x y => f y x. + +Definition iffT (A B : Type) := ((A -> B) * (B -> A))%type. + +(** We allow to unfold the [crelation] definition while doing morphism search. *) + +Section Defs. + Context {A : Type}. + + (** We rebind crelational properties in separate classes to be able to overload each proof. *) + + Class Reflexive (R : crelation A) := + reflexivity : forall x : A, R x x. + + Definition complement (R : crelation A) : crelation A := + fun x y => R x y -> False. + + (** Opaque for proof-search. *) + Typeclasses Opaque complement iffT. + + (** These are convertible. *) + Lemma complement_inverse R : complement (flip R) = flip (complement R). + Proof. reflexivity. Qed. + + Class Irreflexive (R : crelation A) := + irreflexivity : Reflexive (complement R). + + Class Symmetric (R : crelation A) := + symmetry : forall {x y}, R x y -> R y x. + + Class Asymmetric (R : crelation A) := + asymmetry : forall {x y}, R x y -> (complement R y x : Type). + + Class Transitive (R : crelation 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 : crelation A) := { + PreOrder_Reflexive :> Reflexive R | 2 ; + PreOrder_Transitive :> Transitive R | 2 }. + + (** A [StrictOrder] is both Irreflexive and Transitive. *) + + Class StrictOrder (R : crelation A) := { + StrictOrder_Irreflexive :> Irreflexive R ; + StrictOrder_Transitive :> Transitive R }. + + (** By definition, a strict order is also asymmetric *) + Global Instance StrictOrder_Asymmetric `(StrictOrder R) : Asymmetric R. + Proof. firstorder. Qed. + + (** A partial equivalence crelation is Symmetric and Transitive. *) + + Class PER (R : crelation A) := { + PER_Symmetric :> Symmetric R | 3 ; + PER_Transitive :> Transitive R | 3 }. + + (** Equivalence crelations. *) + + Class Equivalence (R : crelation A) := { + Equivalence_Reflexive :> Reflexive R ; + Equivalence_Symmetric :> Symmetric R ; + Equivalence_Transitive :> Transitive R }. + + (** An Equivalence is a PER plus reflexivity. *) + + Global Instance Equivalence_PER {R} `(Equivalence R) : PER R | 10 := + { PER_Symmetric := Equivalence_Symmetric ; + PER_Transitive := Equivalence_Transitive }. + + (** We can now define antisymmetry w.r.t. an equivalence crelation on the carrier. *) + + Class Antisymmetric eqA `{equ : Equivalence eqA} (R : crelation A) := + antisymmetry : forall {x y}, R x y -> R y x -> eqA x y. + + Class subrelation (R R' : crelation A) := + is_subrelation : forall {x y}, R x y -> R' x y. + + (** Any symmetric crelation is equal to its inverse. *) + + Lemma subrelation_symmetric R `(Symmetric R) : subrelation (flip R) R. + Proof. hnf. intros x y H'. red in H'. apply symmetry. assumption. Qed. + + Section flip. + + Lemma flip_Reflexive `{Reflexive R} : Reflexive (flip R). + Proof. tauto. Qed. + + 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). + Proof. firstorder. Qed. + + (** Inversing the larger structures *) + + Lemma flip_PreOrder `(PreOrder R) : PreOrder (flip R). + Proof. firstorder. Qed. + + Lemma flip_StrictOrder `(StrictOrder R) : StrictOrder (flip R). + Proof. firstorder. Qed. + + Lemma flip_PER `(PER R) : PER (flip R). + Proof. firstorder. Qed. + + Lemma flip_Equivalence `(Equivalence R) : Equivalence (flip R). + Proof. firstorder. Qed. + + End flip. + + Section complement. + + Definition complement_Irreflexive `(Reflexive R) + : Irreflexive (complement R). + Proof. firstorder. Qed. + + Definition complement_Symmetric `(Symmetric R) : Symmetric (complement R). + Proof. firstorder. Qed. + End complement. + + + (** Rewrite crelation on a given support: declares a crelation as a rewrite + crelation 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 + crelations. This is also done automatically by the [Declare Relation A RA] + commands. *) + + Class RewriteRelation (RA : crelation A). + + (** Any [Equivalence] declared in the context is automatically considered + a rewrite crelation. *) + + Global Instance equivalence_rewrite_crelation `(Equivalence eqA) : RewriteRelation eqA. + + (** 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 crelation. + 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. + +End Defs. + +(** Default rewrite crelations handled by [setoid_rewrite]. *) +Instance: RewriteRelation impl. +Instance: RewriteRelation iff. + +(** Hints to drive the typeclass resolution avoiding loops + due to the use of full unification. *) +Hint Extern 1 (Reflexive (complement _)) => class_apply @irreflexivity : typeclass_instances. +Hint Extern 3 (Symmetric (complement _)) => class_apply complement_Symmetric : typeclass_instances. +Hint Extern 3 (Irreflexive (complement _)) => class_apply complement_Irreflexive : typeclass_instances. + +Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances. +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 (Antisymmetric (flip _)) => class_apply flip_Antisymmetric : typeclass_instances. +Hint Extern 3 (Transitive (flip _)) => class_apply flip_Transitive : typeclass_instances. +Hint Extern 3 (StrictOrder (flip _)) => class_apply flip_StrictOrder : typeclass_instances. +Hint Extern 3 (PreOrder (flip _)) => class_apply flip_PreOrder : typeclass_instances. + +Hint Extern 4 (subrelation (flip _) _) => + class_apply @subrelation_symmetric : typeclass_instances. + +Hint Resolve irreflexivity : ord. + +Unset Implicit Arguments. + +(** A HintDb for crelations. *) + +Ltac solve_crelation := + match goal with + | [ |- ?R ?x ?x ] => reflexivity + | [ H : ?R ?x ?y |- ?R ?y ?x ] => symmetry ; exact H + end. + +Hint Extern 4 => solve_crelation : crelations. + +(** 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_crelation := + unfold flip, impl, arrow ; try reduce ; program_simpl ; + try ( solve [ dintuition ]). + +Local Obligation Tactic := simpl_crelation. + +(** Logical implication. *) + +Program Instance impl_Reflexive : Reflexive impl. +Program Instance impl_Transitive : Transitive impl. + +(** Logical equivalence. *) + +Instance iff_Reflexive : Reflexive iff := iff_refl. +Instance iff_Symmetric : Symmetric iff := iff_sym. +Instance iff_Transitive : Transitive iff := iff_trans. + +(** Logical equivalence [iff] is an equivalence crelation. *) + +Program Instance iff_equivalence : Equivalence iff. +Program Instance arrow_Reflexive : Reflexive arrow. +Program Instance arrow_Transitive : Transitive arrow. + +Instance iffT_Reflexive : Reflexive iffT. +Proof. firstorder. Defined. +Instance iffT_Symmetric : Symmetric iffT. +Proof. firstorder. Defined. +Instance iffT_Transitive : Transitive iffT. +Proof. firstorder. Defined. + +(** We now develop a generalization of results on crelations for arbitrary predicates. + The resulting theory can be applied to homogeneous binary crelations but also to + arbitrary n-ary predicates. *) + +Local Open Scope list_scope. + +(** A compact representation of non-dependent arities, with the codomain singled-out. *) + +(** We define the various operations which define the algebra on binary crelations *) +Section Binary. + Context {A : Type}. + + Definition relation_equivalence : crelation (crelation A) := + fun R R' => forall x y, iffT (R x y) (R' x y). + + Global Instance: RewriteRelation relation_equivalence. + + Definition relation_conjunction (R : crelation A) (R' : crelation A) : crelation A := + fun x y => prod (R x y) (R' x y). + + Definition relation_disjunction (R : crelation A) (R' : crelation A) : crelation A := + fun x y => sum (R x y) (R' x y). + + (** Relation equivalence is an equivalence, and subrelation defines a partial order. *) + + Set Automatic Introduction. + + Global Instance relation_equivalence_equivalence : + Equivalence relation_equivalence. + Proof. split; red; unfold relation_equivalence, iffT. firstorder. + firstorder. + intros. specialize (X x0 y0). specialize (X0 x0 y0). firstorder. + Qed. + + Global Instance relation_implication_preorder : PreOrder (@subrelation A). + Proof. firstorder. Qed. + + (** *** Partial Order. + A partial order is a preorder which is additionally antisymmetric. + We give an equivalent definition, up-to an equivalence crelation + on the carrier. *) + + Class PartialOrder eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} := + partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (flip 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] *) + + Global Instance partial_order_antisym `(PartialOrder eqA R) : ! Antisymmetric A eqA R. + Proof with auto. + reduce_goal. + apply H. firstorder. + Qed. + + Lemma PartialOrder_inverse `(PartialOrder eqA R) : PartialOrder eqA (flip R). + Proof. unfold flip; constructor; unfold flip. intros. apply H. apply symmetry. apply X. + unfold relation_conjunction. intros [H1 H2]. apply H. constructor; assumption. Qed. +End Binary. + +Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : typeclass_instances. + +(** The partial order defined by subrelation and crelation equivalence. *) + +(* Program Instance subrelation_partial_order : *) +(* ! PartialOrder (crelation A) relation_equivalence subrelation. *) +(* Obligation Tactic := idtac. *) + +(* Next Obligation. *) +(* Proof. *) +(* intros x. refine (fun x => x). *) +(* Qed. *) + +Typeclasses Opaque relation_equivalence. + + diff --git a/theories/Classes/DecidableClass.v b/theories/Classes/DecidableClass.v new file mode 100644 index 00000000..9fe3d0fe --- /dev/null +++ b/theories/Classes/DecidableClass.v @@ -0,0 +1,92 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** * A typeclass to ease the handling of decidable properties. *) + +(** A proposition is decidable whenever it is reflected by a boolean. *) + +Class Decidable (P : Prop) := { + Decidable_witness : bool; + Decidable_spec : Decidable_witness = true <-> P +}. + +(** Alternative ways of specifying the reflection property. *) + +Lemma Decidable_sound : forall P (H : Decidable P), + Decidable_witness = true -> P. +Proof. +intros P H Hp; apply -> Decidable_spec; assumption. +Qed. + +Lemma Decidable_complete : forall P (H : Decidable P), + P -> Decidable_witness = true. +Proof. +intros P H Hp; apply <- Decidable_spec; assumption. +Qed. + +Lemma Decidable_sound_alt : forall P (H : Decidable P), + ~ P -> Decidable_witness = false. +Proof. +intros P [wit spec] Hd; simpl; destruct wit; tauto. +Qed. + +Lemma Decidable_complete_alt : forall P (H : Decidable P), + Decidable_witness = false -> ~ P. +Proof. +intros P [wit spec] Hd Hc; simpl in *; intuition congruence. +Qed. + +(** The generic function that should be used to program, together with some + useful tactics. *) + +Definition decide P {H : Decidable P} := Decidable_witness (Decidable:=H). + +Ltac _decide_ P H := + let b := fresh "b" in + set (b := decide P) in *; + assert (H : decide P = b) by reflexivity; + clearbody b; + destruct b; [apply Decidable_sound in H|apply Decidable_complete_alt in H]. + +Tactic Notation "decide" constr(P) "as" ident(H) := + _decide_ P H. + +Tactic Notation "decide" constr(P) := + let H := fresh "H" in _decide_ P H. + +(** Some usual instances. *) + +Require Import Bool Arith ZArith. + +Program Instance Decidable_eq_bool : forall (x y : bool), Decidable (eq x y) := { + Decidable_witness := Bool.eqb x y +}. +Next Obligation. + apply eqb_true_iff. +Qed. + +Program Instance Decidable_eq_nat : forall (x y : nat), Decidable (eq x y) := { + Decidable_witness := Nat.eqb x y +}. +Next Obligation. + apply Nat.eqb_eq. +Qed. + +Program Instance Decidable_le_nat : forall (x y : nat), Decidable (x <= y) := { + Decidable_witness := Nat.leb x y +}. +Next Obligation. + apply Nat.leb_le. +Qed. + +Program Instance Decidable_eq_Z : forall (x y : Z), Decidable (eq x y) := { + Decidable_witness := Z.eqb x y +}. +Next Obligation. + apply Z.eqb_eq. +Qed. diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index 8e3715ff..59e800c2 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -53,7 +53,9 @@ Local Open Scope program_scope. (** Invert the branches. *) -Program Definition nequiv_dec `{EqDec A} (x y : A) : { x =/= y } + { x === y } := swap_sumbool (x == y). +Program Definition nequiv_dec `{EqDec A} (x y : A) : { x =/= y } + { x === y } := + swap_sumbool (x == y). + (** Overloaded notation for inequality. *) @@ -138,8 +140,7 @@ Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq := | _, _ => in_right end }. - Solve Obligations using unfold equiv, complement in * ; program_simpl ; intuition (discriminate || eauto). - - Next Obligation. destruct y ; intuition eauto. Defined. + Next Obligation. destruct y ; unfold not in *; eauto. Defined. - Solve Obligations using unfold equiv, complement in * ; program_simpl ; intuition (discriminate || eauto). + Solve Obligations with unfold equiv, complement in * ; + program_simpl ; intuition (discriminate || eauto). diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index 0e9adf64..c281af80 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -24,7 +24,7 @@ Set Implicit Arguments. Unset Strict Implicit. Generalizable Variables A R eqA B S eqB. -Local Obligation Tactic := simpl_relation. +Local Obligation Tactic := try solve [simpl_relation]. Local Open Scope signature_scope. @@ -56,8 +56,8 @@ Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv. Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv. Next Obligation. - Proof. - transitivity y ; auto. + Proof. intros A R sa x y z Hxy Hyz. + now transitivity y. Qed. (** Use the [substitute] command which substitutes an equivalence in every hypothesis. *) @@ -105,27 +105,35 @@ Section Respecting. (** Here we build an equivalence instance for functions which relates respectful ones only, we do not export it. *) - Definition respecting `(eqa : Equivalence A (R : relation A), eqb : Equivalence B (R' : relation B)) : Type := + Definition respecting `(eqa : Equivalence A (R : relation A), + eqb : Equivalence B (R' : relation B)) : Type := { morph : A -> B | respectful R R' morph morph }. Program Instance respecting_equiv `(eqa : Equivalence A R, eqb : Equivalence B R') : - Equivalence (fun (f g : respecting eqa eqb) => forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)). + Equivalence (fun (f g : respecting eqa eqb) => + forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)). - Solve Obligations using unfold respecting in * ; simpl_relation ; program_simpl. + Solve Obligations with unfold respecting in * ; simpl_relation ; program_simpl. Next Obligation. - Proof. - unfold respecting in *. program_simpl. transitivity (y y0); auto. apply H0. reflexivity. + Proof. + intros. intros f g h H H' x y Rxy. + unfold respecting in *. program_simpl. transitivity (g y); auto. firstorder. Qed. End Respecting. (** The default equivalence on function spaces, with higher-priority than [eq]. *) -Program Instance pointwise_equivalence {A} `(eqb : Equivalence B eqB) : +Instance pointwise_reflexive {A} `(reflb : Reflexive B eqB) : + Reflexive (pointwise_relation A eqB) | 9. +Proof. firstorder. Qed. +Instance pointwise_symmetric {A} `(symb : Symmetric B eqB) : + Symmetric (pointwise_relation A eqB) | 9. +Proof. firstorder. Qed. +Instance pointwise_transitive {A} `(transb : Transitive B eqB) : + Transitive (pointwise_relation A eqB) | 9. +Proof. firstorder. Qed. +Instance pointwise_equivalence {A} `(eqb : Equivalence B eqB) : Equivalence (pointwise_relation A eqB) | 9. - - Next Obligation. - Proof. - transitivity (y a) ; auto. - Qed. +Proof. split; apply _. Qed. diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v index 1a56c1a3..9574cf85 100644 --- a/theories/Classes/Init.v +++ b/theories/Classes/Init.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 9d5a3233..1bdce654 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -18,7 +18,7 @@ Require Import Coq.Program.Tactics. Require Import Coq.Relations.Relation_Definitions. Require Export Coq.Classes.RelationClasses. -Generalizable All Variables. +Generalizable Variables A eqA B C D R RA RB RC m f x y. Local Obligation Tactic := simpl_relation. (** * Morphisms. @@ -29,15 +29,39 @@ Local Obligation Tactic := simpl_relation. (** A morphism for a relation [R] is a proper element of the relation. The relation [R] will be instantiated by [respectful] and [A] by an arrow type for usual morphisms. *) - -Class Proper {A} (R : relation A) (m : A) : Prop := - proper_prf : R m m. - -(** Respectful morphisms. *) - -(** The fully dependent version, not used yet. *) - -Definition respectful_hetero +Section Proper. + Let U := Type. + Context {A B : U}. + + Class Proper (R : relation A) (m : A) : Prop := + proper_prf : R m m. + + (** Every element in the carrier of a reflexive relation is a morphism + for this relation. We use a proxy class for this case which is used + internally to discharge reflexivity constraints. The [Reflexive] + instance will almost always be used, but it won't apply in general to + any kind of [Proper (A -> B) _ _] goal, making proof-search much + slower. A cleaner solution would be to be able to set different + priorities in different hint bases and select a particular hint + database for resolution of a type class constraint. *) + + Class ProperProxy (R : relation A) (m : A) : Prop := + proper_proxy : R m m. + + Lemma eq_proper_proxy (x : A) : ProperProxy (@eq A) x. + Proof. firstorder. Qed. + + Lemma reflexive_proper_proxy `(Reflexive A R) (x : A) : ProperProxy R x. + Proof. firstorder. Qed. + + Lemma proper_proper_proxy x `(Proper R x) : ProperProxy R x. + Proof. firstorder. Qed. + + (** Respectful morphisms. *) + + (** The fully dependent version, not used yet. *) + + Definition respectful_hetero (A B : Type) (C : A -> Type) (D : B -> Type) (R : A -> B -> Prop) @@ -45,18 +69,24 @@ Definition respectful_hetero (forall x : A, C x) -> (forall x : B, D x) -> Prop := fun f g => forall x y, R x y -> R' x y (f x) (g y). -(** The non-dependent version is an instance where we forget dependencies. *) + (** The non-dependent version is an instance where we forget dependencies. *) + + Definition respectful (R : relation A) (R' : relation B) : relation (A -> B) := + Eval compute in @respectful_hetero A A (fun _ => B) (fun _ => B) R (fun _ _ => R'). -Definition respectful {A B : Type} - (R : relation A) (R' : relation B) : relation (A -> B) := - Eval compute in @respectful_hetero A A (fun _ => B) (fun _ => B) R (fun _ _ => R'). +End Proper. -(** Notations reminiscent of the old syntax for declaring morphisms. *) +(** We favor the use of Leibniz equality or a declared reflexive relation + when resolving [ProperProxy], otherwise, if the relation is given (not an evar), + we fall back to [Proper]. *) +Hint Extern 1 (ProperProxy _ _) => + class_apply @eq_proper_proxy || class_apply @reflexive_proper_proxy : typeclass_instances. -Delimit Scope signature_scope with signature. +Hint Extern 2 (ProperProxy ?R _) => + not_evar R; class_apply @proper_proper_proxy : typeclass_instances. -Arguments Proper {A}%type R%signature m. -Arguments respectful {A B}%type (R R')%signature _ _. +(** Notations reminiscent of the old syntax for declaring morphisms. *) +Delimit Scope signature_scope with signature. Module ProperNotations. @@ -66,11 +96,14 @@ Module ProperNotations. Notation " R ==> R' " := (@respectful _ _ (R%signature) (R'%signature)) (right associativity, at level 55) : signature_scope. - Notation " R --> R' " := (@respectful _ _ (inverse (R%signature)) (R'%signature)) + Notation " R --> R' " := (@respectful _ _ (flip (R%signature)) (R'%signature)) (right associativity, at level 55) : signature_scope. End ProperNotations. +Arguments Proper {A}%type R%signature m. +Arguments respectful {A B}%type (R R')%signature _ _. + Export ProperNotations. Local Open Scope signature_scope. @@ -106,80 +139,89 @@ Ltac f_equiv := assert (H : (Rx==>R)%signature f f'); unfold Rx in *; clear Rx; [ f_equiv | apply H; clear H; try reflexivity ] | |- ?R ?f ?f' => - try reflexivity; - change (Proper R f); eauto with typeclass_instances; fail + solve [change (Proper R f); eauto with typeclass_instances | reflexivity ] | _ => idtac end. -(** [forall_def] reifies the dependent product as a definition. *) - -Definition forall_def {A : Type} (B : A -> Type) : Type := forall x : A, B x. - -(** Dependent pointwise lifting of a relation on the range. *) - -Definition forall_relation {A : Type} {B : A -> Type} - (sig : forall a, relation (B a)) : relation (forall x, B x) := - fun f g => forall a, sig a (f a) (g a). - -Arguments forall_relation {A B}%type sig%signature _ _. - -(** Non-dependent pointwise lifting *) +Section Relations. + Let U := Type. + Context {A B : U} (P : A -> U). + + (** [forall_def] reifies the dependent product as a definition. *) + + Definition forall_def : Type := forall x : A, P x. + + (** Dependent pointwise lifting of a relation on the range. *) + + Definition forall_relation + (sig : forall a, relation (P a)) : relation (forall x, P x) := + fun f g => forall a, sig a (f a) (g a). + + (** Non-dependent pointwise lifting *) + Definition pointwise_relation (R : relation B) : relation (A -> B) := + fun f g => forall a, R (f a) (g a). + + Lemma pointwise_pointwise (R : relation B) : + relation_equivalence (pointwise_relation R) (@eq A ==> R). + Proof. intros. split; reduce; subst; firstorder. Qed. + + (** Subrelations induce a morphism on the identity. *) + + Global Instance subrelation_id_proper `(subrelation A RA RA') : Proper (RA ==> RA') id. + Proof. firstorder. Qed. + + (** The subrelation property goes through products as usual. *) + + Lemma subrelation_respectful `(subl : subrelation A RA' RA, subr : subrelation B RB RB') : + subrelation (RA ==> RB) (RA' ==> RB'). + Proof. unfold subrelation in *; firstorder. Qed. + + (** And of course it is reflexive. *) + + Lemma subrelation_refl R : @subrelation A R R. + Proof. unfold subrelation; firstorder. Qed. + + (** [Proper] is itself a covariant morphism for [subrelation]. + We use an unconvertible premise to avoid looping. + *) + + Lemma subrelation_proper `(mor : Proper A R' m) + `(unc : Unconvertible (relation A) R R') + `(sub : subrelation A R' R) : Proper R m. + Proof. + intros. apply sub. apply mor. + Qed. -Definition pointwise_relation (A : Type) {B : Type} (R : relation B) : relation (A -> B) := - Eval compute in forall_relation (B:=fun _ => B) (fun _ => R). + Global Instance proper_subrelation_proper : + Proper (subrelation ++> eq ==> impl) (@Proper A). + Proof. reduce. subst. firstorder. Qed. -Lemma pointwise_pointwise A B (R : relation B) : - relation_equivalence (pointwise_relation A R) (@eq A ==> R). -Proof. intros. split. simpl_relation. firstorder. Qed. - -(** We can build a PER on the Coq function space if we have PERs on the domain and - codomain. *) + Global Instance pointwise_subrelation `(sub : subrelation B R R') : + subrelation (pointwise_relation R) (pointwise_relation R') | 4. + Proof. reduce. unfold pointwise_relation in *. apply sub. apply H. Qed. + + (** For dependent function types. *) + Lemma forall_subrelation (R S : forall x : A, relation (P x)) : + (forall a, subrelation (R a) (S a)) -> subrelation (forall_relation R) (forall_relation S). + Proof. reduce. apply H. apply H0. Qed. +End Relations. +Typeclasses Opaque respectful pointwise_relation forall_relation. +Arguments forall_relation {A P}%type sig%signature _ _. +Arguments pointwise_relation A%type {B}%type R%signature _ _. + Hint Unfold Reflexive : core. Hint Unfold Symmetric : core. Hint Unfold Transitive : core. -Typeclasses Opaque respectful pointwise_relation forall_relation. - -Program Instance respectful_per `(PER A R, PER B R') : PER (R ==> R'). - - Next Obligation. - Proof with auto. - assert(R x0 x0). - transitivity y0... symmetry... - transitivity (y x0)... - Qed. - -(** Subrelations induce a morphism on the identity. *) - -Instance subrelation_id_proper `(subrelation A R₁ R₂) : Proper (R₁ ==> R₂) id. -Proof. firstorder. Qed. - -(** The subrelation property goes through products as usual. *) - -Lemma subrelation_respectful `(subl : subrelation A R₂ R₁, subr : subrelation B S₁ S₂) : - subrelation (R₁ ==> S₁) (R₂ ==> S₂). -Proof. simpl_relation. apply subr. apply H. apply subl. apply H0. Qed. - -(** And of course it is reflexive. *) - -Lemma subrelation_refl A R : @subrelation A R R. -Proof. simpl_relation. Qed. - +(** Resolution with subrelation: favor decomposing products over applying reflexivity + for unconstrained goals. *) Ltac subrelation_tac T U := (is_ground T ; is_ground U ; class_apply @subrelation_refl) || class_apply @subrelation_respectful || class_apply @subrelation_refl. Hint Extern 3 (@subrelation _ ?T ?U) => subrelation_tac T U : typeclass_instances. -(** [Proper] is itself a covariant morphism for [subrelation]. *) - -Lemma subrelation_proper `(mor : Proper A R₁ m, unc : Unconvertible (relation A) R₁ R₂, - sub : subrelation A R₁ R₂) : Proper R₂ m. -Proof. - intros. apply sub. apply mor. -Qed. - CoInductive apply_subrelation : Prop := do_subrelation. Ltac proper_subrelation := @@ -189,117 +231,112 @@ Ltac proper_subrelation := Hint Extern 5 (@Proper _ ?H _) => proper_subrelation : typeclass_instances. -Instance proper_subrelation_proper : - Proper (subrelation ++> eq ==> impl) (@Proper A). -Proof. reduce. subst. firstorder. Qed. - (** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *) Instance iff_impl_subrelation : subrelation iff impl | 2. Proof. firstorder. Qed. -Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl) | 2. +Instance iff_flip_impl_subrelation : subrelation iff (flip impl) | 2. Proof. firstorder. Qed. -Instance pointwise_subrelation {A} `(sub : subrelation B R R') : - subrelation (pointwise_relation A R) (pointwise_relation A R') | 4. -Proof. reduce. unfold pointwise_relation in *. apply sub. apply H. Qed. - -(** For dependent function types. *) -Lemma forall_subrelation A (B : A -> Type) (R S : forall x : A, relation (B x)) : - (forall a, subrelation (R a) (S a)) -> subrelation (forall_relation R) (forall_relation S). -Proof. reduce. apply H. apply H0. Qed. - (** We use an extern hint to help unification. *) Hint Extern 4 (subrelation (@forall_relation ?A ?B ?R) (@forall_relation _ _ ?S)) => apply (@forall_subrelation A B R S) ; intro : typeclass_instances. -(** Any symmetric relation is equal to its inverse. *) - -Lemma subrelation_symmetric A R `(Symmetric A R) : subrelation (inverse R) R. -Proof. reduce. red in H0. symmetry. assumption. Qed. +Section GenericInstances. + (* Share universes *) + Let U := Type. + Context {A B C : U}. -Hint Extern 4 (subrelation (inverse _) _) => - class_apply @subrelation_symmetric : typeclass_instances. - -(** The complement of a relation conserves its proper elements. *) + (** We can build a PER on the Coq function space if we have PERs on the domain and + codomain. *) + + Program Instance respectful_per `(PER A R, PER B R') : PER (R ==> R'). -Program Definition complement_proper - `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) : - Proper (RA ==> RA ==> iff) (complement R) := _. + Next Obligation. + Proof with auto. + assert(R x0 x0). + transitivity y0... symmetry... + transitivity (y x0)... + Qed. - Next Obligation. + (** The complement of a relation conserves its proper elements. *) + + Program Definition complement_proper + `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) : + Proper (RA ==> RA ==> iff) (complement R) := _. + + Next Obligation. Proof. unfold complement. pose (mR x y H x0 y0 H0). intuition. Qed. -Hint Extern 1 (Proper _ (complement _)) => - apply @complement_proper : typeclass_instances. - -(** The [inverse] too, actually the [flip] instance is a bit more general. *) - -Program Definition flip_proper - `(mor : Proper (A -> B -> C) (RA ==> RB ==> RC) f) : - Proper (RB ==> RA ==> RC) (flip f) := _. + (** The [flip] too, actually the [flip] instance is a bit more general. *) + Program Definition flip_proper + `(mor : Proper (A -> B -> C) (RA ==> RB ==> RC) f) : + Proper (RB ==> RA ==> RC) (flip f) := _. + Next Obligation. Proof. apply mor ; auto. Qed. -Hint Extern 1 (Proper _ (flip _)) => - apply @flip_proper : typeclass_instances. -(** Every Transitive relation gives rise to a binary morphism on [impl], + (** Every Transitive relation gives rise to a binary morphism on [impl], contravariant in the first argument, covariant in the second. *) - -Program Instance trans_contra_co_morphism - `(Transitive A R) : Proper (R --> R ++> impl) R. - + + Global Program + Instance trans_contra_co_morphism + `(Transitive A R) : Proper (R --> R ++> impl) R. + Next Obligation. Proof with auto. transitivity x... transitivity x0... Qed. -(** Proper declarations for partial applications. *) + (** Proper declarations for partial applications. *) -Program Instance trans_contra_inv_impl_morphism - `(Transitive A R) : Proper (R --> inverse impl) (R x) | 3. + Global Program + Instance trans_contra_inv_impl_morphism + `(Transitive A R) : Proper (R --> flip impl) (R x) | 3. Next Obligation. Proof with auto. transitivity y... Qed. -Program Instance trans_co_impl_morphism - `(Transitive A R) : Proper (R ++> impl) (R x) | 3. + Global Program + Instance trans_co_impl_morphism + `(Transitive A R) : Proper (R ++> impl) (R x) | 3. Next Obligation. Proof with auto. transitivity x0... Qed. -Program Instance trans_sym_co_inv_impl_morphism - `(PER A R) : Proper (R ++> inverse impl) (R x) | 3. + Global Program + Instance trans_sym_co_inv_impl_morphism + `(PER A R) : Proper (R ++> flip impl) (R x) | 3. Next Obligation. Proof with auto. transitivity y... symmetry... Qed. -Program Instance trans_sym_contra_impl_morphism - `(PER A R) : Proper (R --> impl) (R x) | 3. + Global Program Instance trans_sym_contra_impl_morphism + `(PER A R) : Proper (R --> impl) (R x) | 3. Next Obligation. Proof with auto. transitivity x0... symmetry... Qed. -Program Instance per_partial_app_morphism + Global Program Instance per_partial_app_morphism `(PER A R) : Proper (R ==> iff) (R x) | 2. Next Obligation. @@ -310,20 +347,21 @@ Program Instance per_partial_app_morphism symmetry... Qed. -(** Every Transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof - to get an [R y z] goal. *) + (** Every Transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof to get an [R y z] goal. *) -Program Instance trans_co_eq_inv_impl_morphism - `(Transitive A R) : Proper (R ==> (@eq A) ==> inverse impl) R | 2. + Global Program + Instance trans_co_eq_inv_impl_morphism + `(Transitive A R) : Proper (R ==> (@eq A) ==> flip impl) R | 2. Next Obligation. Proof with auto. transitivity y... Qed. -(** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *) + (** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *) -Program Instance PER_morphism `(PER A R) : Proper (R ==> R ==> iff) R | 1. + Global Program + Instance PER_morphism `(PER A R) : Proper (R ==> R ==> iff) R | 1. Next Obligation. Proof with auto. @@ -333,11 +371,11 @@ Program Instance PER_morphism `(PER A R) : Proper (R ==> R ==> iff) R | 1. transitivity y... transitivity y0... symmetry... Qed. -Lemma symmetric_equiv_inverse `(Symmetric A R) : relation_equivalence R (flip R). -Proof. firstorder. Qed. + Lemma symmetric_equiv_flip `(Symmetric A R) : relation_equivalence R (flip R). + Proof. firstorder. Qed. -Program Instance compose_proper A B C R₀ R₁ R₂ : - Proper ((R₁ ==> R₂) ==> (R₀ ==> R₁) ==> (R₀ ==> R₂)) (@compose A B C). + Global Program Instance compose_proper RA RB RC : + Proper ((RB ==> RC) ==> (RA ==> RB) ==> (RA ==> RC)) (@compose A B C). Next Obligation. Proof. @@ -345,68 +383,84 @@ Program Instance compose_proper A B C R₀ R₁ R₂ : unfold compose. apply H. apply H0. apply H1. Qed. -(** Coq functions are morphisms for Leibniz equality, - applied only if really needed. *) - -Instance reflexive_eq_dom_reflexive (A : Type) `(Reflexive B R') : - Reflexive (@Logic.eq A ==> R'). -Proof. simpl_relation. Qed. + (** Coq functions are morphisms for Leibniz equality, + applied only if really needed. *) -(** [respectful] is a morphism for relation equivalence. *) - -Instance respectful_morphism : - Proper (relation_equivalence ++> relation_equivalence ++> relation_equivalence) (@respectful A B). -Proof. - reduce. - unfold respectful, relation_equivalence, predicate_equivalence in * ; simpl in *. - split ; intros. + Global Instance reflexive_eq_dom_reflexive `(Reflexive B R') : + Reflexive (@Logic.eq A ==> R'). + Proof. simpl_relation. Qed. + (** [respectful] is a morphism for relation equivalence. *) + + Global Instance respectful_morphism : + Proper (relation_equivalence ++> relation_equivalence ++> relation_equivalence) + (@respectful A B). + Proof. + reduce. + unfold respectful, relation_equivalence, predicate_equivalence in * ; simpl in *. + split ; intros. + rewrite <- H0. apply H1. rewrite H. assumption. - + rewrite H0. apply H1. rewrite <- H. assumption. -Qed. - -(** Every element in the carrier of a reflexive relation is a morphism for this relation. - We use a proxy class for this case which is used internally to discharge reflexivity constraints. - The [Reflexive] instance will almost always be used, but it won't apply in general to any kind of - [Proper (A -> B) _ _] goal, making proof-search much slower. A cleaner solution would be to be able - to set different priorities in different hint bases and select a particular hint database for - resolution of a type class constraint.*) - -Class ProperProxy {A} (R : relation A) (m : A) : Prop := - proper_proxy : R m m. - -Lemma eq_proper_proxy A (x : A) : ProperProxy (@eq A) x. -Proof. firstorder. Qed. - -Lemma reflexive_proper_proxy `(Reflexive A R) (x : A) : ProperProxy R x. -Proof. firstorder. Qed. - -Lemma proper_proper_proxy `(Proper A R x) : ProperProxy R x. -Proof. firstorder. Qed. - -Hint Extern 1 (ProperProxy _ _) => - class_apply @eq_proper_proxy || class_apply @reflexive_proper_proxy : typeclass_instances. -Hint Extern 2 (ProperProxy ?R _) => not_evar R; class_apply @proper_proper_proxy : typeclass_instances. + Qed. -(** [R] is Reflexive, hence we can build the needed proof. *) + (** [R] is Reflexive, hence we can build the needed proof. *) -Lemma Reflexive_partial_app_morphism `(Proper (A -> B) (R ==> R') m, ProperProxy A R x) : - Proper R' (m x). -Proof. simpl_relation. Qed. + Lemma Reflexive_partial_app_morphism `(Proper (A -> B) (R ==> R') m, ProperProxy A R x) : + Proper R' (m x). + Proof. simpl_relation. Qed. + + Lemma flip_respectful (R : relation A) (R' : relation B) : + relation_equivalence (flip (R ==> R')) (flip R ==> flip R'). + Proof. + intros. + unfold flip, respectful. + split ; intros ; intuition. + Qed. -Class Params {A : Type} (of : A) (arity : nat). + + (** Treating flip: can't make them direct instances as we + need at least a [flip] present in the goal. *) + + Lemma flip1 `(subrelation A R' R) : subrelation (flip (flip R')) R. + Proof. firstorder. Qed. + + Lemma flip2 `(subrelation A R R') : subrelation R (flip (flip R')). + Proof. firstorder. Qed. + + (** That's if and only if *) + + Lemma eq_subrelation `(Reflexive A R) : subrelation (@eq A) R. + Proof. simpl_relation. Qed. + + (** Once we have normalized, we will apply this instance to simplify the problem. *) + + Definition proper_flip_proper `(mor : Proper A R m) : Proper (flip R) m := mor. + + (** Every reflexive relation gives rise to a morphism, + only for immediately solving goals without variables. *) + + Lemma reflexive_proper `{Reflexive A R} (x : A) : Proper R x. + Proof. firstorder. Qed. + + Lemma proper_eq (x : A) : Proper (@eq A) x. + Proof. intros. apply reflexive_proper. Qed. + +End GenericInstances. Class PartialApplication. CoInductive normalization_done : Prop := did_normalization. +Class Params {A : Type} (of : A) (arity : nat). + Ltac partial_application_tactic := let rec do_partial_apps H m cont := match m with @@ -450,68 +504,6 @@ Ltac partial_application_tactic := end end. -Hint Extern 4 (@Proper _ _ _) => partial_application_tactic : typeclass_instances. - -Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : relation B), - relation_equivalence (inverse (R ==> R')) (inverse R ==> inverse R'). -Proof. - intros. - unfold flip, respectful. - split ; intros ; intuition. -Qed. - -(** Special-purpose class to do normalization of signatures w.r.t. inverse. *) - -Class Normalizes (A : Type) (m : relation A) (m' : relation A) : Prop := - normalizes : relation_equivalence m m'. - -(** Current strategy: add [inverse] everywhere and reduce using [subrelation] - afterwards. *) - -Lemma inverse_atom A R : Normalizes A R (inverse (inverse R)). -Proof. - firstorder. -Qed. - -Lemma inverse_arrow `(NA : Normalizes A R (inverse R'''), NB : Normalizes B R' (inverse R'')) : - Normalizes (A -> B) (R ==> R') (inverse (R''' ==> R'')%signature). -Proof. unfold Normalizes in *. intros. - rewrite NA, NB. firstorder. -Qed. - -Ltac inverse := - match goal with - | [ |- Normalizes _ (respectful _ _) _ ] => class_apply @inverse_arrow - | _ => class_apply @inverse_atom - end. - -Hint Extern 1 (Normalizes _ _ _) => inverse : typeclass_instances. - -(** Treating inverse: can't make them direct instances as we - need at least a [flip] present in the goal. *) - -Lemma inverse1 `(subrelation A R' R) : subrelation (inverse (inverse R')) R. -Proof. firstorder. Qed. - -Lemma inverse2 `(subrelation A R R') : subrelation R (inverse (inverse R')). -Proof. firstorder. Qed. - -Hint Extern 1 (subrelation (flip _) _) => class_apply @inverse1 : typeclass_instances. -Hint Extern 1 (subrelation _ (flip _)) => class_apply @inverse2 : typeclass_instances. - -(** That's if and only if *) - -Lemma eq_subrelation `(Reflexive A R) : subrelation (@eq A) R. -Proof. simpl_relation. Qed. - -(* Hint Extern 3 (subrelation eq ?R) => not_evar R ; class_apply eq_subrelation : typeclass_instances. *) - -(** Once we have normalized, we will apply this instance to simplify the problem. *) - -Definition proper_inverse_proper `(mor : Proper A R m) : Proper (inverse R) m := mor. - -Hint Extern 2 (@Proper _ (flip _) _) => class_apply @proper_inverse_proper : typeclass_instances. - (** Bootstrap !!! *) Instance proper_proper : Proper (relation_equivalence ==> eq ==> iff) (@Proper A). @@ -525,46 +517,88 @@ Proof. apply H0. Qed. -Lemma proper_normalizes_proper `(Normalizes A R0 R1, Proper A R1 m) : Proper R0 m. -Proof. - red in H, H0. - setoid_rewrite H. - assumption. -Qed. - -Ltac proper_normalization := +Ltac proper_reflexive := match goal with | [ _ : normalization_done |- _ ] => fail 1 - | [ _ : apply_subrelation |- @Proper _ ?R _ ] => let H := fresh "H" in - set(H:=did_normalization) ; class_apply @proper_normalizes_proper + | _ => class_apply proper_eq || class_apply @reflexive_proper end. -Hint Extern 6 (@Proper _ _ _) => proper_normalization : typeclass_instances. -(** Every reflexive relation gives rise to a morphism, only for immediately solving goals without variables. *) +Hint Extern 1 (subrelation (flip _) _) => class_apply @flip1 : typeclass_instances. +Hint Extern 1 (subrelation _ (flip _)) => class_apply @flip2 : typeclass_instances. -Lemma reflexive_proper `{Reflexive A R} (x : A) - : Proper R x. -Proof. firstorder. Qed. +Hint Extern 1 (Proper _ (complement _)) => apply @complement_proper + : typeclass_instances. +Hint Extern 1 (Proper _ (flip _)) => apply @flip_proper + : typeclass_instances. +Hint Extern 2 (@Proper _ (flip _) _) => class_apply @proper_flip_proper + : typeclass_instances. +Hint Extern 4 (@Proper _ _ _) => partial_application_tactic + : typeclass_instances. +Hint Extern 7 (@Proper _ _ _) => proper_reflexive + : typeclass_instances. -Lemma proper_eq A (x : A) : Proper (@eq A) x. -Proof. intros. apply reflexive_proper. Qed. +(** Special-purpose class to do normalization of signatures w.r.t. flip. *) -Ltac proper_reflexive := +Section Normalize. + Context (A : Type). + + Class Normalizes (m : relation A) (m' : relation A) : Prop := + normalizes : relation_equivalence m m'. + + (** Current strategy: add [flip] everywhere and reduce using [subrelation] + afterwards. *) + + Lemma proper_normalizes_proper `(Normalizes R0 R1, Proper A R1 m) : Proper R0 m. + Proof. + red in H, H0. + rewrite H. + assumption. + Qed. + + Lemma flip_atom R : Normalizes R (flip (flip R)). + Proof. + firstorder. + Qed. + +End Normalize. + +Lemma flip_arrow {A : Type} {B : Type} + `(NA : Normalizes A R (flip R'''), NB : Normalizes B R' (flip R'')) : + Normalizes (A -> B) (R ==> R') (flip (R''' ==> R'')%signature). +Proof. + unfold Normalizes in *. intros. + unfold relation_equivalence in *. + unfold predicate_equivalence in *. simpl in *. + unfold respectful. unfold flip in *. firstorder. + apply NB. apply H. apply NA. apply H0. + apply NB. apply H. apply NA. apply H0. +Qed. + +Ltac normalizes := match goal with - | [ _ : normalization_done |- _ ] => fail 1 - | _ => class_apply proper_eq || class_apply @reflexive_proper + | [ |- Normalizes _ (respectful _ _) _ ] => class_apply @flip_arrow + | _ => class_apply @flip_atom end. -Hint Extern 7 (@Proper _ _ _) => proper_reflexive : typeclass_instances. +Ltac proper_normalization := + match goal with + | [ _ : normalization_done |- _ ] => fail 1 + | [ _ : apply_subrelation |- @Proper _ ?R _ ] => + let H := fresh "H" in + set(H:=did_normalization) ; class_apply @proper_normalizes_proper + end. +Hint Extern 1 (Normalizes _ _ _) => normalizes : typeclass_instances. +Hint Extern 6 (@Proper _ _ _) => proper_normalization + : typeclass_instances. (** When the relation on the domain is symmetric, we can - inverse the relation on the codomain. Same for binary functions. *) + flip the relation on the codomain. Same for binary functions. *) Lemma proper_sym_flip : forall `(Symmetric A R1)`(Proper (A->B) (R1==>R2) f), - Proper (R1==>inverse R2) f. + Proper (R1==>flip R2) f. Proof. intros A R1 Sym B R2 f Hf. intros x x' Hxx'. apply Hf, Sym, Hxx'. @@ -572,7 +606,7 @@ Qed. Lemma proper_sym_flip_2 : forall `(Symmetric A R1)`(Symmetric B R2)`(Proper (A->B->C) (R1==>R2==>R3) f), - Proper (R1==>R2==>inverse R3) f. + Proper (R1==>R2==>flip R3) f. Proof. intros A R1 Sym1 B R2 Sym2 C R3 f Hf. intros x x' Hxx' y y' Hyy'. apply Hf; auto. @@ -627,8 +661,6 @@ apply partial_order_antisym; auto. rewrite Hxz; auto. Qed. -Hint Extern 4 (StrictOrder (relation_conjunction _ _)) => - class_apply PartialOrder_StrictOrder : typeclass_instances. (** From a [StrictOrder] to the corresponding [PartialOrder]: [le = lt \/ eq]. @@ -659,5 +691,8 @@ elim (StrictOrder_Irreflexive x). transitivity y; auto. Qed. +Hint Extern 4 (StrictOrder (relation_conjunction _ _)) => + class_apply PartialOrder_StrictOrder : typeclass_instances. + Hint Extern 4 (PartialOrder _ (relation_disjunction _ _)) => class_apply StrictOrder_PartialOrder : typeclass_instances. diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v index c3737658..096c96e5 100644 --- a/theories/Classes/Morphisms_Prop.v +++ b/theories/Classes/Morphisms_Prop.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -16,7 +16,7 @@ Require Import Coq.Classes.Morphisms. Require Import Coq.Program.Basics. Require Import Coq.Program.Tactics. -Local Obligation Tactic := simpl_relation. +Local Obligation Tactic := try solve [simpl_relation | firstorder auto]. (** Standard instances for [not], [iff] and [impl]. *) @@ -52,61 +52,20 @@ Program Instance iff_iff_iff_impl_morphism : Proper (iff ==> iff ==> iff) impl. Program Instance ex_iff_morphism {A : Type} : Proper (pointwise_relation A iff ==> iff) (@ex A). - Next Obligation. - Proof. - unfold pointwise_relation in H. - split ; intros. - destruct H0 as [x1 H1]. - exists x1. rewrite H in H1. assumption. - - destruct H0 as [x1 H1]. - exists x1. rewrite H. assumption. - Qed. - Program Instance ex_impl_morphism {A : Type} : Proper (pointwise_relation A impl ==> impl) (@ex A) | 1. - Next Obligation. - Proof. - unfold pointwise_relation in H. - exists H0. apply H. assumption. - Qed. - -Program Instance ex_inverse_impl_morphism {A : Type} : - Proper (pointwise_relation A (inverse impl) ==> inverse impl) (@ex A) | 1. - - Next Obligation. - Proof. - unfold pointwise_relation in H. - exists H0. apply H. assumption. - Qed. +Program Instance ex_flip_impl_morphism {A : Type} : + Proper (pointwise_relation A (flip impl) ==> flip impl) (@ex A) | 1. Program Instance all_iff_morphism {A : Type} : Proper (pointwise_relation A iff ==> iff) (@all A). - Next Obligation. - Proof. - unfold pointwise_relation, all in *. - intuition ; specialize (H x0) ; intuition. - Qed. - Program Instance all_impl_morphism {A : Type} : Proper (pointwise_relation A impl ==> impl) (@all A) | 1. - Next Obligation. - Proof. - unfold pointwise_relation, all in *. - intuition ; specialize (H x0) ; intuition. - Qed. - -Program Instance all_inverse_impl_morphism {A : Type} : - Proper (pointwise_relation A (inverse impl) ==> inverse impl) (@all A) | 1. - - Next Obligation. - Proof. - unfold pointwise_relation, all in *. - intuition ; specialize (H x0) ; intuition. - Qed. +Program Instance all_flip_impl_morphism {A : Type} : + Proper (pointwise_relation A (flip impl) ==> flip impl) (@all A) | 1. (** Equivalent points are simultaneously accessible or not *) @@ -116,13 +75,13 @@ Instance Acc_pt_morphism {A:Type}(E R : A->A->Prop) Proof. apply proper_sym_impl_iff; auto with *. intros x y EQ WF. apply Acc_intro; intros z Hz. - rewrite <- EQ in Hz. now apply Acc_inv with x. +rewrite <- EQ in Hz. now apply Acc_inv with x. Qed. (** Equivalent relations have the same accessible points *) Instance Acc_rel_morphism {A:Type} : - Proper (@relation_equivalence A ==> Logic.eq ==> iff) (@Acc A). + Proper (relation_equivalence ==> Logic.eq ==> iff) (@Acc A). Proof. apply proper_sym_impl_iff_2. red; now symmetry. red; now symmetry. intros R R' EQ a a' Ha WF. subst a'. @@ -133,7 +92,7 @@ Qed. (** Equivalent relations are simultaneously well-founded or not *) Instance well_founded_morphism {A : Type} : - Proper (@relation_equivalence A ==> iff) (@well_founded A). + Proper (relation_equivalence ==> iff) (@well_founded A). Proof. unfold well_founded. solve_proper. Qed. diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v index 34115e57..68a8c06a 100644 --- a/theories/Classes/Morphisms_Relations.v +++ b/theories/Classes/Morphisms_Relations.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -30,8 +30,6 @@ Instance relation_disjunction_morphism : Proper (relation_equivalence (A:=A) ==> (* Predicate equivalence is exactly the same as the pointwise lifting of [iff]. *) -Require Import List. - Lemma predicate_equivalence_pointwise (l : Tlist) : Proper (@predicate_equivalence l ==> pointwise_lifting iff l) id. Proof. do 2 red. unfold predicate_equivalence. auto. Qed. @@ -40,7 +38,7 @@ Lemma predicate_implication_pointwise (l : Tlist) : Proper (@predicate_implication l ==> pointwise_lifting impl l) id. Proof. do 2 red. unfold predicate_implication. auto. Qed. -(** The instanciation at relation allows to rewrite applications of relations +(** The instantiation at relation allows rewriting applications of relations [R x y] to [R' x y] when [R] and [R'] are in [relation_equivalence]. *) Instance relation_equivalence_pointwise : @@ -52,6 +50,6 @@ Instance subrelation_pointwise : Proof. intro. apply (predicate_implication_pointwise (Tcons A (Tcons A Tnil))). Qed. -Lemma inverse_pointwise_relation A (R : relation A) : - relation_equivalence (pointwise_relation A (inverse R)) (inverse (pointwise_relation A R)). +Lemma flip_pointwise_relation A (R : relation A) : + relation_equivalence (pointwise_relation A (flip R)) (flip (pointwise_relation A R)). Proof. intros. split; firstorder. Qed. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 5c4dd532..1a40e5d5 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -20,43 +20,191 @@ Require Import Coq.Program.Basics. Require Import Coq.Program.Tactics. Require Import Coq.Relations.Relation_Definitions. -(** We allow to unfold the [relation] definition while doing morphism search. *) - -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). -Proof. reflexivity. Qed. +Generalizable Variables A B C D R S T U l eqA eqB eqC eqD. -(** We rebind relations in separate classes to be able to overload each proof. *) +(** We allow to unfold the [relation] definition while doing morphism search. *) -Set Implicit Arguments. -Unset Strict Implicit. +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). + Proof. reflexivity. Qed. + + 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 := { + PreOrder_Reflexive :> Reflexive R | 2 ; + PreOrder_Transitive :> Transitive R | 2 }. + + (** A [StrictOrder] is both Irreflexive and Transitive. *) + + Class StrictOrder (R : relation A) : Prop := { + StrictOrder_Irreflexive :> Irreflexive R ; + StrictOrder_Transitive :> Transitive R }. + + (** By definition, a strict order is also asymmetric *) + Global Instance StrictOrder_Asymmetric `(StrictOrder R) : Asymmetric R. + Proof. firstorder. Qed. + + (** A partial equivalence relation is Symmetric and Transitive. *) + + Class PER (R : relation A) : Prop := { + PER_Symmetric :> Symmetric R | 3 ; + PER_Transitive :> Transitive R | 3 }. + + (** Equivalence relations. *) + + Class Equivalence (R : relation A) : Prop := { + Equivalence_Reflexive :> Reflexive R ; + Equivalence_Symmetric :> Symmetric R ; + Equivalence_Transitive :> Transitive R }. + + (** An Equivalence is a PER plus reflexivity. *) + + Global Instance Equivalence_PER {R} `(E:Equivalence R) : PER 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. + Proof. hnf. intros. red in H0. apply symmetry. assumption. Qed. + + Section flip. + + Lemma flip_Reflexive `{Reflexive R} : Reflexive (flip R). + Proof. tauto. Qed. + + 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). + Proof. firstorder. Qed. + + (** Inversing the larger structures *) + + Lemma flip_PreOrder `(PreOrder R) : PreOrder (flip R). + Proof. firstorder. Qed. + + Lemma flip_StrictOrder `(StrictOrder R) : StrictOrder (flip R). + Proof. firstorder. Qed. + + Lemma flip_PER `(PER R) : PER (flip R). + Proof. firstorder. Qed. + + Lemma flip_Equivalence `(Equivalence R) : Equivalence (flip R). + Proof. firstorder. Qed. + + End flip. + + Section complement. + + Definition complement_Irreflexive `(Reflexive R) + : Irreflexive (complement R). + Proof. firstorder. Qed. + + Definition complement_Symmetric `(Symmetric R) : Symmetric (complement R). + Proof. firstorder. Qed. + 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. This is also done automatically by the [Declare Relation A RA] + commands. *) -Class Reflexive {A} (R : relation A) := - reflexivity : forall x, R x x. + Class RewriteRelation (RA : relation A). -Class Irreflexive {A} (R : relation A) := - irreflexivity : Reflexive (complement R). + (** Any [Equivalence] declared in the context is automatically considered + a rewrite relation. *) + + Global Instance equivalence_rewrite_relation `(Equivalence eqA) : RewriteRelation eqA. + + (** 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. + +End Defs. + +(** Default rewrite relations handled by [setoid_rewrite]. *) +Instance: RewriteRelation impl. +Instance: RewriteRelation iff. +(** Hints to drive the typeclass resolution avoiding loops + due to the use of full unification. *) Hint Extern 1 (Reflexive (complement _)) => class_apply @irreflexivity : typeclass_instances. +Hint Extern 3 (Symmetric (complement _)) => class_apply complement_Symmetric : typeclass_instances. +Hint Extern 3 (Irreflexive (complement _)) => class_apply complement_Irreflexive : typeclass_instances. -Class Symmetric {A} (R : relation A) := - symmetry : forall x y, R x y -> R y x. +Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances. +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 (Antisymmetric (flip _)) => class_apply flip_Antisymmetric : typeclass_instances. +Hint Extern 3 (Transitive (flip _)) => class_apply flip_Transitive : typeclass_instances. +Hint Extern 3 (StrictOrder (flip _)) => class_apply flip_StrictOrder : typeclass_instances. +Hint Extern 3 (PreOrder (flip _)) => class_apply flip_PreOrder : typeclass_instances. -Class Asymmetric {A} (R : relation A) := - asymmetry : forall x y, R x y -> R y x -> False. +Hint Extern 4 (subrelation (flip _) _) => + class_apply @subrelation_symmetric : typeclass_instances. -Class Transitive {A} (R : relation A) := - transitivity : forall x y z, R x y -> R y z -> R x z. +Arguments irreflexivity {A R Irreflexive} [x] _. -Hint Resolve @irreflexivity : ord. +Hint Resolve irreflexivity : ord. Unset Implicit Arguments. @@ -72,40 +220,6 @@ Hint Extern 4 => solve_relation : relations. (** We can already dualize all these properties. *) -Generalizable Variables A B C D R S T U l eqA eqB eqC eqD. - -Lemma flip_Reflexive `{Reflexive A R} : Reflexive (flip R). -Proof. tauto. Qed. - -Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances. - -Program Definition flip_Irreflexive `(Irreflexive A R) : Irreflexive (flip R) := - irreflexivity (R:=R). - -Program Definition flip_Symmetric `(Symmetric A R) : Symmetric (flip R) := - fun x y H => symmetry (R:=R) H. - -Program Definition flip_Asymmetric `(Asymmetric A R) : Asymmetric (flip R) := - fun x y H H' => asymmetry (R:=R) H H'. - -Program Definition flip_Transitive `(Transitive A R) : Transitive (flip R) := - fun x y z H H' => transitivity (R:=R) H' H. - -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. - -Definition Reflexive_complement_Irreflexive `(Reflexive A (R : relation A)) - : Irreflexive (complement R). -Proof. firstorder. Qed. - -Definition complement_Symmetric `(Symmetric A (R : relation A)) : Symmetric (complement R). -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. *) Ltac reduce_hyp H := @@ -130,7 +244,7 @@ Tactic Notation "apply" "*" constr(t) := Ltac simpl_relation := unfold flip, impl, arrow ; try reduce ; program_simpl ; - try ( solve [ intuition ]). + try ( solve [ dintuition ]). Local Obligation Tactic := simpl_relation. @@ -145,54 +259,6 @@ Instance iff_Reflexive : Reflexive iff := iff_refl. Instance iff_Symmetric : Symmetric iff := iff_sym. Instance iff_Transitive : Transitive iff := iff_trans. -(** Leibniz equality. *) - -Instance eq_Reflexive {A} : Reflexive (@eq A) := @eq_refl A. -Instance eq_Symmetric {A} : Symmetric (@eq A) := @eq_sym A. -Instance eq_Transitive {A} : Transitive (@eq A) := @eq_trans A. - -(** Various combinations of reflexivity, symmetry and transitivity. *) - -(** A [PreOrder] is both Reflexive and Transitive. *) - -Class PreOrder {A} (R : relation A) : Prop := { - PreOrder_Reflexive :> Reflexive R | 2 ; - PreOrder_Transitive :> Transitive R | 2 }. - -(** A partial equivalence relation is Symmetric and Transitive. *) - -Class PER {A} (R : relation A) : Prop := { - PER_Symmetric :> Symmetric R | 3 ; - PER_Transitive :> Transitive R | 3 }. - -(** Equivalence relations. *) - -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 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 A eqA `{equ : Equivalence A eqA} (R : relation A) := - antisymmetry : forall {x y}, R x y -> R y x -> eqA x y. - -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 - if only the type is constrained. *) - -Program Instance eq_equivalence : Equivalence (@eq A) | 10. - (** Logical equivalence [iff] is an equivalence relation. *) Program Instance iff_equivalence : Equivalence iff. @@ -203,9 +269,6 @@ Program Instance iff_equivalence : Equivalence iff. Local Open Scope list_scope. -(* Notation " [ ] " := nil : list_scope. *) -(* Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) (at level 1) : list_scope. *) - (** A compact representation of non-dependent arities, with the codomain singled-out. *) (* Note, we do not use [list Type] because it imposes unnecessary universe constraints *) @@ -316,7 +379,8 @@ 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. @@ -345,106 +409,66 @@ Program Instance predicate_implication_preorder : (** 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 (_::_::Tnil). - -Class subrelation {A:Type} (R R' : relation A) : Prop := - is_subrelation : @predicate_implication (A::A::Tnil) R R'. - -Arguments subrelation {A} R R'. - -Definition relation_conjunction {A} (R : relation A) (R' : relation A) : relation A := - @predicate_intersection (A::A::Tnil) R R'. - -Definition relation_disjunction {A} (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. *) - -Set Automatic Introduction. - -Instance relation_equivalence_equivalence (A : Type) : - Equivalence (@relation_equivalence A). -Proof. exact (@predicate_equivalence_equivalence (A::A::Tnil)). Qed. - -Instance relation_implication_preorder A : PreOrder (@subrelation A). -Proof. exact (@predicate_implication_preorder (A::A::Tnil)). Qed. - -(** *** Partial Order. +Section Binary. + Context {A : Type}. + + Definition relation_equivalence : relation (relation A) := + @predicate_equivalence (_::_::Tnil). + + Global Instance: 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. *) + + Set Automatic Introduction. + + Global Instance relation_equivalence_equivalence : + Equivalence relation_equivalence. + Proof. exact (@predicate_equivalence_equivalence (A::A::Tnil)). Qed. + + Global Instance relation_implication_preorder : PreOrder (@subrelation A). + Proof. exact (@predicate_implication_preorder (A::A::Tnil)). Qed. + + (** *** 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. *) -Class PartialOrder {A} eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} := - partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (inverse R)). + Class PartialOrder eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} := + partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (flip 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] *) + + Global Instance partial_order_antisym `(PartialOrder 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. + Qed. -(** 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. - apply <- poe. firstorder. -Qed. + Lemma PartialOrder_inverse `(PartialOrder eqA R) : PartialOrder eqA (flip R). + Proof. firstorder. Qed. +End Binary. + +Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : typeclass_instances. (** The partial order defined by subrelation and relation equivalence. *) Program Instance subrelation_partial_order : ! PartialOrder (relation A) relation_equivalence subrelation. - Next Obligation. - Proof. - unfold relation_equivalence in *. compute; firstorder. - Qed. +Next Obligation. +Proof. + unfold relation_equivalence in *. compute; firstorder. +Qed. 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) : Prop := { - 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. + relation_equivalence pointwise_lifting. diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v index 2b010206..cbde5f9a 100644 --- a/theories/Classes/RelationPairs.v +++ b/theories/Classes/RelationPairs.v @@ -9,8 +9,8 @@ (** * Relations over pairs *) +Require Import SetoidList. Require Import Relations Morphisms. - (* NB: This should be system-wide someday, but for that we need to fix the simpl tactic, since "simpl fst" would be refused for the moment. @@ -40,7 +40,7 @@ Generalizable Variables A B RA RB Ri Ro f. (** Any function from [A] to [B] allow to obtain a relation over [A] out of a relation over [B]. *) -Definition RelCompFun {A B}(R:relation B)(f:A->B) : relation A := +Definition RelCompFun {A} {B : Type}(R:relation B)(f:A->B) : relation A := fun a a' => R (f a) (f a'). Infix "@@" := RelCompFun (at level 30, right associativity) : signature_scope. @@ -62,13 +62,13 @@ Instance snd_measure : @Measure (A * B) B Snd. (** We define a product relation over [A*B]: each components should satisfy the corresponding initial relation. *) -Definition RelProd {A B}(RA:relation A)(RB:relation B) : relation (A*B) := - relation_conjunction (RA @@1) (RB @@2). +Definition RelProd {A : Type} {B : Type} (RA:relation A)(RB:relation B) : relation (A*B) := + relation_conjunction (@RelCompFun (A * B) A RA fst) (RB @@2). Infix "*" := RelProd : signature_scope. Section RelCompFun_Instances. - Context {A B : Type} (R : relation B). + Context {A : Type} {B : Type} (R : relation B). Global Instance RelCompFun_Reflexive `(Measure A B f, Reflexive _ R) : Reflexive (R@@f). @@ -94,57 +94,61 @@ Section RelCompFun_Instances. End RelCompFun_Instances. -Instance RelProd_Reflexive {A B}(RA:relation A)(RB:relation B) - `(Reflexive _ RA, Reflexive _ RB) : Reflexive (RA*RB). -Proof. firstorder. Qed. - -Instance RelProd_Symmetric {A B}(RA:relation A)(RB:relation B) - `(Symmetric _ RA, Symmetric _ RB) : Symmetric (RA*RB). -Proof. firstorder. Qed. - -Instance RelProd_Transitive {A B}(RA:relation A)(RB:relation B) - `(Transitive _ RA, Transitive _ RB) : Transitive (RA*RB). -Proof. firstorder. Qed. - -Program Instance RelProd_Equivalence {A B}(RA:relation A)(RB:relation B) - `(Equivalence _ RA, Equivalence _ RB) : Equivalence (RA*RB). - -Lemma FstRel_ProdRel {A B}(RA:relation A) : - relation_equivalence (RA @@1) (RA*(fun _ _ : B => True)). -Proof. firstorder. Qed. - -Lemma SndRel_ProdRel {A B}(RB:relation B) : - relation_equivalence (RB @@2) ((fun _ _ : A =>True) * RB). -Proof. firstorder. Qed. - -Instance FstRel_sub {A B} (RA:relation A)(RB:relation B): - subrelation (RA*RB) (RA @@1). -Proof. firstorder. Qed. - -Instance SndRel_sub {A B} (RA:relation A)(RB:relation B): - subrelation (RA*RB) (RB @@2). -Proof. firstorder. Qed. - -Instance pair_compat { A B } (RA:relation A)(RB:relation B) : - Proper (RA==>RB==> RA*RB) (@pair _ _). -Proof. firstorder. Qed. - -Instance fst_compat { A B } (RA:relation A)(RB:relation B) : - Proper (RA*RB ==> RA) Fst. -Proof. -intros (x,y) (x',y') (Hx,Hy); compute in *; auto. -Qed. - -Instance snd_compat { A B } (RA:relation A)(RB:relation B) : - Proper (RA*RB ==> RB) Snd. -Proof. -intros (x,y) (x',y') (Hx,Hy); compute in *; auto. -Qed. - -Instance RelCompFun_compat {A B}(f:A->B)(R : relation B) - `(Proper _ (Ri==>Ri==>Ro) R) : - Proper (Ri@@f==>Ri@@f==>Ro) (R@@f)%signature. -Proof. unfold RelCompFun; firstorder. Qed. +Section RelProd_Instances. + + Context {A : Type} {B : Type} (RA : relation A) (RB : relation B). + + Global Instance RelProd_Reflexive `(Reflexive _ RA, Reflexive _ RB) : Reflexive (RA*RB). + Proof. firstorder. Qed. + + Global Instance RelProd_Symmetric `(Symmetric _ RA, Symmetric _ RB) + : Symmetric (RA*RB). + Proof. firstorder. Qed. + + Global Instance RelProd_Transitive + `(Transitive _ RA, Transitive _ RB) : Transitive (RA*RB). + Proof. firstorder. Qed. + + Global Program Instance RelProd_Equivalence + `(Equivalence _ RA, Equivalence _ RB) : Equivalence (RA*RB). + + Lemma FstRel_ProdRel : + relation_equivalence (RA @@1) (RA*(fun _ _ : B => True)). + Proof. firstorder. Qed. + + Lemma SndRel_ProdRel : + relation_equivalence (RB @@2) ((fun _ _ : A =>True) * RB). + Proof. firstorder. Qed. + + Global Instance FstRel_sub : + subrelation (RA*RB) (RA @@1). + Proof. firstorder. Qed. + + Global Instance SndRel_sub : + subrelation (RA*RB) (RB @@2). + Proof. firstorder. Qed. + + Global Instance pair_compat : + Proper (RA==>RB==> RA*RB) (@pair _ _). + Proof. firstorder. Qed. + + Global Instance fst_compat : + Proper (RA*RB ==> RA) Fst. + Proof. + intros (x,y) (x',y') (Hx,Hy); compute in *; auto. + Qed. + + Global Instance snd_compat : + Proper (RA*RB ==> RB) Snd. + Proof. + intros (x,y) (x',y') (Hx,Hy); compute in *; auto. + Qed. + + Global Instance RelCompFun_compat (f:A->B) + `(Proper _ (Ri==>Ri==>Ro) RB) : + Proper (Ri@@f==>Ri@@f==>Ro) (RB@@f)%signature. + Proof. unfold RelCompFun; firstorder. Qed. +End RelProd_Instances. Hint Unfold RelProd RelCompFun. Hint Extern 2 (RelProd _ _ _ _) => split. diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index e7b94081..f20100fe 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index 79168084..bf05934e 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -108,7 +108,7 @@ Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B)) else in_right else in_right. - Solve Obligations using unfold complement ; program_simpl. + Solve Obligations with unfold complement ; program_simpl. (** Objects of function spaces with countable domains like bool have decidable equality. *) @@ -121,7 +121,7 @@ Program Instance bool_function_eqdec `(! EqDec (eq_setoid A)) else in_right else in_right. - Solve Obligations using try red ; unfold equiv, complement ; program_simpl. + Solve Obligations with try red ; unfold complement ; program_simpl. Next Obligation. Proof. diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index 07d1203c..8ca93341 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -12,6 +12,7 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) +Require Coq.Classes.CRelationClasses Coq.Classes.CMorphisms. Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop. Require Export Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions. Require Import Coq.Classes.Equivalence Coq.Program.Basics. diff --git a/theories/Classes/vo.itarget b/theories/Classes/vo.itarget index 9daf133b..18147f2a 100644 --- a/theories/Classes/vo.itarget +++ b/theories/Classes/vo.itarget @@ -1,3 +1,4 @@ +DecidableClass.vo Equivalence.vo EquivDec.vo Init.vo @@ -9,3 +10,6 @@ SetoidClass.vo SetoidDec.vo SetoidTactics.vo RelationPairs.vo +CRelationClasses.vo +CMorphisms.vo +CEquivalence.vo |