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∞). If the goal cannot be proven, finiteness prints a warning and shows its intermediate progress.

This tactic is based on aesop. It calls assumption, intros, positivity, and any lemma or rule added to the finiteness ruleset, except that all simp rules are disabled.

This tactic is extensible. By adding more rules, finiteness can prove more goals. For example:

• @[aesop (rule_sets := [finiteness]) safe 50] lemma ...

• add_aesop_rules safe tactic (rule_sets := [finiteness]) (by ...) (Note that a simp rule cannot be added this way, since all simp rules are disabled.)

• finiteness (clause) customizes the aesop call using the given clause. See aesop documentation for detailed explanation. Note that finiteness disables simp, so finiteness (add simp [lemma1, lemma2]) does not do anything more than a bare finiteness.

• finiteness [t₁, ..., tₙ] adds the terms t₁, ..., tₙ as local hypotheses before applying the search rules.

• finiteness? additionally shows the proof that finiteness found.

• finiteness_nonterminal is a version of finiteness that does not report a warning if it fails 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∞). If the goal cannot be proven, finiteness prints a warning and shows its intermediate progress.

This tactic is based on aesop. It calls assumption, intros, positivity, and any lemma or rule added to the finiteness ruleset, except that all simp rules are disabled.

This tactic is extensible. By adding more rules, finiteness can prove more goals. For example:

• @[aesop (rule_sets := [finiteness]) safe 50] lemma ...

• add_aesop_rules safe tactic (rule_sets := [finiteness]) (by ...) (Note that a simp rule cannot be added this way, since all simp rules are disabled.)

• finiteness (clause) customizes the aesop call using the given clause. See aesop documentation for detailed explanation. Note that finiteness disables simp, so finiteness (add simp [lemma1, lemma2]) does not do anything more than a bare finiteness.

• finiteness [t₁, ..., tₙ] adds the terms t₁, ..., tₙ as local hypotheses before applying the search rules.

• finiteness? additionally shows the proof that finiteness found.

• finiteness_nonterminal is a version of finiteness that does not report a warning if it fails 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∞). If the goal cannot be proven, finiteness prints a warning and shows its intermediate progress.

This tactic is based on aesop. It calls assumption, intros, positivity, and any lemma or rule added to the finiteness ruleset, except that all simp rules are disabled.

This tactic is extensible. By adding more rules, finiteness can prove more goals. For example:

• @[aesop (rule_sets := [finiteness]) safe 50] lemma ...

• add_aesop_rules safe tactic (rule_sets := [finiteness]) (by ...) (Note that a simp rule cannot be added this way, since all simp rules are disabled.)

• finiteness (clause) customizes the aesop call using the given clause. See aesop documentation for detailed explanation. Note that finiteness disables simp, so finiteness (add simp [lemma1, lemma2]) does not do anything more than a bare finiteness.

• finiteness [t₁, ..., tₙ] adds the terms t₁, ..., tₙ as local hypotheses before applying the search rules.

• finiteness? additionally shows the proof that finiteness found.

• finiteness_nonterminal is a version of finiteness that does not report a warning if it fails to close the goal.

Equations

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

We register finiteness with the hint tactic.