dsimp strange behaviour

Stream: new members

[Thorsten Altenkirch]

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?

[Johan Commelin]

I can't reproduce.

[Johan Commelin]

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

[Johan Commelin]

Copy-pasto... let me try again

[Johan Commelin]

Now it just hangs... with the import

[Patrick Massot]

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]

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.

[Patrick Massot]

Oh right. Relying on definitional equality is so weird.

[Patrick Massot]

(This case of associativity is indeed definitional)

[Patrick Massot]

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]

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.

[Thorsten Altenkirch]

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]

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]

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]

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]

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]

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

[Thorsten Altenkirch]

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.

[Patrick Massot]

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

[Shing Tak Lam]

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

[Patrick Massot]

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

[Thorsten Altenkirch]

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

[Thorsten Altenkirch]

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

[Johan Commelin]

Why do you want to use dsimp instead of show?

[Thorsten Altenkirch]

Maybe because I don't know show?

[Patrick Massot]

It's the same as change.

[Patrick Massot]

Do you understand what I wrote about refolding?

[Thorsten Altenkirch]

Because I just want lean to simplify the term.

[Patrick Massot]

No, you don't want to simplify

[Patrick Massot]

You want to unfold and then refold.

[Patrick Massot]

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]

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]

No I am using emacs.

[Johan Commelin]

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

[Johan Commelin]

Your students will love it

[Patrick Massot]

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

[Thorsten Altenkirch]

They use VScode anyway. At leats some of them.

[Johan Commelin]

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]

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

[Patrick Massot]

You need to understand the meaning of notations there.

[Patrick Massot]

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

[Thorsten Altenkirch]

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

[Johan Commelin]

@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]

How come it works for my own definition?

[Johan Commelin]

Is your own definition using + notation?

[Johan Commelin]

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

[Patrick Massot]

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

[Patrick Massot]

Johan, I already told all that to Thorsten.

[Thorsten Altenkirch]

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

[Johan Commelin]

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

[Patrick Massot]

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]

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

[Johan Commelin]

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

[Thorsten Altenkirch]

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

[Patrick Massot]

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]

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

[Thorsten Altenkirch]

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]

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]

The library has this extra has_add layer.

[Thorsten Altenkirch]

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

[Johan Commelin]

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]

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]

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

[Johan Commelin]

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

[Thorsten Altenkirch]

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

[Thorsten Altenkirch]

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]

@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]

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

[Thorsten Altenkirch]

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]

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]

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

[Johan Commelin]

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

[Thorsten Altenkirch]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Reid Barton]

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]

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

[Johan Commelin]

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

[Reid Barton]

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]

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]

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]

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