Open affeldt-aist opened 1 year ago
I have started removing duplicate things from infotheo in convex.v. In particular, I want to use the definition of hull from infotheo. I do not think it really matters that we rely temporarily on the standard library. I guess we will want to generalize fdists anyway, so we would be duplicating work.
Oh! Good. Then we can maybe keep the generalization of fdist for later. Please, feel free to ignore this PR and specialize what you want to the reals of the standard library so as to use infotheo!
Should I raise an issue in infotheo ?
Should I raise an issue in infotheo ?
Yes, please. I will take care of it ASAP (more realistically discuss it with @yoshihiro503 ^_^ for a solution to happen in the next few months).
@ybertot @Tragicus It looks like there is a definition of hull that is similar to the one of infotheo but where the notion of distribution is unfolded in the definition: https://github.com/affeldt-aist/trajectories/blob/830e498d9170cfdcd6fc59af55244547184e2ce4/theories/hulls.v#L25-L26
Ideally we would like to use the type
fdist
of infotheo but unfortunately it depends on the typeR
of the Coq standard library.This is maybe infotheo that should be generalized but it might be faster to introduce a new, more generic
fdist
type in trajectories: https://github.com/affeldt-aist/trajectories/blob/d4da32f8ca7dbff1ad8ef1aafa5071dba5218d6a/theories/hulls.v#L16-L45This what this PR is experimenting.