Dual ereal

[proux01]

In Coquelicot, -oo + +oo was defined as 0, which was nice for morphisms with opposite but terrible as addition was not even associative. In ereal.v, the addition adde is such that -oo + +oo = -oo, making it associative an such that (er R, Order.max, adde) is a semiring (the id element -oo of Order.max is a zero for adde). However, sometimes we rather need (er R, Order.min, adde) to be a semiring, with -oo + +oo = +oo. This PR offers that, I don't know if we want it in analysis?

depends on: #403 (merged)

[CohenCyril]

I'd rather keep extended reals a commutative monoid (which was the case before this PR), this is crucial for taking maximal advantage of bigops.

[proux01]

I fully agree, this PR doesn't change anything about extended reals, just offers dual extended reals where -oo++oo = +oo instead of -oo.

[CohenCyril]

Sorry, I misunderstood your original post and did not open the diff. It seems reasonable to me although:

• I cannot foresee a use yet (could you point me towards a concrete example)
• I would not integrate this within the same scope and same names. We could use for example %dE (for "dual Extended") an the names could be prefixed with dual_?

[CohenCyril]

Also, I would integrate it within ereal.v

[proux01]

• I cannot foresee a use yet (could you point me towards a concrete example)

We use it in a formalization of Network Calculus (a static analysis for networks, used to certify embedded networks in civil aircrafts) that is based on min-plus algebra. Sorry, can't share the code yet due to licencing issues (hope to finally fix that in the coming weeks).

• I would not integrate this within the same scope and same names. We could use for example %dE (for "dual Extended") an the names could be prefixed with dual_?

Would indeed make sense to enable mix use of both regular and dual versions (no idea if that can arise though).

[CohenCyril]

Would indeed make sense to enable mix use of both regular and dual versions (no idea if that can arise though).

I think it can... and I forgot about providing correspondance lemmas under the negation add_undef precondition.
(Although we might very well switch to add_def as per #365)

[proux01]

@CohenCyril all your comments should be taken into account.

[proux01]

This is rebased on top of #403, dual_mule disappeared since it is now the same as mule.

[proux01]

Just rebased this on top of master now that #403 is merged.

[proux01]

@CohenCyril all notation seem to work properly (for instance x + y <= -(x + y))%dE uses dual_adde as expected and prints back identically), I just spotted an omission int the bigop notations and +? was missing in ereal_dual_scope.

[proux01]

@CohenCyril I'd like to rebase this on top of #459 once it is merged (to add lemmas about mine, the dual of maxe)

[CohenCyril]

@CohenCyril I'd like to rebase this on top of #459 once it is merged (to add lemmas about mine, the dual of maxe)

Sure. I also think that the new convention is to use forall x : \bar R, x \in fin_num -> P x rather than forall r : R, P r%:E.
I also think theorems about dual ereal should be encapsulated in a submodule and imported on demand.

[proux01]

Indeed, done, this should now be ready.

BTW, this dual add thing is used there: https://gitlab.mpi-sws.org/proux/nc-coq
I wanted to do opam and nix packages for CI when I realized I'm still using dioid master that relies on a nasty hack to use HB on top of current MC https://github.com/math-comp/dioid/blob/master/HB_wrappers.v . So I should probably wait for MC 2.0.

[CohenCyril]

Ok, thanks!, let's rebase and merge.

[proux01]

rebased

[proux01]

Thanks!