From 95527a924d8f211d18cc965d4c8eab7c26124451 Mon Sep 17 00:00:00 2001 From: thery Date: Tue, 6 Feb 2007 17:24:12 +0000 Subject: doc for field git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9596 85f007b7-540e-0410-9357-904b9bb8a0f7 --- doc/refman/Polynom.tex | 122 ++++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 116 insertions(+), 6 deletions(-) diff --git a/doc/refman/Polynom.tex b/doc/refman/Polynom.tex index e81a0e964..2679acba0 100644 --- a/doc/refman/Polynom.tex +++ b/doc/refman/Polynom.tex @@ -159,7 +159,7 @@ Reset Initial. where $m$ is a monomial (after ``abstraction''), $p$ a polynomial and $=$ the corresponding equality of the ring structure. - \item {\tt ring\_simplify [\term$_1$ {\ldots} \term$_n$] $t_1 \ldots t_n$ in + \item {\tt ring\_simplify [\term$_1$ {\ldots} \term$_n$] $t_1 \ldots t_m$ in {\ident}} performs the simplification in the hypothesis named {\tt ident}. \end{Variants} @@ -337,9 +337,17 @@ describes their syntax and effects: {\tt contrib/setoid\_ring/RealField.v} for examples. By default the tactic does not recognize power expressions as ring expressions. -\item[sign {\term}] -\item[div {\term}] - +\item[sign {\term}] allows {\tt ring\_simplify} to use a minus operation + when outputing its normal form, i.e writing $x - y$ instead of $x + (-y)$. + The term {\term} is a proof that a given sign function indicates expressions + that are signed ({\term} has to be a + proof of {\tt Ring\_theory.get\_sign}). See {\tt contrib/setoid\_ring/IntialRing.v} for examples of sign function. +\item[div {\term}] allows {\tt ring} and {\tt ring\_simplify} to use moniomals +with coefficient other than 1 in the rewriting. The term {\term} is a proof that a given division function satisfies the specification of an euclidean + division function ({\term} has to be a + proof of {\tt Ring\_theory.div\_theory}). For example, this function is + called when trying to rewrite $7x$ by $2x = z$ to tell that $7 = 3 * 2 + 1$. + See {\tt contrib/setoid\_ring/IntialRing.v} for examples of div function. \end{description} @@ -457,10 +465,112 @@ correctness theorem to well-chosen arguments. \tacindex{field\_simplify} \tacindex{field\_simplify\_eq}} + +The {\tt field} tactic is an extension of the {\tt ring} to deal with +rational expresision. Given a rational expression $F=0$. It first reduces the expression $F$ to a common denominator $N/D= 0$ where $N$ and $D$ are two ring +expressions. +For example, if we take $F = (1 - 1/x) x - x + 1$, this gives +$ N= (x -1) x - x^2 + x$ and $D= x$. It then calls {\tt ring} +to solve $N=0$. Note that {\tt field} also generates non-zero conditions +for all the denominators it encounters in the reduction. +In our example, it generates the condition $x \neq 0$. +Non-zero conditions are {\it always} polynomial expressions. For example +when reducing the expression $1/(1 + 1/x)$, two side conditions are +generated: $x\neq 0$ and $x + 1 \neq 0$. % - Faire Require Import Field... % - RealField % - +The tactic must be loaded by \texttt{Require Import Field}. The field +structures must be declared with the \texttt{Add Field} command (see +below). The fiel of reals is predefined; if one wants to use the +tactic on \texttt{R} one must first require the module +\texttt{RealField} (exported by \texttt{Reals}). + +\Example +\begin{coq_eval} +Reset Initial. +\end{coq_eval} +\begin{coq_example} +Require Import Reals. +Open Scope R_scope. +Goal forall x, x <> 0 -> + (1 - 1/x) * x - x + 1 = 0. +\end{coq_example} +\begin{coq_example} +intros; field; auto. +\end{coq_example} +\begin{coq_eval} +Abort. +\end{coq_eval} +\begin{coq_example} +Goal forall x y, y <> 0 -> y = x -> x/y = 1. +\end{coq_example} +\begin{coq_example} +intros x y H H1; field [H1]; auto. +\end{coq_example} +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + +\begin{Variants} + \item {\tt field [\term$_1$ {\ldots} \term$_n$]} decides the equality of two + terms modulo field operations and rewriting of the equalities + defined by \term$_1$ {\ldots} \term$_n$. Each of \term$_1$ + {\ldots} \term$_n$ has to be a proof of some equality $m = p$, + where $m$ is a monomial (after ``abstraction''), + $p$ a polynomial and $=$ the corresponding equality of the field structure. + + \item {\tt field\_simplify} + performs the simplification in the conclusion of the goal, $F_1 = F_2$ + becomes $N_1/D_1 = N_2/D_2$. + + \item {\tt field\_simplify [\term$_1$ {\ldots} \term$_n$]} + performs the simplification in the conclusion of the goal using + the equalities + defined by \term$_1$ {\ldots} \term$_n$. + + \item {\tt field\_simplify [\term$_1$ {\ldots} \term$_n$] $t_1$ \ldots +$t_m$} + performs the simplification in the terms $t_1$ \ldots $t_m$ + of the conclusion of the goal using + the equalities + defined by \term$_1$ {\ldots} \term$_n$. + + \item {\tt field\_simplify in $H$} + performs the simplification in the assumption $H$. + + \item {\tt field\_simplify [\term$_1$ {\ldots} \term$_n$] in $H$} + performs the simplification in the assumption $H$ using + the equalities + defined by \term$_1$ {\ldots} \term$_n$. + + \item {\tt field\_simplify [\term$_1$ {\ldots} \term$_n$] $t_1$ \ldots +$t_m$ in $H$} + performs the simplification in the terms $t_1$ \ldots $t_n$ + of the assumption $H$ using + the equalities + defined by \term$_1$ {\ldots} \term$_m$. + + \item {\tt field\_simplify\_eq} + performs the simplification in the conclusion of the goal removing + the denominator. $F_1 = F_2$ + becomes $N_1 D_2 = N_2 D_1$. + + \item {\tt field\_simplify\_eq [\term$_1$ {\ldots} \term$_n$]} + performs the simplification in the conclusion of the goal using + the equalities + defined by \term$_1$ {\ldots} \term$_n$. + + \item {\tt field\_simplify\_eq} in $H$ + performs the simplification in the assumption $H$. + + \item {\tt field\_simplify\_eq [\term$_1$ {\ldots} \term$_n$] in $H$} + performs the simplification in the assumption $H$ using + the equalities + defined by \term$_1$ {\ldots} \term$_n$. +\end{Variants} + \asection{Adding a new field structure \comindex{Add Field}} @@ -515,9 +625,9 @@ apply. There is only one specific modifier: on coefficients w.r.t. the field equality. \end{description} -{\tt field_simplify_eq} +{\tt field\_simplify\_eq} -{\tt field_simplify} +{\tt field\_simplify} \asection{Legacy implementation} -- cgit v1.2.3