Tests de nsatz avec la geometrie

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

4 files changed, 66 insertions, 42 deletions

diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v
index 4f2010f29..6d5ea258b 100644
--- a/plugins/nsatz/Nsatz.v
+++ b/plugins/nsatz/Nsatz.v
@@ -28,6 +28,8 @@ Require Export Cring.
 
 Declare ML Module "nsatz_plugin".
 
+(* Definition of integral domains: commutative ring without zero divisor *)
+
 Class Integral_domain {R : Type}`{Rcr:Cring R} := {
  integral_domain_product:
    forall x y, x * y == 0 -> x == 0 \/ y == 0;
@@ -278,19 +280,21 @@ Fixpoint interpret3 t fv {struct t}: R :=
 
 End integral_domain.
 
+Ltac equality_to_goal H x y:=
+  let h := fresh "nH" in
+    (assert (h:equality x y);
+    [solve [cring] | clear H; clear h])
+  || (try generalize (@psos_r1 _ _ _ _ _ _ _ _ _ _ _ x y H); clear H)
+.
+
 Ltac equalities_to_goal :=
   lazymatch goal with
-  |  H: (_ ?x ?y) |- _ =>
-          try generalize (@psos_r1 _ _ _ _ _ _ _ _ _ _ _ x y H); clear H
-  |  H: (_ _ ?x ?y) |- _ =>
-          try generalize (@psos_r1 _ _ _ _ _ _ _ _ _ _ _ x y H); clear H
-  |  H: (_ _ _ ?x ?y) |- _ =>
-          try generalize (@psos_r1 _ _ _ _ _ _ _ _ _ _ _ x y H); clear H
-  |  H: (_ _ _ _ ?x ?y) |- _ =>
-          try generalize (@psos_r1 _ _ _ _ _ _ _ _ _ _ _ x y H); clear H
+  |  H: (_ ?x ?y) |- _ => equality_to_goal H x y
+  |  H: (_ _ ?x ?y) |- _ => equality_to_goal H x y
+  |  H: (_ _ _ ?x ?y) |- _ => equality_to_goal H x y
+  |  H: (_ _ _ _ ?x ?y) |- _ => equality_to_goal H x y
 (* extension possible :-) *)
-  |  H: (?x == ?y) |- _ =>
-          try generalize (@psos_r1 _ _ _ _ _ _ _ _ _ _ _ x y H); clear H
+  |  H: (?x == ?y) |- _ => equality_to_goal H x y
    end.
 
 (* lp est incluse dans fv. La met en tete. *)
@@ -392,8 +396,8 @@ match goal with
                        let lp := get_lpol g in 
                        let lpol := eval compute in (List.rev lp) in
 (*                       idtac "polynomes:"; idtac lpol;*)
-                       simpl; intros;
-  simpl;
+                       (*simpl;*) intros;
+  (*simpl;*)
   let SplitPolyList kont :=
     match lpol with
     | ?p2::?lp2 => kont p2 lp2
@@ -411,28 +415,28 @@ match goal with
       [ (vm_compute;reflexivity) || idtac "invalid nsatz certificate"
       | let Hg2 := fresh "Hg" in 
             assert (Hg2: (interpret3 q fv) == 0);
-        [ simpl; 
+        [ (*simpl*) idtac; 
           generalize (@check_correct _ _ _ _ _ _ _ _ _ _ _ fv lp21 q (lci,lq) Hg);
           let cc := fresh "H" in
-             simpl; intro cc; apply cc; clear cc;
-          simpl;
+             (*simpl*) idtac; intro cc; apply cc; clear cc;
+          (*simpl*) idtac;
           repeat (split;[assumption|idtac]); exact I
-        | simpl in Hg2; simpl; 
+        | (*simpl in Hg2;*) (*simpl*) idtac; 
           apply Rintegral_domain_pow with (interpret3 c fv) (nat_of_N r);
-          simpl;
+          (*simpl*) idtac;
             try apply integral_domain_one_zero;
             try apply integral_domain_minus_one_zero;
             try trivial;
             try exact integral_domain_one_zero;
             try exact integral_domain_minus_one_zero
-          || (simpl) || idtac "could not prove discrimination result"
+          || ((*simpl*) idtac) || idtac "could not prove discrimination result"
         ]
       ]
 ) 
 )
 end end end end .
 
-Ltac nsatz:=
+Ltac nsatz_default:=
   intros;
   try apply (@psos_r1b _ _ _ _ _ _ _ _ _ _ _);
   match goal with |- (@equality ?r _ _ _) =>
@@ -440,11 +444,26 @@ Ltac nsatz:=
     nsatz_generic 6%N 1%Z (@nil r) (@nil r)
   end.
 
+Tactic Notation "nsatz" := nsatz_default.
+
+Tactic Notation "nsatz" "with"
+ "radicalmax" ":=" constr(radicalmax) 
+ "strategy" ":=" constr(info) 
+ "parameters" ":=" constr(lparam)
+ "variables" ":=" constr(lvar):=
+  intros;
+  try apply (@psos_r1b _ _ _ _ _ _ _ _ _ _ _);
+  match goal with |- (@equality ?r _ _ _) =>
+    repeat equalities_to_goal;
+    nsatz_generic radicalmax info lparam lvar
+  end.
+
 Section test.
 Context {R:Type}`{Rid:Integral_domain R}.
 
 Goal forall x y:R, x == x.
