slim_check, giving up, deterministic timeout

Stream: new members

[Huỳnh Trần Khanh]

When slim_check fails to find a counterexample, it says "goals accomplished" and when slim_check finds a counterexample, it prints the counterexample. So what does "gave up after X tries" mean? How about deterministic timeout?

[Bryan Gin-ge Chen]

I think "gave up after X tries" means that slim_check was not able to find an example satisfying the hypotheses within X tries.
Deterministic timeout in general means that something exceeded the memory / computation limits in Lean's options. Without seeing a #mwe I can't say what it means.

cc: @Simon Hudon who wrote slim_check.

[Huỳnh Trần Khanh]

This code gives deterministic timeout.

import data.nat.basic
import data.list.range
import tactic.slim_check
open list

def popcount (n : ℕ) := (((range n).map $ nat.to_digits 2).map list.sum).sum

def dp_cardinality : list bool → bool → ℕ
| [] tt := 1
| [] ff := 0
| (ff::the_rest) ff := dp_cardinality the_rest ff
| (tt::the_rest) ff := dp_cardinality the_rest tt + dp_cardinality the_rest ff
| (_::the_rest) tt := 2 * dp_cardinality the_rest tt

def dp_popcount : list bool → bool → ℕ
| [] _ := 0
| (ff::the_rest) ff := dp_popcount the_rest ff
| (tt::the_rest) ff := dp_popcount the_rest tt + (dp_popcount the_rest ff + dp_cardinality the_rest ff)
| (_::the_rest) tt := dp_popcount the_rest tt + (dp_popcount the_rest tt + dp_cardinality the_rest tt)

def to_binary (n : ℕ) := list.reverse ((nat.to_digits 2 n).map (λ x, if x = 0 then ff else tt))

def dp (n : ℕ) := dp_popcount (to_binary n) ff

lemma equivalent (n : ℕ) : dp n = popcount n := begin
  slim_check,
end

[Mario Carneiro]

Most likely, slim_check tried some reasonable sized numbers, but the popcount function takes exponential time so it probably got unlucky and went too far

[Mario Carneiro]

slim_check {max_size := 50} works but it has visible difficulty; you can play with the maximum below the lean timeout which is around 10 seconds