Zulip Chat Archive

Stream: new members

Topic: decidability struggles


view this post on Zulip Miroslav Olšák (Apr 16 2021 at 16:41):

I was trying to prove decidability of some predicates (about inhabited lists), and I got to a point where #eval on to_bool works the way I would expect but #reduce timeouts when using mathlib (and it works fine without it), and the dec_trivial tactic fails. What am I doing wrong? My experiment is attached:
decibility_experiment.lean

view this post on Zulip Eric Wieser (Apr 16 2021 at 16:46):

Since the file is short, I've pasted it here:

view this post on Zulip Yakov Pechersky (Apr 16 2021 at 16:47):

iirc, && does not short circuit in Lean, correct?

view this post on Zulip Miroslav Olšák (Apr 16 2021 at 22:40):

What does "shortening circuit" mean? It is defined as

@[inline] def bor : bool  bool  bool
| tt _  := tt
| ff tt := tt
| ff ff := ff

@[inline] def band : bool  bool  bool
| ff _  := ff
| tt ff := ff
| tt tt := tt

notation x || y := bor x y
notation x && y := band x y

view this post on Zulip Eric Rodriguez (Apr 16 2021 at 22:45):

in normal programming languages, something like f(x) && y(x) will be executed as the following: it first checks f(x). If it's false, then it won't even bother checking y(x), as the and of them is false. Similarly for f(x) || y(x) when f(x)=tt. This is short circuiting

view this post on Zulip Miroslav Olšák (Apr 16 2021 at 22:47):

Ah, I see, then as far as I understand, it does by the definition. However, it shouldn't make a difference anyway when I tested in on 5 simple checks...

view this post on Zulip Yakov Pechersky (Apr 16 2021 at 22:48):

#eval tt && to_bool (1  list.range 10000000)

view this post on Zulip Yakov Pechersky (Apr 16 2021 at 22:48):

then add another 0

view this post on Zulip Miroslav Olšák (Apr 16 2021 at 23:07):

After a bit of more experimenting, any reason why the following code times out with mathlib (and succeeds with tt when I replace the third line with ff)?

def test : list   list   bool
| [] [] := tt
| (h1::t1) [] := test t1 []
| [] (h2::t2) := test [] t2
| (h1::t1) (h2::t2) := ff

#reduce test [0] []

But I don't even know whether this is important, I primarily wanted to make the dec_trivial work in the original question (and similar cases)...

view this post on Zulip Miroslav Olšák (Apr 17 2021 at 00:04):

OK, so after making the function forall2_inh_bool recursive only in one argument (which required defining another helper function), the problem is solved, and my takeover from this is that recursion on multiple arguments is somehow evil.

view this post on Zulip Mario Carneiro (Apr 17 2021 at 01:38):

I'm not sure what you mean by "with mathlib" here. I am not having any trouble evaluating that expression, but the general recommendation on #reduce is "don't use it, it doesn't work beyond toy examples"

view this post on Zulip Miroslav Olšák (Apr 17 2021 at 08:09):

I mean, when I prepend the code of test (I believe should be a toy example) with

import data.list

Then the #reduce times out. By the way, I am using lean version, leanprover-community/lean:3.28.0

And I was trying to use #reduce just to figure out what the problem could be. The original issue was that dec_trivial was not working in the original question.

view this post on Zulip Miroslav Olšák (Apr 17 2021 at 08:54):

This is a minimal working example, I believe:

import tactic

def test : list   list   bool
| [] [] := tt
| (h1::t1) [] := test t1 []
| [] (h2::t2) := test [] t2
| (h1::t1) (h2::t2) := ff

def test2 : list   list   bool
| [] [] := tt
| (h1::t1) [] := test2 t1 []
| [] (h2::t2) := ff
| (h1::t1) (h2::t2) := ff

