Zulip Chat Archive

Stream: general

Topic: dsimp on +

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


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.
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