why norm_num after `have x: Nat.Odd (2*n + 1) := by use n`?

Stream: new members

[rzeta0]

What does the norm_num do in the following, and why is it needed?

have x: Nat.Odd (2*n + 1) := by use n; norm_num

Here is a simpler example:

have x: Nat.Odd 13 := by use 6; norm_num

In my mind, the use should be sufficient to instantiate the "there exists" definition of Odd.

In the second example, the result would be 2*6 + 1 and I can maybe see the norm_num is required to resolve this to 13.

But in the first example, use n instantiate the existence definition to 2*n+1 and it can't be resolved numerically any further. The comparison for equality is lexical in my inexpert opinion. So I can't see what norm_num does.

(the goal state already has n: ℕ)

[Kevin Buzzard]

import Mathlib

example (n : ℕ) : 2 * n + 1 = 2 * n + 1 := by
  norm_num -- silly proof because this goal is not remotely appropriate for `norm_num`...

example (n : ℕ) : 2 * n + 1 = 2 * n + 1 := by
  simp -- ...but `norm_num` tries simp...

example (n : ℕ) : 2 * n + 1 = 2 * n + 1 := by
  rfl -- ...and `simp` tries a weak `rfl`.

[rzeta0]

So I interpret your examples as illustrating that norm_numis actually being too clever in an invisible way by doing algebraic simplification.

Is that right?

(I seem to be getting caught by tactics being over-clever recently...)

[Kevin Buzzard]

If you ctrl-click on norm_num then you jump to its definition:

elab (name := normNum)
    "norm_num" cfg:optConfig only:&" only"? args:(simpArgs ?) loc:(location ?) : tactic =>
  elabNormNum cfg args loc (simpOnly := only.isSome) (useSimp := true)

and whilst this is meta gobble-de-gook to me, you can see that at the very end of the definition it says useSimp := true which is an indication that norm_num will be using simp at some point. The point is that in practice people want to prove theorems as quickly as possible and so tactics are written with this in mind (for example rw tries rfl etc). Just because a tactic closes the goal doesn't mean that it's the best tactic to close the goal. An extreme example would be aesop, an often-slow tactic capable of doing a huge amount of heavy lifting and which will close goals which many other tactics will solve, simply because it tries a ton of them!

[Kyle Miller]

In particular, I think Kevin is saying that norm_num works because in the end it's trying rfl, and rfl works. Just because a tactic works (like norm_num) doesn't mean that it's necessary for the job.

norm_num is not appropriate for tasks that involve variables. It's for normalizing numbers. If it happens to work in other cases, then usually another tactic would have been more appropriate.

[rzeta0]

Kyle - agreed, it isn't appropriate when there is a variable.

What would be a better way to close:

have x: Nat.Odd (2*n + 1) := by use n; norm_num

(note I haven't learned rfl in MoP yet, perhaps I should)

[Kevin Buzzard]

use n; rfl?

[rzeta0]

I guess I better learn about rfl.

I've just reached the end of Chapter 4 of MoP (including all the exercises) and we haven't come across rfl yet.

[Julian Berman]

(It's a lot better to include an #mwe in your questions than a non-working snippet even with the goal state)

rzeta0 said:

The comparison for equality is lexical in my inexpert opinion.

This is a pretty decent first approximation for what rfl means, so you already kind of know it, just now you know it's name!

[Ruben Van de Velde]

I don't know what Nat.Odd is, but I encourage using norm_num rather than rfl for evaluating numeric expressions