dsimp on +

Stream: general

[Thorsten Altenkirch]

Hi,

I am redefining + from the library for pedagogical reasons. When I prove something I noticed that dsimp [(+),add], folds the result back using my notation, e.g. my goal is 0+succ n' = succ n' and I say dsimp [(+),add], I get succ (0+n') = succ n'. But when I use the library version this doesn't work and I have to use nat.add even though I opened nat. Do I need to open something else?

[Thorsten Altenkirch]

See the attached files.
Cheers,
Thorsten
ex-1.lean ex-2.lean

[Floris van Doorn]

In mathlib the n + m and nat.add n m are definitionally equal, but not syntactically equal. The former is has_add.add n m (and the instance nat.has_add is defined to use nat.add. In your file, you made + directly notation for your version of nat.add. That's why the behavior is different.

For the mathlib + you want to use the lemma nat.add_succ (proven by reflexivity) instead: dsimp [nat.add_succ], (and dsimp [nat.add_zero], works in the zero-case).

[Floris van Doorn]

(PS: we prefer code snippets in #backticks instead of Lean files on this Zulip, unless the files are huge.)

[Floris van Doorn]

BTW: I recommend using backticks in

local notation (name := add)
  m ` + ` n := add m n

Then the pretty printer will print spaces around your +.

[Floris van Doorn]

One further comment: in ex-1, dsimp [(+)], dsimp [add], and dsimp [(+), add] all do exactly the same thing (since + is notation for add). In ex-2 both arguments in dsimp [(+), nat.add] do something different.

[Thorsten Altenkirch]

Ah thank you. Ok I should always use the lemmas instead. From agda I am used to just apply definitions but I see that this can have disadvantages in terms of portability of proofs.