coercing between types with different instances

Stream: new members

[ooovi]

Hello!
I'm not sure what my problem is, but I have made a minimal non-working example:

import Mathlib.Data.Real.Basic
import Mathlib.Probability.Distributions.Uniform

open MeasureTheory Finset

lemma mnwe {X : Type} [nenX : Nonempty X] [finX : Fintype X] [meaX : MeasurableSpace X]
    (p : X → Prop) [decp : ∀ i, Decidable (p i)] {meap : Measurable p} {β : Real} :
    ENNReal.ofReal β ≤ ((PMF.uniformOfFintype X).toMeasure { x : X | p x }) →
    β ≤ ↑(Fintype.card { x  : X // p x }) / ↑(Fintype.card X) := by

  intro bound

  simp only [PMF.toMeasure_uniformOfFintype_apply {x : X | p x} (measurableSet_setOf.mpr meap),
    Set.coe_setOf, Set.mem_setOf_eq] at bound
  rw [ENNReal.ofReal_le_iff_le_toReal] at bound
  simp only [ENNReal.toReal_div, ENNReal.toReal_nat] at bound

  exact bound

The last line in the proof results in the following error.

type mismatch
  bound
has type
  β ≤
    ↑(@Fintype.card { x // p x }
          (@Subtype.fintype X (Membership.mem {x | p x}) (fun a ↦ Classical.propDecidable (p a)) finX)) /
      ↑(Fintype.card X) : Prop
but is expected to have type
  β ≤ ↑(@Fintype.card { x // p x } (@Subtype.fintype X p decp finX)) / ↑(Fintype.card X) : Prop

I'm guessing I'll need to do a type coercion somehow, but I'm not sure how?

[Eric Wieser]

convert bound should work

[Eric Wieser]

It looks like there is something to fix in mathlib here though

[ooovi]

Indeed, convert does the trick. I made an even more minimal minimal working example:

lemma emmmwe {X : Type} [Nonempty X] [Fintype X] [MeasurableSpace X] (s : Set X) (hs : MeasurableSet s) [fins : Fintype ↑s] :
    ((PMF.uniformOfFintype X).toMeasure s) = ↑(Fintype.card ↑s) / ↑(Fintype.card X) := by
  exact PMF.toMeasure_uniformOfFintype_apply s hs

Last line errors:

type mismatch
  PMF.toMeasure_uniformOfFintype_apply s hs
has type
  (PMF.uniformOfFintype X).toMeasure s =
    ↑(@Fintype.card (↑s) (Subtype.fintype (Membership.mem s))) / ↑(Fintype.card X) : Prop
but is expected to have type
  (PMF.uniformOfFintype X).toMeasure s = ↑(@Fintype.card (↑s) fins) / ↑(Fintype.card X) : Prop

where the Subtype.fintype bit is actually @Subtype.fintype X (Membership.mem s) (fun a ↦ Classical.propDecidable (a ∈ s)) finX.

My lemma is almost exactly the definition of PMF.toMeasure_uniformOfFintype_apply:

variable [Fintype α] [Nonempty α]
(...)
variable (s : Set α)
(...)
open scoped Classical in
theorem toMeasure_uniformOfFintype_apply [MeasurableSpace α] (hs : MeasurableSet s) :
    (uniformOfFintype α).toMeasure s = Fintype.card s / Fintype.card α := by
  simp [uniformOfFintype, hs]

The Classical allows inferring Fintype s for all s : Set α, and that instance is used for saying Fintype.card s in the theorem type. If another instance is used for saying Fintype.card s somewhere, like the fins instance in my lemma, my problem occurs. But how would I fix this? Is the problem that we choose an instance in the theorem statement while we shouldn't, or is the problem that type equality checking looks at which instance was used when it shouldn't matter for comparing Fintype.card s? Or is this just intended behaviour?

[Eric Wieser]

open scoped Classical in should never appear before theorem

[ooovi]

Hm, I grep over 50 occurances of open scoped Classical in appearing before theorem in mathlib. Maybe I'll make a PR for PMF.toMeasure_uniformOfFintype_apply removing it there, for now? :sweat_smile:
I'm interested in why it should not appear there, if you care to elaborate. Apart form the terrible trouble that is obvious to me now that I ran into it

[Kevin Buzzard]

You are seeing with your own eyes why it should not appear there. Fintype is constructive finiteness, and if it's mixed with classical mathematics it can cause hard-to-debug errors.

[Kevin Buzzard]

The basic rule of thumb is: if your theorem statement does not typecheck without constructive assumptions, add them; if your proof does not typecheck, use classical in the proof.

[ooovi]

Sorry, still a bit confused here. I thought my problem is due to the implicit use of a different instance in the theorem type than the instance that is picked where I want to use the theorem. Could that not have happened with any other instance that lives in some namespace, and any other type? Or is Classical special here somehow?

[Kevin Buzzard]

The mathlib theorem

open scoped Classical in
theorem toMeasure_uniformOfFintype_apply [MeasurableSpace α] (hs : MeasurableSet s) :
    (uniformOfFintype α).toMeasure s = Fintype.card s / Fintype.card α := by
  simp [uniformOfFintype, hs]

should be changed. open scoped Classical in is technical debt and there is an ongoing project to remove this stuff. It causes the problems you're seeing. Probably the theorem statement should have [Fintype s] in it instead of open scoped Classical in front of it.

[Kevin Buzzard]

The theorem should be this:

theorem toMeasure_uniformOfFintype_apply [Fintype s] [MeasurableSpace α] (hs : MeasurableSet s) :
    (uniformOfFintype α).toMeasure s = Fintype.card s / Fintype.card α := by
  classical
  simp [uniformOfFintype, Fintype.card_subtype, hs]

and now your proof works fine.

[ooovi]

Yes, thanks. I suppose my question was more about if this problem will generally arise when I implicitly use local instances in a theorem statement, and whether I should take care not to do that.

[Kevin Buzzard]

The rule is: put constructive assumptions like [DecidableEq α] or [Fintype s] in statements if they're needed to make the statements typecheck (and not open scoped Classical in), and use classical in proofs. Then hopefully your problem will not generally arise.

[Notification Bot]

6 messages were moved from this topic to #lean4 > Instance override phenomenon by Kevin Buzzard.