Finset subtype changes

Stream: mathlib4

[Etienne Marion]

Hi, consider the following #mwe:

import Mathlib.MeasureTheory.Constructions.Projective

open MeasureTheory

variable {ι : Type*} {α : ι → Type*} [∀ i, MeasurableSpace (α i)] {P : ∀ J : Finset ι, Measure (∀ j : J, α j)}
  {I J : Finset ι}

lemma measure_univ_eq_of_subset (hP : IsProjectiveMeasureFamily P) (hJI : J ⊆ I) :
    P I Set.univ = P J Set.univ := by
  classical
  have : (Set.univ : Set (∀ i : I, α i)) =
      Set.restrict₂ hJI ⁻¹' (Set.univ : Set (∀ i : J, α i)) := by
    rw [Set.preimage_univ]
  rw [this, ← Measure.map_apply _ MeasurableSet.univ] -- What happens here?
  · rw [hP I J hJI]
    rfl -- why is this necessary?
  · exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _)

Before the line "What happens here?", the first Set.univ in the goal is printed as @Set.univ ((i : { x // x ∈ J }) → α ↑i) in the infoview, but after the last rewrite on that line it becomes @Set.univ ((a : ↑(Membership.mem J.val)) → α ↑a). This generates a weird goal asking to provide an instance and requires the current goal to be closed with a rfl after a rewrite, which is not very nice.

I had that kind of issues when dealing with finsets in functions asking for sets, and my "solution" was to duplicate code for finsets, but this is getting out of hand, so I would like to understand what happens here to try and find a better solution. Any thoughts?

[Kyle Miller]

Hmm, there's something about how Measure.map_apply is unifying that's turning { x // x ∈ J } into the equivalent Membership.mem J.val, which is a predicate rather than a set. I'm not sure why that would be. All I can suggest is that since rw isn't aware of alpha while it's elaborating the rw rule, it might cause a wrong choice to be made during a later unification.

Something that seems to help is using refine:

lemma measure_univ_eq_of_subset (hP : IsProjectiveMeasureFamily P) (hJI : J ⊆ I) :
    P I Set.univ = P J Set.univ := by
  classical
  have : (Set.univ : Set (∀ i : I, α i)) =
      Set.restrict₂ hJI ⁻¹' (Set.univ : Set (∀ i : J, α i)) := by
    rw [Set.preimage_univ]
  rw [this, hP I J hJI]
  symm
  refine Measure.map_apply ?_ MeasurableSet.univ
  exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _)

[Etienne Marion]

I think the issue comes from the fact that the Finset inclusion is not interpreted as the inclusion of the coercions to sets because it is not the definition, but I don't see how to solve the problem. If I change restrict₂ to a finset version, here is what happens:

import Mathlib.MeasureTheory.Constructions.Projective

open MeasureTheory Set

variable {ι : Type*} {α : ι → Type*}

theorem frestrict₂_comp_restrict {s t : Finset ι} (hst : s ⊆ t) :
    (Finset.restrict₂ hst) ∘ (@restrict ι α t) = restrict s.toSet := rfl

variable [∀ i, MeasurableSpace (α i)]

example (s t : Finset ι) (hst : s ⊆ t) (μ : Measure (Π i, α i)) : μ.map (@Set.restrict ι α s) = sorry := by
  rewrite [← frestrict₂_comp_restrict hst, ← Measure.map_map (Finset.measurable_restrict₂ _) (measurable_restrict _)]
  sorry

I can't put the proof of measurability measurable_restrict in the rewrite because it causes an error, while not putting it right now and proving it after works fine. I don't know what's going on but there typically is a↑↑t which pops in the infoview when I hover and which does not seem natural.

[Etienne Marion]

Kyle Miller said:

Something that seems to help is using refine:

Indeed that fixes it, though I admit I would like to be able to rewrite smoothly without troubles because I'm using finsets and not sets.

[Aaron Liu]

This is what the unification came up with, I guess. I believe the solution would be to create a Finset.Elem (analagous to docs#Set.Elem) and use this in the coercion docs#Finset.instCoeSortType, like what is done with sets.

[Kim Morrison]

I ran into this same issue today while fighting with erw.

[Etienne Marion]

Aaron Liu said:

This is what the unification came up with, I guess. I believe the solution would be to create a Finset.Elem (analagous to docs#Set.Elem) and use this in the coercion docs#Finset.instCoeSortType, like what is done with sets.

Can you tell me more please? I'm not sure why this would solve the issue, it seems only to be an abbreviation. I opened a draft #22037 to see what I can get, I added Finset.Elem but this does not change the behaviour of my #mwe (it is on line 60 in MeasureTheory.Constructions.Projective)

[Aaron Liu]

It looks like this did not fix the problem like I thought it would. Now I'm out of ideas

[Etienne Marion]

I just realized I forgot to remove the old instance so my code does nothing :sweat_smile:

[Etienne Marion]

Okay it still does not solve the problem, I'm gonna try to change the definition of Finset inclusion to inclusion of set coercions

[Etienne Marion]

Changing the definition of Finset inclusion is a bad idea because it requires to deal with coercions even when there are only finsets around. So I thought I would replace finset inclusion by inclusion of coercions in my code, not ideal but maybe better.

import Mathlib.MeasureTheory.Constructions.Projective

open MeasureTheory

variable {ι : Type*} {α : ι → Type*} [∀ i, MeasurableSpace (α i)] {P : ∀ J : Finset ι, Measure (∀ j : J, α j)}
  {I J : Finset ι}

lemma measure_univ_eq_of_subset (hP : IsProjectiveMeasureFamily P) (hJI : J ⊆ I) :
    P I Set.univ = P J Set.univ := by
  classical
  have : (Set.univ : Set (∀ i : I, α i)) =
      Set.restrict₂ (Finset.coe_subset.2 hJI) ⁻¹' (Set.univ : Set (∀ i : J, α i)) := by
    rw [Set.preimage_univ]
  rw [this, ← Measure.map_apply _ MeasurableSet.univ]
  · rw [hP I J hJI]
    rfl
  · exact measurable_pi_lambda _ (fun _ ↦ measurable_pi_apply _)

This does not solve the issue however, because at the end rw does not unify ↑↑I and ↑I (the first one is I.toSet.Elem and the second is just I.Elem). Changing Finset.Elem to fun s ↦ s.toSet.Elem does not seem a good solution because again when you are only dealing with finsets you don't want coercions to sets to get in the way. The solution might be to make unification between ↑↑I and ↑I stronger, or automatically change ↑↑I into ↑I, but I don't know if that is possible and I have no idea how to do it. Otherwise I don't see how to fix this properly: either there are buggy rewrites which require rfl, either we duplicate many things to separate sets and finsets (and potentially triplicate when we want to deal with sets and finsets at the same time).