Zulip Chat Archive

Stream: new members

Topic: simp cancel divide and multiply


view this post on Zulip Chris M (Jul 26 2020 at 04:43):

Consider the code:

import data.real.basic
import tactic
open function

example {c : } (h : c  0) : surjective (λ x, c * x) :=
begin
  intro b,
  use (b/c),
  simp,
end

this gives the tactic state:

c : ,
h : c  0,
b : 
 c * (b / c) = b

simp is not able to simplify this, I think because there are only theorems that cancel for (a * b) / b = a and (a / b) * b = a. We could add separate lemmas for different cases, but I'm curious why it doesn't just apply associativity?

view this post on Zulip Kenny Lau (Jul 26 2020 at 04:45):

it's false when c = 0

view this post on Zulip Kenny Lau (Jul 26 2020 at 04:46):

LHS = 0 * (b / 0) = 0 * 0 = 0 and RHS = b

view this post on Zulip Kenny Lau (Jul 26 2020 at 04:46):

so you need to tell simp to use h, i.e. simp [h]

view this post on Zulip Chris M (Jul 26 2020 at 04:47):

ooh i see

view this post on Zulip Chris M (Jul 26 2020 at 04:48):

no actually it doesn't seem to do that then either. (also, is there a way to make simp just automatically use all assumptions without having to tell it to?)

view this post on Zulip Kenny Lau (Jul 26 2020 at 04:49):

simp * uses all assumptions

view this post on Zulip Kenny Lau (Jul 26 2020 at 04:50):

apparently mul_div_cancel' is not a simp-lemma so you need simp [h, mul_div_cancel']

view this post on Zulip Kenny Lau (Jul 26 2020 at 04:51):

but then why not exact mul_div_cancel' _ h?

view this post on Zulip Chris Wong (Jul 26 2020 at 07:03):

Does library_search work in this case?

view this post on Zulip Kevin Buzzard (Jul 26 2020 at 08:20):

Hopefully!

view this post on Zulip Chris M (Jul 26 2020 at 09:51):

Shall I add @[simp] to mul_div_cancel' and similar?

view this post on Zulip Frédéric Dupuis (Jul 26 2020 at 14:51):

There is also field_simp that can deal with these division issues pretty well:

example {c : } (h : c  0) : surjective (λ x, c * x) :=
begin
  intro b,
  use (b/c),
  field_simp [h, mul_comm],
end

view this post on Zulip Yury G. Kudryashov (Jul 26 2020 at 21:14):

Probably we should make simp use the simp set used by field_simp.

view this post on Zulip Yury G. Kudryashov (Jul 26 2020 at 21:15):

But it is a medium-scale refactor.


Last updated: May 11 2021 at 13:22 UTC