timeout error

Stream: general

[Kondo Yuki]

We attempt to prove a theorem by the tactic dec_trivial,
but Lean outputs an error message "(deterministic) timeout".

Is it possible to change settings about timeout?

[Kenny Lau]

use norm_num instead

[Kondo Yuki]

I tried norm_num, but Lean says: unknown identifier 'norm_num'.
Where is norm_num defined?

[Bryan Gin-ge Chen]

It's a tactic defined in mathlib. You'll need to put import tactic at the top of your file.

[Johan Commelin]

@Kondo Yuki It would be very helpful if you could give a bit more detail about what you are doing. You can paste code here, please use #backticks to format it. Try to make sure that the code runs upon copy-paste, see #mwe.

[Kondo Yuki]

We attempt to prove a theorem, VT_0(4) is optimal.
The following is our formalization of it.

import data.fintype data.vector
import .LevenshteinCode .DelCode .Optimality

lemma optimal_VTCode_4_0 :
  is_optimal (VTCode 4 0) := dec_trivial

[Johan Commelin]

But since we have no idea what VTCode is (or what is in the imports .LevenshteinCode .DelCode .Optimality, it will be very hard to help you.

[Johan Commelin]

@Kondo Yuki Is the code in some online repository that we could look at?

[Kyle Miller]

Kondo Yuki said:

Is it possible to change settings about timeout?

I haven't tried it, but there's the top-level command

set_option timeout NNNN

where NNNN is some number (100000 by default in my installation).

[Kondo Yuki]

@Johan Commelin the code can be download at Cotoleta -lean library for formalized coding theory-. https://manau.jp/Lean/cotoleta/.

[Johan Commelin]

Wow, that project has a really long history already!

[Johan Commelin]

@Kondo Yuki Don't you want to host it as a git repository somewhere?

[Johan Commelin]

I just downloaded the zip file. It seems that your project is not setup as a lean package. So it will take some time to get it working on my machine

[Johan Commelin]

@Kondo Yuki I'm trying to compile your files, but I'm having unrelated lean errors.

[Johan Commelin]

It would be very helpful if you could tell us exactly which version of mathlib you are using (by pasting the git commit hash here)

[Johan Commelin]

My tests were using dd8da5165bd00b07408dbb87173e96908c6926a4, which is the lean-3.4.2 branch of mathlib.

[Mario Carneiro]

@Kondo Yuki It looks like your function works, you just need to raise the timeout to compute is_optimal (VTCode 4 0). You can also run lean at the console, where I believe there is no timeout

[Mario Carneiro]

Then again, it appears you are calculating that is_optimal (VTCode 1 0), is_optimal (VTCode 2 0), is_optimal (VTCode 3 0), is_optimal (VTCode 4 0) are all optimal, so a reasonable conjecture is that they are all optimal, which yields a much faster proof

[Kondo Yuki]

@Mario Carneiro Thank you for your confirmation and advice.

[Kondo Yuki]

@Johan Commelin We are using acf2038a720036d2e6fdc035bc57627da71d343c, which is the lean-3.4.2 branch of mathlib.

[Johan Commelin]

Weird. On my copy of mathlib I have

git show origin/lean-3.4.2 | head -1
commit dd8da5165bd00b07408dbb87173e96908c6926a4

[Johan Commelin]

Which is a commit from Feb 5.

[Johan Commelin]

Otoh,

commit acf2038a720036d2e6fdc035bc57627da71d343c
Date:   Sun Dec 29 03:52:23 2019 -0500