-nsatz.
+nsatz with radicalmax := 6%N strategy := 1%Z parameters := (@nil R)
+ variables := (@nil R).
 Qed.
 
 Goal forall x y:R, x == y -> y*y == x*x.
@@ -510,8 +529,6 @@ Qed.
 (* Rational numbers *)
 Require Import QArith.
 
-Check Q_Setoid.
-
 Instance Qops: (@Ring_ops Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq).
 
 Instance Qri : (Ring (Ro:=Qops)).
@@ -557,3 +574,6 @@ Goal forall x y:Z, x = y -> (x*x-x+1)%Z = ((y*y-y)+1+0)%Z.
 nsatz. 
 Qed.
 
+Goal forall x y:Z, x = y -> x = x -> (x*x-x+1)%Z = ((y*y-y)+1+0)%Z.
+nsatz. 
+Qed.
\ No newline at end of file
diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml
index 84a05f0ee..b635fd1fc 100644
--- a/plugins/nsatz/ideal.ml
+++ b/plugins/nsatz/ideal.ml
@@ -363,7 +363,7 @@ let stringPcut p =
   nsP2:=10;
   let res =
     if (length p)> !nsP2
-    then (stringP [hd p])^" + "^(string_of_int (length p))^" termes"
+    then (stringP [hd p])^" + "^(string_of_int (length p))^" terms"
     else  stringP p in
   (*Polynomesrec.nsP1:= max_int;*)
   nsP2:= max_int;
@@ -992,7 +992,7 @@ let pbuchf pq p lp0=
 		    coefpoldep_remove a q;
 		    coefpoldep_set a q c) lca !poldep;
 		  let a0 = a in
-		  info ("\nnew polynomials: "^(stringPcut (ppol a0))^"\n");
+		  info ("\nnew polynomial: "^(stringPcut (ppol a0))^"\n");
 		  let ct = coef1 (* contentP a0 *) in
 		  (*info ("content: "^(string_of_coef ct)^"\n");*)
 		  poldep:=addS a0 lp;
diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4
index 4b8b706d4..3b8cf137e 100644
--- a/plugins/nsatz/nsatz.ml4
+++ b/plugins/nsatz/nsatz.ml4
@@ -326,6 +326,8 @@ open PIdeal
 let term_pol_sparse np t=
   let d = !nvars in
   let rec aux t =
+(*    info ("conversion de: "^(string_of_term t)^"\n");*)
+    let res =
     match t with
     | Zero -> zeroP
     | Const r ->
@@ -342,9 +344,11 @@ let term_pol_sparse np t=
     | Sub (t1,t2) -> plusP (aux t1) (oppP (aux t2))
     | Mul (t1,t2) -> multP (aux t1) (aux t2)
     | Pow (t1,n) ->  puisP (aux t1) n
-  in (*info ("conversion de: "^(string_of_term t)^"\n");*)
+    in 
+(*       info ("donne: "^(stringP res)^"\n");*)
+       res 
+  in
   let res= aux t in
-  (*info ("donne: "^(stringP res)^"\n");*)
   res
 
 (* sparse polynomial to term *)
@@ -367,7 +371,7 @@ let polrec_to_term p =
 (* approximation of the Horner form used in the tactic ring *)
 
 let pol_sparse_to_term n2 p =
-  info "pol_sparse_to_term ->\n";
+ (* info "pol_sparse_to_term ->\n";*)
   let p = PIdeal.repr p in
   let rec aux p =
     match p with
@@ -411,7 +415,7 @@ let pol_sparse_to_term n2 p =
 	  then Var (string_of_int (i0))
 	  else pow (Var (string_of_int (i0)),e0) in
 	add(mul(vm, aux (List.rev (!p1))), aux (List.rev (!p2))))
