## Stream: new members

### Topic: dsimp strange behaviour

#### Thorsten Altenkirch (Nov 04 2020 at 09:50):

open nat

theorem add_lneutr : ∀ n : ℕ, 0 + n  = n :=
begin
assume n,
induction n with n' ih,
refl,
rewrite ih,
end


doesn't work but it works once I say import tactic?

#### Johan Commelin (Nov 04 2020 at 09:55):

I can't reproduce.

#### Johan Commelin (Nov 04 2020 at 09:55):

For me it fails with and without the import, with the same error

#### Johan Commelin (Nov 04 2020 at 09:56):

Copy-pasto... let me try again

#### Johan Commelin (Nov 04 2020 at 09:57):

Now it just hangs... with the import

#### Patrick Massot (Nov 04 2020 at 10:00):

Thorsten, what are you expecting on paper? This proof won't work, no matter how much you unfold stuff. You need to use associativity.

#### Shing Tak Lam (Nov 04 2020 at 10:01):

I don't think you need associativity? Since this works

open nat

theorem add_lneutr : ∀ n : ℕ, 0 + n  = n :=
begin
assume n,
induction n with n' ih,
refl,
change (0 + n').succ = n'.succ,
rw ih,
end


So I think Thorsten is just expecting dsimp to do what my change line did.

#### Patrick Massot (Nov 04 2020 at 10:05):

Oh right. Relying on definitional equality is so weird.

#### Patrick Massot (Nov 04 2020 at 10:06):

(This case of associativity is indeed definitional)

#### Patrick Massot (Nov 04 2020 at 10:09):

So the issue is that, if you don't want to use change, you need to unfold stuff and then refold some (differently). I don't think we have any tactic doing that besides change (or its twin show).

#### Thorsten Altenkirch (Nov 04 2020 at 10:09):

Ok, originally I defined add myself:

namespace test

open nat

def add : ℕ → ℕ → ℕ
| n zero     := n
| n (succ m) := succ (add n m)

local notation m + n := add m n

theorem add_lneutr : ∀ n : ℕ, 0 + n  = n :=
begin
assume n,
induction n with n' ih,
refl,
rewrite ih,
end

end test


I thought I am just reproducing the definition of + from the standard library but it seems this is different.

#### Thorsten Altenkirch (Nov 04 2020 at 10:11):

In my course I first ask students to show that +,* are a semiaring but then I tell them to use the ring tactic. I wanted to use the official definition of + actually.

#### Thorsten Altenkirch (Nov 04 2020 at 10:13):

OK I shouldn't rely on dsimp , fair enough. It is how I am used to work simplify using definitions but I understand this is nt the lean way because dsimp does more things than I expect.

#### Patrick Massot (Nov 04 2020 at 10:13):

Your last snippet is clearly (technologically) different since you're not using at all has_add, which is what you need to refold in the other proof.

#### Shing Tak Lam (Nov 04 2020 at 10:13):

Johan Commelin said:

Now it just hangs... with the import

btw I think this is because nat.add is protected, so dsimp [(+), add] is just dsimp [(+), has_add.add] so it's looping.

#### Patrick Massot (Nov 04 2020 at 10:14):

No, it's not dsimp doing more than you expect. When you use has_add there are more things to unfold than with your def of add and custom non-polymorphic notation.

#### Thorsten Altenkirch (Nov 04 2020 at 10:14):

but if I don't open has_add it doesn't work at all?

#### Thorsten Altenkirch (Nov 04 2020 at 10:15):

namespace test

open nat

theorem add_lneutr : ∀ n : ℕ, 0 + n  = n :=
begin
assume n,
induction n with n' ih,
refl,
rewrite ih,
end

end test


fails.

#### Patrick Massot (Nov 04 2020 at 10:15):

Of course, there is no add in the root namespace.

#### Shing Tak Lam (Nov 04 2020 at 10:15):

That's because nat.add is protected, so even if you have open nat you still need to write nat.add

#### Patrick Massot (Nov 04 2020 at 10:16):

Right, both nat.add and has_add.add are hidden here, for different reasons.

#### Thorsten Altenkirch (Nov 04 2020 at 10:17):

If I use nat.add my rewrite doesn't work.

namespace test

open nat

theorem add_lneutr : ∀ n : ℕ, 0 + n  = n :=
begin
assume n,
induction n with n' ih,
refl,
rewrite ih,
end

end test


#### Thorsten Altenkirch (Nov 04 2020 at 10:17):

Maybe it is easier if I use my own definition and instantiate ring to this one?

#### Johan Commelin (Nov 04 2020 at 10:18):

Why do you want to use dsimp instead of show?

#### Thorsten Altenkirch (Nov 04 2020 at 10:18):

Maybe because I don't know show?

#### Patrick Massot (Nov 04 2020 at 10:18):

It's the same as change.

#### Patrick Massot (Nov 04 2020 at 10:18):

Do you understand what I wrote about refolding?

#### Thorsten Altenkirch (Nov 04 2020 at 10:19):

Because I just want lean to simplify the term.

#### Patrick Massot (Nov 04 2020 at 10:19):

No, you don't want to simplify

#### Patrick Massot (Nov 04 2020 at 10:19):

You want to unfold and then refold.

#### Patrick Massot (Nov 04 2020 at 10:19):

Do you use VSCode? Do you know how to use the tactic state widget to understand what is the meaning of each notation?

#### Thorsten Altenkirch (Nov 04 2020 at 10:20):

I want to apply an equation that follows from the definition of the function. It works for my own definition and I thought that the library definition behaves the same way.

#### Thorsten Altenkirch (Nov 04 2020 at 10:20):

No I am using emacs.

#### Johan Commelin (Nov 04 2020 at 10:20):

You should just try out VScode once to experience the tactic state widget

#### Johan Commelin (Nov 04 2020 at 10:20):

Your students will love it

#### Patrick Massot (Nov 04 2020 at 10:21):

Can you copy-paste the way you see tactic state in emacs after the dsimp?

#### Thorsten Altenkirch (Nov 04 2020 at 10:21):

They use VScode anyway. At leats some of them.

#### Johan Commelin (Nov 04 2020 at 10:21):

Thorsten Altenkirch said:

I want to apply an equation that follows from the definition of the function. It works for my own definition and I thought that the library definition behaves the same way.

Does erw work, instead of the rw?

#### Thorsten Altenkirch (Nov 04 2020 at 10:21):

n' : ℕ,
ih : 0 + n' = n'
⊢ (0.add n').succ = n'.succ


#### Patrick Massot (Nov 04 2020 at 10:21):

You need to understand the meaning of notations there.

#### Patrick Massot (Nov 04 2020 at 10:22):

Ok, great. What is + on line 2 and what is .add on line 3 in your opinion?

#### Thorsten Altenkirch (Nov 04 2020 at 10:22):

I just looked for a way to explain and use the definition of add.

#### Johan Commelin (Nov 04 2020 at 10:22):

@Thorsten Altenkirch Voila:

namespace test

open nat

theorem add_lneutr : ∀ n : ℕ, 0 + n  = n :=
begin
assume n,
induction n with n' ih,
refl,
dsimp [(+),nat.add] at *,
rw ih,
end

end test


#### Thorsten Altenkirch (Nov 04 2020 at 10:22):

How come it works for my own definition?

#### Johan Commelin (Nov 04 2020 at 10:23):

Is your own definition using + notation?

#### Johan Commelin (Nov 04 2020 at 10:23):

As in, did you define an instance of has_add for it?

#### Patrick Massot (Nov 04 2020 at 10:23):

Here is how you answer those crucial question in VSCode:
thorsten.gif

#### Patrick Massot (Nov 04 2020 at 10:23):

Johan, I already told all that to Thorsten.

#### Thorsten Altenkirch (Nov 04 2020 at 10:24):

namespace test

open nat

def add : ℕ → ℕ → ℕ
| n zero     := n
| n (succ m) := succ (add n m)

local notation m + n := add m n

theorem add_lneutr : ∀ n : ℕ, 0 + n  = n :=
begin
assume n,
induction n with n' ih,
refl,
rewrite ih,
end

end test


works

#### Johan Commelin (Nov 04 2020 at 10:24):

@Thorsten Altenkirch I think you want to dsimp at ih and the goal

#### Patrick Massot (Nov 04 2020 at 10:24):

He is not using has_add.add at all in his custom example hence there is no need to refold nat.add into has_add.add

#### Johan Commelin (Nov 04 2020 at 10:24):

@Thorsten Altenkirch there is a has_add.add in ih blocking your rewrite.

#### Johan Commelin (Nov 04 2020 at 10:25):

That's why my code is working, because I dsimp at *

#### Thorsten Altenkirch (Nov 04 2020 at 10:25):

OK so there is no way to port my way of using dsimp in my example to using the library definition of +?

#### Patrick Massot (Nov 04 2020 at 10:25):

At the stage where things go wrong, my VSCode screencast show he has has_add.add in the assumption but not in the goal, hence need to reintroduce it in the goal or unfold it in the assumption.

#### Johan Commelin (Nov 04 2020 at 10:25):

In particular local notation m + n := add m n is not syntactically equal to using has_add.add

#### Thorsten Altenkirch (Nov 04 2020 at 10:27):

I understand partially why it doesn't work but basically the conclusion is that I cannot easily simulate the behaviour of my own definition using the library.

#### Patrick Massot (Nov 04 2020 at 10:28):

That seems 100% fair. The library is meant to handle extremely general stuff, where the addition symbol could mean hundreds of things, it does make things a bit more complicated.

#### Patrick Massot (Nov 04 2020 at 10:29):

The library has this extra has_add layer.

#### Thorsten Altenkirch (Nov 04 2020 at 10:29):

I guess I should have just proven the definitional equations and then used rewrite and completely avoid dsimp?

#### Johan Commelin (Nov 04 2020 at 10:30):

Thorsten Altenkirch said:

I understand partially why it doesn't work but basically the conclusion is that I cannot easily simulate the behaviour of my own definition using the library.

Well... if you dsimp away the has_add.add everywhere, then after that you should be in a state that's similar to your own definition.

#### Johan Commelin (Nov 04 2020 at 10:30):

I don't see why you are ok with dsimping it away in the goal, but don't like the idea of dsimping it away in assumptions as well.

#### Thorsten Altenkirch (Nov 04 2020 at 10:31):

Because I just want to dsimp the goal, that is reduce using definitional equations.

#### Johan Commelin (Nov 04 2020 at 10:34):

Well, if you insist on only dsimping the goal:

namespace test

open nat

theorem add_lneutr : ∀ n : ℕ, 0 + n  = n :=
begin
assume n,
induction n with n' ih,
refl,
revert ih,
intro ih,
rewrite ih,
end

end test


#### Thorsten Altenkirch (Nov 04 2020 at 11:28):

Thank you, but I don't think this is pedagogically helpful.

#### Thorsten Altenkirch (Nov 04 2020 at 11:31):

Ok, I understand that it may be a god idea to package away definitional equalities. However, I do find it useful to be able to apply them easily when defining a function. It does work for my own definition of + but I can't simulate this with the library definition. Maybe for good reasons but this spoils the way I wanted to explain things. I guess maybe what I want to do is to prove the definitional equalities and then add them to dsimp and not to use has_add. How would I go about this?

#### Johan Commelin (Nov 04 2020 at 12:09):

@Thorsten Altenkirch if you want to use the mathlib, then you need to use has_add. And this has_add will be part of the type of ih. I don't see a way around this.

#### Thorsten Altenkirch (Nov 04 2020 at 12:26):

So basically I shouldn't use dsimp but prove the definitional equalities and then rewrite with them?

#### Thorsten Altenkirch (Nov 04 2020 at 12:28):

I mean I don't want to use the math lib when I am re-proving that Nat is a semiring - obviously. But once we have done this I am happy to use ring. However, I would like that the tactics I have introduced before still work. If I understand you correctly, then basically I shouldn't use dsimp?

#### Johan Commelin (Nov 04 2020 at 12:30):

Thorsten Altenkirch said:

So basically shouldn't use dsimp but prove the definitional equalities and then rewrite with them?

This will not help you if you don't want to rewrite at ih.

#### Thorsten Altenkirch (Nov 04 2020 at 12:33):

I mean

theorem add_succ : ∀ m n : ℕ, m + succ n = succ (m + n) :=
begin
assume m n,
reflexivity,
end

theorem add_lneutr : ∀ n : ℕ, 0 + n  = n :=
begin
assume n,
induction n with n' ih,
refl,
rewrite ih,
end


#### Johan Commelin (Nov 04 2020 at 12:35):

Ooh, ok, that would work yes. Because add_succ mentions + on both sides

#### Thorsten Altenkirch (Nov 04 2020 at 12:39):

I better don't comment on lean's notation mechanism. Seriously, have a look at agda...

#### Johan Commelin (Nov 04 2020 at 12:41):

Seriously, we are all waiting for Lean 4 to happen (-;

#### Johan Commelin (Nov 04 2020 at 12:42):

Also, seriously, I have no idea whether agda's notation mechanism can deal with an algebraic hierarchy similar to what we have in mathlib. (But that's mainly because I have no experience with agda at all.)

#### Reid Barton (Nov 04 2020 at 14:20):

Thorsten, this doesn't really have to do with notation at all, but rather type classes.

#### Reid Barton (Nov 04 2020 at 14:22):

The global + notation refers to has_add.add not (say) nat.add. The cost is that there is this extra layer of indirection which may need to be unfolded. The gain is that we can use + everywhere and it just works, and we can use a single set of lemmas like add_zero to reason about it.

#### Reid Barton (Nov 04 2020 at 14:23):

From what I have seen of Agda, it doesn't attempt to address this at all.

#### Johan Commelin (Nov 04 2020 at 15:05):

@Thorsten Altenkirch In Agda, can I say: "let G be an additive group", and use + for its group operation?

#### Reid Barton (Nov 04 2020 at 15:06):

or "let R and S be rings, M an R-module and N an S-module" and then use + for addition in all of them?

#### Reid Barton (Nov 04 2020 at 15:09):

but just writing expressions is only half the story--we also want to uniformly reason about these situations by rewriting with add_comm, or using tactics like abel

#### Kevin Lacker (Nov 04 2020 at 20:13):

pedagogically I would just avoid redefining the + syntax - you are running into extra weirdness because of it, it's fundamentally not a very basic part of the programming language, so you're kind of running into these weird meta-type-problem things and your students will run into them too. if you want to prove basic arithmetic stuff in order to teach how it works, just stick with calling it add

#### Mario Carneiro (Nov 04 2020 at 20:49):

and/or make a local notation to clobber the global + to make it look good

Last updated: May 08 2021 at 09:11 UTC