Why is this simp lemma failing?

Stream: new members

[Marc Masdeu]

Hi,

I don't understand why this fails:

@[simp] lemma mul_div_eq {a x : ℝ} (h : x ≠ 0) : a * x / x = a :=
begin
    suffices : x / x = 1,
        rw [mul_div_assoc, this, mul_one],
    rw div_eq_one_iff_eq h,
end

example {a x : ℝ} (h : x ≠ 0) : a * x / x = a :=
begin
    simp only [mul_div_eq], -- fails
end

When I look at the trace, I see that it can't prove that x is nonzero, which is in fact a hypothesis in the example.

More generally, I am surprised that it takes quite a bit of effort to prove the following multiplicative identity:

example (x : ℝ) (h : x ≠ 0): 1 / 12 * (x / 2)⁻¹ * x ^ 3 = 1 / 6 * x ^ 2 := sorry

Is there something that I am missing?

Thank you!

[Kevin Buzzard]

[grumble grumble not MWE grumble]

[Anne Baanen]

Presumably simp only [mul_div_eq, h] will work?

[Kevin Buzzard]

It doesn't, but simp only [mul_div_eq h] does.

[Marc Masdeu]

Kevin Buzzard said:

[grumble grumble not MWE grumble]

Yes, I should have sorry'ed the first lemma. But it was 3 lines...

[Kevin Buzzard]

no it's a missing import :-)

[Kevin Buzzard]

Sometimes you get people saying "this doesn't work" and then other people say "yes it does" and it's all because someone posted something without any imports and then other people use different imports and get different behaviour. That's why it's important.

[Marc Masdeu]

I should have known this by now...my apologies. I'll edit it to fix the example.

[Kenny Lau]

Kevin Buzzard said:

[grumble grumble not MWE grumble]

#mwe

[Kevin Buzzard]

So for your example, this should be closed with field_simp [h], ring and I'm surprised it isn't. field_simp is the tactic you're missing, it should clear denominators. But for some reason it's not doing so.

[Kevin Buzzard]

example (x : ℝ) (h : x ≠ 0): 1 / 12 * (x / 2)⁻¹ * x ^ 3 = 1 / 6 * x ^ 2 :=
begin
  have h12x : x * 12 ≠ 0 := mul_ne_zero h (by norm_num),
  field_simp [h12x],
  ring_exp,
end

[Eric Wieser]

Yeah, I was also surprised that I couldn't close this with field_simp

[Kevin Buzzard]

I thought that field_simp knew that 12 wasn't 0 and the product of two nonzero things was nonzero, but apparently it doesn't in this case.

[Marc Masdeu]

OK, I thought that ring would suffice (I'm happy to add some things are nonzero in the hypotheses list).

[Eric Wieser]

Even this didn't work:

example (x : ℝ) (h : x ≠ 0): 1 / 12 * (x / 2)⁻¹ * x ^ 3 = 1 / 6 * x ^ 2 := by {
  have : 12 ≠ 0 := by norm_num,
  field_simp [h, this],
  ring_exp,
}

[Kevin Buzzard]

That's probably the wrong 12

[Marc Masdeu]

About simp: is it possible to make it take the context hypotheses into account when you apply it?

[Kevin Buzzard]

simp *

[Eric Wieser]

Yep, with the right 12 that works:

example (x : ℝ) (h : x ≠ 0): 1 / 12 * (x / 2)⁻¹ * x ^ 3 = 1 / 6 * x ^ 2 := by {
  have : (12 : ℝ) ≠ 0 := by norm_num,
  field_simp [h, this],
  ring_exp,
}

[Kevin Buzzard]

ring doesn't know about division, and division is thorny because of division by zero. field_simp is exactly the tactic which puts things over a common denominator and then clears denominators if it can find proofs that they're nonzero.

[Eric Wieser]

So I guess field_simp doesn't try using norm_num

[Kevin Buzzard]

but it does because there's a 1/6 in there. I think the product is the issue. [Eric seems to be right]

[Marc Masdeu]

Thanks! I'll clear my proofs a bit with this info... Glad to have learned field_simp (which should be called field, right?)

[Kevin Buzzard]

"The fact that a product is nonzero when all factors are, and that a power of a nonzero number is nonzero, are included in the simpset" (from the field_simp docstring)

[Kevin Buzzard]

field_simp doesn't attempt to close the goal like ring does, it only attempts to simplify it by clearing denominators.

[Eric Wieser]

Kevin Buzzard said:

"The fact that a product is nonzero when all factors are, and that a power of a nonzero number is nonzero, are included in the simpset" (from the field_simp docstring)

I guess that description is missing "a nonzero number is nonzero"?

[Kevin Buzzard]

example {a x : ℝ} (h : x ≠ 0) : a * x / x = a :=
begin
    simp *,
end

does work.

[Kevin Buzzard]

As does simp [h]. So it's the simp only which is blocking things. Aah -- squeeze_simp reports that the issue is that the simplifier algorithm also uses not_false_iff and ne.def.

[Marc Masdeu]

I though that simp * applied simp to the goal and to the hypotheses. But I see that it apply simp to the goal using the hypotheses, which is quite different. Thanks!

[Marc Masdeu]

(OK I see, otherwise it's simp at h, my bad.

[Kevin Buzzard]

PS Marc -- Lean already has mul_div_cancel marked as simp so

@[simp] lemma mul_div_eq {a x : ℝ} (h : x ≠ 0) : a * x / x = a :=
begin
  simp [h],
end

works.

[Kevin Buzzard]

Eric you do seem to be right about the 12 though, which really confuses me because the 6 wasn't a problem on the RHS.

[Kevin Buzzard]

Oh I see my mistake -- the 6 doesn't get cancelled but ring deals with it anyway somehow.