simp cancel divide and multiply

Stream: new members

[Chris M]

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]

it's false when c = 0

[Kenny Lau]

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

[Kenny Lau]

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

[Chris M]

ooh i see

[Chris M]

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]

simp * uses all assumptions

[Kenny Lau]

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

[Kenny Lau]

but then why not exact mul_div_cancel' _ h?

[Chris Wong]

Does library_search work in this case?

[Kevin Buzzard]

Hopefully!

[Chris M]

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

[Frédéric Dupuis]

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]

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

[Yury G. Kudryashov]

But it is a medium-scale refactor.