Amélioration de DiscrR

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

1 files changed, 12 insertions, 33 deletions

diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v
index ff5d807e0..94307dc85 100644
--- a/theories/Reals/DiscrR.v
+++ b/theories/Reals/DiscrR.v
@@ -11,35 +11,6 @@
 Require RIneq.
 Require Omega.
 
-Recursive Tactic Definition Isrealint trm:=
-  Match trm With
-  | [``0``] -> Idtac
-  | [``1``] -> Idtac
-  | [``?1+?2``] -> (Isrealint ?1);(Isrealint ?2)
-  | [``?1-?2``] -> (Isrealint ?1);(Isrealint ?2)
-  | [``?1*?2``] -> (Isrealint ?1);(Isrealint ?2)
-  | [``-?1``] -> (Isrealint ?1)
-  | _ -> Fail.
-
-Recursive Meta Definition ToINR trm:=
-  Match trm With
-  | [ ``1`` ] ->  '(S O)
-  | [ ``1 + ?1`` ] -> Let t=(ToINR ?1) In '(S t).
-
-Tactic Definition DiscrR :=
-  Try Match Context With
-  | [ |- ~(?1==?2) ] ->
-    Isrealint ?1;Isrealint ?2;
-    Apply Rminus_not_eq; Ring ``?1-?2``; 
-      (Match Context With
-      | [ |- [``-1``] ] -> 
-        Repeat Rewrite <- Ropp_distr1;Apply Ropp_neq
-      | _ -> Idtac);
-      (Match Context With
-      | [ |- ``?1<>0``] -> Let nbr=(ToINR ?1) In
-        Replace ?1 with (INR nbr);
-          [Apply not_O_INR;Discriminate|Simpl;Ring]).
-
 Lemma Rlt_R0_R2 : ``0<2``.
 Replace ``2`` with (INR (2)); [Apply lt_INR_0; Apply lt_O_Sn | Reflexivity].
 Qed.
@@ -53,6 +24,18 @@ Apply Rlt_compatibility.
 Assumption.
 Qed.
 
+Lemma IZR_eq : (z1,z2:Z) z1=z2 -> (IZR z1)==(IZR z2).
+Intros; Rewrite H; Reflexivity.
+Qed.
+
+Lemma IZR_neq : (z1,z2:Z) `z1<>z2` -> ``(IZR z1)<>(IZR z2)``.
+Intros; Red; Intro; Elim H; Apply eq_IZR; Assumption.
+Qed.
+
+Tactic Definition DiscrR :=
+  Try Match Context With
+  | [ |- ~(?1==?2) ] -> Replace ``2`` with (IZR `2`); [Replace R1 with (IZR `1`); [Replace R0 with (IZR `0`); [Repeat Rewrite <- plus_IZR Orelse Rewrite <- mult_IZR Orelse Rewrite <- Ropp_Ropp_IZR Orelse Rewrite Z_R_minus; Apply IZR_neq; Try Discriminate | Reflexivity] | Reflexivity] | Reflexivity].
+
 Recursive Tactic Definition Sup0 :=
   Match Context With
   | [ |- ``0<1`` ] -> Apply Rlt_R0_R1
@@ -71,8 +54,4 @@ Recursive Tactic Definition Sup :=
   | [ |- (Rlt ?1 ?2) ] -> SupOmega
   | _ -> Idtac.
 
-Lemma IZR_eq : (z1,z2:Z) z1=z2 -> (IZR z1)==(IZR z2).
-Intros; Rewrite H; Reflexivity.
-Qed.
-
 Tactic Definition RCompute := Replace ``2`` with (IZR `2`); [Replace R1 with (IZR `1`); [Replace R0 with (IZR `0`); [Repeat Rewrite <- plus_IZR Orelse Rewrite <- mult_IZR Orelse Rewrite <- Ropp_Ropp_IZR Orelse Rewrite Z_R_minus; Apply IZR_eq; Try Reflexivity | Reflexivity] | Reflexivity] | Reflexivity].