start porting to MathComp 2

[affeldt-aist]

fyi @garrigue @t6s

[t6s]

CI needs to be fixed

[affeldt-aist]

The currenty error is:

COQC proba_lib.v
File "./proba_lib.v", line 252, characters 0-188:
Error: convex_isConvexSpace__to__convex_isConvexSpace0 already exists.

It looks like a confusion due to the fact that we define isConvexSpace both in analysis and in infotheo
Maybe we should rename the one of infotheo into say isConvexSpaceProb to avoid that.
Or is there another trick?

[t6s]

Commenting out the Import ... line makes this section go through. Is this not enough?

Section altprob_semilattconvtype.
Variable M : altProbMonad R.
Variable T : Type.
(*Import convex necset SemiLattice.*)

Definition altProb_semiLattConvType := M T.

Let axiom (p : {prob R}) (x y z : altProb_semiLattConvType) :
  x <| p |> (y [~] z) = (x <| p |> y) [~] (x <| p |> z).
Proof. by rewrite choiceDr. Qed.

HB.instance Definition _ := boolp.gen_eqMixin altProb_semiLattConvType.
HB.instance Definition _ := boolp.gen_choiceMixin altProb_semiLattConvType.

HB.instance Definition _ := @isSemiLattice.Build altProb_semiLattConvType
  (fun x y => x [~] y)
  (@altC M T) (@altA M T) (@altmm M T).

HB.instance Definition _ := @probability.convex.isConvexSpace.Build altProb_semiLattConvType
  (fun p : {prob R} => choice p T)
  (choice1 _) choicemm choiceC (@choiceA_real_realType M T).

HB.instance Definition _ := @isSemiLattConv.Build altProb_semiLattConvType axiom.

End altprob_semilattconvtype.

[affeldt-aist]

I didn't try this one yet. Thanks. This is worrisome though.

I think that we still want to rename isConvexSpace in infotheo because it is very likely that both definitions of convex space will need to coexist for a while (and/or one will become a factory for the other). Don't you think?

[t6s]

I am reluctant to rename either of them since they are exactly the same notion and the definitions will eventually converge; the renaming will induce many changes in dependent code, and later renaming back all of them.

[affeldt-aist]

In any case, we'll have to do something about the coexistence of these two definitions.
Should we try to accommodate both conventions (I mean (1-t)x + ty vs. tx + (1-t)y definitions),
or should we port monae to the MathComp-Analysis convention?

[affeldt-aist]

3 versions of Coq in the CI, I guess we can merge it in master now @t6s @garrigue