Commit 559ae77d authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp/doc] Document induction tactic

parent 3aa99b84
......@@ -444,6 +444,18 @@ n|k, n|k', & (k/n).a = (k'/n).b &\Longleftrightarrow& k.a = k'.b
\end{array}
\]
\paragraph{Induction} Start a proof by integer induction \\
The user select any integer expression $e$ in the proof and a base value $b$ (which defaults to
0). The tactic generates a proof by strong (integer) induction on $e$, that is, the base case
$e = b$ and then the cases $e < b$ and $b < e$. Formally:
\[\TACTIC{\Delta\models\,G}{%
\begin{array}[t]{llll}
\Delta, & G[e \leftarrow n], & n = b & \models G[e \leftarrow n] \\
\Delta, & G[e \leftarrow i], & b \leq i < n & \models G[e \leftarrow n] \\
\Delta, & G[e \leftarrow i], & n < i \leq b & \models G[e \leftarrow n]
\end{array}} \]
\paragraph{Overflow} Integer Conversions \\
This tactic rewrites machine integer conversions by identity,
providing the converted value is in available range. The tactic applies on expression
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment