why `dsimp` made no progress?

Stream: lean4

[Asei Inoue]

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

namespace MyNat

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

instance : OfNat MyNat 0 where
  ofNat := .zero

instance : OfNat MyNat 1 where
  ofNat := .succ .zero

instance : Add MyNat where
  add := MyNat.add

@[simp] theorem add_zero (n : MyNat) : n + 0 = n := by rfl
@[simp] theorem zero_add (n : MyNat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ n ih =>
    dsimp [Add.add, MyNat.add]
    -- there is no error. it doesnt say "dsimp made no progress".
    -- but goal state: 0 + n.succ = n.succ
    -- why goal is not changed?

    rw [show 0 + n.succ = .succ (0 + n) from by rfl]
    rw [ih]

[Kevin Buzzard]

Try set_option pp.all true and then re-examine your claim that the goal is not changed. I suspect it should be replaced by the weaker claim "the goal changed but lean pretty prints the old and new goals in the same way, when the default pretty print options are on".

[Asei Inoue]

@Kevin Buzzard Thank you, but goal state seems to be exactly same...

set_option pp.all true

@[simp] theorem zero_add (n : MyNat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ n ih =>
    --    @Eq.{1} MyNat
    -- (@HAdd.hAdd.{0, 0, 0} MyNat MyNat MyNat (@instHAdd.{0} MyNat MyNat.instAdd)
    --   (@OfNat.ofNat.{0} MyNat 0 MyNat.instOfNatOfNatNat) (MyNat.succ n))
    -- (MyNat.succ n)
    dsimp [Add.add, MyNat.add]

    --   @Eq.{1} MyNat
    -- (@HAdd.hAdd.{0, 0, 0} MyNat MyNat MyNat (@instHAdd.{0} MyNat MyNat.instAdd)
    --   (@OfNat.ofNat.{0} MyNat 0 MyNat.instOfNatOfNatNat) (MyNat.succ n))
    -- (MyNat.succ n)

    rw [show 0 + n.succ = .succ (0 + n) from by rfl]
    rw [ih]

[Asei Inoue]

is this a bug of dsimp...?

[Asei Inoue]

I have two questions

• No error with no progress in dsimp
• Why is there no progress in dsimp?

[Asei Inoue]

I forget to apply dsimp [HAdd.hAdd]