From 1097ec1f5f140e49fa6ea6211d3066b73662cb28 Mon Sep 17 00:00:00 2001 From: Leopold Haller Date: Tue, 22 Oct 2024 17:13:20 -0700 Subject: [PATCH] Use eval! to evaluate functions that use sorry. --- induction_and_recursion.md | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/induction_and_recursion.md b/induction_and_recursion.md index 29abb83..dd05d3c 100644 --- a/induction_and_recursion.md +++ b/induction_and_recursion.md @@ -796,7 +796,11 @@ The following example is similar: it converts any natural number to a binary expression, represented as a list of 0's and 1's. We have to provide evidence that the recursive call is decreasing, which we do here with a ``sorry``. The ``sorry`` does not -prevent the interpreter from evaluating the function successfully. +prevent the interpreter from evaluating the function successfully, but +by default it will refuse to do so as evaluating a non-terminating +function could cause Lean to crash. +We can use the command ``#eval!`` to override this behavior and evaluate it +anyway. ```lean def natToBin : Nat → List Nat @@ -806,7 +810,7 @@ def natToBin : Nat → List Nat have : (n + 2) / 2 < n + 2 := sorry natToBin ((n + 2) / 2) ++ [n % 2] -#eval natToBin 1234567 +#eval! natToBin 1234567 ``` As a final example, we observe that Ackermann's function can be @@ -882,7 +886,8 @@ decreasing_by · apply Prod.Lex.left; simp_arith ``` -We can use `decreasing_by sorry` to instruct Lean to "trust" us that the function terminates. +We can use `decreasing_by sorry` to instruct Lean to "trust" us that the function terminates +and use the command ``#eval!`` to evaluate it. ```lean def natToBin : Nat → List Nat @@ -891,7 +896,7 @@ def natToBin : Nat → List Nat | n + 2 => natToBin ((n + 2) / 2) ++ [n % 2] decreasing_by sorry -#eval natToBin 1234567 +#eval! natToBin 1234567 ``` Recall that using `sorry` is equivalent to using a new axiom, and should be avoided. In the following example, we used the `sorry` to prove `False`.