slim_check

Stream: general

[Scott Morrison]

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

[Scott Morrison]

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.

[Scott Morrison]

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.

[Simon Hudon]

That's true, you need open slim_check. Sorry

[Simon Hudon]

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

[Scott Morrison]

ah, of course!

[Scott Morrison]

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

[Simon Hudon]

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

[Simon Hudon]

I think that's a good idea

[Scott Morrison]

Your todo list or mine? :-)

[Simon Hudon]

How about whoever gets there first?

[Bryan Gin-ge Chen]

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

[Simon Hudon]

That was one swift review!