@@ -163,8 +163,8 @@ plusReducesZ' (S k) = let ih = plusReducesZ' k in
163\useverb{prOstruct}
163\useverb{prOstruct}
166−On running \Idris{}, two global names are created, \texttt{plusredO\_O} and
166+On running \Idris{}, two global names are created, \texttt{plusredZ\_O} and
167−\texttt{plusredO\_S}, with no definition. We can use the \texttt{:m} command
167+\texttt{plusredZ\_S}, with no definition. We can use the \texttt{:m} command
168at the prompt to find out which metavariables are still to be solved (or, more
168at the prompt to find out which metavariables are still to be solved (or, more
169precisely, which functions exist but have no definitions), then the
169precisely, which functions exist but have no definitions), then the
170\texttt{:t} command to see their types:
170\texttt{:t} command to see their types:
@@ -183,7 +183,7 @@ Global metavariables:
183plusredZ_Z : Z = plus Z Z
183plusredZ_Z : Z = plus Z Z
185*theorems> :t plusredZ_S
185*theorems> :t plusredZ_S
186−plusredZ_S : (k : Nat) -> (k = plus k Z) -> S k = S (plus k Z)
186+plusredZ_S : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z
188\end{SaveVerbatim}
188\end{SaveVerbatim}
189\useverb{showmetas}
189\useverb{showmetas}
@@ -265,17 +265,17 @@ Global metavariables:
266The \texttt{:addproof} command, at the interactive prompt, will add the proof to
266The \texttt{:addproof} command, at the interactive prompt, will add the proof to
267the source file (effectively in an appendix).
267the source file (effectively in an appendix).
268−Let us now prove the other required lemma, \texttt{plusredO\_S}:
268+Let us now prove the other required lemma, \texttt{plusredZ\_S}:
270−\begin{SaveVerbatim}{plusredOSprf}
270+\begin{SaveVerbatim}{plusredZSprf}
272*theorems> :p plusredZ_S
272*theorems> :p plusredZ_S
274---------------------------------- (plusredZ_S) --------
274---------------------------------- (plusredZ_S) --------
275−{hole0} : (k : Nat) -> (k = plus k Z) -> S k = S (plus k Z)
275+{hole0} : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z
277\end{SaveVerbatim}
277\end{SaveVerbatim}
278−\useverb{plusredOSprf}
278+\useverb{plusredZSprf}
281In this case, the goal is a function type, using \texttt{k} (the argument accessible by
281In this case, the goal is a function type, using \texttt{k} (the argument accessible by
@@ -288,11 +288,25 @@ twice (or \texttt{intros}, which introduces all arguments as premisses). This gi
289 ih : k = plus k Z
289 ih : k = plus k Z
290---------------------------------- (plusredZ_S) --------
290---------------------------------- (plusredZ_S) --------
291−{hole2} : S k = S (plus k Z)
291+{hole2} : S k = plus (S k) Z
293\end{SaveVerbatim}
293\end{SaveVerbatim}
294\useverb{prSintros}
294\useverb{prSintros}
297+Since plus is defined is defined by recursion on its first argument, the term
298+\texttt{plus (S k) Z} in the goal can be simplified, so we use
301+\begin{SaveVerbatim}{prScompute}
304+---------------------------------- (plusredZ_S) --------
305+{hole2} : S k = S (plus k Z)
297We know, from the type of \texttt{ih}, that \texttt{k = plus k Z}, so we would like to
311We know, from the type of \texttt{ih}, that \texttt{k = plus k Z}, so we would like to
298use this knowledge to replace \texttt{plus k Z} in the goal with \texttt{k}. We can
312use this knowledge to replace \texttt{plus k Z} in the goal with \texttt{k}. We can