From 99a7d8cd75463dfc4a18fe1f8b91a5d160848ad5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Cl=C3=A9ment=20Pit--Claudel?= Date: Wed, 3 Feb 2016 18:12:06 -0500 Subject: [PATCH] Fix typo in 'arithmetic' --- frap.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/frap.tex b/frap.tex index 9ac1076..21eee28 100644 --- a/frap.tex +++ b/frap.tex @@ -508,7 +508,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{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{linear\_arithemtic}] 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}. \item[\texttt{rewrite} $H$] Where $H$ is a hypothesis or previously proved theorem, establishing \texttt{forall x1 .. xN, e1 = e2}, find a subterm of the goal that equals \texttt{e1}, given the right choices of \texttt{xi} values, and replace that subterm with \texttt{e2}. \item[\texttt{ring}] Prove goals that are equalities over some registered ring or semiring, in the sense of algebra, where the goal follows solely from the axioms of that algebraic structure. See Section \ref{decidable}. \item[\texttt{simplify}] Simplify throughout the goal, applying the definitions of recursive functions directly. That is, when a subterm matches one of the \texttt{match} cases in a defining \texttt{Fixpoint}, replace with the body of that case, then repeat.