git.iko.soy/Idris-dev
on master help sign in
Merge pull request #519 from reynir/master

Update tutorial

commitb3976923298358a98269a0af00b6d41a9497ab64 authorEdwin Brady <edwin.brady@gmail.com> dateMon 7 Oct 2013, 00:41 (13 years ago) parent0d5c5b6d861727
3 files changed+43−14
compare with master
unifiedsplit
tutorial/miscellany.tex+3−3 tutorial/provisional.tex+18−3 tutorial/theorems.tex+22−8
tutorial/miscellany.tex+3−3
@@ -224,11 +224,11 @@ Often this will require extra libraries to be linked in, or extra header and obj
224224This is made possible through the following directives:
225225
226226\begin{itemize}
227−\item \texttt{\%lib target "x"} --- include the \texttt{libx} library. If the target is \texttt{C} this is equivalent to passing the
227+\item \texttt{\%lib \emph{target} "x"} --- include the \texttt{libx} library. If the target is \texttt{C} this is equivalent to passing the
228228\texttt{-lx} option to \texttt{gcc}. If the target is Java the library will be interpreted as a
229229"groupId:artifactId:packaging:version" dependency coordinate for maven.
230−\item \texttt{\%include target "x"} --- use the header file or import \texttt{x} for the given back end target.
231−\item \texttt{\%link target "x.o"} --- link with the object file \texttt{x.o} when using the given back end target.
230+\item \texttt{\%include \emph{target} "x"} --- use the header file or import \texttt{x} for the given back end target.
231+\item \texttt{\%link \emph{target} "x.o"} --- link with the object file \texttt{x.o} when using the given back end target.
232232\item \texttt{\%dynamic "x.so"} --- dynamically link the interpreter with the shared object \texttt{x.so}.
233233\end{itemize}
234234
tutorial/provisional.tex+18−3
@@ -109,7 +109,7 @@ The first of these has the following type:
109109*views> :p views.parity_lemma_1
110110
111111---------------------------------- (views.parity_lemma_1) --------
112−{hole0} : (j : Nat) -> (Parity (plus (S j) (S j))) -> Parity (S (S (plus j j)))
112+{hole0} : (j : Nat) -> (Parity (plus (S j) (S j))) -> Parity (S (S (j + j)))
113113
114114-views.parity_lemma_1>
115115
@@ -127,7 +127,7 @@ the prelude:
127127\begin{SaveVerbatim}{plusnsm}
128128
129129plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
130− S (plus left right) = plus left (S right)
130+ S (left + right) = left + (S right)
131131
132132
133133\end{SaveVerbatim}
@@ -143,11 +143,26 @@ After applying \texttt{intro} twice, we have:
143143 j : Nat
144144 value : Parity (S (plus j (S j)))
145145---------------------------------- (views.parity_lemma_1) --------
146−{hole2} : Parity (S (S (plus j j)))
146+{hole2} : Parity (S (S (j + j)))
147147
148148\end{SaveVerbatim}
149149\useverb{prolemii}
150150
151+\noindent
152+We need to use \texttt{compute} again to unfold the definition of \texttt{(+)}.
153+
154+\begin{SaveVerbatim}{prolemcomp}
155+
156+-views.parity_lemma_1> intro
157+
158+ j : Nat
159+ value : Parity (S (plus j (S j)))
160+---------------------------------- (views.parity_lemma_1) --------
161+{hole2} : Parity (S (S (plus j j)))
162+
163+\end{SaveVerbatim}
164+\useverb{prolemcomp}
165+
151166\noindent
152167Then we apply the \texttt{plusSuccRightSucc} rewrite rule, symmetrically,
153168to \texttt{j} and \texttt{j}, giving:
tutorial/theorems.tex+22−8
@@ -163,8 +163,8 @@ plusReducesZ' (S k) = let ih = plusReducesZ' k in
163163\useverb{prOstruct}
164164
165165\noindent
166−On running \Idris{}, two global names are created, \texttt{plusredO\_O} and
167−\texttt{plusredO\_S}, with no definition. We can use the \texttt{:m} command
166+On running \Idris{}, two global names are created, \texttt{plusredZ\_O} and
167+\texttt{plusredZ\_S}, with no definition. We can use the \texttt{:m} command
168168at the prompt to find out which metavariables are still to be solved (or, more
169169precisely, which functions exist but have no definitions), then the
170170\texttt{:t} command to see their types:
@@ -183,7 +183,7 @@ Global metavariables:
183183plusredZ_Z : Z = plus Z Z
184184
185185*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
187187
188188\end{SaveVerbatim}
189189\useverb{showmetas}
@@ -265,17 +265,17 @@ Global metavariables:
265265\noindent
266266The \texttt{:addproof} command, at the interactive prompt, will add the proof to
267267the 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}:
269269
270−\begin{SaveVerbatim}{plusredOSprf}
270+\begin{SaveVerbatim}{plusredZSprf}
271271
272272*theorems> :p plusredZ_S
273273
274274---------------------------------- (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
276276
277277\end{SaveVerbatim}
278−\useverb{plusredOSprf}
278+\useverb{plusredZSprf}
279279
280280\noindent
281281In 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
288288 k : Nat
289289 ih : k = plus k Z
290290---------------------------------- (plusredZ_S) --------
291−{hole2} : S k = S (plus k Z)
291+{hole2} : S k = plus (S k) Z
292292
293293\end{SaveVerbatim}
294294\useverb{prSintros}
295295
296+\noindent
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
299+\texttt{compute}.
300+
301+\begin{SaveVerbatim}{prScompute}
302+ k : Nat
303+ ih : k = plus k Z
304+---------------------------------- (plusredZ_S) --------
305+{hole2} : S k = S (plus k Z)
306+
307+\end{SaveVerbatim}
308+\useverb{prScompute}
309+
296310\noindent
297311We know, from the type of \texttt{ih}, that \texttt{k = plus k Z}, so we would like to
298312use this knowledge to replace \texttt{plus k Z} in the goal with \texttt{k}. We can