diff options
Diffstat (limited to 'theories/Classes/Morphisms.v')
| -rw-r--r-- | theories/Classes/Morphisms.v | 577 |
1 files changed, 306 insertions, 271 deletions
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. |