unification des tactiques nsatz pour R Z avec celle des anneaux integres

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

7 files changed, 158 insertions, 834 deletions

diff --git a/doc/refman/Nsatz.tex b/doc/refman/Nsatz.tex
index be93d5dd7..794e461f0 100644
--- a/doc/refman/Nsatz.tex
+++ b/doc/refman/Nsatz.tex
@@ -1,42 +1,44 @@
-\achapter{Nsatz: tactics for proving equalities in $\mathbb{R}$ and $\mathbb{Z}$}
+\achapter{Nsatz: tactics for proving equalities in integral domains}
 \aauthor{Loïc Pottier}
 
 The tactic \texttt{nsatz} proves goals of the form
 
 \[ \begin{array}{l}
-  \forall X_1,\ldots,X_n \in \mathbb{R},\\
+  \forall X_1,\ldots,X_n \in A,\\
    P_1(X_1,\ldots,X_n) = Q_1(X_1,\ldots,X_n) , \ldots ,  P_s(X_1,\ldots,X_n) =Q_s(X_1,\ldots,X_n)\\ 
  \vdash P(X_1,\ldots,X_n) = Q(X_1,\ldots,X_n)\\
   \end{array}
 \]
-where $P,Q, P_1,Q_1,\ldots,P_s,Q_s$ are polynomials.
+where $P,Q, P_1,Q_1,\ldots,P_s,Q_s$ are polynomials and A is an integral
+domain, i.e. a commutative ring with no zero divisor. For example, A can be
+$\mathbb{R}$, $\mathbb{Z}$, of $\mathbb{Q}$. Note that the equality $=$ used in these
+goals can be any setoid equality 
+(see \ref{setoidtactics})
+, not only Leibnitz equality.
+
 It also proves formulas
 \[ \begin{array}{l}
-  \forall X_1,\ldots,X_n \in \mathbb{R},\\
+  \forall X_1,\ldots,X_n \in A,\\
    P_1(X_1,\ldots,X_n) = Q_1(X_1,\ldots,X_n) \wedge \ldots \wedge  P_s(X_1,\ldots,X_n) =Q_s(X_1,\ldots,X_n)\\ 
  \rightarrow P(X_1,\ldots,X_n) = Q(X_1,\ldots,X_n)\\
   \end{array}
 \] doing automatic introductions.
  
-The tactic \texttt{nsatzZ} proves the same goals where the $X_i$ are in $\mathbb{Z}$.
-
 \asection{Using the basic tactic \texttt{nsatz}}
 \tacindex{nsatz}
 
-If you work in $\mathbb{R}$, load the
-\texttt{NsatzR} module: \texttt{Require Import
-NsatzR}.\\
- and use the tactic \texttt{nsatz} or \texttt{nsatzR}.
-If you work in $\mathbb{Z}$ do the same thing {\em mutatis mutandis}.
+Load the
+\texttt{Nsatz} module: \texttt{Require Import Nsatz}.\\
+ and use the tactic \texttt{nsatz}.
 
 \asection{More about \texttt{nsatz}}
 
 Hilbert's Nullstellensatz theorem shows how to reduce proofs of equalities on
-polynomials on a ring R (with no zero divisor) to algebraic computations: it is easy to see that if a polynomial
-$P$ in $R[X_1,\ldots,X_n]$ verifies $c P^r = \sum_{i=1}^{s} S_i P_i$, with $c
-\in R$, $c \not = 0$, $r$ a positive integer, and the $S_i$s in
-$R[X_1,\ldots,X_n]$, then $P$ is zero whenever polynomials $P_1,...,P_s$  are
-zero (the converse is also true when R is an algebraic closed field:
+polynomials on a commutative ring A with no zero divisor to algebraic computations: it is easy to see that if a polynomial
+$P$ in $A[X_1,\ldots,X_n]$ verifies $c P^r = \sum_{i=1}^{s} S_i P_i$, with $c
+\in A$, $c \not = 0$, $r$ a positive integer, and the $S_i$s in
+$A[X_1,\ldots,X_n]$, then $P$ is zero whenever polynomials $P_1,...,P_s$  are
+zero (the converse is also true when A is an algebraic closed field:
 the method is complete). 
 
 So, proving our initial problem can reduce into finding $S_1,\ldots,S_s$, $c$
@@ -47,17 +49,27 @@ This is achieved by the computation of a Groebner basis of the
 ideal generated by $P_1-Q_1,...,P_s-Q_s$, with an adapted version of the Buchberger
 algorithm.
 
+This computation is done after a step of {\em reification}, which is
+performed using {\em Type Classes} 
+(see \ref{typeclasses})
+.
+
+The \texttt{Nsatz} module defines the generic tactic
+\texttt{nsatz}, which uses the low-level tactic \texttt{nsatz\_domainpv}: \\
+\vspace*{3mm}
+\texttt{nsatz\_domainpv pretac rmax strategy lparam lvar simpltac domain}
+
+where:
 
-The \texttt{NsatzR} module defines the tactics
-\texttt{nsatz},  \texttt{nsatzRradical}, \texttt{nsatzRparameters}, and
-the generic tactic \texttt{nsatzRpv}, which are used as follows:
+\begin{itemize}
+    \item \texttt{pretac} is a tactic depending on the ring A; its goal is to
+make apparent the generic operations of a domain (ring\_eq, ring\_plus, etc),
+both in the goal and the hypotheses; it is executed first. By default it is \texttt{ltac:idtac}.
 
-  \begin{itemize}
-  \item \texttt{nsatzRpv rmax strategy lparam lvar}:
-    \begin{itemize}
-	\item \texttt{rmax} is a bound when for searching r s.t.$c (P-Q)^r =
+    \item \texttt{rmax} is a bound when for searching r s.t.$c (P-Q)^r =
 \sum_{i=1..s} S_i (P_i - Q_i)$
-	\item \texttt{strategy} gives the order on variables $X_1,...X_n$ and
+	
+    \item \texttt{strategy} gives the order on variables $X_1,...X_n$ and
 the strategy used in Buchberger algorithm (see
 \cite{sugar} for details): 
 
@@ -78,15 +90,19 @@ which states that $c$ is not zero.
 
 	\item \texttt{lvar} is the list of the variables
 in the decreasing order in which they will be used in Buchberger algorithm. If \texttt{lvar} = {(@nil
-R)}, then \texttt{lvar} is replaced by all the variables which are not in lparam.
-     \end{itemize}
-  \item \texttt{nsatzRparameters lparam} is equivalent to 
-        \texttt{nsatzRpv 6\%N 1\%Z lparam (@nil R)}
-  \item \texttt{nsatzRradical rmax} is equivalent to 
-	\texttt{nsatzRpv rmax 1\%Z (@nil R) (@nil R)}
-  \item \texttt{nsatz} is equivalent to 
-	\texttt{nsatzRpv 6\%N 1\%Z (@nil R) (@nil R)}ls
-  \end{itemize}
+R)}, then \texttt{lvar} is replaced by all the variables which are not in
+lparam.
+
+    \item \texttt{simpltac} is a tactic depending on the ring A; its goal is to
+simplify goals and make apparent the generic operations of a domain after
+simplifications. By default it is \texttt{ltac:simpl}.
+
+ \item \texttt{domain} is the object of type Domain representing A, its
+operations and properties of integral domain.
+
+\end{itemize}
+
+See file \texttt{Nsatz.v} for examples.
 
 %%% Local Variables: 
 %%% mode: latex
