MyNat の足し算を簡約するsimprocs がかけるか？

[Seasawher]

1 + (2 + 3) とかを 6 に簡約するsimprocs を、MyNat上で定義できるかといってもいいかも

[Seasawher]

reduce タクティクを使えば終わりな気もする

[Seasawher]

reduce タクティクは確かに使えるのだが，ちょっとやりたいことと違う気がするし， そもそも rfl で証明は通る

ローカルコンテキストにある x + 1 = 2 みたいな命題を x = 1 に単純化したいなという気持ちがある

import Mathlib.Tactic

namespace Ex

inductive Nat : Type where
  | zero : Nat
  | succ : Nat → Nat

def Nat.add (n m : Nat) : Nat :=
  match m with
  | zero => n
  | succ m => succ (Nat.add n m)

def Nat.ofNat (n : _root_.Nat) : Nat :=
  match n with
  | 0 => zero
  | n + 1 => succ (Nat.ofNat n)

instance (n : _root_.Nat) : OfNat Nat n where
  ofNat := Nat.ofNat n

instance : Add Nat where
  add := Nat.add

example : 1 + (2 + 3) = (6 : Nat) := by
  reduce
  rfl

end Ex