Something missing from `norm_cast`?

Stream: general

[Heather Macbeth]

I'd have thought norm_cast or simp could do this, but seemingly not -- is there a missing lemma in norm_cast's instructions perhaps?

import data.real.basic

example (a : ℝ) : a + -1 = a - 1 :=
begin
  norm_cast,
  -- ⊢ a + ↑(int.neg_of_nat 1) = a - 1
end

[Kevin Buzzard]

This is the dreaded sub_eq_add_neg, right? The .symm of your goal was a simp lemma in core for years and it drove everyone nuts -- I think it was one of the first things changed when we forked!

[Heather Macbeth]

Oh! So I have to provide sub_eq_add_neg explicitly or invoke abel?

[Heather Macbeth]

Strange I haven't hit this before!

[Anne Baanen]

Should we add add_neg_eq_sub as a simp lemma instead? The main objection I can think of is that this would be asymmetric with the multiplicative version: presumably we don't want to simp x * y⁻¹ to x / y.

[Kevin Buzzard]

I am still amazed about how I look at the multiplicative and the additive questions, both formally isomorphic, and yet immediately come to "obvious" distinct conclusions. Maybe it's something to do with addition often being commutative in practice and multiplication often being not commutative

[Damiano Testa]

I completely agree with Kevin's point! If x / y was written as x * (1 / y), I could bring myself to viewing this as an "only slightly worst version of x * y⁻¹"!

[Anne Baanen]

I was suddenly reminded of "Mathematics is the art of giving different names to the same thing" (or was it "giving the same name to different things"? eh, both are the same) :grinning:

[Damiano Testa]

Mostly for my own clarification, but the issue with making only one of the additive/multiplicative simp is that then to_additive might fail to produce an additive proof out of a correct multiplicative one?

E.g. simp could solve one version, but not the other, right?

[Floris van Doorn]

Having a difference in simp lemmas should not confuse to_additive. It traverses the fully elaborated multiplicative term, where simp lemmas are irrelevant.

[Johan Commelin]

I think that will actually not be a problem. Because to_additive operates at a lower level. It doesn't replay simp, but it translates the proof terms.

[Floris van Doorn]

That said, I'm not sure whether I like this asymmetry.

[Damiano Testa]

Floris, Johan, thank you for the explanation: it makes more sense now!

[Kevin Buzzard]

Floris van Doorn said:

That said, I'm not sure whether I like this asymmetry.

The only justification would be "sub becomes more important when things are commutative" and I don't know whether this is even true or whether it's just some incorrect thing I've picked up.