helm/software/matita/contribs/procedural/Coq/Reals/DiscrR.mma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "Coq.ma".
  18
  19 (*#***********************************************************************)
  20
  21 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
  22
  23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
  24
  25 (*   \VV/  **************************************************************)
  26
  27 (*    //   *      This file is distributed under the terms of the       *)
  28
  29 (*         *       GNU Lesser General Public License Version 2.1        *)
  30
  31 (*#***********************************************************************)
  32
  33 (*i        $Id: DiscrR.v,v 1.21.2.1 2004/07/16 19:31:10 herbelin Exp $       i*)
  34
  35 include "Reals/RIneq.ma".
  36
  37 (* UNEXPORTED
  38 Open Local Scope R_scope.
  39 *)
  40
  41 inline procedural "cic:/Coq/Reals/DiscrR/Rlt_R0_R2.con" as lemma.
  42
  43 inline procedural "cic:/Coq/Reals/DiscrR/Rplus_lt_pos.con" as lemma.
  44
  45 inline procedural "cic:/Coq/Reals/DiscrR/IZR_eq.con" as lemma.
  46
  47 inline procedural "cic:/Coq/Reals/DiscrR/IZR_neq.con" as lemma.
  48
  49 (* UNEXPORTED
  50 Ltac discrR :=
  51   try
  52    match goal with
  53    |  |- (?X1 <> ?X2) =>
  54        replace 2 with (IZR 2);
  55         [ replace 1 with (IZR 1);
  56            [ replace 0 with (IZR 0);
  57               [ repeat
  58                  rewrite <- plus_IZR ||
  59                    rewrite <- mult_IZR ||
  60                      rewrite <- Ropp_Ropp_IZR || rewrite Z_R_minus;
  61                  apply IZR_neq; try discriminate
  62               | reflexivity ]
  63            | reflexivity ]
  64         | reflexivity ]
  65    end.
  66 *)
  67
  68 (* UNEXPORTED
  69 Ltac prove_sup0 :=
  70   match goal with
  71   |  |- (0 < 1) => apply Rlt_0_1
  72   |  |- (0 < ?X1) =>
  73       repeat
  74        (apply Rmult_lt_0_compat || apply Rplus_lt_pos;
  75          try apply Rlt_0_1 || apply Rlt_R0_R2)
  76   |  |- (?X1 > 0) => change (0 < X1) in |- *; prove_sup0
  77   end.
  78 *)
  79
  80 (* UNEXPORTED
  81 Ltac omega_sup :=
  82   replace 2 with (IZR 2);
  83    [ replace 1 with (IZR 1);
  84       [ replace 0 with (IZR 0);
  85          [ repeat
  86             rewrite <- plus_IZR ||
  87               rewrite <- mult_IZR ||
  88                 rewrite <- Ropp_Ropp_IZR || rewrite Z_R_minus;
  89             apply IZR_lt; omega
  90          | reflexivity ]
  91       | reflexivity ]
  92    | reflexivity ].
  93 *)
  94
  95 (* UNEXPORTED
  96 Ltac prove_sup :=
  97   match goal with
  98   |  |- (?X1 > ?X2) => change (X2 < X1) in |- *; prove_sup
  99   |  |- (0 < ?X1) => prove_sup0
 100   |  |- (- ?X1 < 0) => rewrite <- Ropp_0; prove_sup
 101   |  |- (- ?X1 < - ?X2) => apply Ropp_lt_gt_contravar; prove_sup
 102   |  |- (- ?X1 < ?X2) => apply Rlt_trans with 0; prove_sup
 103   |  |- (?X1 < ?X2) => omega_sup
 104   | _ => idtac
 105   end.
 106 *)
 107
 108 (* UNEXPORTED
 109 Ltac Rcompute :=
 110   replace 2 with (IZR 2);
 111    [ replace 1 with (IZR 1);
 112       [ replace 0 with (IZR 0);
 113          [ repeat
 114             rewrite <- plus_IZR ||
 115               rewrite <- mult_IZR ||
 116                 rewrite <- Ropp_Ropp_IZR || rewrite Z_R_minus;
 117             apply IZR_eq; try reflexivity
 118          | reflexivity ]
 119       | reflexivity ]
 120    | reflexivity ].
 121 *)
 122