Missing simp lemma

Stream: mathlib4

[Michael Stoll]

Note the following:

import Mathlib

example : (1 / 2 : ℚ) + (1 / 2) = 1 := by
  simp -- leaves `2⁻¹ + 2⁻¹ = 1`
  sorry

example : (1 / 2 : ℚ) + (1 / 2) = 1 := by
  simp [-one_div] -- succeeds using `add_halves`

So it seems that we need 2⁻¹ + 2⁻¹ = 1 as a simp lemma. It currently exists only for docs#ENNReal , for whatever strange reason:

@loogle 2⁻¹ + 2⁻¹ = 1

[loogle]

:search: ENNReal.inv_two_add_inv_two

[Robin Arnez]

norm_num should be sufficient, no?

[Michael Stoll]

But we still want simp to be confluent.

[Robin Arnez]

Yeah, good point

[Robin Arnez]

Yeah we should probably have 2⁻¹ + 2⁻¹ = 1 and 3⁻¹ + 3⁻¹ + 3⁻¹ = 1 corresponding to add_halves and add_thirds

[Kevin Buzzard]

Apparently asking that simp be confluent is asking too much in general?

[Ruben Van de Velde]

It is, but we should still aim for it

[Bolton Bailey]

I got annoyed that sin (π / 2) = 1 but sin (π * 2⁻¹) = 1 wasn't so I filed #25912 and @Yaël Dillies suggested I could try making the reverse of div_eq_mul_inv a simp lemma. This would mean that 2⁻¹ would simplify to 1 / 2. Perhaps at that point we could make div_add_div_same a simp lemma to make 2⁻¹ + 2⁻¹ -> 1/2 + 1/2 -> 1+1/2 -> 1 happen automatically.

[Yaël Dillies]

Bolton Bailey said:

This would mean that 2⁻¹ would simplify to 1 / 2.

What?

[Bolton Bailey]

Oh sorry, maybe I am still stuck on my earlier misunderstanding of what you were saying, you were saying that a * b.inv should simplify to a / b, but that a.inv shouldn't simplify to 1/a right? My bad.

[Bolton Bailey]

Anyway, I had thought it was cleaner to make a⁻¹ simplify to 1 / a, which would just remove expressions involving ⁻¹ from simp normal form entirely. I guess this would mean making inv_eq_one_div simp too

[Yaël Dillies]

Yes, no, that's a step too far IMO

[Kenny Lau]

Kevin Buzzard said:

Apparently asking that simp be confluent is asking too much in general?

Why?

[Kevin Buzzard]

Yeah I was surprised by this but a few months ago I was suggesting some trig lemmas to make simp confluent and this was the response I got. I can't find the thread right now because I'm travelling and on mobile which no longer has a search function?

[Eric Wieser]

I deliberately blocked the update to the new mobile Zulip because of teething issues like that (and losing LaTeX). Their release notes tell you how to manually install the old version

[Eric Wieser]

Bolton Bailey said:

I guess this would mean making inv_eq_one_div simp too

I think we should make it simp in the reverse direction

[Eric Wieser]

The one_divs are quite annoying when using PiLp

[Kenny Lau]

I think either way we'll end up having to change/add a lot of simp lemmas

[Kenny Lau]

I don't see the harm of starting with 2^-1 + 2^-1 = 1