'measurability' failing after change to fun_prop

Stream: mathlib4

[Lua Viana Reis]

I'm trying to merge master into #26923. I've run into an issue where a call to measurability is not working anymore, and using git bisect I narrowed it down to this specific commit:

refactor: use `fun_prop` in `measurability` (#30511)

I'm having trouble understanding it enough to #mwe it. I found I can fix the error by applying apply Measurable.sup manually, but the commit message of #30511 makes me think that this error was not expected from the change in the first place. I know a #mwe would be better, but perhaps the diff of the aesop trace outputs below will let someone understand what is going on? Green is the working version before #30511, in red is after #30511. It seems that before #30511, there was this [aesop] ✅️ <norm unfold> step that was removed. Is that expected?

diff -u --label \#\<buffer\ \*diags-Pointwise.lean\<mathlib-butterley\>\*\> --label \#\<buffer\ \*diags-Pointwise.lean\<before-modules-debug\>\*\> /tmp/buffer-content-NHt1Eb /tmp/buffer-content-nO8xIp
--- #<buffer *diags-Pointwise.lean<mathlib-butterley>*>
+++ #<buffer *diags-Pointwise.lean<before-modules-debug>*>
@@ -48,7 +48,7 @@
       ⊢ Measurable ((partialSups (birkhoffSum f φ ∘ Nat.succ)) n ⊔ birkhoffSum f φ (n + 1 + 1))
   [aesop] Metadata
     [aesop] ID: 1
-    [aesop] Pre-normalisation goal (_uniq.8202):
+    [aesop] Pre-normalisation goal (_uniq.66127):
       [aesop] α : Type u_1
           inst : MeasurableSpace α
           f : α → α
@@ -74,7 +74,7 @@
       [aesop]
     [aesop] Unsafe rule queue: <not selected>
     [aesop] Failed rules: <none>
-[aesop] ❌️ (G1) [100.0000%] ⋯ ⊢ Measurable ((partialSups (birkhoffSum f φ ∘ Nat.succ)) n ⊔ birkhoffSum f φ (n + 1 + 1))
+[aesop] ✅️ (G1) [100.0000%] ⋯ ⊢ Measurable ((partialSups (birkhoffSum f φ ∘ Nat.succ)) n ⊔ birkhoffSum f φ (n + 1 + 1))
   [aesop] Initial goal:
         α : Type u_1
         inst : MeasurableSpace α
@@ -88,6 +88,32 @@
   [aesop] ✅️ Normalisation
     [aesop] ❌️ norm|tactic|global|Aesop.BuiltinRules.intros
       [aesop] nothing to introduce
+    [aesop] ✅️ <norm unfold>
+      [aesop] α : Type u_1
+          inst : MeasurableSpace α
+          f : α → α
+          hf : Measurable f
+          φ : α → ℝ
+          hφ : Measurable φ
+          n : ℕ
+          a : Measurable ((birkhoffMax f φ) n)
+          ⊢ Measurable ((partialSups fun x ↦ birkhoffSum f φ x.succ) n ⊔ birkhoffSum f φ (n + 1 + 1))
+    [aesop] ❌️ norm|tactic|global|Aesop.BuiltinRules.intros
+      [aesop] nothing to introduce
+    [aesop] ❌️ <norm unfold>
+      [aesop] nothing to unfold
+    [aesop] ✅️ <norm simp>
+      [aesop] α : Type u_1
+          inst : MeasurableSpace α
+          f : α → α
+          hf : Measurable f
+          φ : α → ℝ
+          hφ : Measurable φ
+          n : ℕ
+          a : Measurable ((birkhoffMax f φ) n)
+          ⊢ Measurable ((partialSups fun x ↦ birkhoffSum f φ (x + 1)) n ⊔ birkhoffSum f φ (n + 1 + 1))
+    [aesop] ❌️ norm|tactic|global|Aesop.BuiltinRules.intros
+      [aesop] nothing to introduce
     [aesop] ❌️ <norm unfold>
       [aesop] nothing to unfold
     [aesop] ❌️ <norm simp>
@@ -101,8 +127,8 @@
         hφ : Measurable φ
         n : ℕ
         a : Measurable ((birkhoffMax f φ) n)
-        ⊢ Measurable ((partialSups (birkhoffSum f φ ∘ Nat.succ)) n ⊔ birkhoffSum f φ (n + 1 + 1))
-  [aesop] ❌️ Safe rules
+        ⊢ Measurable ((partialSups fun x ↦ birkhoffSum f φ (x + 1)) n ⊔ birkhoffSum f φ (n + 1 + 1))
+  [aesop] ✅️ Safe rules
     [aesop] ❌️ safe|tactic|global|Aesop.BuiltinRules.assumption
       [aesop] Tactic `Aesop.BuiltinRules.assumption` failed: no matching assumption found

[Lua Viana Reis]

There is more to the aesop trace outputs, I truncated the diff to this first change because afterwards they both diverge considerably

[Floris van Doorn]

It is possible that fun_prop is slightly weaker than aesop in some cases when working with complicated functions.
In #30511 there was also a lemma that couldn't be tagged with fun_prop (that was formerly tagged with measurability).

Can you try to use aesop? on the working version of your proof and just port that expanded proof to the latest master version? Hopefully that won't break. Then afterwards you can try to see which parts of the expanded proof can be automated by fun_prop (and potentially extract a MWE if fun_prop cannot do something that it should do - but maybe it's just a matter of tagging an extra lemma with @[fun_prop]).

