Move some examples for groebner into a test-suite file

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

2 files changed, 80 insertions, 87 deletions

diff --git a/plugins/groebner/GroebnerR.v b/plugins/groebner/GroebnerR.v
index 0ab135500..9122540d7 100644
--- a/plugins/groebner/GroebnerR.v
+++ b/plugins/groebner/GroebnerR.v
@@ -407,90 +407,4 @@ Ltac groebnerR := groebnerRpv (@nil R) (@nil R).
 
 Ltac groebnerRp lparam := groebnerRpv lparam (@nil R).
 
-
-(*************** Examples *)
-(*
-Section Examples.
-
-Require Import List Ring_polynom.
-Delimit Scope PE_scope with PE.
-Infix "+" := PEadd : PE_scope.
-Infix "*" := PEmul : PE_scope.
-Infix "-" := PEsub : PE_scope.
-Infix "^" := PEpow : PE_scope.
-Notation "[ n ]" := (@PEc Z n) (at level 0).
-
-Open Scope R_scope.
-
-Goal forall x y,
-  x+y=0 -> 
-  x*y=0 ->
-  x^2=0.
-groebnerR.
-Qed.
-
-Goal forall x, x^2=0 -> x=0.
-groebnerR.
-Qed.
-
-(*
-Notation X  := (PEX Z 3).
-Notation Y  := (PEX Z 2).
-Notation Z_ := (PEX Z 1).
-*)
-Goal forall x y z,
-  x+y+z=0 -> 
-  x*y+x*z+y*z=0->
-  x*y*z=0 -> x^3=0.
-Time groebnerR.
-Qed.
-
-(*
-Notation X  := (PEX Z 4).
-Notation Y  := (PEX Z 3).
-Notation Z_ := (PEX Z 2).
-Notation U  := (PEX Z 1).
-*)
-Goal forall x y z u,
-  x+y+z+u=0 -> 
-  x*y+x*z+x*u+y*z+y*u+z*u=0->
-  x*y*z+x*y*u+x*z*u+y*z*u=0->
-  x*y*z*u=0 -> x^4=0.
-Time groebnerR.
-Qed.
-
-(*
-Notation x_ := (PEX Z 5).
-Notation y_ := (PEX Z 4).
-Notation z_ := (PEX Z 3).
-Notation u_ := (PEX Z 2).
-Notation v_ := (PEX Z 1).
-Notation "x :: y" := (List.cons x y)
-(at level 60, right associativity, format "'[hv' x  ::  '/' y ']'").
-Notation "x :: y" := (List.app x y)
-(at level 60, right associativity, format "x :: y").
-*)
-
-Goal forall x y z u v,
-  x+y+z+u+v=0 -> 
-  x*y+x*z+x*u+x*v+y*z+y*u+y*v+z*u+z*v+u*v=0->
-  x*y*z+x*y*u+x*y*v+x*z*u+x*z*v+x*u*v+y*z*u+y*z*v+y*u*v+z*u*v=0->
-  x*y*z*u+y*z*u*v+z*u*v*x+u*v*x*y+v*x*y*z=0 ->
-  x*y*z*u*v=0 -> x^5=0.
-Time groebnerR.
-Qed.
-
-End Examples.
-*)
-
-
-
-
-
-
-
-
-
-
-
-
+(**** Examples : see test-suite/success/Groebner.v ****)
diff --git a/test-suite/success/Groebner.v b/test-suite/success/Groebner.v
new file mode 100644
index 000000000..7312d16bf
--- /dev/null
+++ b/test-suite/success/Groebner.v
@@ -0,0 +1,79 @@
+Require Import GroebnerR ZArith Reals List Ring_polynom.
+
+(** These exemples were initially in GroebnerR.v *)
+
+Section Examples.
+
+Delimit Scope PE_scope with PE.
+Infix "+" := PEadd : PE_scope.
+Infix "*" := PEmul : PE_scope.
+Infix "-" := PEsub : PE_scope.
+Infix "^" := PEpow : PE_scope.
+Notation "[ n ]" := (@PEc Z n) (at level 0).
+
+Open Scope R_scope.
+
+Lemma example1 : forall x y,
+  x+y=0 ->
+  x*y=0 ->
+  x^2=0.
+Proof.
+ groebnerR.
+Qed.
+
+Lemma example2 : forall x, x^2=0 -> x=0.
+Proof.
+ groebnerR.
+Qed.
+
+(*
+Notation X  := (PEX Z 3).
+Notation Y  := (PEX Z 2).
+Notation Z_ := (PEX Z 1).
+*)
+Lemma example3 : forall x y z,
+  x+y+z=0 ->
+  x*y+x*z+y*z=0->
+  x*y*z=0 -> x^3=0.
+Proof.
+Time groebnerR.
+Qed.
+
+(*
+Notation X  := (PEX Z 4).
+Notation Y  := (PEX Z 3).
+Notation Z_ := (PEX Z 2).
+Notation U  := (PEX Z 1).
+*)
+Lemma example4 : forall x y z u,
+  x+y+z+u=0 ->
+  x*y+x*z+x*u+y*z+y*u+z*u=0->
+  x*y*z+x*y*u+x*z*u+y*z*u=0->
+  x*y*z*u=0 -> x^4=0.
+Proof.
+Time groebnerR.
+Qed.
+
+(*
+Notation x_ := (PEX Z 5).
+Notation y_ := (PEX Z 4).
+Notation z_ := (PEX Z 3).
+Notation u_ := (PEX Z 2).
+Notation v_ := (PEX Z 1).
+Notation "x :: y" := (List.cons x y)
+(at level 60, right associativity, format "'[hv' x  ::  '/' y ']'").
+Notation "x :: y" := (List.app x y)
+(at level 60, right associativity, format "x :: y").
+*)
+
+Lemma example5 : forall x y z u v,
+  x+y+z+u+v=0 ->
+  x*y+x*z+x*u+x*v+y*z+y*u+y*v+z*u+z*v+u*v=0->
+  x*y*z+x*y*u+x*y*v+x*z*u+x*z*v+x*u*v+y*z*u+y*z*v+y*u*v+z*u*v=0->
+  x*y*z*u+y*z*u*v+z*u*v*x+u*v*x*y+v*x*y*z=0 ->
+  x*y*z*u*v=0 -> x^5=0.
+Proof.
+Time groebnerR.
+Qed.
+
+End Examples.
\ No newline at end of file