pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-12-01 00:26:18 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Clarify what linear_arithmetic does these days

Browse source
This commit is contained in:
Adam Chlipala 2020-03-17 15:50:19 -04:00
parent 72c0bc3a04
commit b5e1ae0c29
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
frap_book.tex
View file

@ -5506,7 +5506,7 @@ Note that many of these are specific to the \texttt{Frap} library distributed wi
\item[\texttt{f\_equal}] When the goal is an equality between two applications of the same function, switch to proving that the function arguments are pairwise equal. \item[\texttt{f\_equal}] When the goal is an equality between two applications of the same function, switch to proving that the function arguments are pairwise equal.
\item[\texttt{induct} $x$] Where $x$ is a variable in the theorem statement, structure the proof by induction on the structure of $x$. You will get one generated subgoal per constructor in the inductive definition of $x$. (Indeed, it is required that $x$'s type was introduced with \texttt{Inductive}.) \item[\texttt{induct} $x$] Where $x$ is a variable in the theorem statement, structure the proof by induction on the structure of $x$. You will get one generated subgoal per constructor in the inductive definition of $x$. (Indeed, it is required that $x$'s type was introduced with \texttt{Inductive}.)
\item[\texttt{invert} $H$] Replace hypothesis $H$ with other facts that can be deduced from the structure of $H$'s statement. More detail to be added here soon! \item[\texttt{invert} $H$] Replace hypothesis $H$ with other facts that can be deduced from the structure of $H$'s statement. More detail to be added here soon!
\item[\texttt{linear\_arithmetic}] A complete decision procedure for linear arithmetic. Relevant formulas are essentially those built up from variables and constant natural numbers and integers using only addition and subtraction, with equality and inequality comparisons on top. (Multiplication by constants is supported, as a shorthand for repeated addition.) See Section \ref{decidable}. \item[\texttt{linear\_arithmetic}] A complete decision procedure for linear arithmetic. Relevant formulas are essentially those built up from variables and constant natural numbers and integers using only addition and subtraction, with equality and inequality comparisons on top. (Multiplication by constants is supported, as a shorthand for repeated addition.) See Section \ref{decidable}. Also note that this tactic goes a bit beyond that theory, by (1) converting multivariable terms into a standard polynomial form and then (2) treating each different product of powers of variables as one variable in a linear-arithmetic problem. So, for instance, \texttt{linear\_arithmetic} can prove $x \times y = y \times x$ simply by deciding that a new variable $z = x \times y$, rewriting the goal to $z = z$ after putting polynomials in canonical form (in this case, commuting argument order in products to make it consistent).
\item[\texttt{left}] Prove a disjunction by proving its left side. \item[\texttt{left}] Prove a disjunction by proving its left side.
\item[\texttt{maps\_equal}] Prove that two finite maps are equal by considering all the relevant cases for mappings of different keys. \item[\texttt{maps\_equal}] Prove that two finite maps are equal by considering all the relevant cases for mappings of different keys.
\item[\texttt{propositional}] Simplify a goal into zero or more new goals, based on the rules of propositional logic alone. \item[\texttt{propositional}] Simplify a goal into zero or more new goals, based on the rules of propositional logic alone.