[Lua Viana Reis]

I can fix it, but I was trying to figure out what went wrong in the first place. Since in #30511 it seems that no proofs had to be fixed :confusion:

I will try to find a #mwe

[Lua Viana Reis]

Here is the full aesop trace diff for completeness

aesop-diff.diff

[Floris van Doorn]

The change was definitely not intended to be backwards compatible in all cases, just in most cases (which happens to include all Mathlib-proofs).
It's probably more fruitful to answer the question "how can we ensure that fun_prop(/measurability) can solve your goal on master" than it is to answer "what exactly is different now compared to what aesop used to do" (though an answer to the second question can lead to an answer of the first one).

[Lua Viana Reis]

Here is the #mwe:

import Mathlib

example [MeasurableSpace α] (f g : α → ℝ) (hg : Measurable g) :
    Measurable (f ⊔ g) := by
  let s := f
  have : Measurable s := sorry
  measurability

this works before #30511, but doesn't afterwards.

[Floris van Doorn]

Can you add imports/variables etc to your #mwe?

[Lua Viana Reis]

sorry, this example is not right.

[Floris van Doorn]

It might point at a weakness of fun_prop compared to measurability. This fails:

import Mathlib

example {α : Type*} [MeasurableSpace α] (f g : α → ℝ) (hg : Measurable g) :
    Measurable (f ⊔ g) := by
  let s := f
  have : Measurable s := sorry
  fun_prop

[Lua Viana Reis]

Yes! that was what I found, so I thought that was the issue, but there is something more because measurability with fun_prop still works in this case

[Floris van Doorn]

I'm not sure if we want fun_prop to unfold let-definitions. Tactics like simp used to do that by default, but now also require explicit prompting to be unfolded.

[Floris van Doorn]

Is this important in your use case? Is it easy to rewrite your proof now that you know where the problem lies? It's a bit of an anti-pattern to use let, but also keep using the original definition (though in some cases that might be unavoidable)

[Floris van Doorn]

For example, this just avoids talking about f altogether (though that might not be as easily applicable in your example):

import Mathlib

example {α : Type*} [MeasurableSpace α] (f g : α → ℝ) (hg : Measurable g) :
    Measurable (f ⊔ g) := by
  set s := f -- `set` is like `let` that also replaces `f` with `s` everywhere
  have : Measurable s := sorry
  fun_prop

[Lua Viana Reis]

It's not, actually, debugging this made me realize the proper fix to the previous code in #26923. Instead of

@[measurability]
lemma birkhoffMax_measurable [MeasurableSpace α] {f : α → α} (hf : Measurable f) {φ : α → ℝ}
    (hφ : Measurable φ) {n} : Measurable (birkhoffMax f φ n) := by
  induction n <;> unfold birkhoffMax <;> measurability

it should have unfolded the definition before the induction:

@[measurability]
lemma birkhoffMax_measurable [MeasurableSpace α] {f : α → α} (hf : Measurable f) {φ : α → ℝ}
    (hφ : Measurable φ) {n} : Measurable (birkhoffMax f φ n) := by
  unfold birkhoffMax
  induction n <;> measurability

[Lua Viana Reis]

That's where the problem appeared, because in the induction hypothesis, birkhoffMax was not unfolded (so fun_prop was not being able to use it)