`MyNat` に対して `0 ≠ 1` を示すのが面倒

Seasawher commented 14 hours ago

/-- 自前で実装した自然数 -/
inductive MyNat where
  | zero
  | succ (n : MyNat)

/-- 自然数から `MyNat` の項を得る -/
def MyNat.ofNat (n : Nat) : MyNat :=
  match n with
  | 0 => MyNat.zero
  | n + 1 => MyNat.succ (MyNat.ofNat n)

/-- `OfNat` のインスタンスを実装する -/
@[default_instance]
instance (n : Nat) : OfNat MyNat n where
  ofNat := MyNat.ofNat n

/-- `MyNat` の各コンストラクタの像は重ならない -/
example (n : MyNat) : MyNat.succ n ≠ MyNat.zero := by
  simp

example : 0 ≠ 1 := by
  simp
  -- unsolved goals...
  -- how to unfold numeric literal automatically?

Seasawher commented 14 hours ago

Zulip: > how to unfold numeric literals

Seasawher commented 13 hours ago

simproc を定義すれば MyNat に対しても simp で示せるようになるっぽいぞ！これは simproc の良い応用例でもある。

https://github.com/leanprover/lean4/blob/ffac974dba799956a97d63ffcb13a774f700149c/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Core.lean#L79-L88

Seasawher commented 9 hours ago

simp だと面倒だが、injection または cases を使うと可能。

lean-ja / lean-by-example

`MyNat` に対して `0 ≠ 1` を示すのが面倒 #1176