Zulip Chat Archive

Stream: new members

Topic: TPIL chaper 8 Ackermann function


view this post on Zulip 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?

view this post on Zulip Chris Hughes (Mar 16 2020 at 00:54):

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

view this post on Zulip Lucas Allen (Mar 16 2020 at 01:05):

I don't know

view this post on Zulip Lucas Allen (Mar 16 2020 at 01:05):

How do I find out?

view this post on Zulip Reid Barton (Mar 16 2020 at 01:06):

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

view this post on Zulip Reid Barton (Mar 16 2020 at 01:06):

Actually, better is #print lean.version

view this post on Zulip Lucas Allen (Mar 16 2020 at 01:07):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Lucas Allen (Mar 16 2020 at 01:16):

I created a new file and now it works.

view this post on Zulip 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.

view this post on Zulip Lucas Allen (Mar 16 2020 at 01:21):

The problem is with the imports...

view this post on Zulip 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.

view this post on Zulip Lucas Allen (Mar 16 2020 at 01:29):

I gtg.

view this post on Zulip Reid Barton (Mar 16 2020 at 01:33):

I can reproduce this

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 17 2020 at 18:55):

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

view this post on Zulip Chris Hughes (Mar 17 2020 at 19:02):

No

view this post on Zulip Chris Hughes (Mar 17 2020 at 19:31):

This is all fixed in 3.6.1

view this post on Zulip Chris Hughes (Mar 17 2020 at 19:32):

So the solution is to upgrade your Lean


Last updated: May 13 2021 at 22:15 UTC