Numbers: some improvements in proofs

 - a ltac solve_proper which generalizes solve_predicate_wd and co
 - using le_elim is nicer that (apply le_lteq; destruct ...)
 - "apply ->" can now be "apply" most of the time.

 Benefit: NumPrelude is now almost empty

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13762 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 15 insertions, 0 deletions

diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 8f7bab072..b2994e632 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -81,6 +81,21 @@ 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).
+
 (** 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) :=