plugin groebner updated and renamed as nsatz; first version of the doc of nsatz in the refman

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

1 files changed, 0 insertions, 73 deletions

diff --git a/plugins/groebner/GroebnerZ.v b/plugins/groebner/GroebnerZ.v
deleted file mode 100644
index 7c40bbb70f..0000000000
--- a/plugins/groebner/GroebnerZ.v
+++ /dev/null
@@ -1,73 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Import Reals ZArith.
-Require Export GroebnerR.
-
-Open Scope Z_scope.
-
-Lemma groebnerZhypR: forall x y:Z, x=y -> IZR x = IZR y.
-Proof IZR_eq. (* or f_equal ... *)
-
-Lemma groebnerZconclR: forall x y:Z, IZR x = IZR y -> x = y.
-Proof eq_IZR.
-
-Lemma groebnerZhypnotR: forall x y:Z, x<>y -> IZR x <> IZR y.
-Proof IZR_neq.
-
-Lemma groebnerZconclnotR: forall x y:Z, IZR x <> IZR y -> x <> y.
-Proof.
-intros x y H. contradict H. f_equal. assumption.
-Qed.
-
-Ltac groebnerZversR1 :=
- repeat
-  (match goal with
-   | H:(@eq Z ?x ?y) |- _ =>
-       generalize (@groebnerZhypR _ _ H); clear H; intro H
-   | |- (@eq Z ?x ?y) => apply groebnerZconclR
-   | H:not (@eq Z ?x ?y) |- _ =>
-       generalize (@groebnerZhypnotR _ _ H); clear H; intro H
-   | |- not (@eq Z ?x ?y) => apply groebnerZconclnotR
-   end).
-
-Lemma groebnerZR1: forall x y:Z, IZR(x+y) = (IZR x + IZR y)%R.
-Proof plus_IZR.
-
-Lemma groebnerZR2: forall x y:Z, IZR(x*y) = (IZR x * IZR y)%R.
-Proof mult_IZR.
-
-Lemma groebnerZR3: forall x y:Z, IZR(x-y) = (IZR x - IZR y)%R.
-Proof.
-intros; symmetry. apply Z_R_minus.
-Qed.
-
-Lemma groebnerZR4: forall (x:Z) p, IZR(x ^ Zpos p) = (IZR x ^ nat_of_P p)%R.
-Proof.
-intros. rewrite pow_IZR.
-do 2 f_equal.
-apply Zpos_eq_Z_of_nat_o_nat_of_P.
-Qed.
-
-Ltac groebnerZversR2:=
-  repeat
-   (rewrite groebnerZR1 in * ||
-    rewrite groebnerZR2 in * ||
-    rewrite groebnerZR3 in * ||
-    rewrite groebnerZR4 in *).
-
-Ltac groebnerZ_begin :=
- intros;
- groebnerZversR1;
- groebnerZversR2;
- simpl in *.
- (*cbv beta iota zeta delta [nat_of_P Pmult_nat plus mult] in *.*)
-
-Ltac groebnerZ :=
- groebnerZ_begin; (*idtac "groebnerZ_begin;";*)
- groebnerR.