Discharger for field_simp tactic

The field_simp tactic (implemented downstream from this file) clears denominators in algebraic expressions. In order to do this, the denominators need to be certified as nonzero. This file contains the discharger which carries out these checks.

Currently the discharger tries four strategies:

1. assumption
2. positivity
3. norm_num
4. simp with the same simp-context as the field_simp call which invoked it

TODO: Ideally the discharger would be just positivity (which, despite the name, has robust handling of general ≠ 0 goals, not just > 0 goals). We need the other strategies currently to get (a cheap approximation of) positivity on fields without a partial order.

The refactor of positivity to avoid a partial order assumption would be large but not fundamentally difficult.

Main declarations

• Mathlib.Tactic.FieldSimp.discharge: the discharger, of type Expr → SimpM (Option Expr)

• field_simp_discharge: tactic syntax for the discharger (most useful for testing/debugging)

partial def Mathlib.Tactic.FieldSimp.discharge (prop : Lean.Expr) : Lean.Meta.SimpM (Option Lean.Expr)

Default discharge strategy for field and field_simp: try to solve the (in)equality prop, of the form t = 0 or t > 0, by one of the following strategies:

• Use an assumption from the context.
• Use the norm_num tactic.
• Use the positivity tactic.
• Use the simp tactic with discharge as discharger and lemmas stating:
  • 2 ≠ 0, 3 ≠ 0, 4 ≠ 0
  • x ≠ 0 → y ≠ 0 → x * y ≠ 0
  • a ≠ 0 → a ^ n ≠ 0 (for n : ℕ and n : ℤ)
  • ↑n + 1 ≠ 0, if n : ℕ and the field has characteristic 0.

If none of the strategies finds a proof for prop, the result is none.

def Mathlib.Tactic.FieldSimp.tacticField_simp_discharge : Lean.ParserDescr

Default discharge strategy for field and field_simp: try to solve the (in)equality prop, of the form t = 0 or t > 0, by one of the following strategies:

• Use an assumption from the context.
• Use the norm_num tactic.
• Use the positivity tactic.
• Use the simp tactic with discharge as discharger and lemmas stating:
  • 2 ≠ 0, 3 ≠ 0, 4 ≠ 0
  • x ≠ 0 → y ≠ 0 → x * y ≠ 0
  • a ≠ 0 → a ^ n ≠ 0 (for n : ℕ and n : ℤ)
  • ↑n + 1 ≠ 0, if n : ℕ and the field has characteristic 0.

If none of the strategies finds a proof for prop, the result is none.

Equations

• One or more equations did not get rendered due to their size.