## Stream: new members

### Topic: decidability struggles

#### 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

#### Eric Wieser (Apr 16 2021 at 16:46):

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

#### Yakov Pechersky (Apr 16 2021 at 16:47):

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

#### 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


#### 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

#### 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...

#### Yakov Pechersky (Apr 16 2021 at 22:48):

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


#### 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  []


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)...

#### 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.

#### 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"

#### 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.

#### 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  []
-- tt
#eval test2  []
-- tt
--#reduce test  [] -- times out
#reduce test2  []
-- tt
example : test  [] = tt := by dec_trivial
-- fails
example : test2  [] = tt := by dec_trivial
-- succeeds


#### 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

#### 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  []


#### 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.

#### Miroslav Olšák (Apr 17 2021 at 20:08):

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


(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)

-- fast
-- slow


#### 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.

#### 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


#### Miroslav Olšák (Apr 18 2021 at 09:23):

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

#### Mario Carneiro (Apr 18 2021 at 09:50):

Heh, that's because lean cheats:

set_option trace.compiler.optimize_bytecode true

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


#### 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

#### 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