diff options
Diffstat (limited to 'theories/Classes/Morphisms.v')
-rw-r--r-- | theories/Classes/Morphisms.v | 125 |
1 files changed, 84 insertions, 41 deletions
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index ea869a66..8e491b1b 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-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -13,8 +13,6 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -(* $Id: Morphisms.v 14641 2011-11-06 11:59:10Z herbelin $ *) - Require Import Coq.Program.Basics. Require Import Coq.Program.Tactics. Require Import Coq.Relations.Relation_Definitions. @@ -23,12 +21,6 @@ Require Export Coq.Classes.RelationClasses. Generalizable All Variables. Local Obligation Tactic := simpl_relation. -Local Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..) - (at level 200, x binder, y binder, right associativity). - -Local Notation "'Π' x .. y , P" := (forall x, .. (forall y, P) ..) - (at level 200, x binder, y binder, right associativity) : type_scope. - (** * Morphisms. We now turn to the definition of [Proper] and declare standard instances. @@ -63,8 +55,8 @@ Definition respectful {A B : Type} Delimit Scope signature_scope with signature. -Arguments Scope Proper [type_scope signature_scope]. -Arguments Scope respectful [type_scope type_scope signature_scope signature_scope]. +Arguments Proper {A}%type R%signature m. +Arguments respectful {A B}%type (R R')%signature _ _. Module ProperNotations. @@ -83,17 +75,58 @@ Export ProperNotations. Open Local 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 : relation 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' => + try reflexivity; + change (Proper R f); eauto with typeclass_instances; fail + | _ => 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 : Π a : A, relation (B a)) : relation (Π x : A, B x) := - λ f g, Π a : A, sig a (f a) (g a). +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 Scope forall_relation [type_scope type_scope signature_scope]. +Arguments forall_relation {A B}%type sig%signature _ _. (** Non-dependent pointwise lifting *) Definition pointwise_relation (A : Type) {B : Type} (R : relation B) : relation (A -> B) := - Eval compute in forall_relation (B:=λ _, B) (λ _, R). + Eval compute in forall_relation (B:=fun _ => B) (fun _ => R). Lemma pointwise_pointwise A B (R : relation B) : relation_equivalence (pointwise_relation A R) (@eq A ==> R). @@ -192,28 +225,34 @@ Hint Extern 4 (subrelation (inverse _) _) => (** The complement of a relation conserves its proper elements. *) -Program Instance complement_proper +Program Definition complement_proper `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) : - Proper (RA ==> RA ==> iff) (complement R). + Proper (RA ==> RA ==> iff) (complement R) := _. - Next Obligation. + 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 Instance flip_proper +Program Definition flip_proper `(mor : Proper (A -> B -> C) (RA ==> RB ==> RC) f) : - Proper (RB ==> RA ==> RC) (flip 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], contravariant in the first argument, covariant in the second. *) @@ -369,41 +408,45 @@ Class PartialApplication. CoInductive normalization_done : Prop := did_normalization. Ltac partial_application_tactic := - let rec do_partial_apps H m := + let rec do_partial_apps H m cont := match m with - | ?m' ?x => class_apply @Reflexive_partial_app_morphism ; [do_partial_apps H m'|clear H] - | _ => idtac + | ?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 := + let rec do_partial H ar m := match ar with - | 0 => do_partial_apps H m + | 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 on_morphism m := - 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'; - do_partial H v' m - 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 - | [ _ : PartialApplication |- _ ] => - class_apply @Reflexive_partial_app_morphism - | _ => - on_morphism (m x) || - (class_apply @Reflexive_partial_app_morphism ; - [ pose Build_PartialApplication | idtac ]) + | [ H : PartialApplication |- _ ] => + class_apply @Reflexive_partial_app_morphism; [|clear H] + | _ => on_morphism (m x) + ltac:(class_apply @Reflexive_partial_app_morphism) end end. @@ -432,7 +475,7 @@ 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. +Proof. unfold Normalizes in *. intros. rewrite NA, NB. firstorder. Qed. |