How to use `plausible`

Stream: new members

[Gareth Ma]

I don't understand the output of

import Mathlib

set_option trace.plausible.success true
set_option trace.plausible.instance true
example (x y : ℕ) (h : x.gcd y = 1) :
    (x * x).gcd y = 1 := by
  plausible

it says Gave up after failing to generate values that fulfill the preconditions 1 times.. However the tracing (at the word "example") shows that it does generate quite a few examples, some of which are coprime. What does the "gave up ... 1 times." message mean?

(Last time I used this tactic was a year ago when it was named slim_check, and there it worked fine IIRC...)

[Gareth Ma]

(Not super important but also the $\gcd(x, y) = 1$ condition holds for $6 / \pi^2 \approx 60.8\%$ of the time for random x y so it shouldn't fail often)

[Gareth Ma]

For reference

example (x y : ℕ) : x + y = y + x := by
  plausible -- Unable to find a counter-example

This is what I expect

[Kenny Lau]

@Gareth Ma (I have never seen this tactic before) yeah it's a bit weird that it says 1 time because in your trace it clearly tried a lot of different values and h is met quite a lot of times lol

[Gareth Ma]

I only knew about it because @Damiano Testa told me about it for my bachelor's thesis haha

[Eric Wieser]

@Kenny Lau, you might remember it as slim_check

[Kenny Lau]

hmm, don't think I used that one either

[Henrik Böving]

Kenny Lau said:

Gareth Ma (I have never seen this tactic before) yeah it's a bit weird that it says 1 time because in your trace it clearly tried a lot of different values and h is met quite a lot of times lol

No it is much more specific, it says values fulfilling the pre conditions. Meaning that it trier a bunch of values randomly, had one pair where h holds and for that pair found that the theorem holds as well