Zulip Chat Archive

Stream: new members

Topic: Why is this simp lemma failing?


view this post on Zulip 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!

view this post on Zulip Kevin Buzzard (Dec 15 2020 at 10:09):

[grumble grumble not MWE grumble]

view this post on Zulip Anne Baanen (Dec 15 2020 at 10:09):

Presumably simp only [mul_div_eq, h] will work?

view this post on Zulip Kevin Buzzard (Dec 15 2020 at 10:10):

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

view this post on Zulip 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...

view this post on Zulip Kevin Buzzard (Dec 15 2020 at 10:14):

no it's a missing import :-)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Dec 15 2020 at 10:16):

Kevin Buzzard said:

[grumble grumble not MWE grumble]

#mwe

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Eric Wieser (Dec 15 2020 at 10:19):

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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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,
}

view this post on Zulip Kevin Buzzard (Dec 15 2020 at 10:20):

That's probably the wrong 12

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Dec 15 2020 at 10:20):

simp *

view this post on Zulip 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,
}

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Dec 15 2020 at 10:21):

So I guess field_simp doesn't try using norm_num

view this post on Zulip 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]

view this post on Zulip 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?)

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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"?

view this post on Zulip Kevin Buzzard (Dec 15 2020 at 10:25):

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

does work.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Marc Masdeu (Dec 15 2020 at 10:28):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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