nnnorm and int.nat_abs

Stream: Is there code for X?

[Damiano Testa]

Dear All,

is the lemma below already in mathlib?

Two challenges.

• Can you find a simpler proof?
• Can you find a clunkier proof? :stuck_out_tongue_wink:

Thanks!

import data.real.nnreal
import analysis.normed_space.basic

open_locale nnreal classical

lemma int.nnnorm_eq_nat_abs (n : ℤ) : ∥n∥₊ = n.nat_abs :=
begin
  rw [← norm_to_nnreal],
  ext,
  simp only [real.coe_to_nnreal', max_eq_left, norm_nonneg, nnreal.coe_nat_cast],
  rw [int.norm_eq_abs],
  rw_mod_cast ← n.abs_eq_nat_abs
end

[Kyle Miller]

lemma int.nnnorm_eq_nat_abs (n : ℤ) : ∥n∥₊ = n.nat_abs :=
(nnreal.coe_nat_abs n).symm

[Damiano Testa]

Thank you very much! I had not imagined that the lemma could go the opposite way!

[Kyle Miller]

My high-tech method was that I grepped mathlib for nat_abs and then searched for ∥ in the output (in emacs, when you run a shell command the output goes into an editable and searchable buffer)

[Damiano Testa]

Thank you also for teaching me another way to search the library!

[Damiano Testa]

Working with this, I am always hoping for (nnreal.coe_nat_abs n).symm to be a simp lemma. Am I wrong in thinking that this lemma should be stated in the opposite direction and be simp?

[Kyle Miller]

Here's a simplified proof:

lemma int.nnnorm_eq_nat_abs (n : ℤ) : ∥n∥₊ = n.nat_abs :=
begin
  apply nnreal.eq,
  rw [coe_nnnorm, int.norm_eq_abs, ←int.cast_abs, int.abs_eq_nat_abs, int.cast_coe_nat, nnreal.coe_nat_cast],
end

I did this because the proof of nnreal.coe_nat_abs took advantage of some definitional equalities, and I wanted to be sure there actually were lemmas linking the two sides.

[Kyle Miller]

Damiano Testa said:

Working with this, I am always hoping for (nnreal.coe_nat_abs n).symm to be a simp lemma. Am I wrong in thinking that this lemma should be stated in the opposite direction and be simp?

I'm not sure... Maybe the idea is that when you have a real-valued expression, you'd rather put things into the ∥n∥₊ form since it's more likely that you have expressions involving nnnorm rather than nat_abs?

[Damiano Testa]

Makes sense, thanks! This is not the direction I'm going, but I can see that your point of view is more sensible in general!

[Kevin Buzzard]

The fact that we have both norm_cast and push_cast indicates that mathematicians don't have any hard and fast rules about which way they want to argue. I've also seen examples where when you're making the API you want something to simp in one direction but then in an application you'd rather it went in the other direction

[Damiano Testa]

I did not know that push_cast was a thing! Whenever two expressions look the same, I will add push_cast to the loop of tactics to try to get lean to agree that they are really the same!