## Stream: new members

### Topic: Why is this simp lemma failing?

#### Marc Masdeu (Dec 15 2020 at 10:08):

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 (Dec 15 2020 at 10:09):

[grumble grumble not MWE grumble]

#### Anne Baanen (Dec 15 2020 at 10:09):

Presumably simp only [mul_div_eq, h] will work?

#### Kevin Buzzard (Dec 15 2020 at 10:10):

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

#### Marc Masdeu (Dec 15 2020 at 10:14):

Kevin Buzzard said:

[grumble grumble not MWE grumble]

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

#### Kevin Buzzard (Dec 15 2020 at 10:14):

no it's a missing import :-)

#### Kevin Buzzard (Dec 15 2020 at 10:15):

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 (Dec 15 2020 at 10:16):

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

#### Kenny Lau (Dec 15 2020 at 10:16):

Kevin Buzzard said:

[grumble grumble not MWE grumble]

#mwe

#### Kevin Buzzard (Dec 15 2020 at 10:17):

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 (Dec 15 2020 at 10:18):

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 (Dec 15 2020 at 10:19):

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

#### Kevin Buzzard (Dec 15 2020 at 10:19):

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 (Dec 15 2020 at 10:19):

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

#### Eric Wieser (Dec 15 2020 at 10:19):

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 (Dec 15 2020 at 10:20):

That's probably the wrong 12

#### Marc Masdeu (Dec 15 2020 at 10:20):

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

#### Kevin Buzzard (Dec 15 2020 at 10:20):

simp *

#### Eric Wieser (Dec 15 2020 at 10:20):

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 (Dec 15 2020 at 10:21):

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 (Dec 15 2020 at 10:21):

So I guess field_simp doesn't try using norm_num

#### Kevin Buzzard (Dec 15 2020 at 10:21):

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 (Dec 15 2020 at 10:22):

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 (Dec 15 2020 at 10:22):

"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 (Dec 15 2020 at 10:22):

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

#### Eric Wieser (Dec 15 2020 at 10:23):

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 (Dec 15 2020 at 10:25):

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


does work.

#### Kevin Buzzard (Dec 15 2020 at 10:26):

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 (Dec 15 2020 at 10:27):

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 (Dec 15 2020 at 10:28):

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

#### Kevin Buzzard (Dec 15 2020 at 10:28):

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 (Dec 15 2020 at 10:33):

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 (Dec 15 2020 at 10:37):

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

Last updated: May 11 2021 at 23:11 UTC