simp non-confluence

Stream: mathlib4

[Michael Stoll]

import Mathlib

example (f : Polynomial ℤ) : Polynomial.coeff (Polynomial.C (Polynomial.coeff f 0)) 1 = 0 := by
  -- simp?  says simp only [eq_intCast]
    -- ⊢ Polynomial.coeff (↑(Polynomial.coeff f 0)) 1 = 0
  simp? [-eq_intCast] says simp only [Polynomial.coeff_C_succ] -- success!

It looks like some simp lemmas are missing to make things confluent here.

[Ruben Van de Velde]

See also https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Polynomial.20coefficient/near/396948492

[Michael Stoll]

@Alex J. Best Maybe you can add a couple more lemmas?

[Kevin Buzzard]

I found another simp non-confluence issue.

import Mathlib

example (x : ℝ) : (Real.exp x : ℂ).re = Real.exp x := by
  /-
  `simp` gives
  ⊢ (Complex.exp ↑x).re = Real.exp x
  `simp?` gives
  Try this: simp only [Complex.ofReal_exp]
  -/
  simp [-Complex.ofReal_exp] -- success

Here is my proposed fix:

import Mathlib

@[simp] theorem Complex.re_exp (x : ℝ) : (Complex.exp x).re = Real.exp x := by
  simp [← Complex.ofReal_exp]

example (x : ℝ) : (Real.exp x : ℂ).re = Real.exp x := by
  simp -- now works

Is this the correct fix? Should we also have

-- example (x : ℝ) : (Real.sin x : ℂ).re = Real.sin x := by simp -- :-(

@[simp] theorem Complex.re_sin (x : ℝ) : (Complex.sin x).re = Real.sin x := by
  simp [← Complex.ofReal_sin]

example (x : ℝ) : (Real.sin x : ℂ).re = Real.sin x := by simp -- :-)

-- example (x : ℝ) : (Real.cos x : ℂ).re = Real.cos x := by simp -- :-(

@[simp] theorem Complex.re_cos (x : ℝ) : (Complex.cos x).re = Real.cos x := by
  simp [← Complex.ofReal_cos]

example (x : ℝ) : (Real.cos x : ℂ).re = Real.cos x := by simp -- :-)

? Are the names OK? Are there any more functions for which we need these (if my diagnosis and fix is OK)?

[Kevin Buzzard]

One sign that this is going in the right direction is that with these lemmas added we have

import Mathlib

@[simp] theorem Complex.re_exp (x : ℝ) : (Complex.exp x).re = Real.exp x := by
  simp [← Complex.ofReal_exp]

@[simp] theorem Complex.re_sin (x : ℝ) : (Complex.sin x).re = Real.sin x := by
  simp [← Complex.ofReal_sin]

@[simp] theorem Complex.re_cos (x : ℝ) : (Complex.cos x).re = Real.cos x := by
  simp [← Complex.ofReal_cos]

example : (-1 : ℝ) ^ (1 / 3 : ℝ) = 1 / 2 := by
  simp [Real.rpow_def, Complex.cpow_def_of_ne_zero, Complex.log_neg_one, -Complex.ofReal_inv]
  rw [mul_right_comm, Complex.exp_mul_I]
  norm_cast
  rw [← div_eq_mul_inv]
  simp

whereas my previous effort was far worse. The -Complex.ofReal_inv is to work around this issue.

[Eric Wieser]

These should be called re_exp_ofReal etc, not just re_exp

[Eric Wieser]

Is docs#Complex.ofReal_exp just a bad simp lemma?

[Kevin Buzzard]

It's definitely a good norm_cast lemma (and my understanding of norm_cast is that it should be this way around). My experiments with ofReal_cos was that it was rewritten forwards more than it was rewritten backwards, but it's still rewritten backwards a fair few times (of course it might be being rewritten forwards many times in simps). I think there is no good direction really, this is exactly why we have both norm_cast and push_cast.

[Kevin Buzzard]

@Mario Carneiro you understand this stuff well, do you have an opinion on whether docs#Complex.ofReal_exp should be a simp lemma? I remember discussing this stuff with you before norm_cast existed and you had a clear opinion that it wasn't simps job to do norm_cast and push_cast and we needed a new tactic (and this is why we got them). But are you clear on how the tagging should work?

[Kevin Buzzard]

Does my fix not scale? Is that the issue?

[Mario Carneiro]

it seems good to me, that is indeed the lemma you need to fix the non-confluence

[Eric Wieser]

Yes, the new lemmas is the right lemma to have assuming the original one should be simp

[Eric Wieser]

Do you also think the existing lemma is correct in being tagged simp, Mario?

[Mario Carneiro]

regarding which direction is right, I think the precedent from nat->int casts is that simp pushes casts to the leaves, so Complex.ofReal_exp makes sense from that perspective. But .re is a function which goes the other way, making it play a similar role to the int less equal operation which originally motivated norm_cast

[Mario Carneiro]

Actually I guess the real problem is that we don't have a simp lemma for (Complex.sin z).re, presumably because the formula is too much of a mess to be a good idea in general

[Mario Carneiro]

if it wasn't for that, .re would get evaluated recursively over a complex number expression (i.e. also getting pushed to the leaves)

[Kevin Buzzard]

$Re(e^{z})=e^{Re(z)}\cos(Im(z))$ and $Im(e^z)=e^{Re(z)}\sin(Im(z))$ and you can get it from that, it shouldn't be too bad.

[Kevin Buzzard]

Knuth would rather we said $\Re(e^{z})=e^{\Re(z)}\cos(\Im(z))$ and $\Im(e^z)=e^{\Re(z)}\sin(\Im(z))$ but this was one design decision in $\TeX$ which I was never mad keen on.

[Mario Carneiro]

I don't mean we don't have a theorem, I assume we do but it's not a simp lemma

[Mario Carneiro]

also I was thinking specifically about sin/cos, not exp

[Kevin Buzzard]

yeah but they're defined in terms of exp as you well know

[Mario Carneiro]

exp has less messy equations indeed

[Mario Carneiro]

what I mean is that if you had a (sin z).re in your goal you might not like lean expanding it out to exponentials

[Mario Carneiro]

which is why it should be a theorem but not a simp lemma, so you choose to use it explicitly

[Kevin Buzzard]

I think Re(sin(z)) is (modulo errors) cosh(Im(z))sin(Re(z))

[Kevin Buzzard]

which at least passes the sanity check when z is real, as cosh(0)=1

[Mario Carneiro]

Is (z * w).re a simp lemma?

[Mario Carneiro]

I guess these formulas are not much worse than the one for multiplication

[Aaron Liu]

Mario Carneiro said:

Is (z * w).re a simp lemma?

yes (docs#Complex.mul_re)

[Mario Carneiro]

If you had Re(sin(z)) = cosh(Im(z))sin(Re(z)) as a simp lemma, then Re(sin(x)) would eventually work its way to sin(x)

[Kevin Buzzard]

Aaron Liu said:

Mario Carneiro said:

Is (z * w).re a simp lemma?

yes (docs#Complex.mul_re)

That was part of my first mathlib PR ;-) (which you reviewed!)

[Jireh Loreaux]

That simp lemma has bothered me on many occasions. :laughing:

[Yaël Dillies]

Me too! :grinning:

[Kevin Buzzard]

Well I can't really claim that I knew what I was doing in 2017. IIRC it's really useful to have it as a "temporary simp lemma" in order to prove e.g. multiplication on $\mathbb{C}$ is associative by checking real and imaginary parts (you want the proof to be ext; simp; ring). But then later on it might become a burden?