Trying to generalize mfun, updated

[hoheinzollern]

Motivation for this change

fixes #662

closes #672

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md
• added corresponding documentation in the headers

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

@CohenCyril this seems to actually generalize isMeasurableFun that was specialized to realType, we had to get rid a cst instantiation that wouldn't go through but does not seem useful anyway, maybe it was there to solve an inference problem that has been solved in the meantime?

[affeldt-aist]

the remaining problem is to generalize the instance of cst which have not been able to figure out yet,
but already in the current form this PR is an improvement we think

Context {d} {aT : sigmaRingType d} {rT : realType}.

Let cst_mfun_subproof x : @measurable_fun d _ aT rT [set: aT] (cst x).
Proof. by []. Qed.

HB.instance Definition _ x := isMeasurableFun.Build d _ aT rT (cst x)
  (@cst_mfun_subproof x).

[CohenCyril]

the remaining problem is to generalize the instance of cst which have not been able to figure out yet,
but already in the current form this PR is an improvement we think

Context {d} {aT : sigmaRingType d} {rT : realType}.

Let cst_mfun_subproof x : @measurable_fun d _ aT rT [set: aT] (cst x).
Proof. by []. Qed.

HB.instance Definition _ x := isMeasurableFun.Build d _ aT rT (cst x)
  (@cst_mfun_subproof x).

What is the issue exactly? The preimage of any set by a constant function should be measurable (because either set0 or setT)

[affeldt-aist]

What is the issue exactly? The preimage of any set by a constant function should be measurable (because either set0 or setT)

Of course generalizing cst_mfun_subproof is perfectly fine (it is even a hint).
The problem occurs when doing HB.instance. There is a type inference problem.
Inspection of the type error seems to indicate that HB really wants cst to be simple function,
that returns real numbers. In particular, if you move this part of the code earlier in the file
it will type check but then this is the declaration of cst as a simple function that causes a problem.
We haven't been able to figure it out.

[affeldt-aist]

@CohenCyril The last commit is generalizing the mfun instance of cst to a codomain of type measurableType instead of realType (at least in lebesgue_integral.v). To prevent HB to be too eager (and infer that the codomain should be at the same measurableType and realType which seems to cause the problem---maybe we can play with measurableTypeR to avoid that but we were not successful at that in the past, let's maybe reconsider that but later), the structure for simple functions has been put into a module that is opened when needed. The problem is that when we do that and need to infer more elaborate types for cst we also need to regenerate fimfun/mfun/nnfun instances locally. This is dirty because it is only a try, but if it makes sense we can clean that up. What do you think?

[CohenCyril]

This is what I advocated, but I think it is a bit too hackish, we must fix hb instead.

[affeldt-aist]

This is what I advocated, but I think it is a bit too hackish, we must fix hb instead.

Great! In the meantime, should we try to merge this hack (in a more proper form and clearly marked as a hack of course)? In particular, the generalization of mfun is likely to be useful for the Giry monad and for probability theory.

[affeldt-aist]

CI is ok, the kludge is well-localized and documented, plus this will serve as a test bed for the forthcoming coding sprint, I can maybe interpret your thumb up @CohenCyril as an OK to merge?