From fdda04b92b7347f252d41aa76693ec221a07fe47 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 4 Jan 2011 16:53:58 +0000 Subject: f_equiv : 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']. This way, we can remove most of the explicit use of the morphism instances in Numbers (lemmas foo_wd for each operator foo). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13763 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Classes/Morphisms.v | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) (limited to 'theories/Classes/Morphisms.v') diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index b2994e632..03e0ee8f8 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -96,6 +96,27 @@ Ltac solve_respectful t := 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. + (** 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) := -- cgit v1.2.3