feat(Tactic): add finiteness tactic (#18034)

Upstreamed from the [PFR](https://github.com/teorth/pfr) project.

From PFR, Carleson, GibbsMeasure

Co-authored-by: Heather Macbeth <[email protected]>



Co-authored-by: Pietro Monticone <[email protected]>

Archive/Wiedijk100Theorems/BirthdayProblem.lean

@@ -76,12 +76,9 @@ theorem birthday_measure :
     · rw [Fintype.card_embedding_eq, Fintype.card_fin, Fintype.card_fin]
       rfl
   rw [this, ENNReal.lt_div_iff_mul_lt, mul_comm, mul_div, ENNReal.div_lt_iff]
-  rotate_left
-  iterate 2 right; norm_num
-  · decide
-  iterate 2 left; norm_num
-  simp only [Fintype.card_pi]
-  norm_num
+  all_goals
+    simp only [Fintype.card_pi, Fintype.card_fin, Finset.prod_const, Finset.card_univ]
+    norm_num
 
 end MeasureTheory
 

Mathlib.lean

@@ -4413,6 +4413,8 @@ import Mathlib.Tactic.FailIfNoProgress
 import Mathlib.Tactic.FieldSimp
 import Mathlib.Tactic.FinCases
 import Mathlib.Tactic.Find
+import Mathlib.Tactic.Finiteness
+import Mathlib.Tactic.Finiteness.Attr
 import Mathlib.Tactic.FunProp
 import Mathlib.Tactic.FunProp.Attr
 import Mathlib.Tactic.FunProp.ContDiff

Mathlib/Data/ENNReal/Basic.lean

@@ -282,13 +282,15 @@ theorem toNNReal_ne_one : a.toNNReal ≠ 1 ↔ a ≠ 1 :=
 theorem toReal_ne_one : a.toReal ≠ 1 ↔ a ≠ 1 :=
   a.toReal_eq_one_iff.not
 
-@[simp] theorem coe_ne_top : (r : ℝ≥0∞) ≠ ∞ := WithTop.coe_ne_top
+@[simp, aesop (rule_sets := [finiteness]) safe apply]
+theorem coe_ne_top : (r : ℝ≥0∞) ≠ ∞ := WithTop.coe_ne_top
 
 @[simp] theorem top_ne_coe : ∞ ≠ (r : ℝ≥0∞) := WithTop.top_ne_coe
 
 @[simp] theorem coe_lt_top : (r : ℝ≥0∞) < ∞ := WithTop.coe_lt_top r
 
-@[simp] theorem ofReal_ne_top {r : ℝ} : ENNReal.ofReal r ≠ ∞ := coe_ne_top
+@[simp, aesop (rule_sets := [finiteness]) safe apply]
+theorem ofReal_ne_top {r : ℝ} : ENNReal.ofReal r ≠ ∞ := coe_ne_top
 
 @[simp] theorem ofReal_lt_top {r : ℝ} : ENNReal.ofReal r < ∞ := coe_lt_top
 
@@ -306,11 +308,11 @@ theorem toReal_ofReal_eq_iff {a : ℝ} : (ENNReal.ofReal a).toReal = a ↔ 0 ≤
     rw [← h]
     exact toReal_nonneg, toReal_ofReal⟩
 
-@[simp] theorem zero_ne_top : 0 ≠ ∞ := coe_ne_top
+@[simp, aesop (rule_sets := [finiteness]) safe apply] theorem zero_ne_top : 0 ≠ ∞ := coe_ne_top
 
 @[simp] theorem top_ne_zero : ∞ ≠ 0 := top_ne_coe
 
-@[simp] theorem one_ne_top : 1 ≠ ∞ := coe_ne_top
+@[simp, aesop (rule_sets := [finiteness]) safe apply] theorem one_ne_top : 1 ≠ ∞ := coe_ne_top
 
 @[simp] theorem top_ne_one : ∞ ≠ 1 := top_ne_coe
 
@@ -381,9 +383,9 @@ theorem toReal_eq_toReal_iff' {x y : ℝ≥0∞} (hx : x ≠ ⊤) (hy : y ≠ 
 
 theorem one_lt_two : (1 : ℝ≥0∞) < 2 := Nat.one_lt_ofNat
 
-@[simp] theorem two_ne_top : (2 : ℝ≥0∞) ≠ ∞ := coe_ne_top
+theorem two_ne_top : (2 : ℝ≥0∞) ≠ ∞ := coe_ne_top
 
-@[simp] theorem two_lt_top : (2 : ℝ≥0∞) < ∞ := coe_lt_top
+theorem two_lt_top : (2 : ℝ≥0∞) < ∞ := coe_lt_top
 
 /-- `(1 : ℝ≥0∞) ≤ 1`, recorded as a `Fact` for use with `Lp` spaces. -/
 instance _root_.fact_one_le_one_ennreal : Fact ((1 : ℝ≥0∞) ≤ 1) :=
@@ -465,9 +467,17 @@ theorem coe_natCast (n : ℕ) : ((n : ℝ≥0) : ℝ≥0∞) = n := rfl
     ENNReal.ofReal (no_index (OfNat.ofNat n)) = OfNat.ofNat n :=
   ofReal_natCast n
 
-@[simp] theorem natCast_ne_top (n : ℕ) : (n : ℝ≥0∞) ≠ ∞ := WithTop.natCast_ne_top n
+@[simp, aesop (rule_sets := [finiteness]) safe apply]
+theorem natCast_ne_top (n : ℕ) : (n : ℝ≥0∞) ≠ ∞ := WithTop.natCast_ne_top n
+
 @[simp] theorem natCast_lt_top (n : ℕ) : (n : ℝ≥0∞) < ∞ := WithTop.natCast_lt_top n
 
+@[simp, aesop (rule_sets := [finiteness]) safe apply]
+lemma ofNat_ne_top {n : ℕ} [Nat.AtLeastTwo n] : no_index (OfNat.ofNat n) ≠ ∞ := natCast_ne_top n
+
+@[simp]
+lemma ofNat_lt_top {n : ℕ} [Nat.AtLeastTwo n] : no_index (OfNat.ofNat n) < ∞ := natCast_lt_top n
+
 @[simp] theorem top_ne_natCast (n : ℕ) : ∞ ≠ n := WithTop.top_ne_natCast n
 
 @[simp] theorem one_lt_top : 1 < ∞ := coe_lt_top

Mathlib/Data/ENNReal/Inv.lean

@@ -123,6 +123,9 @@ instance : InvolutiveInv ℝ≥0∞ where
 
 theorem inv_ne_top : a⁻¹ ≠ ∞ ↔ a ≠ 0 := by simp
 
+@[aesop (rule_sets := [finiteness]) safe apply]
+protected alias ⟨_, Finiteness.inv_ne_top⟩ := ENNReal.inv_ne_top
+
 @[simp]
 theorem inv_lt_top {x : ℝ≥0∞} : x⁻¹ < ∞ ↔ 0 < x := by
   simp only [lt_top_iff_ne_top, inv_ne_top, pos_iff_ne_zero]

Mathlib/Data/ENNReal/Operations.lean

@@ -169,6 +169,10 @@ theorem not_lt_top {x : ℝ≥0∞} : ¬x < ∞ ↔ x = ∞ := by rw [lt_top_iff
 
 theorem add_ne_top : a + b ≠ ∞ ↔ a ≠ ∞ ∧ b ≠ ∞ := by simpa only [lt_top_iff_ne_top] using add_lt_top
 
+@[aesop (rule_sets := [finiteness]) safe apply]
+protected lemma Finiteness.add_ne_top {a b : ℝ≥0∞} (ha : a ≠ ∞) (hb : b ≠ ∞) : a + b ≠ ∞ :=
+  ENNReal.add_ne_top.2 ⟨ha, hb⟩
+
 theorem mul_top' : a * ∞ = if a = 0 then 0 else ∞ := by convert WithTop.mul_top' a
 
 -- Porting note: added because `simp` no longer uses `WithTop` lemmas for `ℝ≥0∞`
@@ -188,6 +192,9 @@ theorem mul_eq_top : a * b = ∞ ↔ a ≠ 0 ∧ b = ∞ ∨ a = ∞ ∧ b ≠ 0
   WithTop.mul_eq_top_iff
 
 theorem mul_lt_top : a < ∞ → b < ∞ → a * b < ∞ := WithTop.mul_lt_top
+
+-- This is unsafe because we could have `a = ∞` and `b = 0` or vice-versa
+@[aesop (rule_sets := [finiteness]) unsafe 75% apply]
 theorem mul_ne_top : a ≠ ∞ → b ≠ ∞ → a * b ≠ ∞ := WithTop.mul_ne_top
 
 theorem lt_top_of_mul_ne_top_left (h : a * b ≠ ∞) (hb : b ≠ 0) : a < ∞ :=
@@ -308,6 +315,8 @@ theorem sub_top : a - ∞ = 0 := WithTop.sub_top
 -- Porting note: added `@[simp]`
 @[simp] theorem sub_eq_top_iff : a - b = ∞ ↔ a = ∞ ∧ b ≠ ∞ := WithTop.sub_eq_top_iff
 
+-- This is unsafe because we could have `a = b = ∞`
+@[aesop (rule_sets := [finiteness]) unsafe 75% apply]
 theorem sub_ne_top (ha : a ≠ ∞) : a - b ≠ ∞ := mt sub_eq_top_iff.mp <| mt And.left ha
 
 @[simp, norm_cast]

Mathlib/MeasureTheory/Measure/Typeclasses.lean

@@ -53,7 +53,7 @@ theorem measure_lt_top (μ : Measure α) [IsFiniteMeasure μ] (s : Set α) : μ
 instance isFiniteMeasureRestrict (μ : Measure α) (s : Set α) [h : IsFiniteMeasure μ] :
     IsFiniteMeasure (μ.restrict s) := ⟨by simp⟩
 
-@[simp]
+@[simp, aesop (rule_sets := [finiteness]) safe apply]
 theorem measure_ne_top (μ : Measure α) [IsFiniteMeasure μ] (s : Set α) : μ s ≠ ∞ :=
   ne_of_lt (measure_lt_top μ s)
 

Mathlib/Order/BoundedOrder.lean

@@ -6,6 +6,7 @@ Authors: Johannes Hölzl
 import Mathlib.Order.Lattice
 import Mathlib.Order.ULift
 import Mathlib.Tactic.PushNeg
+import Mathlib.Tactic.Finiteness.Attr
 
 /-!
 # ⊤ and ⊥, bounded lattices and variants
@@ -89,6 +90,10 @@ theorem lt_top_of_lt (h : a < b) : a < ⊤ :=
 
 alias LT.lt.lt_top := lt_top_of_lt
 
+attribute [aesop (rule_sets := [finiteness]) unsafe 20%] ne_top_of_lt
+-- would have been better to implement this as a "safe" "forward" rule, why doesn't this work?
+-- attribute [aesop (rule_sets := [finiteness]) safe forward] ne_top_of_lt
+
 end Preorder
 
 variable [PartialOrder α] [OrderTop α] [Preorder β] {f : α → β} {a b : α}
@@ -134,6 +139,7 @@ theorem not_lt_top_iff : ¬a < ⊤ ↔ a = ⊤ :=
 theorem eq_top_or_lt_top (a : α) : a = ⊤ ∨ a < ⊤ :=
   le_top.eq_or_lt
 
+@[aesop (rule_sets := [finiteness]) safe apply]
 theorem Ne.lt_top (h : a ≠ ⊤) : a < ⊤ :=
   lt_top_iff_ne_top.mpr h
 

Mathlib/Tactic.lean

@@ -82,6 +82,8 @@ import Mathlib.Tactic.FailIfNoProgress
 import Mathlib.Tactic.FieldSimp
 import Mathlib.Tactic.FinCases
 import Mathlib.Tactic.Find
+import Mathlib.Tactic.Finiteness
+import Mathlib.Tactic.Finiteness.Attr
 import Mathlib.Tactic.FunProp
 import Mathlib.Tactic.FunProp.Attr
 import Mathlib.Tactic.FunProp.ContDiff

Mathlib/Tactic/Finiteness.lean

@@ -0,0 +1,64 @@
+/-
+Copyright (c) 2023 Heather Macbeth. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Heather Macbeth
+-/
+import Mathlib.Tactic.Positivity.Core
+
+/-!
+# 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`
+* `finiteness?` for the tactic to show what proof it found
+* etc
+* Note that `finiteness` disables `simp`, so `finiteness (add simp [lemma1, lemma2])` does not do
+  anything more than a bare `finiteness`.
+
+We also provide `finiteness_nonterminal` as a version of `finiteness` that doesn't have to close the
+goal.
+
+## TODO
+
+Improve `finiteness` to also deal with other situations, such as balls in proper spaces with
+a locally finite measure.
+-/
+
+open Aesop.BuiltinRules in
+attribute [aesop (rule_sets := [finiteness]) safe -50] assumption intros
+
+set_option linter.unusedTactic false in
+add_aesop_rules safe tactic (rule_sets := [finiteness]) (by positivity)
+
+/-- Tactic to solve goals of the form `*** < ∞` and (equivalently) `*** ≠ ∞` in the extended
+nonnegative reals (`ℝ≥0∞`). -/
+macro (name := finiteness) "finiteness" c:Aesop.tactic_clause* : tactic =>
+`(tactic|
+  aesop $c*
+    (config := { introsTransparency? := some .reducible, terminal := true, enableSimp := false })
+    (rule_sets := [$(Lean.mkIdent `finiteness):ident, -default, -builtin]))
+
+/-- Tactic to solve goals of the form `*** < ∞` and (equivalently) `*** ≠ ∞` in the extended
+nonnegative reals (`ℝ≥0∞`). -/
+macro (name := finiteness?) "finiteness?" c:Aesop.tactic_clause* : tactic =>
+`(tactic|
+  aesop? $c*
+    (config := { introsTransparency? := some .reducible, terminal := true, enableSimp := false })
+    (rule_sets := [$(Lean.mkIdent `finiteness):ident, -default, -builtin]))
+
+/-- Tactic to solve goals of the form `*** < ∞` and (equivalently) `*** ≠ ∞` in the extended
+nonnegative reals (`ℝ≥0∞`). -/
+macro (name := finiteness_nonterminal) "finiteness_nonterminal" c:Aesop.tactic_clause* : tactic =>
+`(tactic|
+  aesop $c*
+    (config := { introsTransparency? := some .reducible, terminal := false, enableSimp := false,
+                 warnOnNonterminal := false  })
+    (rule_sets := [$(Lean.mkIdent `finiteness):ident, -default, -builtin]))

