The nonnegative elements

Stream: Is there code for X?

[Floris van Doorn]

Given a ordered ring, do we have properties about the subtype of nonnegative elements {x : α // 0 ≤ x}? Like that it is an additive monoid, and sometimes even a docs#canonically_ordered_add_monoid?

Related:
https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/The.20submonoid.20of.20positive.20elements

[Kevin Buzzard]

@Damiano Testa was thinking about this in the context of toric varieties and there was even some minor development on some LTE branch but then I think he rather went down the inequality rabbithole...

[Damiano Testa]

Indeed, I had been thinking about this, but did not push anything to mathlib. Also, a couple of days ago, Eric asked about the positive elements in this stream (I am on mobile and do not know how to get a link for the topic).

[Floris van Doorn]

I've started something on branch#ordered_sub_continue, and use it to simplify some instances for nnreal.
I already linked to the positive element thread in my previous post :)

[Johan Commelin]

Note that LTE has a file for_mathlib/nnrat.lean which can hopefully also be simplified using this method.

[Johan Commelin]

nonneg R for a linearly ordered field can get an instance of linearly ordered comm group with zero.

[Floris van Doorn]

Ok, I'll add that instance as well

[Damiano Testa]

Floris, I should have at least read the URL address that you had linked!

I am very happy that this is happening! I have been a little drained by the initial part of the order refactor, but seeing it progressing is very encouraging!

[Floris van Doorn]

Done in #9598

[Johan Commelin]

Very nice!

[Johan Commelin]

Hopefully it will now be really easy to port nnrat from LTE to mathlib.

[Yaël Dillies]

Does your nnrat take in a natural or integer numerator?

[Johan Commelin]

nnrat should just be {x : rat // 0 \le x}

[Yury G. Kudryashov]

Could you please double check that your instances don't create diamonds about min/max?

[Yury G. Kudryashov]

I guess, function.injective.linear_ordered_semiring and some other subtype instance can define different min/max.

[Floris van Doorn]

Yury G. Kudryashov said:

Could you please double check that your instances don't create diamonds about min/max?

I checked, and they're all are definitionally equal.

example [linear_ordered_add_comm_monoid α] (a b : {x : α // 0 ≤ x}) :
  max a b = linear_ordered_add_comm_monoid.max a b :=
by tactic.reflexivity tactic.transparency.instances

example [linear_ordered_cancel_add_comm_monoid α] (a b : {x : α // 0 ≤ x}) :
  max a b = linear_ordered_cancel_add_comm_monoid.max a b :=
by tactic.reflexivity tactic.transparency.instances

example [linear_ordered_semiring α] (a b : {x : α // 0 ≤ x}) :
  max a b = linear_ordered_semiring.max a b :=
by tactic.reflexivity tactic.transparency.instances

example [linear_ordered_comm_ring α] (a b : {x : α // 0 ≤ x}) :
  max a b = linear_ordered_comm_monoid_with_zero.max a b :=
by tactic.reflexivity tactic.transparency.instances

example [linear_ordered_field α] (a b : {x : α // 0 ≤ x}) :
  max a b = linear_ordered_comm_group_with_zero.max a b :=
by tactic.reflexivity tactic.transparency.instances

example [linear_ordered_ring α] (a b : {x : α // 0 ≤ x}) :
  max a b = canonically_linear_ordered_add_monoid.max a b :=
by tactic.reflexivity tactic.transparency.instances

(I was a little surprised that they were even definitionally equal when unfolding only reducible decls, since it feels like we need to unfold non-reducible instances for this. Maybe there is something weird going on since max is a field of a class)

[Floris van Doorn]

@Yury G. Kudryashov
Ah, I think I see what you're referring to.
This fails:

example [conditionally_complete_linear_order α] {z : α} (h : Sup ∅ ≤ z) (a b : {x : α // z ≤ x}) :
  max a b = @conditionally_complete_linear_order_bot.max _ (nonneg.conditionally_complete_linear_order_bot h) a b :=
by tactic.reflexivity tactic.transparency.instances

But it succeeds with semireducible transparency. This is likely the cause of the error I encountered in the PR:

We currently do not yet define conditionally_complete_linear_order_bot nnreal using nonneg, since that causes some errors (I think Lean then thinks that there are two orders that are not definitionally equal (unfolding only instances)).

This probably involves making a few definitions reducible. I'll try to do that and make a PR.