Arithmetic tactics

This file defines the positivity! and arith tactics, which are slight extensions of the existing arithmetic tactics in mathlib (positivity and linarith).

def Tactic.cases_and : Lean.ParserDescr

Equations

• Tactic.cases_and = Lean.ParserDescr.node `Tactic.cases_and 1024 (Lean.ParserDescr.nonReservedSymbol "cases_and" false)

def Tactic.preparePositivity (mvarId : Lean.MVarId) : Lean.MetaM Lean.MVarId

Positivity can only work with goals and hypotheses of the form 0 R x, where R ∈ {<, ≤, ≠}. Our positivity extension is designed to admit hypotheses of the form a R x and x R a where a ≠ 0. For example, 1 ≤ x → 0 ≤ log x. To be able to use positivity, we rewrite 1 ≤ x into 0 ≤ x - 1. This procedure does exactly that, changing goals and hypotheses to make them compatible with positivity.

Equations

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

def Tactic.prepare_positivity : Lean.ParserDescr

Equations

• Tactic.prepare_positivity = Lean.ParserDescr.node `Tactic.prepare_positivity 1024 (Lean.ParserDescr.nonReservedSymbol "prepare_positivity" false)

def Tactic.positivityMaybeNormNum : Lean.Elab.Tactic.TacticM Unit

Call positivity but if the expression has no free variables, we try to apply norm_num first.

Equations

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

def Tactic.positivity : Lean.ParserDescr

Equations

• Tactic.positivity = Lean.ParserDescr.node `Tactic.positivity 1024 (Lean.ParserDescr.nonReservedSymbol "positivity_maybe_norm_num" false)

def tacticPositivity! : Lean.ParserDescr

Extension of positivity with some pre-processing and the option to call norm_num.

Equations

• tacticPositivity! = Lean.ParserDescr.node `tacticPositivity! 1024 (Lean.ParserDescr.nonReservedSymbol "positivity!" false)

def tacticArith : Lean.ParserDescr

Combination of tactics. We try positivity!, then linarith, then norm_num, then simp.

Equations

• tacticArith = Lean.ParserDescr.node `tacticArith 1024 (Lean.ParserDescr.nonReservedSymbol "arith" false)