Zulip Chat Archive

Stream: new members

Topic: slim_check, giving up, deterministic timeout


view this post on Zulip Huỳnh Trần Khanh (Jan 21 2021 at 16:18):

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?

view this post on Zulip Bryan Gin-ge Chen (Jan 21 2021 at 16:20):

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.

view this post on Zulip Huỳnh Trần Khanh (Jan 21 2021 at 16:22):

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

view this post on Zulip Mario Carneiro (Jan 21 2021 at 16:28):

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

view this post on Zulip Mario Carneiro (Jan 21 2021 at 16:31):

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


Last updated: May 08 2021 at 10:12 UTC