git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4731 from martinbaker/fixInteractiveDoc
26fa6c3Niklas Larsson
docs/proofs/interactive.rst+53−3
compare with master
unifiedsplit
@@ -4,7 +4,7 @@ Interactive Theorem Proving
4
4
5Idris supports interactive theorem proving via elaborator reflection.
5Idris supports interactive theorem proving via elaborator reflection.
6
6
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
8the core language and for customising the language. Here we show how to use it
8the core language and for customising the language. Here we show how to use it
9to interactively construct proofs.
9to interactively construct proofs.
10
10
@@ -237,10 +237,60 @@ which is trivially provable using reflexivity:
237 Proof completed!
237 Proof completed!
238 Main.plusredZ_S = %runElab (do intro `{{k}}
238 Main.plusredZ_S = %runElab (do intro `{{k}}
239 intro `{{ih}}
239 intro `{{ih}}
240− compute
241 rewriteWith (Var `{{ih}})
240 rewriteWith (Var `{{ih}})
242 reflexivity)
241 reflexivity)
243
242
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
245
295
246.. |image| image:: ../image/plusReducesProof.png
296.. |image| image:: ../image/plusReducesProof.png