@@ -4,7 +4,7 @@ Interactive Theorem Proving
44
55Idris supports interactive theorem proving via elaborator reflection.
66
7−:ref:'elaborator-reflection' is also used to convert high-level Idris code into
7+:ref:`elaborator-reflection` is also used to convert high-level Idris code into
88the core language and for customising the language. Here we show how to use it
99to interactively construct proofs.
1010
@@ -237,10 +237,60 @@ which is trivially provable using reflexivity:
237237 Proof completed!
238238 Main.plusredZ_S = %runElab (do intro `{{k}}
239239 intro `{{ih}}
240− compute
241240 rewriteWith (Var `{{ih}})
242241 reflexivity)
243242
244−Again, we can cut & paste this into the hole in the original file.
243+We can't just cut & paste this into the hole in the original file like this:
244+
245+.. code-block:: idris
246+
247+ import Pruviloj
248+ import Pruviloj.Induction
249+
250+ %language ElabReflection
251+
252+ plusReducesZ' : (n:Nat) -> n = plus n Z
253+ plusReducesZ' Z = %runElab (do reflexivity)
254+ plusReducesZ' (S k) = let ih = plusReducesZ' k in
255+ (%runElab (do intro `{{k}}
256+ intro `{{ih}}
257+ rewriteWith (Var `{{ih}})
258+ reflexivity)
259+ )
260+
261+because this gives the following error:
262+
263+.. code-block:: idris
264+
265+ Idris> :load elabInteractiveEx2.idr
266+ elabInteractiveEx2.idr:10:32:
267+ |
268+ 10 | intro `{{ih}}
269+ | ^
270+ unexpected "in"
271+ expecting dependent type signature
272+
273+However if we put the proof into a separate function like this:
274+
275+.. code-block:: idris
276+
277+ import Pruviloj
278+ import Pruviloj.Induction
279+
280+ %language ElabReflection
281+
282+ plusredZ_S : (k : Nat) -> (ih:(k = plus k Z)) -> (S k = S (plus k Z))
283+ plusredZ_S = %runElab (do intro `{{k}}
284+ intro `{{ih}}
285+ rewriteWith (Var `{{ih}})
286+ reflexivity)
287+
288+ plusReducesZ' : (n:Nat) -> n = plus n Z
289+ plusReducesZ' Z = %runElab (do reflexivity)
290+ plusReducesZ' (S k) = let ih = plusReducesZ' k in plusredZ_S k ih
291+
292+This then loads.
293+
294+.. [#f1] https://github.com/idris-lang/Idris-dev/issues/4556
245295
246296.. |image| image:: ../image/plusReducesProof.png