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/Numbers/Natural/Abstract/NLcm.v | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) (limited to 'theories/Numbers/Natural/Abstract/NLcm.v') diff --git a/theories/Numbers/Natural/Abstract/NLcm.v b/theories/Numbers/Natural/Abstract/NLcm.v index 8a1a4def6..321508f58 100644 --- a/theories/Numbers/Natural/Abstract/NLcm.v +++ b/theories/Numbers/Natural/Abstract/NLcm.v @@ -59,7 +59,7 @@ Proof. apply mod_divide, div_exact in H; try order. rewrite <- H. rewrite <- gcd_mul_mono_l; try order. - apply gcd_wd; symmetry; apply div_exact; try order; + f_equiv; symmetry; apply div_exact; try order; apply mod_divide; trivial; try order. Qed. @@ -95,9 +95,7 @@ Qed. Definition lcm a b := a*(b/gcd a b). Instance lcm_wd : Proper (eq==>eq==>eq) lcm. -Proof. - unfold lcm. intros x x' Hx y y' Hy. now rewrite Hx, Hy. -Qed. +Proof. unfold lcm. solve_proper. Qed. Lemma lcm_equiv1 : forall a b, gcd a b ~= 0 -> a * (b / gcd a b) == (a*b)/gcd a b. @@ -154,7 +152,7 @@ Proof. exists b'. rewrite <- mul_assoc, Hb'. rewrite (proj2 (div_exact c g NEQ)). - rewrite <- Ha', mul_assoc. apply mul_wd; try easy. + rewrite <- Ha', mul_assoc. f_equiv. apply div_exact; trivial. apply mod_divide; trivial. apply mod_divide; trivial. transitivity a; trivial. @@ -264,7 +262,7 @@ Proof. nzsimpl. rewrite lcm_0_l. now nzsimpl. unfold lcm. rewrite gcd_mul_mono_l. - rewrite mul_assoc. apply mul_wd; try easy. + rewrite mul_assoc. f_equiv. now rewrite div_mul_cancel_l. Qed. -- cgit v1.2.3