Understanding field_simp

Stream: new members

[Sabbir Rahman]

I am trying to get an intuition for how field_simp works and tried out lots of examples and I really can't seem to get a good mental model of when field_simp will work. So any help on understanding will be good.

import Mathlib

example (a b: ℝ) (ha: a ≠ 0) (hb: b ≠ 0) : a * b / a / b = 1 := by
  field_simp    -- easy, cancels stuff

example (a b: ℝ) (ha: a ≠ 0) (hb: b ≠ 0) : a * b / b / a = 1 := by
  field_simp    -- denominators were reordered, understandable

example (a b: ℝ) (ha: a ≠ 0) (hb: b ≠ 0) : 1 / a / b * a * b = 1 := by
  field_simp    -- still understandable

example (a b: ℝ) (ha: a ≠ 0) (hb: b ≠ 0) : 1 / a / b * b * a = 1 := by
  field_simp    -- kinda confused now, I though denominators can be reordered
  sorry

example (a b: ℝ) (ha: a ≠ 0) (hb: b ≠ 0) : a * b / (a * b) = 1 := by
  field_simp    -- assuming field_simp figured out (a*b) is invertible

example (a b: ℝ) (ha: a ≠ 0) (hb: b ≠ 0) : a * b / (b * a) = 1 := by
  field_simp    -- kinda understandable, won't reorder inside products
  ring

example (a b c :ℝ) (hc: c ≠ 0) (h : a * c = (-2) * b * c) : a = 2 * b := by
  field_simp at h -- why does this bring out a Or result, why can't it see the hc prop
  sorry

example (a b c :ℝ) (hc: c ≠ 0) (h : a * c = 2 * b * c) : a = 2 * b := by
  field_simp [hc] at h    -- it works if I give the hc
  assumption

example (a b c :ℝ) (hc: c ≠ 0) (h : a * c = (-2) * b * c) : a = 2 * b := by
  field_simp [hc] at h    -- but if -2 is used, giving hc also doesn't work
  sorry

example (a b c :ℝ) (hc: c ≠ 0) (h : a * c = (-2) * b * c) : a = -4 * b := by
  calc
    a = a * c / c := by field_simp
    _ = (-2) * b * c / c := by rw[h]
    _ = (-2) * b := by field_simp
  -- but using individual steps in calc works despite -2

In particular, why can it reorder denominators sometimes and sometimes it can't. And why does (-2) mess up the ability to do field_simp?

[Kevin Buzzard]

example (a b: ℝ) (ha: a ≠ 0) (hb: b ≠ 0) : 1 / a / b * b * a = 1 := by
  field_simp    -- kinda confused now, I though denominators can be reordered
  sorry

The workflow is field_simp; ring, but for particularly simple examples you're lucky enough that simp can solve them so you don't need ring. I feel like the question should really be "why did I not have to use ring before", not "why do I have to use it now". The job of field_simp is to clear denominators, not prove theorems.

[Kevin Buzzard]

example (a b c :ℝ) (hc: c ≠ 0) (h : a * c = (-2) * b * c) : a = 2 * b := by
  field_simp at h -- why does this bring out a Or result, why can't it see the hc prop
  sorry

The job of field_simp is to clear denominators, not to solve this goal. field_simp at h is the same as simp at h here.

[Kevin Buzzard]

example (a b c :ℝ) (hc: c ≠ 0) (h : a * c = 2 * b * c) : a = 2 * b := by
  field_simp [hc] at h    -- it works if I give the hc
  assumption

That's because simp works, this has nothing to do with field_simp. field_simp is "simp plus extra rules to clear denominators". You use field_simp if your goal has a / in and the denominator is known to be non-zero; its job is to clear it by multiplying up.

[Sabbir Rahman]

I see now, I had mistakenly thought field_simp also cancels out terms from two side of equation. I realize now that simp was doing that. Thanks