Ajout tactics Reals

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

1 files changed, 38 insertions, 0 deletions

diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v
new file mode 100644
index 000000000..a5155163b
--- /dev/null
+++ b/theories/Reals/DiscrR.v
@@ -0,0 +1,38 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+Require Rbase.
+
+Tactic Definition Sup0 :=
+  Match Context With
+  | [ |- (Rgt R1 R0) ] -> Unfold Rgt;Apply Rlt_R0_R1
+  | [ |- (Rgt (Rplus R1 ?1) R0) ] ->
+    Apply (Rgt_trans (Rplus R1 ?1) ?1 R0);
+    [Pattern 1 (Rplus R1 ?1);Rewrite Rplus_sym;Unfold Rgt;
+     Apply Rlt_r_r_plus_R1
+    |Sup0].
+
+Tactic Definition DiscrR :=
+  Match Context With
+  | [ |- ~R1==R0 ] -> Red;Intro;Apply R1_neq_R0;Assumption
+  | [ |- ~((Rplus R1 ?1)==R0) ] -> Apply Rgt_not_eq;Sup0
+  | [ |- ~(Ropp ?1)==R0 ] -> Apply Ropp_neq; DiscrR
+  | [ |- ~(?1==?1) ] -> ElimType False
+  | [ |- ~(Rminus R0 ?1)==R0 ] -> Rewrite Rminus_Ropp; DiscrR
+  | [ |- ~(?1==?2) ] -> 
+    (Apply Rminus_not_eq; Ring (Rminus ?1 ?2); 
+      (Match Context With
+      | [ |- ~(Rplus (Ropp R1) ?)==R0 ] -> 
+        Repeat Rewrite <-Ropp_distr1; DiscrR
+      | [ |- ? ] -> DiscrR)
+     Orelse (Apply Rminus_not_eq_right; DiscrR)).
+  
+
+