-  in   info "-> pol_sparse_to_term\n";
+  in   (*info "-> pol_sparse_to_term\n";*)
   aux p
 
 
@@ -492,35 +496,35 @@ let theoremedeszeros_termes lp =
   match lp with
   | Const (Int sugarparam)::Const (Int nparam)::lp ->
       ((match sugarparam with
-      |0 -> info "calcul sans sugar\n";
+      |0 -> info "computation without sugar\n";
 	  lexico:=false;
 	  sugar_flag := false;
 	  divide_rem_with_critical_pair := false
-      |1 -> info "calcul avec sugar\n";
+      |1 -> info "computation with sugar\n";
 	  lexico:=false;
 	  sugar_flag := true;
 	  divide_rem_with_critical_pair := false
-      |2 -> info "ordre lexico calcul sans sugar\n";
+      |2 -> info "ordre lexico computation without sugar\n";
 	  lexico:=true;
 	  sugar_flag := false;
 	  divide_rem_with_critical_pair := false
-      |3 -> info "ordre lexico calcul avec sugar\n";
+      |3 -> info "ordre lexico computation with sugar\n";
 	  lexico:=true;
 	  sugar_flag := true;
 	  divide_rem_with_critical_pair := false
-      |4 -> info "calcul sans sugar, division par les paires\n";
+      |4 -> info "computation without sugar, division by pairs\n";
 	  lexico:=false;
 	  sugar_flag := false;
 	  divide_rem_with_critical_pair := true
-      |5 -> info "calcul avec sugar, division par les paires\n";
+      |5 -> info "computation with sugar, division by pairs\n";
 	  lexico:=false;
 	  sugar_flag := true;
 	  divide_rem_with_critical_pair := true
-      |6 -> info "ordre lexico calcul sans sugar, division par les paires\n";
+      |6 -> info "ordre lexico computation without sugar, division by pairs\n";
 	  lexico:=true;
 	  sugar_flag := false;
 	  divide_rem_with_critical_pair := true
-      |7 -> info "ordre lexico calcul avec sugar, division par les paires\n";
+      |7 -> info "ordre lexico computation with sugar, division by pairs\n";
 	  lexico:=true;
 	  sugar_flag := true;
 	  divide_rem_with_critical_pair := true
@@ -537,6 +541,7 @@ let theoremedeszeros_termes lp =
       | p::lp1 ->
 	  let lpol = List.rev lp1 in
 	  let (cert,lp0,p,_lct) = theoremedeszeros lpol p in
+          info "cert ok\n";
 	  let lc = cert.last_comb::List.rev cert.gb_comb in
 	  match remove_zeros (fun x -> x=zeroP) lc with
 	  | [] -> assert false
@@ -548,8 +553,8 @@ let theoremedeszeros_termes lp =
 	      let lci = List.rev lci in
 	      let lci = List.map (List.map (pol_sparse_to_term m)) lci in
 	      let lq = List.map (pol_sparse_to_term m) lq in
-	      info ("nombre de parametres: "^string_of_int nparam^"\n");
-	      info "terme calcule\n";
+	      info ("number of parametres: "^string_of_int nparam^"\n");
+	      info "term computed\n";
 	      (c,r,lci,lq)
       )
   |_ -> assert false
@@ -568,7 +573,7 @@ let nsatz lpol =
   let certif = hash_certif certif in
   let certif = certif_term certif in
   let c = mkt_term c in
-  info "constr calcule\n";
+  info "constr computed\n";
   (c, certif)
 *)
 
@@ -589,7 +594,7 @@ let nsatz lpol =
 	 mkt_app lcons [tlp ();ltterm;r])
       res
       (mkt_app lnil [tlp ()]) in
-  info "terme calcule\n";
+  info "term computed\n";
   res
 
 let return_term t =
diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml
index b8210bd39..45fcb2d25 100644
--- a/plugins/nsatz/polynom.ml
+++ b/plugins/nsatz/polynom.ml
@@ -282,12 +282,11 @@ let rec multx n v p =
           p2.(i+n)<-p1.(i);
         done;
         Prec (x,p2)
-    |_ -> if p = (Pint coef0) then (Pint coef0)
+    |_ -> if equal p (Pint coef0) then (Pint coef0)
        else (let p2=Array.create (n+1) (Pint coef0) in
                p2.(n)<-p;
                Prec (v,p2))
 
-
 (* product *)
 let rec multP p q =
   match (p,q) with