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

2 files changed, 45 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) :=
diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v
index d4ce9aaa9..256bcc377 100644
--- a/theories/Classes/Morphisms_Prop.v
+++ b/theories/Classes/Morphisms_Prop.v
@@ -107,3 +107,33 @@ Program Instance all_inverse_impl_morphism {A : Type} :
     unfold pointwise_relation, all in *.
     intuition ; specialize (H x0) ; intuition.
   Qed.
+
+(** Equivalent points are simultaneously accessible or not *)
+
+Instance Acc_pt_morphism {A:Type}(E R : A->A->Prop)
+ `(Equivalence _ E) `(Proper _ (E==>E==>iff) R) :
+ Proper (E==>iff) (Acc R).
+Proof.
+ apply proper_sym_impl_iff; auto with *.
+ intros x y EQ WF. apply Acc_intro; intros z Hz.
+ rewrite <- EQ in Hz. now apply Acc_inv with x.
+Qed.
+
+(** Equivalent relations have the same accessible points *)
+
+Instance Acc_rel_morphism {A:Type} :
+ Proper (@relation_equivalence A ==> Logic.eq ==> iff) (@Acc A).
+Proof.
+ apply proper_sym_impl_iff_2. red; now symmetry. red; now symmetry.
+ intros R R' EQ a a' Ha WF. subst a'.
+ induction WF as [x _ WF']. constructor.
+ intros y Ryx. now apply WF', EQ.
+Qed.
+
+(** Equivalent relations are simultaneously well-founded or not *)
+
+Instance well_founded_morphism {A : Type} :
+ Proper (@relation_equivalence A ==> iff) (@well_founded A).
+Proof.
+ unfold well_founded. solve_proper.
+Qed.