Mathlib/Tactic/Finiteness/Attr.lean

@@ -0,0 +1,10 @@
+/-
+Copyright (c) 2024 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+-/
+import Aesop
+
+/-! # Finiteness tactic attribute -/
+
+declare_aesop_rule_sets [finiteness]

scripts/noshake.json

@@ -266,6 +266,10 @@
    "Mathlib.Analysis.SpecialFunctions.Log.Deriv",
    "Mathlib.Tactic.FunProp",
    "Mathlib.Tactic.FunProp.Differentiable"],
+  "Mathlib.Tactic.Finiteness":
+  ["Mathlib.MeasureTheory.Constructions.Prod.Basic",
+   "Mathlib.Tactic.Finiteness.Attr",
+   "Mathlib.Tactic.Positivity.Core"],
   "Mathlib.Tactic.FinCases": ["Mathlib.Data.Fintype.Basic"],
   "Mathlib.Tactic.Eval": ["Qq.Macro"],
   "Mathlib.Tactic.DeriveToExpr": ["Lean.Elab.Deriving.Ord"],
@@ -330,6 +334,7 @@
   "Mathlib.Order.Filter.ListTraverse":
   ["Mathlib.Control.Traversable.Instances"],
   "Mathlib.Order.Defs": ["Batteries.Tactic.Trans"],
