diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-07-20 09:26:46 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-07-20 09:26:46 +0000 |
| commit | 54861297c8f837cc7617b52737811c30356b6ad7 (patch) | |
| tree | a403960203f414fe342432e6cdcdcadbfc5c09f8 /plugins/groebner | |
| parent | f21daa3756627a718153d7aa661f05ebae0c66c1 (diff) | |
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
Diffstat (limited to 'plugins/groebner')
| -rw-r--r-- | plugins/groebner/GroebnerR.v | 88 |
1 files changed, 1 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 ****) |