Skip to content

Use eval! to evaluate functions that use sorry. #133

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
lcrh wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Use eval! to evaluate functions that use sorry. #133

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 9 additions & 4 deletions induction_and_recursion.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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`.
Expand Down