git.iko.soy/Idris-dev
on master help sign in
Merge pull request #519 from reynir/master
b397692Edwin Brady
tutorial/miscellany.tex+3−3
compare with master
unifiedsplit
@@ -224,11 +224,11 @@ Often this will require extra libraries to be linked in, or extra header and obj
224This is made possible through the following directives:
224This is made possible through the following directives:
225
225
226\begin{itemize}
226\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
228\texttt{-lx} option to \texttt{gcc}. If the target is Java the library will be interpreted as a
228\texttt{-lx} option to \texttt{gcc}. If the target is Java the library will be interpreted as a
229"groupId:artifactId:packaging:version" dependency coordinate for maven.
229"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.
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 target "x.o"} --- link with the object file \texttt{x.o} when using 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.
232\item \texttt{\%dynamic "x.so"} --- dynamically link the interpreter with the shared object \texttt{x.so}.
232\item \texttt{\%dynamic "x.so"} --- dynamically link the interpreter with the shared object \texttt{x.so}.
233\end{itemize}
233\end{itemize}
234
234
tutorial/provisional.tex+18−3
@@ -109,7 +109,7 @@ The first of these has the following type:
109*views> :p views.parity_lemma_1
109*views> :p views.parity_lemma_1
110
110
111---------------------------------- (views.parity_lemma_1) --------
111---------------------------------- (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)))
113
113
114-views.parity_lemma_1>
114-views.parity_lemma_1>
115
115
@@ -127,7 +127,7 @@ the prelude:
127\begin{SaveVerbatim}{plusnsm}
127\begin{SaveVerbatim}{plusnsm}
128
128
129plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
129plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
130− S (plus left right) = plus left (S right)
130+ S (left + right) = left + (S right)
131
131
132
132
133\end{SaveVerbatim}
133\end{SaveVerbatim}
@@ -143,11 +143,26 @@ After applying \texttt{intro} twice, we have:
143 j : Nat
143 j : Nat
144 value : Parity (S (plus j (S j)))
144 value : Parity (S (plus j (S j)))
145---------------------------------- (views.parity_lemma_1) --------
145---------------------------------- (views.parity_lemma_1) --------
146−{hole2} : Parity (S (S (plus j j)))
146+{hole2} : Parity (S (S (j + j)))
147
147
148\end{SaveVerbatim}
148\end{SaveVerbatim}
149\useverb{prolemii}
149\useverb{prolemii}
150
150
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+
151\noindent
166\noindent
152Then we apply the \texttt{plusSuccRightSucc} rewrite rule, symmetrically,
167Then we apply the \texttt{plusSuccRightSucc} rewrite rule, symmetrically,
153to \texttt{j} and \texttt{j}, giving:
168to \texttt{j} and \texttt{j}, giving:
tutorial/theorems.tex+22−8
@@ -163,8 +163,8 @@ plusReducesZ' (S k) = let ih = plusReducesZ' k in
163\useverb{prOstruct}
163\useverb{prOstruct}
164
164
165\noindent
165\noindent
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
184
184
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
187
187
188\end{SaveVerbatim}
188\end{SaveVerbatim}
189\useverb{showmetas}
189\useverb{showmetas}
@@ -265,17 +265,17 @@ Global metavariables:
265\noindent
265\noindent
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}:
269
269
270−\begin{SaveVerbatim}{plusredOSprf}
270+\begin{SaveVerbatim}{plusredZSprf}
271
271
272*theorems> :p plusredZ_S
272*theorems> :p plusredZ_S
273
273
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
276
276
277\end{SaveVerbatim}
277\end{SaveVerbatim}
278−\useverb{plusredOSprf}
278+\useverb{plusredZSprf}
279
279
280\noindent
280\noindent
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
288 k : Nat
288 k : Nat
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
292
292
293\end{SaveVerbatim}
293\end{SaveVerbatim}
294\useverb{prSintros}
294\useverb{prSintros}
295
295
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+
296\noindent
310\noindent
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