finiteness tactic

Stream: Polynomial Freiman-Ruzsa conjecture

[Sebastien Gouezel]

@Heather Macbeth , the new version of the finiteness tactic you have cooked up with aesop does not close some goals the naive version used to close. For instance

lemma foo {α Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] (f : α → Set Ω) :
    ∀ i, μ (f i) ≠ ∞ := by finiteness

fails. Do you have an idea how to fix this?

[Heather Macbeth]

I can look later today. I turned off the default Aesop intros rule because it seemed to also be introducing A ≠ ∞ to a hypothesis of A = ∞ and goal of False. There's hopefully a reducibility setting to tweak which avoids this.

[Heather Macbeth]

Note: positivity doesn't do this; eventually we should make a consistent choice for the two tactics.

[Heather Macbeth]

@Sebastien Gouezel Done, https://github.com/teorth/pfr/pull/85

[Sebastien Gouezel]

Thanks a lot! As a test case, can you remove the explicit argument in https://github.com/teorth/pfr/blob/24cfc61a0815fa6be19dd50e6e1e48861f1bf059/PFR/main.lean#L39C5-L39C33?

[Heather Macbeth]

Yes, now added to PR!

[Terence Tao]

Heather Macbeth said:

Yes, now added to PR!

By the way, finiteness worked out of the box when I was proving a lemma and needed that the probability of some event was finite. Not a particularly challenging application, but just wanted to report a use case "in the wild".