git.iko.soy/Idris-dev
on master help sign in
tutorial: update interactive proof
d861727Reynir Reynisson
tutorial/provisional.tex+18−3
compare with master
unifiedsplit
@@ -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: