# Zulip Chat Archive

## Stream: general

### Topic: dsimp on +

#### Thorsten Altenkirch (Nov 10 2022 at 10:42):

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 (Nov 10 2022 at 10:43):

See the attached files.

Cheers,

Thorsten

ex-1.lean ex-2.lean

#### Floris van Doorn (Nov 10 2022 at 13:05):

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 (Nov 10 2022 at 13:06):

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

#### Floris van Doorn (Nov 10 2022 at 13:07):

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 (Nov 10 2022 at 13:10):

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 (Nov 10 2022 at 15:14):

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.

Last updated: Dec 20 2023 at 11:08 UTC