plausible

plausible は、証明しようとしているゴールが間違っていないかチェックし、反例を見つけるとエラーで警告するタクティクです。

import Plausible

variable (a b : Nat)

/-- error: Found a counter-example! -/
#guard_msgs (error) in
  example (h : 0 ≤ a + b) : 1 ≤ a := by
    plausible (config := { quiet := true })

    sorry

反例が見つからない時

100 個のテストケースでテストしてOKならエラーにならないのですが、途中でギブアップした場合はエラーになります。

/--
warning: Gave up after failing to generate values that fulfill the preconditions 100 times.
---
warning: declaration uses 'sorry'
-/
#guard_msgs (warning) in
  example (a : Nat) : a ≠ a → a ≤ 1 := by
    plausible