diff --git a/plugins/nsatz/Nsatz_domain.v b/plugins/nsatz/Nsatz.v
index 7da698db5..aa32b386c 100644
--- a/plugins/nsatz/Nsatz_domain.v
+++ b/plugins/nsatz/Nsatz.v
@@ -8,8 +8,13 @@
 
 (*
  Tactic nsatz: proofs of polynomials equalities in a domain (ring without zero divisor).
- Reification is done by type classes.
- Example: see test-suite/success/Nsatz_domain.v
+ Reification is done by type classes, following a technique shown by Mathieu
+Sozeau. Verification of certificate is done by a code written by Benjamin
+Gregoire, following an idea of Laurent Théry.
+
+Examples: see test-suite/success/Nsatz.v
+
+Loïc Pottier, july 2010
 *)
 
 Require Import List.
diff --git a/plugins/nsatz/NsatzR.v b/plugins/nsatz/NsatzR.v
deleted file mode 100644
index 2009dc16d..000000000
--- a/plugins/nsatz/NsatzR.v
+++ /dev/null
@@ -1,406 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*
- Tactic nsatz: proofs of polynomials equalities with variables in R.
- Uses Hilbert Nullstellensatz and Buchberger algorithm.
- Thanks to B.Gregoire and L.Thery for help on ring tactic, 
- and to B.Barras for modularization of the ocaml code.
- Example: see test-suite/success/Nsatz.v
- L.Pottier, june 2010
-*)
-
-Require Import List.
-Require Import Setoid.
-Require Import BinPos.
-Require Import BinList.
-Require Import Znumtheory.
-Require Import RealField Rdefinitions Rfunctions RIneq DiscrR.
-Require Import Ring_polynom Ring_tac InitialRing.
-
-Declare ML Module "nsatz_plugin".
-
-Local Open Scope R_scope.
-
-Lemma psos_r1b: forall x y, x - y = 0 -> x = y.
-intros x y H; replace x with ((x - y) + y);
-  [rewrite H | idtac]; ring.
-Qed.
-
-Lemma psos_r1: forall x y, x = y -> x - y = 0.
-intros x y H; rewrite H; ring.
-Qed.
-
-Lemma nsatzR_not1: forall x y:R, x<>y -> exists z:R, z*(x-y)-1=0.
-intros.
-exists (1/(x-y)).
-field.
-unfold not.
-unfold not in H.
-intros.
-apply H.
-replace x with ((x-y)+y).
-rewrite H0.
-ring.
-ring.
-Qed.
-
-Lemma nsatzR_not1_0: forall x:R, x<>0 -> exists z:R, z*x-1=0.
-intros.
-exists (1/(x)).
-field.
-auto.
-Qed.
-
-
-Ltac equalities_to_goal :=
-  lazymatch goal with
-  |  H: (@eq R ?x 0) |- _ => try revert H
-  |  H: (@eq R 0 ?x) |- _ =>
-          try generalize (sym_equal H); clear H
-  |  H: (@eq R ?x ?y) |- _ =>
-          try generalize (psos_r1 _ _ H); clear H
-   end.
-
-Lemma nsatzR_not2: 1<>0.
-auto with *.
-Qed.
-
-Lemma nsatzR_diff: forall x y:R, x<>y -> x-y<>0.
-intros.
-intro; apply H.
-replace x with (x-y+y) by ring.
-rewrite H0; ring.
-Qed.
-
-(* Removes x<>0 from hypothesis *)
-Ltac nsatzR_not_hyp:=
- match goal with
- | H: ?x<>?y |- _ =>
-  match y with
-   |0 =>
-     let H1:=fresh "Hnsatz" in
-     let y:=fresh "x" in
-     destruct (@nsatzR_not1_0 _ H) as (y,H1); clear H
-   |_ => generalize (@nsatzR_diff _ _ H); clear H; intro
-  end
- end.
-
-Ltac nsatzR_not_goal :=
- match goal with
- | |- ?x<>?y :> R => red; intro; apply nsatzR_not2
- | |- False       => apply nsatzR_not2
- end.
-
-Ltac nsatzR_begin :=
-  intros;
-  repeat nsatzR_not_hyp;
-  try nsatzR_not_goal;
-  try apply psos_r1b;
-  repeat equalities_to_goal.
-
-(* code de Benjamin *)
-
-Definition PolZ := Pol Z.
-Definition PEZ := PExpr Z.
-
-Definition P0Z : PolZ := @P0 Z 0%Z.
-
-Definition PolZadd : PolZ -> PolZ -> PolZ :=
-  @Padd Z 0%Z Zplus Zeq_bool.
-
-Definition PolZmul : PolZ -> PolZ -> PolZ :=
-  @Pmul Z 0%Z 1%Z Zplus Zmult Zeq_bool.
-
-Definition PolZeq := @Peq Z Zeq_bool.
-
-Definition norm :=
-  @norm_aux Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool.
-
-Fixpoint mult_l (la : list PEZ) (lp: list PolZ) : PolZ :=
- match la, lp with
- | a::la, p::lp => PolZadd (PolZmul (norm a) p) (mult_l la lp)
- | _, _ => P0Z
- end.
-
-Fixpoint compute_list (lla: list (list PEZ)) (lp:list PolZ) :=
- match lla with
- | List.nil => lp
- | la::lla => compute_list lla ((mult_l la lp)::lp)
- end.
-
-Definition check (lpe:list PEZ) (qe:PEZ) (certif: list (list PEZ) * list PEZ) :=
- let (lla, lq) := certif in
- let lp := List.map norm lpe in
- PolZeq (norm qe) (mult_l lq (compute_list lla lp)).
-
-
-(* Correction *)
-Definition PhiR : list R -> PolZ -> R :=
-  (Pphi 0 Rplus Rmult (gen_phiZ 0 1 Rplus Rmult Ropp)).
-
-Definition PEevalR : list R -> PEZ -> R :=
-   PEeval 0 Rplus Rmult Rminus Ropp (gen_phiZ 0 1 Rplus Rmult Ropp)
-         Nnat.nat_of_N pow.
-
-Lemma P0Z_correct : forall l, PhiR l P0Z = 0.
-Proof. trivial. Qed.
-
-
-Lemma PolZadd_correct : forall P' P l,
-  PhiR l (PolZadd P P') = (PhiR l P + PhiR l P').
-Proof.
- refine (Padd_ok Rset Rext (Rth_ARth Rset Rext (F_R Rfield))
-           (gen_phiZ_morph Rset Rext (F_R Rfield))).
-Qed.
-
-Lemma PolZmul_correct : forall P P' l,
-  PhiR l (PolZmul P P') = (PhiR l P * PhiR l P').
-Proof.
- refine (Pmul_ok Rset Rext (Rth_ARth Rset Rext (F_R Rfield))
-           (gen_phiZ_morph Rset Rext (F_R Rfield))).
-Qed.
-
-Lemma norm_correct :
-  forall (l : list R) (pe : PEZ), PEevalR l pe = PhiR l (norm pe).
-Proof.
- intros;apply (norm_aux_spec Rset Rext (Rth_ARth Rset Rext (F_R Rfield))
-           (gen_phiZ_morph Rset Rext (F_R Rfield)) R_power_theory) with (lmp:= List.nil).
- compute;trivial.
-Qed.
-
-Lemma PolZeq_correct : forall P P' l,
-  PolZeq P P' = true ->
-  PhiR l P = PhiR l P'.
-Proof.
- intros;apply
-   (Peq_ok Rset Rext (gen_phiZ_morph Rset Rext (F_R Rfield)));trivial.
-Qed.
-
-Fixpoint Cond0 (A:Type) (Interp:A->R) (l:list A) : Prop :=
-  match l with
-  | List.nil => True
-  | a::l => Interp a = 0 /\ Cond0 A Interp l
-  end.
-
-Lemma mult_l_correct : forall l la lp,
-  Cond0 PolZ (PhiR l) lp ->
-  PhiR l (mult_l la lp) = 0.
-Proof.
- induction la;simpl;intros;trivial.
- destruct lp;trivial.
- simpl in H;destruct H.
- rewrite PolZadd_correct, PolZmul_correct, H, IHla;[ring | trivial].
-Qed.
-
-Lemma compute_list_correct : forall l lla lp,
-  Cond0 PolZ (PhiR l) lp ->
-  Cond0 PolZ (PhiR l) (compute_list lla lp).
-Proof.
- induction lla;simpl;intros;trivial.
- apply IHlla;simpl;split;trivial.
- apply mult_l_correct;trivial.
-Qed.
-
-Lemma check_correct :
-  forall l lpe qe certif,
-    check lpe qe certif = true ->
-    Cond0 PEZ (PEevalR l) lpe ->
-    PEevalR l qe = 0.
-Proof.
- unfold check;intros l lpe qe (lla, lq) H2 H1.
- apply PolZeq_correct with (l:=l) in H2.
- rewrite norm_correct, H2.
- apply mult_l_correct.
- apply compute_list_correct.
- clear H2 lq lla qe;induction lpe;simpl;trivial.
- simpl in H1;destruct H1.
- rewrite <- norm_correct;auto.
-Qed.
-
-(* fin du code de Benjamin *)
-
-Lemma nsatzR_l3:forall c p r, ~c=0 -> c*p^r=0 -> p=0.
-intros.
-elim (Rmult_integral _ _ H0);intros.
- absurd (c=0);auto.
-
- clear H0; induction r; simpl in *.
-  contradict H1; discrR.
-
-  elim (Rmult_integral _ _ H1); auto.
-Qed.
-
-
-Ltac generalise_eq_hyps:=
-  repeat
-    (match goal with
-     |h : (?p = ?q)|- _ => revert h
-     end).
-
-Ltac lpol_goal t :=
-  match t with
-  | ?a = 0 -> ?b =>
-    let r:= lpol_goal b in
-    constr:(a::r)
-  | ?a = 0 => constr:(a::nil)
- end.
-
-Fixpoint IPR p {struct p}: R :=
-  match p with
-    xH => 1
-  | xO xH => 1 + 1
-  | xO p1 => 2 * (IPR p1)
-  | xI xH => 1 + (1 + 1)
-  | xI p1 => 1 + 2 * (IPR p1)
-  end.
-
-Definition IZR1 z :=
-  match z with Z0 => 0
-             | Zpos p => IPR p
-             | Zneg p => -(IPR p)
-  end.
-
-Fixpoint interpret3 t fv {struct t}: R :=
-  match t with
-  | (PEadd t1 t2) =>
-       let v1  := interpret3 t1 fv in
-       let v2  := interpret3 t2 fv in (v1 + v2)
-  | (PEmul t1 t2) =>
-       let v1  := interpret3 t1 fv in
-       let v2  := interpret3 t2 fv in (v1 * v2)
-  | (PEsub t1 t2) =>
-       let v1  := interpret3 t1 fv in
-       let v2  := interpret3 t2 fv in (v1 - v2)
-  | (PEopp t1) =>
-       let v1  := interpret3 t1 fv in (-v1)
-  | (PEpow t1 t2) =>
-       let v1  := interpret3 t1 fv in v1 ^(Nnat.nat_of_N t2)
-  | (PEc t1) => (IZR1 t1)
-  | (PEX n) => List.nth (pred (nat_of_P n)) fv 0
-  end.
-
-(* lp est incluse dans fv. La met en tete. *)
-
-Ltac parametres_en_tete fv lp :=
-    match fv with
-     | (@nil _)          => lp
-     | (@cons _ ?x ?fv1) =>
-       let res := AddFvTail x lp in
-         parametres_en_tete fv1 res
-    end.
-
-Ltac append1 a l :=
- match l with
- | (@nil _)     => constr:(cons a l)
- | (cons ?x ?l) => let l' := append1 a l in constr:(cons x l')
- end.
-
-Ltac rev l :=
-  match l with
-   |(@nil _)      => l
-   | (cons ?x ?l) => let l' := rev l in append1 x l'
-  end.
-
-
-Ltac nsatz_call_n info nparam p rr lp kont :=
-  nsatz_compute (PEc info :: PEc nparam :: PEpow p rr :: lp);
-  match goal with
-  | |- (?c::PEpow _ ?r::?lq0)::?lci0 = _ -> _ =>
-    intros _;
-    set (lci:=lci0);
-    set (lq:=lq0);
-    kont c rr lq lci
-  end.
-
-Ltac nsatz_call radicalmax info nparam p lp kont :=
-  let rec try_n n :=
-    lazymatch n with
-    | 0%N => fail
-    | _ =>
-(*        idtac "Trying power: " n;*)
-        (let r := eval compute in (Nminus radicalmax (Npred n)) in
-         nsatz_call_n info nparam p r lp kont) ||
-         let n' := eval compute in (Npred n) in try_n n'
-    end in
-  try_n radicalmax.
-
-
-Ltac nsatzR_gen radicalmax info lparam lvar n RNG lH _rl :=
-  get_Pre RNG ();
-  let mkFV := Ring_tac.get_RingFV RNG in
-  let mkPol := Ring_tac.get_RingMeta RNG in
-  generalise_eq_hyps;
-  let t := Get_goal in
-  let lpol := lpol_goal t in
-  intros;
-  let fv :=
-    match lvar with
-    | nil =>
-        let fv1 := FV_hypo_tac mkFV ltac:(get_Eq RNG) lH in
-        let fv1 := list_fold_right mkFV fv1 lpol in
-        rev fv1
-    (* heuristique: les dernieres variables auront le poid le plus fort *)
-    | _ => lvar
-    end in
-  check_fv fv;
-  (*idtac "variables:";idtac fv;*)
-  let nparam := eval compute in (Z_of_nat (List.length lparam)) in
-  let fv := parametres_en_tete fv lparam in
-  idtac "variables:"; idtac fv;
-   (* idtac "nparam:"; idtac nparam;*)
-  let lpol := list_fold_right
-    ltac:(fun p l => let p' := mkPol p fv in constr:(p'::l))
-    (@nil (PExpr Z))
-    lpol in
-  let lpol := eval compute in (List.rev lpol) in
-  (*idtac lpol;*)
-  let SplitPolyList kont :=
-    match lpol with
-    | ?p2::?lp2 => kont p2 lp2
-    | _ => idtac "polynomial not in the ideal"
-    end in
-  SplitPolyList ltac:(fun p lp =>
-    set (p21:=p) ;
-    set (lp21:=lp);
-    nsatz_call radicalmax info nparam p lp ltac:(fun c r lq lci =>
-      set (q := PEmul c (PEpow p21 r));
-      let Hg := fresh "Hg" in
-      assert (Hg:check lp21 q (lci,lq) = true);
-      [ (vm_compute;reflexivity) || idtac "invalid nsatz certificate"
-      | let Hg2 := fresh "Hg" in
-        assert (Hg2: interpret3 q fv = 0);
-        [ simpl; apply (@check_correct fv lp21 q (lci,lq) Hg); simpl;
-          repeat (split;[assumption|idtac]); exact I
-        | simpl in Hg2; simpl;
-          apply nsatzR_l3 with (interpret3 c fv) (Nnat.nat_of_N r);simpl;
-          [ discrR || idtac "could not prove discrimination result"
-          | exact Hg2]
-        ]
-      ])).
-
-Ltac nsatzRpv radicalmax info lparam lvar:=
-  nsatzR_begin;
-  intros;
-  let G := Get_goal in
-  ring_lookup
-    (PackRing ltac:(nsatzR_gen radicalmax info lparam lvar ring_subst_niter))
-    [] G.
-
-Ltac nsatzR := nsatzRpv 6%N 1%Z (@nil R) (@nil R).
-Ltac nsatzRradical radicalmax := nsatzRpv radicalmax 1%Z (@nil R) (@nil R).
-Ltac nsatzRparameters lparam := nsatzRpv 6%N 1%Z lparam (@nil R).
-
-Tactic Notation "nsatz" "with" "lexico" := 
-  nsatzRpv 6%N 2%Z (@nil R) (@nil R).
-Tactic Notation "nsatz" "with" "lexico" "sugar":= 
-  nsatzRpv 6%N 3%Z (@nil R) (@nil R).
-Tactic Notation "nsatz" "without" "sugar":= 
-  nsatzRpv 6%N 0%Z (@nil R) (@nil R).
-
-
diff --git a/plugins/nsatz/NsatzZ.v b/plugins/nsatz/NsatzZ.v
deleted file mode 100644
index b57aa0ed6..000000000
--- a/plugins/nsatz/NsatzZ.v
+++ /dev/null
@@ -1,73 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Import Reals ZArith.
-Require Export NsatzR.
-
-Open Scope Z_scope.
-
-Lemma nsatzZhypR: forall x y:Z, x=y -> IZR x = IZR y.
-Proof IZR_eq. (* or f_equal ... *)
-
-Lemma nsatzZconclR: forall x y:Z, IZR x = IZR y -> x = y.
-Proof eq_IZR.
-
-Lemma nsatzZhypnotR: forall x y:Z, x<>y -> IZR x <> IZR y.
-Proof IZR_neq.
-
-Lemma nsatzZconclnotR: forall x y:Z, IZR x <> IZR y -> x <> y.
-Proof.
-intros x y H. contradict H. f_equal. assumption.
-Qed.
-
-Ltac nsatzZtoR1 :=
- repeat
-  (match goal with
-   | H:(@eq Z ?x ?y) |- _ =>
-       generalize (@nsatzZhypR _ _ H); clear H; intro H
-   | |- (@eq Z ?x ?y) => apply nsatzZconclR
-   | H:not (@eq Z ?x ?y) |- _ =>
-       generalize (@nsatzZhypnotR _ _ H); clear H; intro H
-   | |- not (@eq Z ?x ?y) => apply nsatzZconclnotR
-   end).
-
-Lemma nsatzZR1: forall x y:Z, IZR(x+y) = (IZR x + IZR y)%R.
-Proof plus_IZR.
-
-Lemma nsatzZR2: forall x y:Z, IZR(x*y) = (IZR x * IZR y)%R.
-Proof mult_IZR.
-
-Lemma nsatzZR3: forall x y:Z, IZR(x-y) = (IZR x - IZR y)%R.
-Proof.
-intros; symmetry. apply Z_R_minus.
-Qed.
-
-Lemma nsatzZR4: 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 nsatzZtoR2:=
-  repeat
-   (rewrite nsatzZR1 in * ||
-    rewrite nsatzZR2 in * ||
-    rewrite nsatzZR3 in * ||
-    rewrite nsatzZR4 in *).
-
-Ltac nsatzZ_begin :=
- intros;
- nsatzZtoR1;
- nsatzZtoR2;
- simpl in *.
- (*cbv beta iota zeta delta [nat_of_P Pmult_nat plus mult] in *.*)
-
-Ltac nsatzZ :=
- nsatzZ_begin; (*idtac "nsatzZ_begin;";*)
- nsatzR.
diff --git a/plugins/nsatz/vo.itarget b/plugins/nsatz/vo.itarget
index 4af4786dd..06fc88343 100644
--- a/plugins/nsatz/vo.itarget
+++ b/plugins/nsatz/vo.itarget
@@ -1,3 +1 @@
-NsatzR.vo
-Nsatz_domain.vo
-NsatzZ.vo
+Nsatz.vo
diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v
index fde9f4700..518d22e98 100644
--- a/test-suite/success/Nsatz.v
+++ b/test-suite/success/Nsatz.v
@@ -1,4 +1,74 @@
-Require Import NsatzR ZArith Reals List Ring_polynom.
+Require Import Nsatz ZArith Reals List Ring_polynom.
+
+(* Example with a generic domain *)
+
+Variable A: Type.
+Variable Ad: Domain A.
+
+Definition Ari : Ring A:= (@domain_ring A Ad).
+Existing Instance Ari.
+
+Existing Instance ring_setoid.
+Existing Instance ring_plus_comp.
+Existing Instance ring_mult_comp.
+Existing Instance ring_sub_comp.
+Existing Instance ring_opp_comp.
+
+Add Ring Ar: (@ring_ring A (@domain_ring A Ad)).
+
+Instance zero_ring2 : Zero A := {zero := ring0}.
+Instance one_ring2 : One A := {one := ring1}.
+Instance addition_ring2 : Addition A := {addition x y := ring_plus x y}.
+Instance multiplication_ring2 : Multiplication A := {multiplication x y := ring_mult x y}.
+Instance subtraction_ring2 : Subtraction A := {subtraction x y := ring_sub x y}.
+Instance opposite_ring2 : Opposite A := {opposite x := ring_opp x}.
+
+Infix "==" := ring_eq (at level 70, no associativity).
+
+Ltac nsatzA := simpl; unfold Ari; nsatz_domain.
+
+Goal forall x y:A,  x == y -> x+0 == y*1+0.
+nsatzA.
+Qed.
+
+Lemma example3 : forall x y z,
+  x+y+z==0 ->
+  x*y+x*z+y*z==0->
+  x*y*z==0 -> x*x*x==0.
+Proof.
+Time nsatzA. 
+Admitted.
+
+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*x*x*x==0.
+Proof.
+Time nsatzA.
+Qed.
+
+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*x*x*x*x ==0.
+Proof.
+Time nsatzA.
+Qed.
+
+Goal forall x y:Z,  x = y -> (x+0)%Z = (y*1+0)%Z.
+nsatz.
+Qed.
+
+Goal forall x y:R,  x = y -> (x+0)%R = (y*1+0)%R.
+nsatz.
+Qed.
+
+Goal forall a b c x:R, a = b -> b = c -> (a*a)%R = (c*c)%R.
+nsatz.
+Qed.
 
 Section Examples.
 
