decidability struggles

Stream: new members

[Miroslav Olšák]

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]

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

--import data.list -- import some mathlib, or not

variables {α : Type} {β : Type}
variables [inhabited α] [inhabited β]

def forall2_inh_bool (P : α → β → bool) : list α → list β → bool
| [] [] := P (default α) (default β)
| (h1::t1) [] := P h1 (default β) && (forall2_inh_bool t1 [])
| [] (h2::t2) := P (default α) h2 && (forall2_inh_bool [] t2)
| (h1::t1) (h2::t2) := P h1 h2 && (forall2_inh_bool t1 t2)

#reduce forall2_inh_bool (λ a b, to_bool (a = b)) [1,2,3] [1,2,3,0]
-- tt without mathlib
-- timeout with mathlib

def my_get : ℕ → list α → α
| 0 l := l.head
| (n+1) l := my_get n l.tail

lemma my_get_nil : ∀ n, my_get n list.nil = default α
| 0 := rfl
| (n+1) := my_get_nil n

lemma forall2_inh_bool.correct (P : α → β → Prop) [Hdec : Π a b, decidable (P a b)]
: ∀ l1 : list α, ∀ l2 : list β,
forall2_inh_bool (λ a b, to_bool (P a b)) l1 l2 = tt
↔ (∀ n, P (my_get n l1) (my_get n l2))
| [] [] := begin
  simp [my_get_nil, forall2_inh_bool],
  exact ⟨λ H n, H, λ H, H 0⟩ -- comment this line when using mathlib
end
| (h1::t1) [] := begin
  simp [forall2_inh_bool, forall2_inh_bool.correct],
  split,
  { intros H n, cases n, exact H.1, exact H.2 n },
  intro H,
  exact ⟨H 0, λ n, H n.succ⟩
end
| [] (h2::t2) := begin
  simp [forall2_inh_bool, forall2_inh_bool.correct],
  split,
  { intros H n, cases n, exact H.1, exact H.2 n },
  intro H,
  exact ⟨H 0, λ n, H n.succ⟩
end
| (h1::t1) (h2::t2) := begin
  simp [forall2_inh_bool, forall2_inh_bool.correct],
  split,
  { intros H n, cases n, exact H.1, exact H.2 n },
  intro H,
  exact ⟨H 0, λ n, H n.succ⟩
end

def forall2_inh_dec (P : α → β → Prop) [Hdec : Π a b, decidable (P a b)]
(l1 : list α) (l2 : list β)
: decidable (∀ n, P (my_get n l1) (my_get n l2))
:=
if C : forall2_inh_bool (λ a b, to_bool (P a b)) l1 l2 = tt then
  is_true ((forall2_inh_bool.correct P l1 l2).mp C)
else is_false (mt (forall2_inh_bool.correct P l1 l2).mpr C)

def my_equiv (l1 l2 : list α) : Prop := ∀ n : ℕ, my_get n l1 = my_get n l2

instance equiv_decidable [decidable_eq α] : @decidable_rel (list α) my_equiv
:= forall2_inh_dec eq

#eval to_bool (my_equiv [1,2,3] [1,2,3,0])
-- tt

#reduce to_bool (my_equiv [1,2,3] [1,2,3,0])
-- tt without mathlib
-- timeout with mathlib

example : my_equiv [1,2,3] [1,2,3,0] := by dec_trivial
-- fails

[Yakov Pechersky]

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

[Miroslav Olšák]

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]

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]

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]

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

[Yakov Pechersky]

then add another 0

[Miroslav Olšák]

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

[Miroslav Olšák]

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]

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]

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]

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

[Mario Carneiro]

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]

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

[Miroslav Olšák]

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]

#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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Ben Selfridge]

Hello! My name is Ben Selfridge. I work at Galois, Inc. in Portland and am learning Lean in my spare time, both for joy and professional development. I've been learning the proofs of Gödel's incompleteness theorems at a deeper level than I've ever had time to lately, and I partly decided to learn Lean to see if I could formalize them as a fun challenge. I initially started with Lean4, but gave up as soon as I realized that most of the relevant mathlib work had not been ported yet, so now I'm on Lean3.

I have a newbie question. I have a prop definition

def divides (m : ℕ) (n : ℕ) : Prop :=
  ∃ a : ℕ, a * m = n

I want to show that the following function dividesF decides this proposition:

def dividesF_aux : ℕ → ℕ → ℕ → bool
| 0 := λ m n, n = 0
| (nat.succ a) := λ m n, if a.succ * m = n
  then tt
  else dividesF_aux a m n

def dividesF (m n : ℕ) : bool := dividesF_aux n m n

In proving the following lemma, I got stuck:

theorem divides_of_dividesF_aux {a m n : ℕ} (h : dividesF_aux a m n) : divides m n :=
begin
  cases a with pa,
  -- a = 0
    simp [dividesF_aux] at h,
    rw [divides],
    apply exists.intro nat.zero,
    -- How do I get to_bool (n = 0) to turn into n = 0?
    admit,
  -- a = pa.succ
    admit,
end

As indicated in the comment, I have to_bool(n = 0) as my hypothesis, and I'd like it to resolve to n = 0. In Lean4, simp did the trick, but not here.

Any suggestions? Also, any pointers for code quality are welcome.

[Mauricio Collares]

Should h be of type dividesF_aux a m n = tt?

[Mario Carneiro]

simp should do this reduction, but you need the file containing the simp lemma to be imported. In this case I would guess it's data.bool.basic

[Ben Selfridge]

Mauricio Collares said:

Should h be of type dividesF_aux a m n = tt?

Yes, it should! That fixed the problem. Do you know if Lean4 automatically figures out that's what I meant? Because I've tried it both ways in Lean4 and it didn't seem to affect anything.

[Ben Selfridge]

Mario Carneiro said:

simp should do this reduction, but you need the file containing the simp lemma to be imported. In this case I would guess it's data.bool.basic

Thank you -- this also worked!