nonneg

Stream: condensed mathematics

[Johan Commelin]

Here is a little (big) project for anyone who's interested. (Maybe Damiano even has some code in this direction already, I think we experimented with this on the toric branch.)

• Define nonneg A, whenever [has_zero A] [has_le A]. Add a coe to A.
• If A is an ordered_add_monoid, so is nonneg A.
• If A is an ordered_add_group, then nonneg A is cancellative.
• If A is an ordered_semiring, so is nonneg A. In this case nonneg A is also comm_monoid_with_zero (even an ordered one, do we have a class for that?)
• If A is an linear_ordered_field, then nonneg A is a linear_ordered_comm_group_with_zero
• Define an ordered ring equiv between nat and nonneg int
• Refactor nnreal to use this machinery.
• Define nnrat to be nonneg rat

[Johan Commelin]

We already have nnrat in LTE, thanks to Bhavik and Yael's work on Gordan.

[Johan Commelin]

It seems time that we abstract these constructions.

[Adam Topaz]

Johan Commelin said:

• Refactor nnreal to use this machinery.

:expressionless:

[Damiano Testa]

Actually, this is something that I was planning to do for the ordered refactor. Once you get to a type with add and mul and \le, multiplication is monotone only by the non-negative elements. Thus, my plan was to define the type of nonnegative elements of exactly what you said and start proving stuff about this!

[Damiano Testa]

It is even in one of the PR messages! :smile:

[Damiano Testa]

... and it did start in order to prove stuff for nnreal, arising from liquid, both from the toric side and from the real inequalities side!

[Damiano Testa]

By the way, the first PR in the ordered refactor has already received positive comments from Anne and Floris. In case anyone is interested in taking a look, this is the current winner:
#7371 :wink: :upside_down:

[Damiano Testa]

(and don't feel daunted by the size of the PR: the 442 removed lines are essentially lemmas that changed files. The PR really only contains fewer than 300 new lines, most of which are doc-strings.)

[Damiano Testa]

Now that the PRs splitting the ordered hierarchy have (mostly) taken care of monoids and groups, the next on the list is rings. In this case, the assumption on monotonicity for addition is already there, but the assumption on monotonicity of multiplication is going to require a non-negativity/positivity assumption on the multiplier.

For flexibility, given the experiment in the liquid project, I would set this up as a function from a Type to a [Type with le and zero] such that the function is injective and the elements in the image are... non-negative? Positive?

• Pro of non-negative/Con of positive
  mostly, the source could be assumed to be, for instance, a semiring, which could come in handy, e.g. when saying that we multiply a real number by a nnreal number (or a nat!).

• Con of non-negative/Pro of positive
  for roughly half the statements, there would have to be a non-zero assumption on the (image of the) multiplier, instead of a single check when setting up the action.

Which of these two do you think outweighs the other? Is there something else that you think could be a deciding factor?

Thanks!

PS The second refactor is #7645, freshly opened!

[Johan Commelin]

The first option is the more flexible/general one, right?

[Damiano Testa]

I think so: the first option includes all second options, plus the ones which happen to have zero in the image. I am just worried of a lot of ne_zero showing up in proofs and names of lemmas.

[Damiano Testa]

Although, I think that this already happens and is also my preference.

[Damiano Testa]

An alternative, would be to define semiring_without_zero... :upside_down:

[Johan Commelin]

semi_rig?

[Damiano Testa]

I see where this is going...

[Johan Commelin]

I guess that would be a distrib_with_one?

[Damiano Testa]

:lol: Indeed! Although I want to make sure that we are just joking around, right? :lol:

[Damiano Testa]

A philosophical question could be to ponder about the positive elements in semi_rig.