+  "Mathlib.Order.BoundedOrder": ["Mathlib.Tactic.Finiteness.Attr"],
   "Mathlib.Order.Basic": ["Batteries.Tactic.Classical"],
   "Mathlib.NumberTheory.Cyclotomic.Basic": ["Mathlib.Init.Core"],
   "Mathlib.NumberTheory.ArithmeticFunction": ["Mathlib.Tactic.ArithMult"],

test/finiteness.lean

@@ -0,0 +1,26 @@
+import Mathlib.Tactic.Finiteness
+import Mathlib.Data.ENNReal.Real
+import Mathlib.MeasureTheory.Measure.Typeclasses
+
+open MeasureTheory
+open scoped ENNReal
+
+example : (1 : ℝ≥0∞) < ∞ := by finiteness
+example : (3 : ℝ≥0∞) ≠ ∞ := by finiteness
+
+example (a : ℝ) (b : ℕ) : ENNReal.ofReal a + b < ∞ := by finiteness
+
+example {a : ℝ≥0∞} (ha : a ≠ ∞) : a + 3 < ∞ := by finiteness
+example {a : ℝ≥0∞} (ha : a < ∞) : a + 3 < ∞ := by finiteness
+/-- 
+Test that `finiteness_nonterminal` makes progress but does not fail on not 
+closing the goal. 
+-/
+example {a : ℝ≥0∞} (ha : a = 0) : a + 3 < ∞ := by finiteness_nonterminal; simp [ha]
+
+example (a : ℝ) : (ENNReal.ofReal (1 + a ^ 2))⁻¹ < ∞ := by finiteness
+
+example {α : Type*} (f : α → ℕ) : ∀ i, (f i : ℝ≥0∞) ≠ ∞ := by finiteness
+
+example {_ : MeasurableSpace α} (μ : Measure α) [IsFiniteMeasure μ] (s : Set α) : μ s ≠ ∞ := by
+  finiteness