Zulip Chat Archive

Stream: new members

Topic: dsimp strange behaviour


view this post on Zulip Thorsten Altenkirch (Nov 04 2020 at 09:50):

open nat
open has_add

theorem add_lneutr :  n : , 0 + n  = n :=
begin
  assume n,
  induction n with n' ih,
  refl,
  dsimp [(+),add],
  rewrite ih,
end

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

view this post on Zulip Johan Commelin (Nov 04 2020 at 09:55):

I can't reproduce.

view this post on Zulip Johan Commelin (Nov 04 2020 at 09:55):

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

view this post on Zulip Johan Commelin (Nov 04 2020 at 09:56):

Copy-pasto... let me try again

view this post on Zulip Johan Commelin (Nov 04 2020 at 09:57):

Now it just hangs... with the import

view this post on Zulip 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.

view this post on Zulip Shing Tak Lam (Nov 04 2020 at 10:01):

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

open nat
open has_add

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.

view this post on Zulip Patrick Massot (Nov 04 2020 at 10:05):

Oh right. Relying on definitional equality is so weird.

view this post on Zulip Patrick Massot (Nov 04 2020 at 10:06):

(This case of associativity is indeed definitional)

view this post on Zulip 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).

view this post on Zulip 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,
  dsimp [(+),add],
  rewrite ih,
end

end test

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Thorsten Altenkirch (Nov 04 2020 at 10:14):

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

view this post on Zulip 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,
  dsimp [(+),add],
  rewrite ih,
end

end test

fails.

view this post on Zulip Patrick Massot (Nov 04 2020 at 10:15):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Nov 04 2020 at 10:16):

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

view this post on Zulip 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,
  dsimp [(+),nat.add],
  rewrite ih,
end

end test

view this post on Zulip Thorsten Altenkirch (Nov 04 2020 at 10:17):

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

view this post on Zulip Johan Commelin (Nov 04 2020 at 10:18):

Why do you want to use dsimp instead of show?

view this post on Zulip Thorsten Altenkirch (Nov 04 2020 at 10:18):

Maybe because I don't know show?

view this post on Zulip Patrick Massot (Nov 04 2020 at 10:18):

It's the same as change.

view this post on Zulip Patrick Massot (Nov 04 2020 at 10:18):

Do you understand what I wrote about refolding?

view this post on Zulip Thorsten Altenkirch (Nov 04 2020 at 10:19):

Because I just want lean to simplify the term.

view this post on Zulip Patrick Massot (Nov 04 2020 at 10:19):

No, you don't want to simplify

view this post on Zulip Patrick Massot (Nov 04 2020 at 10:19):

You want to unfold and then refold.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Thorsten Altenkirch (Nov 04 2020 at 10:20):

No I am using emacs.

view this post on Zulip Johan Commelin (Nov 04 2020 at 10:20):

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

view this post on Zulip Johan Commelin (Nov 04 2020 at 10:20):

Your students will love it

view this post on Zulip Patrick Massot (Nov 04 2020 at 10:21):

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

view this post on Zulip Thorsten Altenkirch (Nov 04 2020 at 10:21):

They use VScode anyway. At leats some of them.

view this post on Zulip 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?

view this post on Zulip Thorsten Altenkirch (Nov 04 2020 at 10:21):

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

view this post on Zulip Patrick Massot (Nov 04 2020 at 10:21):

You need to understand the meaning of notations there.

view this post on Zulip 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?

view this post on Zulip Thorsten Altenkirch (Nov 04 2020 at 10:22):

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

view this post on Zulip 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

view this post on Zulip Thorsten Altenkirch (Nov 04 2020 at 10:22):

How come it works for my own definition?

view this post on Zulip Johan Commelin (Nov 04 2020 at 10:23):

Is your own definition using + notation?

view this post on Zulip Johan Commelin (Nov 04 2020 at 10:23):

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

view this post on Zulip Patrick Massot (Nov 04 2020 at 10:23):

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

view this post on Zulip Patrick Massot (Nov 04 2020 at 10:23):

Johan, I already told all that to Thorsten.

view this post on Zulip 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,
  dsimp [(+),nat.add],
  rewrite ih,
end

end test

works

view this post on Zulip Johan Commelin (Nov 04 2020 at 10:24):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 04 2020 at 10:24):

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

view this post on Zulip Johan Commelin (Nov 04 2020 at 10:25):

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

view this post on Zulip 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 +?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Nov 04 2020 at 10:29):

The library has this extra has_add layer.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Thorsten Altenkirch (Nov 04 2020 at 10:31):

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

view this post on Zulip 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,
  dsimp [(+),nat.add],
  intro ih,
  rewrite ih,
end

end test

view this post on Zulip Thorsten Altenkirch (Nov 04 2020 at 11:28):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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 add_succ,
  rewrite ih,
end

view this post on Zulip Johan Commelin (Nov 04 2020 at 12:35):

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

view this post on Zulip Thorsten Altenkirch (Nov 04 2020 at 12:39):

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

view this post on Zulip Johan Commelin (Nov 04 2020 at 12:41):

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

view this post on Zulip 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.)

view this post on Zulip Reid Barton (Nov 04 2020 at 14:20):

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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Nov 04 2020 at 14:23):

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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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