Weird behavior of fun_prop

Stream: mathlib4

[Etienne Marion]

Hi! Consider the following #mwe:

import Mathlib.MeasureTheory.Function.LpSeminorm.Defs

open MeasureTheory

variable {Ω ι : Type*} [Fintype ι] {mΩ : MeasurableSpace Ω} {μ : Measure Ω} {X : ι → Ω → ℝ}

example (hX : ∀ i, MemLp (X i) 2 μ) : AEMeasurable (fun ω i ↦ X i ω) μ := by
  fun_prop -- fails, ok

example (hX : ∀ i, MemLp (X i) 2 μ) : AEMeasurable (fun ω i ↦ X i ω) μ := by
  have : ∀ i, AEMeasurable (X i) μ := fun i ↦ (hX i).aestronglyMeasurable.aemeasurable
  fun_prop -- works, ok

example (hX : ∀ i, MemLp (X i) 2 μ) : AEMeasurable (fun ω i ↦ X i ω) μ := by
  have := fun i ↦ (hX i).aestronglyMeasurable.aemeasurable
  fun_prop -- fails, why?

fun_prop works in the second case but not in the third, while if I'm not mistaken the contexts are exactly the same. Any idea of what is going on?

[Aaron Liu]

I thought they were the same too, but I guess not:

elab "t " i:ident : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let hyp ← Lean.Meta.getLocalDeclFromUserName i.getId
    Lean.logInfo hyp.type.ctorName

example (hX : ∀ i, MemLp (X i) 2 μ) : AEMeasurable (fun ω i ↦ X i ω) μ := by
  have : ∀ i, AEMeasurable (X i) μ := fun i ↦ (hX i).aestronglyMeasurable.aemeasurable
  t this -- forallE
  fun_prop -- works, ok

example (hX : ∀ i, MemLp (X i) 2 μ) : AEMeasurable (fun ω i ↦ X i ω) μ := by
  have := fun i ↦ (hX i).aestronglyMeasurable.aemeasurable
  t this -- mvar
  fun_prop -- fails, why?

[Kevin Buzzard]

Oh interesting! Even with pp.all on, the two thiss look identical:

this : ∀ (i : ι), @AEMeasurable.{u_1, 0} Ω Real Real.measurableSpace mΩ (X i) μ
this : ∀ (i : ι), @AEMeasurable.{u_1, 0} Ω Real Real.measurableSpace mΩ (X i) μ

[Aaron Liu]

I even turned off pp.instantiateMVars and it still looked the same

[Aaron Liu]

So I guess fun_prop forgot an instantiateMVars somewhere?

[Etienne Marion]

If it's an easy fix, that'd be great.

example (hX : ∀ i, MemLp (X i) 2 μ) : AEMeasurable (fun ω i ↦ X i ω) μ := by
  have (i : ι) := (hX i).aestronglyMeasurable.aemeasurable
  fun_prop

also works.

[Tomas Skrivan]

example (hX : ∀ i, MemLp (X i) 2 μ) : AEMeasurable (fun ω i ↦ X i ω) μ := by
  fun_prop -- fails, ok

does not work because MemLp is not marked with fun_prop so it does not try to infer AEMeasurable from MemLp

This works

import Mathlib.MeasureTheory.Function.LpSeminorm.Defs
open MeasureTheory

variable {Ω ι : Type*} [Fintype ι] {mΩ : MeasurableSpace Ω} {μ : Measure Ω} {X : ι → Ω → ℝ}

attribute [fun_prop]
  MemLp
  MemLp.aestronglyMeasurable
  AEStronglyMeasurable.aemeasurable

example (hX : ∀ i, MemLp (X i) 2 μ) : AEMeasurable (fun ω i ↦ X i ω) μ := by
  fun_prop (maxTransitionDepth := 2)

Not sure if it actually make sense to have MemLp marked with fun_prop as it does not play well with composition. In general, fun_prop is not good/designed at proving integrability.

[Tomas Skrivan]

Aaron Liu said:

I thought they were the same too, but I guess not:

elab "t " i:ident : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let hyp ← Lean.Meta.getLocalDeclFromUserName i.getId
    Lean.logInfo hyp.type.ctorName

example (hX : ∀ i, MemLp (X i) 2 μ) : AEMeasurable (fun ω i ↦ X i ω) μ := by
  have : ∀ i, AEMeasurable (X i) μ := fun i ↦ (hX i).aestronglyMeasurable.aemeasurable
  t this -- forallE
  fun_prop -- works, ok

example (hX : ∀ i, MemLp (X i) 2 μ) : AEMeasurable (fun ω i ↦ X i ω) μ := by
  have := fun i ↦ (hX i).aestronglyMeasurable.aemeasurable
  t this -- mvar
  fun_prop -- fails, why?

This indeed seems like a problem. There must be some minor but at the last stage as trace for fun_prop correctly finds the local hypothesis but fails to apply it.

fun_prop trace:

[Meta.Tactic.fun_prop] [❌️] AEMeasurable (fun ω i => X i ω) μ ▼
  [] [❌️] AEMeasurable (fun ω i => X i ω) μ ▼
    [] [❌️] applying: aemeasurable_pi_lambda ▼
      [] [❌️] ∀ (a : ι), AEMeasurable (fun c => X a c) μ ▼
        [] [❌️] AEMeasurable (fun c => X a c) μ ▼
          [] candidate local theorems for X #[this : ∀ (i : ι), AEMeasurable (X i) μ]
          [] [❌️] applying: this : ∀ (i : ι), AEMeasurable (X i) μ ▼
            [] failed to unify this
                ∀ (i : ι), AEMeasurable (X i) μ
                with
                AEMeasurable (fun c => X a c) μ
          ....

It looks like that it is missing an application of forallMetaTelescope to the local hypothesis before the unification.