realType structure over fourcolor's reals

[lweqx]

During an internship with @CohenCyril, I worked on proving the equivalence between math-comp's realType and fourcolor's Real.model.

The original idea was to transfer Fourcolor's proof of categoricity for their reals to math-comp using Trocq.

However, it turns out that fourcolor's real type is missing some properties to obtain a realType structure over them. Notably:

• fourcolor's real type use their own Real.eq predicate to state equalities properties. So, we need a eqR_is_eq : forall {x y: R}, Real.eq x y -> x = y
• the inverse of 0 is not given an explicit value, whereas it is 0 in math-comp. So, we need a inv00 : Real.eq (Real.inv (Real.zero R)) (Real.zero R)
• fourcolor's real type does not contain a truncation operator trunc : R -> nat. We also need to have a property satisfied by this operator:

  truncP : forall (x: R),
    if leb 0 x
    then ((Real.le (Real.nat _ (trunc x)) x) /\ (Real.lt x (Real.nat _ (trunc x).+1)))
    else (trunc x == 0)
  

• fourcolor's real type does not give immediately the sup_adherent_subdef property, so I assumed it. I think we could obtain it classically. I didn't investigate this further.

I defined a new realModel record that adds these properties to fourcolor's Real.model. We won't have an equivalence between Real.model and realType, so our original plan is a bit foiled...

The proof is incomplete because I struggle to obtain a normedModType R structure on R to apply the math-comp's continuity lemmas. Moreover, my proof of the Intermediate value theorem is incomplete because lra/nra creates many shelved subgoals and I don't understand why (and I don't want to prove inequalities by hand). Another possibility for the proof of the IVT would be to proceed by connectedness of p([a, b]), by continuity of p but I didn't find this easier.

I'm fed up with this so I didn't bother to properly include my proof file as part of math-comp analysis, sorry. A nicer and reproductible environment is available there. I lack automony so it's difficult to solve the remaining issues, hence why I'm stopping there.

[CohenCyril]

Thanks @lweqx!