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):
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
dsimp [add], and
dsimp [(+), add] all do exactly the same thing (since
+ is notation for
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: Aug 03 2023 at 10:10 UTC