measurability tactic times out on Prod.fst \circ Prod.fst

Stream: mathlib4

[Terence Tao]

measurability has a tough time with

import Mathlib
open MeasureTheory
variable (Ω : Type*) [MeasurableSpace Ω]

example : Measurable (fun ω : ((Ω × Ω) × Ω) ↦ ω.1.1) := by
  measurability

timing out after 20000 heartbeats. Not sure if this is a bug, or the intended behavior. (Of course, in this case exact measurable_fst.comp measurable_fst works instead.) Adding show Measurable (Prod.fst ∘ Prod.fst) initially doesn't seem to help. On the other hand, measurability works for fun ω : Ω × Ω ↦ ω.1.

[Shreyas Srinivas]

I don't have a complete answer to this, but measurability is implemented using aesop. Here's the second example with aesop tracing turned on:

import Mathlib
open MeasureTheory
variable (Ω : Type*) [MeasurableSpace Ω]

set_option trace.aesop true

example : Measurable (fun ω : Ω × Ω ↦ ω.1) := by
  measurability

#check measurable_fst

[Shreyas Srinivas]

In the trace messages you see on the infoview, the first safe rule that succeeds is measurable_fst. So I tried this out, but this time by hand:

example : Measurable (fun ω : Ω × Ω ↦ ω.1) := by
  unfold Measurable
  intro t mt
  apply measurable_fst
  exact mt

[Shreyas Srinivas]

here lean is able to tell that fun ω : Ω × Ω ↦ ω.1 is the same as Prod.fst.

[Shreyas Srinivas]

Doing the same for your original example yields

tactic 'apply' failed, failed to unify
  MeasurableSet (Prod.fst ⁻¹' ?t)
with
  MeasurableSet ((fun ω => ω.1.1) ⁻¹' t)

[Eric Wieser]

Yeah, because those types don't match Shreyas Srinivas. My understanding is that measurability tries to apply .comp, but unification gets out of hand

[Eric Wieser]

Do we have docs#MeasureTheory.Measurable.fst to match docs#Continuous.fst ?

[Shreyas Srinivas]

You mean this: measurable_fst (closest in name)?

[Eric Wieser]

No, the .fst version would work with apply; though I can't tell whether it's used by continuity (it's not tagged inline with the attribute, but maybe the attribute is added later)

[Shreyas Srinivas]

Found it

[Shreyas Srinivas]

and it is not tagged with measurability at the point of definition

[Shreyas Srinivas]

Is it possible to find a prefix of aesop's trace when the maxheartbeat issue occurs (something like the head -n shell command)?

[Shreyas Srinivas]

@Eric Wieser :
The following also fails for some reason (EDIT : Removed unfolds and intros as suggested by Eric below. Same result):

import Mathlib
open MeasureTheory
variable (Ω : Type*) [MeasurableSpace Ω]

set_option trace.aesop true

example : Measurable (fun (ω : (Ω × Ω) × Ω) => (Prod.fst ∘ Prod.fst) ω) := by
  apply Measurable.fst
  apply measurable_fst
  done

example : Measurable (fun (ω : (Ω × Ω) × Ω) => (Prod.fst ∘ Prod.fst) ω) := by
  apply Measurable.fst
  measurability -- fails even though the goal resembles the third example
  /-apply measurable_fst
  exact m_t-/
  done

example : Measurable (fun ω : Ω × Ω ↦ ω.1) := by
  measurability

[Eric Wieser]

Why did you do the unfold and intro steps?

[Shreyas Srinivas]

It was copy pasted from the first proof which works

[Shreyas Srinivas]

I am not sure why this would affect the measurability tactic since the first goal before the measurability line is :

case hf
Ω: Type u_1
inst✝: MeasurableSpace Ω
t: Set Ω
m_t: MeasurableSet t
⊢ Measurable fun a => a.1

[Shreyas Srinivas]

Eric Wieser said:

Why did you do the unfold and intro steps?

Removed them now. It doesn't make a difference to the result. What I was trying to do was remove the obstacle of measurability not applying Measurable.fst by manually applying it. My hope was that measurability can do the rest.