## Stream: general

### Topic: Something missing from norm_cast?

#### Heather Macbeth (Jul 06 2021 at 23:19):

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 (Jul 06 2021 at 23:21):

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 (Jul 06 2021 at 23:22):

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

#### Heather Macbeth (Jul 06 2021 at 23:22):

Strange I haven't hit this before!

#### Anne Baanen (Jul 07 2021 at 09:05):

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 (Jul 07 2021 at 09:28):

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 (Jul 07 2021 at 09:36):

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 (Jul 07 2021 at 09:50):

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 (Jul 07 2021 at 09:51):

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 (Jul 07 2021 at 09:54):

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 (Jul 07 2021 at 09:54):

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 (Jul 07 2021 at 09:54):

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

#### Damiano Testa (Jul 07 2021 at 09:56):

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

#### Kevin Buzzard (Jul 07 2021 at 09:59):

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.

Last updated: Dec 20 2023 at 11:08 UTC