Zulip Chat Archive

Stream: general

Topic: slim_check


view this post on Zulip Scott Morrison (Oct 07 2020 at 23:23):

An example just came up on another thread where some missing parentheses garbled a statement. I was hoping to be able to run slim_check on it, but couldn't.

import tactic.slim_check

example (f g :   Prop) :  k : , f k   k : , g k   k : , f k  g k :=
by slim_check

view this post on Zulip Scott Morrison (Oct 07 2020 at 23:24):

First, a little bug report: when this fails, it suggests running

set_option trace.class_instances true
#check (by apply_instance : testable (slim_check.named_binder "f"
  ( (f :   Prop),
     slim_check.named_binder "g"
       ( (g :   Prop),  (k : ), f k   (k : ), g k   (k : ), f k  g k))))

to see which instances are missing, but we get unknown identifier testable.

view this post on Zulip Scott Morrison (Oct 07 2020 at 23:25):

I can see that with the recent PR about sampleable, we at least get off the ground here:

#sample   Prop

produces lots of good candidate functions.

view this post on Zulip Simon Hudon (Oct 07 2020 at 23:25):

That's true, you need open slim_check. Sorry

view this post on Zulip Simon Hudon (Oct 07 2020 at 23:26):

An existential is difficult to test because there's no witness that shows that it's false

view this post on Zulip Scott Morrison (Oct 07 2020 at 23:27):

ah, of course!

view this post on Zulip Scott Morrison (Oct 07 2020 at 23:27):

How about we just replace testable with slim_check.testable in the suggestion text?

view this post on Zulip Simon Hudon (Oct 07 2020 at 23:27):

If it ranged over fin n even if you quantify over all n that should be better

view this post on Zulip Simon Hudon (Oct 07 2020 at 23:28):

I think that's a good idea

view this post on Zulip Scott Morrison (Oct 07 2020 at 23:28):

Your todo list or mine? :-)

view this post on Zulip Simon Hudon (Oct 07 2020 at 23:30):

How about whoever gets there first?

view this post on Zulip Bryan Gin-ge Chen (Oct 08 2020 at 03:44):

Simon won the race: #4520 (now on the queue)

view this post on Zulip Simon Hudon (Oct 08 2020 at 04:02):

That was one swift review!


Last updated: May 06 2021 at 22:13 UTC