plausible のカスタマイズ方法を紹介する

[Seasawher]

https://github.com/leanprover-community/plausible

[Seasawher]

MyNat 型を作って、それを plausible で扱えるようにした例を作った。

import Plausible

open Plausible

/-- 自前で `Nat` を模倣して定義した型 -/
inductive MyNat where
  | zero : MyNat
  | succ : MyNat → MyNat
  deriving Repr

open MyNat

/-- 組み込みの自然数を `MyNat` に変換する -/
def MyNat.ofNat : Nat → MyNat
  | 0 => zero
  | n + 1 => succ (ofNat n)

def MyNat.shrink : MyNat → List MyNat
  | zero => []
  | succ n => n :: n.shrink

open SampleableExt

#check Shrinkable.shrink


instance : Shrinkable MyNat where
  shrink := fun x => x.shrink

#eval Shrinkable.shrink (MyNat.succ (MyNat.succ MyNat.zero))

instance : SampleableExt MyNat := mkSelfContained do
  let x ← SampleableExt.interpSample Nat
  return MyNat.ofNat x

-- ランダムな `MyNat` の例を生成する
#sample MyNat

-- `DecidableEq` を付加する
deriving instance DecidableEq for MyNat

/-- error: Found a counter-example! -/
#guard_msgs in
  example (a b : MyNat) : a = b := by
    plausible (config := {quiet := true})