Notation

Stream: mathlib4

[Antoine Chambert-Loir]

I have a strange notation problem in this example I explain to students

import Mathlib.Tactic

inductive N : Type
  | zero : N
  | succ : N → N

namespace N

instance : Zero N := ⟨zero⟩

/-- addition de deux entiers -/
def add (n : N) : N → N
| 0 => n
| succ m => succ (add n m)

instance : Add N := ⟨add⟩ -- Pour pouvoir utiliser la notation `n + m`

lemma add_zero (n : N) : n + 0 = n := by
  rfl
  done

lemma add_succ (n m : N) : n + (succ m) = succ (n + m) := by
  rfl
  done

lemma zero_add (n: N) : 0 + n = n := by
  induction n with
  | zero => -- rfl
    -- I know `rfl` is enough, but…
    change 0 + 0 = 0 -- doesn't work otherwise
    rw [add_zero]
  | succ a hrec => rw [add_succ, hrec]

For pedagogical reasons, I would like to be able to rw [add_zero], but the induction pattern inserts the litteral zero and Lean does not recognize this zero as 0.

[Kevin Buzzard]

You should write your own induction tactic which uses the right notation, and do induction ... using.

[Antoine Chambert-Loir]

Thanks. But shouldn't the instance : Zero N := <zero> provide a rewriting lemma?