@@ -16,12 +86,12 @@ Lemma example1 : forall x y,
   x*y=0 ->
   x^2=0.
 Proof.
- nsatzR.
+ nsatz.
 Qed.
 
 Lemma example2 : forall x, x^2=0 -> x=0.
 Proof.
- nsatzR.
+ nsatz.
 Qed.
 
 (*
@@ -29,12 +99,12 @@ Notation X  := (PEX Z 3).
 Notation Y  := (PEX Z 2).
 Notation Z_ := (PEX Z 1).
 *)
-Lemma example3 : forall x y z,
+Lemma example3b : forall x y z,
   x+y+z=0 ->
   x*y+x*z+y*z=0->
   x*y*z=0 -> x^3=0.
 Proof.
-Time nsatzR.
+Time nsatz. 
 Qed.
 
 (*
@@ -43,13 +113,13 @@ Notation Y  := (PEX Z 3).
 Notation Z_ := (PEX Z 2).
 Notation U  := (PEX Z 1).
 *)
-Lemma example4 : forall x y z u,
+Lemma example4b : 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 nsatzR.
+Time nsatz.
 Qed.
 
 (*
@@ -64,20 +134,20 @@ Notation "x :: y" := (List.app x y)
 (at level 60, right associativity, format "x :: y").
 *)
 
