## 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