TPIL chaper 8 Ackermann function

Stream: new members

[Lucas Allen]

In chapter 8 section 4 of TPIL the Ackermann function is defined,

def ack : ℕ → ℕ → ℕ
| 0     y     := y+1
| (x+1) 0     := ack x 1
| (x+1) (y+1) := ack x (ack (x+1) y)

#eval ack 3 5

and it says, "As a final example, we observe that Ackermann’s function can be defined directly, because it is justified by the well foundedness of the lexicographic order on the natural numbers."

But when I copy and paste it into VS code I get red squiggles under ack telling me that it's not well founded and asking me to prove x < x, which is false. How can I prove the well foundedness of ack using the lexicographic order on the natural numbers?

[Chris Hughes]

It works for me. What lean version are you using?

[Lucas Allen]

I don't know

[Lucas Allen]

How do I find out?

[Reid Barton]

lean --version from the command line, if you have one

[Reid Barton]

Actually, better is #print lean.version

[Lucas Allen]

def lean.version : ℕ × ℕ × ℕ :=
(3, 5, 1)

[Bryan Gin-ge Chen]

Odd, it works in the web editor, which is currently on 3.5.1c as well.

[Lucas Allen]

Here's the message:

failed to prove recursive application is decreasing, well founded relation
  @has_well_founded.r (Σ' (a : ℕ), ℕ)
    (@psigma.has_well_founded ℕ (λ (a : ℕ), ℕ) (@has_well_founded_of_has_sizeof ℕ nat.has_sizeof)
       (λ (a : ℕ), @has_well_founded_of_has_sizeof ℕ nat.has_sizeof))
Possible solutions:
  - Use 'using_well_founded' keyword in the end of your definition to specify tactics for synthesizing well founded relations and decreasing proofs.
  - The default decreasing tactic uses the 'assumption' tactic, thus hints (aka local proofs) can be provided using 'have'-expressions.
The nested exception contains the failure state for the decreasing tactic.
nested exception message:
invalid apply tactic, failed to unify
  x < x
with
  ?m_1 < ?m_1 + ?m_2
state:
ack : (Σ' (a : ℕ), ℕ) → ℕ,
x y : ℕ
⊢ x < x

[Lucas Allen]

I created a new file and now it works.

[Lucas Allen]

I originally had it in a scrap file full of lots of other stuff. Maybe I messed with some options which stuffed it or something.

[Lucas Allen]

The problem is with the imports...

[Lucas Allen]

Ok I got it down to this, which doesn't work, and gives the same error,

-- import tactic.hint
import tactic.suggest
import tactic

def ack : ℕ → ℕ → ℕ
| 0     y     := y+1
| (x+1) 0     := ack x 1
| (x+1) (y+1) := ack x (ack (x+1) y)

#eval ack 3 5

You can swap import tactic.suggest with import tactic.hint and get the same error, but if you take either of the imports out the error goes away.

[Lucas Allen]

I gtg.

[Reid Barton]

I can reproduce this

[Bryan Gin-ge Chen]

tactic.suggest and tactic.hint are both imported by import tactic, so commenting or uncommenting those doesn't really do anything if import tactic is there.

Chasing the other tactics I found that something in data.nat.basic can cause ack to break:

-- comment this and it works
import data.nat.basic
-- imports of data.nat.basic, comment or uncomment, doesn't matter
import logic.basic algebra.ordered_ring data.option.basic algebra.order_functions

def ack : ℕ → ℕ → ℕ
| 0     y     := y+1
| (x+1) 0     := ack x 1
| (x+1) (y+1) := ack x (ack (x+1) y)

#eval ack 3 5

[Chris Hughes]

It's the @[simp] attribute on nat.succ_pos' that causes the failure. I'm really not sure why.

[Kevin Buzzard]

Does it work if you change (x + 1) etc to nat.succ x etc?

[Chris Hughes]

No

[Chris Hughes]

This is all fixed in 3.6.1

[Chris Hughes]

So the solution is to upgrade your Lean