From 729c4847ef3736829727948cd2c542149432970d Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 22 Mar 2018 15:09:00 +0100 Subject: [Sphinx] Move chapter 26 to new infrastructure --- Makefile.doc | 2 +- doc/refman/Nsatz.tex | 102 ---------------------------------------- doc/refman/Reference-Manual.tex | 1 - doc/sphinx/addendum/nsatz.rst | 102 ++++++++++++++++++++++++++++++++++++++++ 4 files changed, 103 insertions(+), 104 deletions(-) delete mode 100644 doc/refman/Nsatz.tex create mode 100644 doc/sphinx/addendum/nsatz.rst diff --git a/Makefile.doc b/Makefile.doc index 8a3d3a307..08b4cb7fb 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -60,7 +60,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ RefMan-gal.v.tex \ RefMan-oth.v.tex RefMan-ltac.v.tex \ RefMan-pro.v.tex \ - Polynom.v.tex Nsatz.v.tex \ + Polynom.v.tex \ Setoid.v.tex Universes.v.tex \ Misc.v.tex) diff --git a/doc/refman/Nsatz.tex b/doc/refman/Nsatz.tex deleted file mode 100644 index 1401af10f..000000000 --- a/doc/refman/Nsatz.tex +++ /dev/null @@ -1,102 +0,0 @@ -\achapter{Nsatz: tactics for proving equalities in integral domains} -%HEVEA\cutname{nsatz.html} -\aauthor{Loïc Pottier} - -The tactic \texttt{nsatz} proves goals of the form - -\[ \begin{array}{l} - \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 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 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. - -\asection{Using the basic tactic \texttt{nsatz}} -\tacindex{nsatz} - -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 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$ -and $r$ such that $c (P-Q)^r = \sum_{i} S_i (P_i-Q_i)$, which will be proved by the -tactic \texttt{ring}. - -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 tactic -\texttt{nsatz}, which can be used without arguments: \\ -\vspace*{3mm} -\texttt{nsatz}\\ -or with the syntax: \\ -\vspace*{3mm} -\texttt{nsatz with radicalmax:={\em number}\%N strategy:={\em number}\%Z parameters:={\em list of variables} variables:={\em list of variables}}\\ -where: - -\begin{itemize} - \item \texttt{radicalmax} 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 -the strategy used in Buchberger algorithm (see -\cite{sugar} for details): - - \begin{itemize} - \item strategy = 0: reverse lexicographic order and newest s-polynomial. - \item strategy = 1: reverse lexicographic order and sugar strategy. - \item strategy = 2: pure lexicographic order and newest s-polynomial. - \item strategy = 3: pure lexicographic order and sugar strategy. - \end{itemize} - - \item \texttt{parameters} is the list of variables -$X_{i_1},\ldots,X_{i_k}$ among $X_1,...,X_n$ which are considered as - parameters: computation will be performed with rational fractions in these - variables, i.e. polynomials are considered with coefficients in -$R(X_{i_1},\ldots,X_{i_k})$. In this case, the coefficient $c$ can be a non -constant polynomial in $X_{i_1},\ldots,X_{i_k}$, and the tactic produces a goal -which states that $c$ is not zero. - - \item \texttt{variables} is the list of the variables -in the decreasing order in which they will be used in Buchberger algorithm. If \texttt{variables} = {(@nil -R)}, then \texttt{lvar} is replaced by all the variables which are not in -parameters. - -\end{itemize} - -See file \texttt{Nsatz.v} for many examples, specially in geometry. - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index a652a121c..13c3c0aac 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -118,7 +118,6 @@ Options A and B of the licence are {\em not} elected.} \part{Addendum to the Reference Manual} \include{AddRefMan-pre}% \include{Polynom.v}% = Ring -\include{Nsatz.v}% \include{Setoid.v}% Tactique pour les setoides \include{AsyncProofs}% Paral-ITP \include{Universes.v}% Universe polymorphes diff --git a/doc/sphinx/addendum/nsatz.rst b/doc/sphinx/addendum/nsatz.rst new file mode 100644 index 000000000..1401af10f --- /dev/null +++ b/doc/sphinx/addendum/nsatz.rst @@ -0,0 +1,102 @@ +\achapter{Nsatz: tactics for proving equalities in integral domains} +%HEVEA\cutname{nsatz.html} +\aauthor{Loïc Pottier} + +The tactic \texttt{nsatz} proves goals of the form + +\[ \begin{array}{l} + \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 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 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. + +\asection{Using the basic tactic \texttt{nsatz}} +\tacindex{nsatz} + +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 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$ +and $r$ such that $c (P-Q)^r = \sum_{i} S_i (P_i-Q_i)$, which will be proved by the +tactic \texttt{ring}. + +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 tactic +\texttt{nsatz}, which can be used without arguments: \\ +\vspace*{3mm} +\texttt{nsatz}\\ +or with the syntax: \\ +\vspace*{3mm} +\texttt{nsatz with radicalmax:={\em number}\%N strategy:={\em number}\%Z parameters:={\em list of variables} variables:={\em list of variables}}\\ +where: + +\begin{itemize} + \item \texttt{radicalmax} 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 +the strategy used in Buchberger algorithm (see +\cite{sugar} for details): + + \begin{itemize} + \item strategy = 0: reverse lexicographic order and newest s-polynomial. + \item strategy = 1: reverse lexicographic order and sugar strategy. + \item strategy = 2: pure lexicographic order and newest s-polynomial. + \item strategy = 3: pure lexicographic order and sugar strategy. + \end{itemize} + + \item \texttt{parameters} is the list of variables +$X_{i_1},\ldots,X_{i_k}$ among $X_1,...,X_n$ which are considered as + parameters: computation will be performed with rational fractions in these + variables, i.e. polynomials are considered with coefficients in +$R(X_{i_1},\ldots,X_{i_k})$. In this case, the coefficient $c$ can be a non +constant polynomial in $X_{i_1},\ldots,X_{i_k}$, and the tactic produces a goal +which states that $c$ is not zero. + + \item \texttt{variables} is the list of the variables +in the decreasing order in which they will be used in Buchberger algorithm. If \texttt{variables} = {(@nil +R)}, then \texttt{lvar} is replaced by all the variables which are not in +parameters. + +\end{itemize} + +See file \texttt{Nsatz.v} for many examples, specially in geometry. + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "Reference-Manual" +%%% End: -- cgit v1.2.3 From beef18502c3848609cda96b90a47777fa8a52e99 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 22 Mar 2018 15:10:16 +0100 Subject: [Sphinx] Add chapter 26 Thanks to Paul Steckler for porting this chapter. --- doc/sphinx/addendum/nsatz.rst | 195 +++++++++++++++++++++--------------------- doc/sphinx/index.rst | 1 + 2 files changed, 98 insertions(+), 98 deletions(-) diff --git a/doc/sphinx/addendum/nsatz.rst b/doc/sphinx/addendum/nsatz.rst index 1401af10f..ef9b3505d 100644 --- a/doc/sphinx/addendum/nsatz.rst +++ b/doc/sphinx/addendum/nsatz.rst @@ -1,102 +1,101 @@ -\achapter{Nsatz: tactics for proving equalities in integral domains} -%HEVEA\cutname{nsatz.html} -\aauthor{Loïc Pottier} - -The tactic \texttt{nsatz} proves goals of the form - -\[ \begin{array}{l} - \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 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. +.. include:: ../preamble.rst + +.. _nsatz: + +Nsatz: tactics for proving equalities in integral domains +=========================================================== + +:Author: Loïc Pottier + +The tactic `nsatz` proves goals of the form + +:math:`\begin{array}{l} +\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 :math:`P, Q, P₁,Q₁,\ldots,Pₛ, Qₛ` are polynomials and :math:`A` is an integral +domain, i.e. a commutative ring with no zero divisor. For example, :math:`A` +can be :math:`\mathbb{R}`, :math:`\mathbb{Z}`, or :math:`\mathbb{Q}`. +Note that the equality :math:`=` used in these goals can be +any setoid equality (see :ref:`TODO-27.2.2`) , not only Leibnitz equality. It also proves formulas -\[ \begin{array}{l} - \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. - -\asection{Using the basic tactic \texttt{nsatz}} -\tacindex{nsatz} - -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 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$ -and $r$ such that $c (P-Q)^r = \sum_{i} S_i (P_i-Q_i)$, which will be proved by the -tactic \texttt{ring}. - -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 tactic -\texttt{nsatz}, which can be used without arguments: \\ -\vspace*{3mm} -\texttt{nsatz}\\ -or with the syntax: \\ -\vspace*{3mm} -\texttt{nsatz with radicalmax:={\em number}\%N strategy:={\em number}\%Z parameters:={\em list of variables} variables:={\em list of variables}}\\ + +:math:`\begin{array}{l} +\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. + + +Using the basic tactic `nsatz` +------------------------------ + + +Load the Nsatz module: + +.. coqtop:: all + + Require Import Nsatz. + +and use the tactic `nsatz`. + +More about `nsatz` +--------------------- + +Hilbert’s Nullstellensatz theorem shows how to reduce proofs of +equalities on polynomials on a commutative ring :math:`A` with no zero divisor +to algebraic computations: it is easy to see that if a polynomial :math:`P` in +:math:`A[X_1,\ldots,X_n]` verifies :math:`c P^r = \sum_{i=1}^{s} S_i P_i`, with +:math:`c \in A`, :math:`c \not = 0`, +:math:`r` a positive integer, and the :math:`S_i` s in :math:`A[X_1,\ldots,X_n ]`, +then :math:`P` is zero whenever polynomials :math:`P_1,\ldots,P_s` are zero +(the converse is also true when :math:`A` is an algebraic closed field: the method is +complete). + +So, proving our initial problem can reduce into finding :math:`S_1,\ldots,S_s`, +:math:`c` and :math:`r` such that :math:`c (P-Q)^r = \sum_{i} S_i (P_i-Q_i)`, +which will be proved by the tactic ring. + +This is achieved by the computation of a Gröbner basis of the ideal +generated by :math:`P_1-Q_1,...,P_s-Q_s`, with an adapted version of the +Buchberger algorithm. + +This computation is done after a step of *reification*, which is +performed using :ref:`typeclasses`. + +The ``Nsatz`` module defines the tactic `nsatz`, which can be used without +arguments, or with the syntax: + +| nsatz with radicalmax:=num%N strategy:=num%Z parameters:= :n:`{* var}` variables:= :n:`{* var}` + where: -\begin{itemize} - \item \texttt{radicalmax} 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 -the strategy used in Buchberger algorithm (see -\cite{sugar} for details): - - \begin{itemize} - \item strategy = 0: reverse lexicographic order and newest s-polynomial. - \item strategy = 1: reverse lexicographic order and sugar strategy. - \item strategy = 2: pure lexicographic order and newest s-polynomial. - \item strategy = 3: pure lexicographic order and sugar strategy. - \end{itemize} - - \item \texttt{parameters} is the list of variables -$X_{i_1},\ldots,X_{i_k}$ among $X_1,...,X_n$ which are considered as - parameters: computation will be performed with rational fractions in these - variables, i.e. polynomials are considered with coefficients in -$R(X_{i_1},\ldots,X_{i_k})$. In this case, the coefficient $c$ can be a non -constant polynomial in $X_{i_1},\ldots,X_{i_k}$, and the tactic produces a goal -which states that $c$ is not zero. - - \item \texttt{variables} is the list of the variables -in the decreasing order in which they will be used in Buchberger algorithm. If \texttt{variables} = {(@nil -R)}, then \texttt{lvar} is replaced by all the variables which are not in -parameters. - -\end{itemize} - -See file \texttt{Nsatz.v} for many examples, specially in geometry. - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: +* `radicalmax` is a bound when for searching r s.t. + :math:`c (P−Q) r = \sum_{i=1..s} S_i (P i − Q i)` + +* `strategy` gives the order on variables :math:`X_1,\ldots,X_n` and the strategy + used in Buchberger algorithm (see :cite:`sugar` for details): + + * strategy = 0: reverse lexicographic order and newest s-polynomial. + * strategy = 1: reverse lexicographic order and sugar strategy. + * strategy = 2: pure lexicographic order and newest s-polynomial. + * strategy = 3: pure lexicographic order and sugar strategy. + +* `parameters` is the list of variables :math:`X_{i_1},\ldots,X_{i_k}` among + :math:`X_1,\ldots,X_n` which are considered as parameters: computation will be performed with + rational fractions in these variables, i.e. polynomials are considered + with coefficients in :math:`R(X_{i_1},\ldots,X_{i_k})`. In this case, the coefficient + :math:`c` can be a non constant polynomial in :math:`X_{i_1},\ldots,X_{i_k}`, and the tactic + produces a goal which states that :math:`c` is not zero. + +* `variables` is the list of the variables in the decreasing order in + which they will be used in Buchberger algorithm. If `variables` = `(@nil R)`, + then `lvar` is replaced by all the variables which are not in + `parameters`. + +See file `Nsatz.v` for many examples, especially in geometry. diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst index 31c5e9a07..6f4b28759 100644 --- a/doc/sphinx/index.rst +++ b/doc/sphinx/index.rst @@ -51,6 +51,7 @@ Table of contents addendum/micromega addendum/extraction addendum/program + addendum/nsatz .. toctree:: :caption: Reference -- cgit v1.2.3