Stream: new members

Topic: simp cancel divide and multiply

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?

Kenny Lau (Jul 26 2020 at 04:45):

it's false when c = 0

Kenny Lau (Jul 26 2020 at 04:46):

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

Kenny Lau (Jul 26 2020 at 04:46):

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

ooh i see

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?)

Kenny Lau (Jul 26 2020 at 04:49):

simp * uses all assumptions

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']

Kenny Lau (Jul 26 2020 at 04:51):

but then why not exact mul_div_cancel' _ h?

Chris Wong (Jul 26 2020 at 07:03):

Does library_search work in this case?

Hopefully!

Chris M (Jul 26 2020 at 09:51):

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

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


Yury G. Kudryashov (Jul 26 2020 at 21:14):

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

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