From 559ae77d0ba993645fda7112dbeec23a4c7aa452 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 4 Nov 2020 16:06:43 +0100
Subject: [PATCH] [wp/doc] Document induction tactic
---
src/plugins/wp/doc/manual/wp_plugin.tex | 12 ++++++++++++
1 file changed, 12 insertions(+)
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 26be616ced4..9a818d72011 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -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
--
GitLab