-Lemma example5 : forall x y z u v,
+Lemma example5b : 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 nsatzR.
+Time nsatz.
 Qed.
 
 End Examples.
 
 Section Geometry.
-Require Export Reals NsatzR.
+
 Open Scope R_scope.
 
 Record point:Type:={
@@ -169,6 +239,7 @@ Ltac geo_begin:=
 
 (* Examples *)
 
+
 Lemma Thales: forall O A B C D:point,
   collinear O A C -> collinear O B D ->
   parallel A B C D ->
@@ -176,26 +247,7 @@ Lemma Thales: forall O A B C D:point,
   /\ distance2 O B * distance2 C D = distance2 O D * distance2 A B)
  \/ collinear O A B.
 repeat geo_begin.
-(*
 Time nsatz.
-*)
-Time nsatz without sugar.
-(*
-Time nsatz with lexico sugar.
-Time nsatz with lexico.
-*)
-(*
-Time nsatzRpv 1%N 1%Z (@nil R) (@nil R). (* revlex, sugar, no div *)
-(*Finished transaction in 1. secs (0.479927u,0.s)*)
-Time nsatzRpv 1%N 0%Z (@nil R) (@nil R). (* revlex, no sugar, no div *)
-(*Finished transaction in 0. secs (0.543917u,0.s)*)
-Time nsatzRpv 1%N 2%Z (@nil R) (@nil R). (* lex, no sugar, no div *)
-(*Finished transaction in 0. secs (0.586911u,0.s)*)
-Time nsatzRpv 1%N 3%Z (@nil R) (@nil R). (* lex, sugar, no div *)
-(*Finished transaction in 0. secs (0.481927u,0.s)*)
-Time nsatzRpv 1%N 5%Z (@nil R) (@nil R). (* revlex, sugar, div *)
-(*Finished transaction in 1. secs (0.601909u,0.s)*)
-*)
 Time nsatz.
 Qed.
 
@@ -209,8 +261,26 @@ Lemma hauteurs:forall A B C A1 B1 C1 H:point,
   \/ collinear A B C.
 
 geo_begin.
-Time nsatz.
-(*Finished transaction in 3. secs (2.43263u,0.010998s)*)
+ 
+(* Time nsatzRpv 2%N 1%Z (@nil R) (@nil R).*)
+(*Finished transaction in 3. secs (2.363641u,0.s)*)
+(*Time nsatz_domainR. trop long! *)
+Time 
+ let lv := constr:(Y A1
+ :: X A1
+    :: Y B1
+       :: X B1
+          :: Y A0
+             :: Y B
+                :: X B
+                   :: X A0
+                      :: X H
+                         :: Y C
+                            :: Y C1 :: Y H :: X C1 :: X C :: (@Datatypes.nil R)) in
+ nsatz_domainpv ltac:pretacR 2%N 1%Z (@Datatypes.nil R) lv ltac:simplR Rdi;
+  discrR.
+(* Finished transaction in 6. secs (5.579152u,0.001s) *)
 Qed.
 
 End Geometry.
+
diff --git a/test-suite/success/Nsatz_domain.v b/test-suite/success/Nsatz_domain.v
deleted file mode 100644
index dd190e3b8..000000000
--- a/test-suite/success/Nsatz_domain.v
+++ /dev/null
@@ -1,286 +0,0 @@
-Require Import Nsatz_domain ZArith Reals List Ring_polynom.
-
-(* Example with a generic domain *)
-
-Variable A: Type.
-Variable Ad: Domain A.
-
-Definition Ari : Ring A:= (@domain_ring A Ad).
-Existing Instance Ari.
-
-Existing Instance ring_setoid.
-Existing Instance ring_plus_comp.
-Existing Instance ring_mult_comp.
-Existing Instance ring_sub_comp.
-Existing Instance ring_opp_comp.
-
-Add Ring Ar: (@ring_ring A (@domain_ring A Ad)).
-
-Instance zero_ring2 : Zero A := {zero := ring0}.
-Instance one_ring2 : One A := {one := ring1}.
-Instance addition_ring2 : Addition A := {addition x y := ring_plus x y}.
-Instance multiplication_ring2 : Multiplication A := {multiplication x y := ring_mult x y}.
-Instance subtraction_ring2 : Subtraction A := {subtraction x y := ring_sub x y}.
-Instance opposite_ring2 : Opposite A := {opposite x := ring_opp x}.
-
-Infix "==" := ring_eq (at level 70, no associativity).
-
-Ltac nsatzA := simpl; unfold Ari; nsatz_domain.
-
-Goal forall x y:A,  x == y -> x+0 == y*1+0.
-nsatzA.
-Qed.
-
-Lemma example3 : forall x y z,
-  x+y+z==0 ->
-  x*y+x*z+y*z==0->
-  x*y*z==0 -> x*x*x==0.
-Proof.
-Time nsatzA. 
-Admitted.
-
-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*x*x*x==0.
-Proof.
-Time nsatzA.
-Qed.
-
-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*x*x*x*x ==0.
-Proof.
-Time nsatzA.
-Qed.
-
-Goal forall x y:Z,  x = y -> (x+0)%Z = (y*1+0)%Z.
-nsatz.
-Qed.
-
-Goal forall x y:R,  x = y -> (x+0)%R = (y*1+0)%R.
-nsatz.
-Qed.
-
-Goal forall a b c x:R, a = b -> b = c -> (a*a)%R = (c*c)%R.
-nsatz.
-Qed.
-
-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.
- nsatz.
-Qed.
-
-Lemma example2 : forall x, x^2=0 -> x=0.
-Proof.
- nsatz.
-Qed.
-
-(*
-Notation X  := (PEX Z 3).
-Notation Y  := (PEX Z 2).
-Notation Z_ := (PEX Z 1).
-*)
-Lemma example3b : forall x y z,
-  x+y+z=0 ->
-  x*y+x*z+y*z=0->
-  x*y*z=0 -> x^3=0.
-Proof.
-Time nsatz. 
-Qed.
-
-(*
-Notation X  := (PEX Z 4).
-Notation Y  := (PEX Z 3).
-Notation Z_ := (PEX Z 2).
-Notation U  := (PEX Z 1).
-*)
-Lemma example4b : 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 nsatz.
-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 example5b : 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 nsatz.
-Qed.
-
-End Examples.
-
-Section Geometry.
-
-Open Scope R_scope.
-
-Record point:Type:={
- X:R;
- Y:R}.
-
-Definition collinear(A B C:point):=
-  (X A - X B)*(Y C - Y B)-(Y A - Y B)*(X C - X B)=0.
-
-Definition parallel (A B C D:point):=
-  ((X A)-(X B))*((Y C)-(Y D))=((Y A)-(Y B))*((X C)-(X D)).
-
-Definition notparallel (A B C D:point)(x:R):=
-  x*(((X A)-(X B))*((Y C)-(Y D))-((Y A)-(Y B))*((X C)-(X D)))=1.
-
-Definition orthogonal (A B C D:point):=
-  ((X A)-(X B))*((X C)-(X D))+((Y A)-(Y B))*((Y C)-(Y D))=0.
-
-Definition equal2(A B:point):=
-  (X A)=(X B) /\ (Y A)=(Y B).
-
-Definition equal3(A B:point):=
-  ((X A)-(X B))^2+((Y A)-(Y B))^2 = 0.
-
-Definition nequal2(A B:point):=
-  (X A)<>(X B) \/ (Y A)<>(Y B).
-
-Definition nequal3(A B:point):=
-  not (((X A)-(X B))^2+((Y A)-(Y B))^2 = 0).
-
-Definition middle(A B I:point):=
-  2*(X I)=(X A)+(X B) /\ 2*(Y I)=(Y A)+(Y B).
-
-Definition distance2(A B:point):=
-  (X B - X A)^2 + (Y B - Y A)^2.
-
-(* AB = CD *)
-Definition samedistance2(A B C D:point):=
-  (X B - X A)^2 + (Y B - Y A)^2 = (X D - X C)^2 + (Y D - Y C)^2.
-Definition determinant(A O B:point):=
-  (X A - X O)*(Y B - Y O) - (Y A - Y O)*(X B - X O).
-Definition scalarproduct(A O B:point):=
-  (X A - X O)*(X B - X O) + (Y A - Y O)*(Y B - Y O).
-Definition norm2(A O B:point):=
-  ((X A - X O)^2+(Y A - Y O)^2)*((X B - X O)^2+(Y B - Y O)^2).
-
-
-Lemma a1:forall A B C:Prop, ((A\/B)/\(A\/C)) -> (A\/(B/\C)).
-intuition.
-Qed.
- 
-Lemma a2:forall A B C:Prop, ((A\/C)/\(B\/C)) -> ((A/\B)\/C).
-intuition.
-Qed.
-
-Lemma a3:forall a b c d:R, (a-b)*(c-d)=0 -> (a=b \/ c=d).
-intros.
-assert ( (a-b = 0) \/ (c-d = 0)).
-apply Rmult_integral.
-trivial.
-destruct H0.
-left; nsatz.
-right; nsatz.
-Qed.
-
-Ltac geo_unfold :=
-  unfold collinear; unfold parallel; unfold notparallel; unfold orthogonal;
-  unfold equal2; unfold equal3; unfold nequal2; unfold nequal3; 
-  unfold middle; unfold samedistance2; 
-  unfold determinant; unfold scalarproduct; unfold norm2; unfold distance2.
-
-Ltac geo_end :=
-  repeat (
-  repeat (match goal with h:_/\_ |- _ => decompose [and] h; clear h end);
-  repeat (apply a1 || apply a2 || apply a3);
-  repeat split).
-
-Ltac geo_rewrite_hyps:=
-  repeat (match goal with
-           | h:X _ = _ |- _ => rewrite h in *; clear h
-           | h:Y _ = _ |- _ => rewrite h in *; clear h
-          end).
-
-Ltac geo_begin:=
-  geo_unfold;
-  intros;
-  geo_rewrite_hyps;
-  geo_end.
-
-(* Examples *)
-
-
-Lemma Thales: forall O A B C D:point,
-  collinear O A C -> collinear O B D ->
-  parallel A B C D ->
-  (distance2 O B * distance2 O C = distance2 O D * distance2 O A
-  /\ distance2 O B * distance2 C D = distance2 O D * distance2 A B)
- \/ collinear O A B.
-repeat geo_begin.
-Time nsatz.
-Time nsatz.
-Qed.
-
-Lemma hauteurs:forall A B C A1 B1 C1 H:point,
-  collinear B C A1 ->  orthogonal A A1 B C ->
-  collinear A C B1 -> orthogonal B B1 A C -> 
-  collinear A B C1 -> orthogonal C C1 A B ->
-  collinear A A1 H -> collinear B B1 H -> 
-  
-  collinear C C1 H
-  \/ collinear A B C.
-
-geo_begin.
- 
-(* Time nsatzRpv 2%N 1%Z (@nil R) (@nil R).*)
-(*Finished transaction in 3. secs (2.363641u,0.s)*)
-(*Time nsatz_domainR. trop long! *)
-Time 
- let lv := constr:(Y A1
- :: X A1
-    :: Y B1
-       :: X B1
-          :: Y A0
-             :: Y B
-                :: X B
-                   :: X A0
-                      :: X H
-                         :: Y C
-                            :: Y C1 :: Y H :: X C1 :: X C :: (@Datatypes.nil R)) in
- nsatz_domainpv ltac:pretacR 2%N 1%Z (@Datatypes.nil R) lv ltac:simplR Rdi;
-  discrR.
-(* Finished transaction in 6. secs (5.579152u,0.001s) *)
-Qed.
-
-End Geometry.
-