#eval test [0] []
-- tt
#eval test2 [0] []
-- tt
--#reduce test [0] [] -- times out
#reduce test2 [0] []
-- tt
example : test [0] [] = tt := by dec_trivial
-- fails
example : test2 [0] [] = tt := by dec_trivial
-- succeeds

view this post on Zulip Mario Carneiro (Apr 17 2021 at 09:03):

Oh interesting. test is apparently compiled using well founded recursion, which is going to cause problems with #reduce for sure, but importantly the default well founded recursion tactic uses simp, so importing mathlib can change the proof that is discovered, from one that computes to one that uses axioms. There is a recent "fix" to lean 3 that should be arriving in the next version, which will make this fail rather than unfold the proof

view this post on Zulip Mario Carneiro (Apr 17 2021 at 09:06):

If you want to avoid well founded recursion, you can rewrite it to make it more obviously structural recursive:

def test1 : list   bool
| [] := tt
| (h2::t2) := test1 t2

def test2 (IH : list   bool) : list   bool
| [] := IH []
| (h2::t2) := ff

def test : list   list   bool
| [] := test1
| (h1::t1) := test2 (test t1)

#eval test [0] []

view this post on Zulip Miroslav Olšák (Apr 17 2021 at 09:17):

OK, I did it this way in the end. Originally, I found it convenient that lean (contrary to say coq) can handle recursion on multiple parameters on its own but it is apparently not for free.

view this post on Zulip Miroslav Olšák (Apr 17 2021 at 20:08):

#eval tt && to_bool (1  list.range 10000000)

then add another 0

(a bit offtopic)
I was still a bit puzzled by this. First, let's just clarify that it is not an example of not shortening circuit for && since tt && must continue with the evaluation. If we replace it with tt || or ff &&, lean handles it without problem. But still, I thought that 1 should be at the beginning of the range, so it should be possible to find it quickly. So I looked up the definition of list.range, and it turned out that by lean's definition, it counts down to zero until it starts making the list. So I wrote my own range definition, however, even that one didn't turn out working fast. Why it is the case seems to be a technical detail of how lean do / doesn't do lazy evaluation which is beyond my understanding.

def list.my_range :     list 
| n0 0 := []
| n0 (l+1) := n0::(list.my_range (n0+1) l)

#eval (0::(list.my_range 1 9999999)).head
-- fast
#eval ((list.my_range 0 10000000)).head
-- slow

view this post on Zulip Mario Carneiro (Apr 18 2021 at 00:33):

Lean is an eager, or call-by-value language, like ML and unlike Haskell. That means that it won't evaluate list.mem until it has fully evaluated the list.range 10000000 into a list with 10000000 elements. If you used lazy lists (which lean has btw, as lazy_list A) then it would only evaluate as many elements as needed and leave the rest as thunks, so the operation would evaluate quickly.

view this post on Zulip Miroslav Olšák (Apr 18 2021 at 09:03):

Well, but not exactly, when I run the following code in OCaml,

let rec range n0 = function | 0 -> [] | l -> n0::(range (n0+1) (l-1));;
List.hd (0::(range 0 1000000));;

I get an error. On the other hand, lean can handle

#eval (0::(list.range 1000000000)).head

view this post on Zulip Miroslav Olšák (Apr 18 2021 at 09:23):

I guess, it is not so important, just that it surprised me a bit.

view this post on Zulip Mario Carneiro (Apr 18 2021 at 09:50):

Heh, that's because lean cheats:

set_option trace.compiler.optimize_bytecode true
def foo := (0::(list.range 1000000000)).head

-- [compiler.optimize_bytecode]  foo 0
-- 0: scnstr #0
-- 1: ret

view this post on Zulip Mario Carneiro (Apr 18 2021 at 09:51):

Using the magic of pure functional programming it was able to prove that the thing evaluates to 0 without having to work out the tail of the list

view this post on Zulip Mario Carneiro (Apr 18 2021 at 09:54):

It doesn't need laziness to justify this transformation because all functions are total


Last updated: May 13 2021 at 00:41 UTC