## Stream: new members

### Topic: TPIL chaper 8 Ackermann function

#### Lucas Allen (Mar 16 2020 at 00:47):

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 (Mar 16 2020 at 00:54):

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

I don't know

#### Lucas Allen (Mar 16 2020 at 01:05):

How do I find out?

#### Reid Barton (Mar 16 2020 at 01:06):

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

#### Reid Barton (Mar 16 2020 at 01:06):

Actually, better is #print lean.version

#### Lucas Allen (Mar 16 2020 at 01:07):

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


#### Bryan Gin-ge Chen (Mar 16 2020 at 01:11):

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

#### Lucas Allen (Mar 16 2020 at 01:12):

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 (Mar 16 2020 at 01:16):

I created a new file and now it works.

#### Lucas Allen (Mar 16 2020 at 01:17):

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 (Mar 16 2020 at 01:21):

The problem is with the imports...

#### Lucas Allen (Mar 16 2020 at 01:29):

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.

I gtg.

#### Reid Barton (Mar 16 2020 at 01:33):

I can reproduce this

#### Bryan Gin-ge Chen (Mar 16 2020 at 01:42):

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 (Mar 17 2020 at 18:32):

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

#### Kevin Buzzard (Mar 17 2020 at 18:55):

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

No

#### Chris Hughes (Mar 17 2020 at 19:31):

This is all fixed in 3.6.1