Finiteness tactic

This file implements a basic finiteness tactic, designed to solve goals of the form *** < ∞ and (equivalently) *** ≠ ∞ in the extended nonnegative reals (ENNReal, aka ℝ≥0∞).

It works recursively according to the syntax of the expression. It is implemented as an aesop rule set.

Syntax

Standard aesop syntax applies. Namely one can write

• finiteness (add unfold [def1, def2]) to make finiteness unfold def1, def2
• Note that finiteness disables simp, so finiteness (add simp [lemma1, lemma2]) does not do anything more than a bare finiteness.

One can pass additional expressions as local hypotheses: finiteness [c] is equivalent to have := c; finiteness. (This can be combined with the aesop syntax above.)

• finiteness? (supporting the same syntax) shows the proof that finiteness found
• finiteness_nonterminal is a version of finiteness that doesn't have to close the goal.

Note to users: when tagging a lemma for finiteness, prefer tagging a lemma with ≠ ⊤. Aesop can deduce < ∞ from ≠ ∞ safely (Ne.lt_top is a safe rule), but not conversely (ne_top_of_lt is an unsafe rule): in simpler words, aesop tries to use ≠ as its intermediate representation that things are finite, so we do so as well.

TODO

Improve finiteness to also deal with other situations, such as balls in proper spaces with a locally finite measure.

def finiteness : Lean.ParserDescr

finiteness proves goals of the form *** < ∞ and (equivalently) *** ≠ ∞ in the extended nonnegative reals (ℝ≥0∞). Supports passing additional expressions as local hypotheses.

• finiteness? additionally shows the proof that finiteness found
• finiteness_nonterminal is a version of finiteness that may (but doesn't have to) close the goal.

Equations

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

def finiteness? : Lean.ParserDescr

finiteness proves goals of the form *** < ∞ and (equivalently) *** ≠ ∞ in the extended nonnegative reals (ℝ≥0∞). Supports passing additional expressions as local hypotheses.

• finiteness? additionally shows the proof that finiteness found
• finiteness_nonterminal is a version of finiteness that may (but doesn't have to) close the goal.

Equations

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

def finiteness_nonterminal : Lean.ParserDescr

finiteness proves goals of the form *** < ∞ and (equivalently) *** ≠ ∞ in the extended nonnegative reals (ℝ≥0∞). Supports passing additional expressions as local hypotheses.

• finiteness? additionally shows the proof that finiteness found
• finiteness_nonterminal is a version of finiteness that may (but doesn't have to) close the goal.

Equations

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

We register finiteness with the hint tactic.