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)

Discharge strategy for the field_simp tactic.

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

Discharge strategy for the field_simp tactic.

Equations

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