canonically_ordered pathology

Stream: new members

[Damiano Testa]

Dear All,

the doc-strings for canonically_ordered_comm_semiring says:

A canonically ordered commutative semiring is an ordered, commutative semiring in which a ≤ b iff there exists c with b = a + c. This is satisfied by the natural numbers, for example, but not the integers or other ordered groups.

However, it does not seem like a canonically_ordered_comm_semiring is actually an ordered_semiring. At least, Lean could not generate the instance in this example:

import algebra.ordered_ring

instance cosr {α : Type*} [canonically_ordered_comm_semiring α] : ordered_semiring α :=
by apply_instance

Playing with it a bit, it seems that the left/right cancellative properties of addition cause problems. I do not know enough pathological examples of ordered_semirings or canonically_ordered_comm_semiring to form an opinion on whether the instance above can be proven.

Any ideas?

Thank you very much!

[Damiano Testa]

(In case people are curious, this is an offspring of trying to prove

lemma add_le_mul {α : Type*} [canonically_ordered_comm_semiring α] [nontrivial α]
  {a b : α} (a2 : 2 ≤ a) (b2 : 2 ≤ b) : a + b ≤ a * b :=

While I only care about the case in which α = ℕ, a case that I can prove, I was trying to port this to mathlib in greater generality.)

[Johan Commelin]

you don't need nontrivial for that, right?

[Johan Commelin]

I think your lemma should be true in any ordered_semiring, you don't need the canonical either, do you?

[Damiano Testa]

I may not need either one of these assumptions, but I did assume nontrivial in the lemma that I intend to use to prove my application.

In my actual proof, I wanted to use the implication "a \leq b means that there exists a c such that b = a + c", hence the canonical!

[Damiano Testa]

To fully disclose my arguments, see the code below!

import data.nat.basic
import algebra.ordered_ring

lemma add_le_mul_two_add {R : Type*} [ordered_semiring R] [nontrivial R] {a b : R}
  (a2 : 2 ≤ a) (b0 : 0 ≤ b) : a + (2 + b) ≤ a * (2 + b) :=
calc a + (2 + b) ≤ a + (a + a * b) :
      add_le_add_left (add_le_add a2 (le_mul_of_one_le_left b0 (one_le_two.trans a2))) a
             ... ≤ a * (2 + b) :
      le_trans (le_trans (le_of_eq (add_assoc a a _).symm) (le_trans rfl.ge (add_le_add_right
      (le_of_eq (mul_two a).symm) _))) (le_of_eq (mul_add a 2 b).symm)


-- the lemma that I really care about, that works
lemma add_le_mul {a b : ℕ} (a2 : 2 ≤ a) (b2 : 2 ≤ b) : a + b ≤ a * b :=
begin
  rcases le_iff_exists_add.mp b2 with ⟨k, rfl⟩,
  exact add_le_mul_two_add a2 k.zero_le
end

-- how I would like to port it to mathlib, possibly with different assumptions, since now the exact line fails
lemma add_le_mul_canonical {R : Type*} [canonically_ordered_comm_semiring R]
  {a b : R} (a2 : 2 ≤ a) (b2 : 2 ≤ b) : a + b ≤ a * b :=
begin
  rcases le_iff_exists_add.mp b2 with ⟨k, rfl⟩,
  exact add_le_mul_two_add a2 k.zero_le
end

[Kevin Buzzard]

There's been quite some discussion about this lemma on the Discord. Without subtraction it's not clear how to prove it but conversely we don't know enough weird ordered semirings to know if there's a counterexample. It's true if 2a<=2b implies a<=b but we think we know canonically ordered semirings where this fails, except that these semirings do not satisfy additive cancellation. The trick is to start with a ring like the naturals and then if S is a random subset of the naturals to add extra "ghost" elements to the ring, one for each element of S, such that addition of non-ghost 0 and multiplication by non-ghost 1 are the identity maps but the answer to everything else is the non-ghost number, so for example 2+2=non-ghost 4 whether the original 2s are ghosts or not

[Eric Wieser]

I think #6034 resolves the nontrivial comment.

[Damiano Testa]

I was wondering about something like N+N/2, where you have (1,0)+(1,0)=(1,1)+(1,1).

I am not sure though whether you need a total order, or not... I do not know enough about these canonically_[stuff].

[Kevin Buzzard]

For canonically ordered comm semirings can't you just write a=2+x and b=2+y and deduce it from the fact that a+b+(x+y+xy)=ab?

[Kevin Buzzard]

Canonically ordered stuff us easy because it just means that the order is determined by the addition

[Damiano Testa]

Ok, I will try with your version!

[Kevin Buzzard]

The problem with canonically ordered things is that essentially nothing is canonically ordered, eg the integers aren't canonically ordered

[Damiano Testa]

(Note that I added the canonically_ordered after I tried to use the previous lemma, so I have actually not really thought about canonically_ordered things...)

[Damiano Testa]

If you have a multiplication, you could try to use squares to make canonically_ordered things more applicable? I am thinking along the lines of sums of squares are non-negative... Anyway, this is a separate issue!

[Kevin Buzzard]

The moment there's a nontrivial solution to a+b=0 you're not canonically ordered. However things like 2<=a and 2<=b implies a+b<=ab are true for any totally ordered semiring because then wlog a<=b and so a+b<=2b<=ab

[Kevin Buzzard]

I don't think I know a single example of an ordered semiring which isn't canonically ordered or totally ordered though

[Johan Commelin]

lemma add_le_mul₁ {α : Type*} [linear_ordered_semiring α]
  {a b : α} (a2 : 2 ≤ a) (ab : a ≤ b) : a + b ≤ a * b :=
have 0 < b, from
calc 0 < 2 : zero_lt_two
   ... ≤ a : a2
   ... ≤ b : ab,
calc a + b ≤ b + b : add_le_add_right ab b
       ... = 2 * b : (two_mul b).symm
       ... ≤ a * b : (mul_le_mul_right this).mpr a2

lemma add_le_mul₂ {α : Type*} [linear_ordered_semiring α]
  {a b : α} (b2 : 2 ≤ b) (ba : b ≤ a) : a + b ≤ a * b :=
have 0 < a, from
calc 0 < 2 : zero_lt_two
   ... ≤ b : b2
   ... ≤ a : ba,
calc a + b ≤ a + a : add_le_add_left ba a
       ... = a * 2 : (mul_two a).symm
       ... ≤ a * b : (mul_le_mul_left this).mpr b2

lemma add_le_mul {α : Type*} [linear_ordered_semiring α]
  {a b : α} (a2 : 2 ≤ a) (b2 : 2 ≤ b) : a + b ≤ a * b :=
begin
  by_cases hab : a ≤ b,
  { exact add_le_mul₁ a2 hab },
  { push_neg at hab,
    exact add_le_mul₂ b2 hab.le }
end

[Johan Commelin]

This assumes linearity...

[Johan Commelin]

But not commutativity

[Damiano Testa]

Does ℕ ⊕ (ℤ / 2) with the partial order induced by projection onto the first component fail to be an ordered semiring?

[Kevin Buzzard]

Maybe the complexes with a<=b iff b-a is a non-negative real? No idea

[Kevin Buzzard]

Johan you should just use wlog for add_le_mul to save code duplication

[Johan Commelin]

Can wlog do that without assume comm?

[Kevin Buzzard]

Oh! No! I'd not spotted that you didn't assume commutativity. Sorry

[Johan Commelin]

Dunno...

[Johan Commelin]

I guess I can remove the \_2 version by using the opposite ring

[Kevin Buzzard]

What the heck is Z/2? How do you do multiplication on that?

[Damiano Testa]

I meant the commutative ring with exactly two elements. I may be missing something very basic, though...

[Johan Commelin]

I guess he means zmod 2?

[Kevin Buzzard]

And what is the partial order induced by the first component? Does it really satisfy the partial order axiom a<=b and b<=a implies a=b?

[Kevin Buzzard]

Aah, Z mod 2 :-) But what is the order?

[Kevin Buzzard]

It's not canonically ordered because there are nontrivial solutions to a+b=0

[Damiano Testa]

Maybe it does not work, but I had in mind (x,y) \leq (x',y') iff
x < x'
or
x = x' and they are actually equal

[Damiano Testa]

I believe it might be the lex order

[Kevin Buzzard]

No, lex is a total order

[Damiano Testa]

Ok, so this example is not canonically ordered! I have tried to unfold all the properties of canonically_ordered, but I am constantly missing some...

[Kevin Buzzard]

And here you're saying (X,0) and (X,1) are incomparable

[Damiano Testa]

Ah, you are right about lex! I want to make incomparable the two different elements with the same first component. Anyway, this does not work!

[Johan Commelin]

(0,0) < (0,1)? But (0,1) + (0,1) = (0,0), right?

[Kevin Buzzard]

I think 00 and 01 are incomparable?

[Johan Commelin]

aha, ok

[Kevin Buzzard]

This might be an ordered semiring

[Damiano Testa]

Yes, (0,0) incomp with (0,1), but still (0,1)+(0,1)=(0,0)...

[Kevin Buzzard]

Which isn't canonically or totally ordered

[Kevin Buzzard]

Is that a problem?

[Damiano Testa]

No, I am floating on the surface of definitions and I remember you saying that a non-trivial sol to a+b=0 was a problem... ahahha

[Kevin Buzzard]

Rather irritatingly it seems to satisfy 2<=a and 2<=b implies a+b<=ab though

[Damiano Testa]

This is somewhat frustrating. I may have to write all the definitions down on a piece of paper, since chasing them around with extends makes it very hard for me to remember what we are assuming and what not!

[Kevin Buzzard]

Canonical order is easy Damiano. From the ring axioms you can easily check that a<=b iff exists c such that b=a+c is reflexive and transitive, but you don't get antisymmetry usually

[Kevin Buzzard]

And any questions about <= just immediately translate into questions about algebra with no <=

[Kevin Buzzard]

Eg 2<=a and 2<=b implies a+b<=ab is easy

[Kevin Buzzard]

The problem is that it's basically never antisymmetric

[Damiano Testa]

Ok, canonically ordered implies that you cannot keep adding non-zero elements to an element and get back to a place you already visited. I am on board with this!

[Kevin Buzzard]

Canonically ordered means that the order is not there

[Damiano Testa]

(I am going to have to meet with a student in 5 mins, but I am finding this discussion strangely interesting!)

[Kevin Buzzard]

I think we still have the question as to whether add_le_mul is true in a general commutative ordered semiring

[Damiano Testa]

Or maybe even not commutative... :smile:

[Kevin Buzzard]

I suspect not but I don't have enough good examples

[Damiano Testa]

What about Z+Z/3 and (2,1)+(2,1) not le (4,1)?

[Damiano Testa]

I need to go now!

[Kevin Buzzard]

But independent of that, the question of whether a canonically ordered comm semiring is an ordered semiring should be resolved because either there's a missing instance or there's an argument that we have our axioms wrong.

[Kevin Buzzard]

But (2,1) isn't >= 2

[Damiano Testa]

Aaargh!!

[Kevin Buzzard]

At least in the order we were discussing

[Kevin Buzzard]

Just make it >= 2 maybe?

[Damiano Testa]

Yes, that was the order I had in mind... My example does not work... again!

[Kevin Buzzard]

The problem is that this might also cause problems at 4

[Kevin Buzzard]

Maybe R=nat x nat with (a,b)<=(c,d) iff either a<c or (a=c and b=0) is an ordered semiring. If so then we're good because a=b=(2,1) would be a counterexample

[Kevin Buzzard]

Hmm it doesn't work because a<=b implies a+c<=b+c fails. I'm assuming that's an axiom!

[Kevin Buzzard]

Maybe drop random stuff like (0,0)<(0,1) too?

[Alex J. Best]

If anyone can actually extract all the axioms and make @Andrej Bauers alg work on this that might shed some light, https://github.com/andrejbauer/alg as we're only working with semirings there may exist finite examples?

[Kevin Buzzard]

I want to say the following: define a relation on nat x nat^2 (with the obvious ring structure) by demanding (a,b)<=(c,d) if a<=c and b=d, and also (2,00)<=(2,01) and (2,00)<=(2,10). Now take the smallest preorder structure which extends this and makes N x N^2 into a preordered semiring. Three things can happen. Either it's not an ordered semiring, in which case the argument that it isn't can be turned into a proof of add_le_mul for ordered semirings. Or it is an ordered semiring and (4,11)<=(4,00) (this to me is unlikely) and then this will also turn into a proof for ordered semirings. Or, finally, it is an ordered semiring and (4,11) is not <= (4,00), which gives us our counterexample.

[Kevin Buzzard]

Something still looks wrong with what I've said

[Johan Commelin]

what does gpt say?

[Kevin Buzzard]

Lol

[Kevin Buzzard]

I want to say the following: define a relation on nat x nat^2 (with the obvious ring structure) by demanding (a,b)<=(c,d) if a<=c and b=d, and also (2,00)<=(2,01) and (2,00)<=(2,10). Now take the smallest preorder structure which extends this and makes N x N^2 into a preordered semiring. Three things can happen. Either it's not an ordered semiring, in which case the argument that it isn't can be turned into a proof of add_le_mul for ordered semirings. Or it is an ordered semiring and (4,11)<=(4,00) (this to me is unlikely) and then this will also turn into a proof for ordered semirings. Or, finally, it is an ordered semiring and (4,11) is not <= (4,00), which gives us our counterexample.

[Kevin Buzzard]

Oh my mistake is that (2,0) is not 2 in nat X nat with the obvious ring structure

[Kevin Buzzard]

But I think that one can still make this strategy work. Consider the polynomial ring N[a,b] with the usual ring structure. Now define f<=g if g in f+nat, and also say 2<=a and 2<=b. Now take the smallest pre-order extending this and making it into a preordered semiring, and then take the smallest quotient making it an ordered semiring. Either this is a counterexample or there is no counterexample

[Kevin Buzzard]

I like the idea of using Bauer's tool. Is antisymmetry ok? It's an implication

[Damiano Testa]

My meeting is over.

Kevin, I like your approach!
About finite examples: I need to look whether ordered semirings must have some form of assumption saying that 1+1+... never repeats.

[Alex J. Best]

Yeah I just played with it a bit and you can specify not (..), a -> b, a <-> b, and exists z, y = x + z all fine, I'm just not sure what the complete list of axioms we need is!

[Johan Commelin]

#print ordered_semiring should give you a full list, right?

[Damiano Testa]

indeed!

#print ordered_semiring

@[class, protect_proj list.nil.{0} name]
structure ordered_semiring : Type u → Type u
fields:
ordered_semiring.add : Π {α : Type u} [c : ordered_semiring α], α → α → α
ordered_semiring.add_assoc : ∀ {α : Type u} [c : ordered_semiring α] (a b c_1 : α), a + b + c_1 = a + (b + c_1)
ordered_semiring.zero : Π {α : Type u} [c : ordered_semiring α], α
ordered_semiring.zero_add : ∀ {α : Type u} [c : ordered_semiring α] (a : α), 0 + a = a
ordered_semiring.add_zero : ∀ {α : Type u} [c : ordered_semiring α] (a : α), a + 0 = a
ordered_semiring.add_comm : ∀ {α : Type u} [c : ordered_semiring α] (a b : α), a + b = b + a
ordered_semiring.mul : Π {α : Type u} [c : ordered_semiring α], α → α → α
ordered_semiring.mul_assoc : ∀ {α : Type u} [c : ordered_semiring α] (a b c_1 : α), a * b * c_1 = a * (b * c_1)
ordered_semiring.one : Π {α : Type u} [c : ordered_semiring α], α
ordered_semiring.one_mul : ∀ {α : Type u} [c : ordered_semiring α] (a : α), 1 * a = a
ordered_semiring.mul_one : ∀ {α : Type u} [c : ordered_semiring α] (a : α), a * 1 = a
ordered_semiring.zero_mul : ∀ {α : Type u} [c : ordered_semiring α] (a : α), 0 * a = 0
ordered_semiring.mul_zero : ∀ {α : Type u} [c : ordered_semiring α] (a : α), a * 0 = 0
ordered_semiring.left_distrib : ∀ {α : Type u} [c : ordered_semiring α] (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
ordered_semiring.right_distrib : ∀ {α : Type u} [c : ordered_semiring α] (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
ordered_semiring.add_left_cancel : ∀ {α : Type u} [c : ordered_semiring α] (a b c_1 : α), a + b = a + c_1 → b = c_1
ordered_semiring.add_right_cancel : ∀ {α : Type u} [c : ordered_semiring α] (a b c_1 : α), a + b = c_1 + b → a = c_1
ordered_semiring.le : Π {α : Type u} [c : ordered_semiring α], α → α → Prop
ordered_semiring.lt : Π {α : Type u} [c : ordered_semiring α], α → α → Prop
ordered_semiring.le_refl : ∀ {α : Type u} [c : ordered_semiring α] (a : α), a ≤ a
ordered_semiring.le_trans : ∀ {α : Type u} [c : ordered_semiring α] (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
ordered_semiring.lt_iff_le_not_le : ∀ {α : Type u} [c : ordered_semiring α],
  auto_param (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) (name.mk_string "order_laws_tac" name.anonymous)
ordered_semiring.le_antisymm : ∀ {α : Type u} [c : ordered_semiring α] (a b : α), a ≤ b → b ≤ a → a = b
ordered_semiring.add_le_add_left : ∀ {α : Type u} [c : ordered_semiring α] (a b : α), a ≤ b → ∀ (c_1 : α), c_1 + a ≤ c_1 + b
ordered_semiring.le_of_add_le_add_left : ∀ {α : Type u} [c : ordered_semiring α] (a b c_1 : α), a + b ≤ a + c_1 → b ≤ c_1
ordered_semiring.zero_le_one : ∀ {α : Type u} [c : ordered_semiring α], 0 ≤ 1
ordered_semiring.mul_lt_mul_of_pos_left : ∀ {α : Type u} [c : ordered_semiring α] (a b c_1 : α), a < b → 0 < c_1 → c_1 * a < c_1 * b
ordered_semiring.mul_lt_mul_of_pos_right : ∀ {α : Type u} [c : ordered_semiring α] (a b c_1 : α), a < b → 0 < c_1 → a * c_1 < b * c_1

[Damiano Testa]

Ok, but most of these are easy: the ones with 0 and 1 we know!

[Alex J. Best]

Ok I can't do this alg thing now but if nobody else does I'll try tomorrow (who knows maybe someone will have a non brute force genuine math proof by then :grimacing: )

[Damiano Testa]

Removing the axioms having to do with ring (associative, distributive,...), the ones with 0 and 1 and order relation:

#print ordered_semiring

@[class, protect_proj list.nil.{0} name]
structure ordered_semiring : Type u → Type u
fields:
ordered_semiring.add_left_cancel : ∀ {α : Type u} [c : ordered_semiring α] (a b c_1 : α),
  a + b = a + c_1 → b = c_1
ordered_semiring.add_le_add_left : ∀ {α : Type u} [c : ordered_semiring α] (a b : α),
  a ≤ b → ∀ (c_1 : α), c_1 + a ≤ c_1 + b
ordered_semiring.le_of_add_le_add_left : ∀ {α : Type u} [c : ordered_semiring α] (a b c_1 : α),
  a + b ≤ a + c_1 → b ≤ c_1
ordered_semiring.zero_le_one : ∀ {α : Type u} [c : ordered_semiring α], 0 ≤ 1
ordered_semiring.mul_lt_mul_of_pos_left : ∀ {α : Type u} [c : ordered_semiring α] (a b c_1 : α),
  a < b → 0 < c_1 → c_1 * a < c_1 * b
ordered_semiring.mul_lt_mul_of_pos_right : ∀ {α : Type u} [c : ordered_semiring α] (a b c_1 : α),
  a < b → 0 < c_1 → a * c_1 < b * c_1

[Damiano Testa]

In particular, such rings have characteristic zero: if n, m are natural numbers, then n+m=mimplies n = 0 by writing n+m=n+0 and using one of the add_cancel.

[Damiano Testa]

So a non-trivial ordered ring is necessarily infinite.

[Johan Commelin]

Can Lean find the char_zero instance?

[Damiano Testa]

hmmm, I am not sure what char_zero in lean means...

[Damiano Testa]

let me try

[Damiano Testa]

I cannot find char_zero... should I import something?

[Damiano Testa]

(I'll make some tea in the meanwhile!)

[Johan Commelin]

$ rg -l char_zero
test/norm_num.lean
scripts/style-exceptions.txt
docs/undergrad.yaml
docs/overview.yaml
test/ring.lean
src/field_theory/separable.lean
src/field_theory/polynomial_galois_group.lean
src/algebra/char_zero.lean
src/algebra/field_power.lean
src/algebra/invertible.lean
src/tactic/norm_num.lean
archive/imo/imo1962_q4.lean
src/data/quaternion.lean
src/ring_theory/roots_of_unity.lean
src/algebra/char_p/basic.lean
src/algebra/algebra/basic.lean
src/algebra/module/basic.lean
src/algebra/algebra/tower.lean
src/ring_theory/polynomial/cyclotomic.lean
src/analysis/normed_space/basic.lean
src/data/polynomial/derivative.lean
src/data/num/lemmas.lean
src/data/int/char_zero.lean
src/ring_theory/witt_vector/witt_polynomial.lean
src/linear_algebra/affine_space/independent.lean
src/linear_algebra/affine_space/midpoint.lean
src/linear_algebra/affine_space/combination.lean
src/data/complex/basic.lean
src/data/complex/is_R_or_C.lean
src/data/padics/padic_numbers.lean
src/data/padics/padic_integers.lean
src/data/rat/cast.lean
src/data/real/ennreal.lean
src/data/zsqrtd/basic.lean

[Johan Commelin]

-- src/algebra/char_zero.lean
@[priority 100] -- see Note [lower instance priority]
instance linear_ordered_semiring.to_char_zero {R : Type*}
  [linear_ordered_semiring R] : char_zero R :=
⟨nat.strict_mono_cast.injective⟩

[Kevin Buzzard]

Damiano Testa said:

I cannot find char_zero... should I import something?

Search in VS Code for char_zero, find any file which uses it, open that file, wait for the orange bars to go away, and then right click on it to find where it's defined.

[Johan Commelin]

So Lean knows it for linear ordered semirings...

[Johan Commelin]

If you don't like waiting for orange bars... just use grep (-;

[Johan Commelin]

Just guess that it's defined as a class, and grep for class char_zero.

[Kevin Buzzard]

But grep won't find where the definition is, it will just print a gazillion times when it's used. Then you have to start guessing about whether it's a structure or class or a def.

[Johan Commelin]

$ rg "class char_zero"
src/algebra/char_zero.lean
14:class char_zero (R : Type*) [add_monoid R] [has_one R] : Prop :=

[Kevin Buzzard]

Aah right, if you can guess it's a class then you might be fine. Except that things like topological_space are a class but are defined as a structure

[Johan Commelin]

If you use the -l flag, then the gazillion times it's used will be reduced to the dozen filenames where it's used. Often I can guess which filename is the most "elementary" and likely contains the def'n.

[Damiano Testa]

I like the -l trick!

[Alex J. Best]

Damiano Testa said:

In particular, such rings have characteristic zero: if n, m are natural numbers, then n+m=mimplies n = 0 by writing n+m=n+0 and using one of the add_cancel.
So a non-trivial ordered ring is necessarily infinite.

Does char_zero imply infinite in this setting? It needn't in general right, adding 1 can just be absorbative into itself (1+1=1)?

[Kevin Buzzard]

Is fin n an ordered semiring?

[Damiano Testa]

I think that I can prove that n+m=n implies m=0, though...

[Kevin Buzzard]

because that isn't true in fin n

[Kevin Buzzard]

(this is not Z/n, this is the stupid addition where big+big=n-1)

[Damiano Testa]

I think that the proof above shows that fin n is not an ordered semiring

[Kevin Buzzard]

It's the quotient of nat by the relation n-1=n=n+1=n+2=.... Why is this not an ordered semiring?

[Damiano Testa]

n+1=n implies n+1=n+0 and you cancel n

[Alex J. Best]

Yeah this cancellative property is way stronger than my internal model of what an ordered semiring is!

[Kevin Buzzard]

Cancellation is an axiom for ordered semiring? :-/

[Damiano Testa]

Yes, the axioms are further up in the thread

[Kevin Buzzard]

Is ordered semiring just something which some mathlib dev just made up? It's not like there's a Wikipedia page on it.

[Damiano Testa]

I do not know the source of the concept: I did not know it before yesterday evening!

[Damiano Testa]

And I only looked at all the axioms on the same place after Johan's suggestion of printing them!

[Kevin Buzzard]

In mathlib it extends ordered_cancel_add_comm_monoid. In the few references I can find on the internet, this is not mentioned. The definition in mathlib does not really seem to match the docstring.

[Johan Commelin]

sounds like we are in for a giant refactor :rofl:

[Kevin Buzzard]

I do not see the point of the class at all

[Damiano Testa]

And just to prove that the sum is less than the product...

[Kevin Buzzard]

But for this add_mul thing, this cancellation axiom presents a big problem for my strategy.

[Kevin Buzzard]

The idea is this. Construct the "universal commutative ordered semiring with 2<=a and 2<=b" and check it there.

[Kevin Buzzard]

Now I had imagined that this would not be too hard. Here's a sketch of what I had in mind. First start with $\N[a,b]$ and assume $0<1$ and $2\leq a$ and $2\leq b$. Certainly there are orders making this into an ordered semiring, for example you can map into the reals sending a to [random transcendental number bigger than 2] and b to [random independent transcendental bigger than 2] and then pull the order back.

[Damiano Testa]

From this perspective, the cancellation axioms appear very strange. However, I am perfectly happy to assume existence of opposites and it seems a weak condition to assume

[Kevin Buzzard]

Now I suspect that the order structures on a fixed semiring making it into an ordered semiring will form a lattice with arbitrary infs (just intersect the relations). So we can look at the intersection of all the orders satisfying 0<1 and 2<=a and 2<=b.

[Kevin Buzzard]

The intersection is an "abstract" way of constructing the minimal ordering, but as we all know there is also a "constructive" way of constructing this minimal order, by defining an inductive prop <=, throwing in 0<1 and 2<=a and 2<=b as constructors, and also one constructor for each axiom.

[Kevin Buzzard]

Now the idea was that each constructor "makes stuff bigger", and in particular any proof of a+b<=ab will have to only use facts about things smaller than ab in some appropriate order, where the axiom constructors all say (small <='s implies big <=)

[Kevin Buzzard]

However le_of_add_le_add_left does not satisfy this "well-foundedness" property, meaning that I cannot eliminate proving a+b<=ab from a+b+a^100+37b^100 <= ab+a^100+37b^100 :-(

[Kevin Buzzard]

Anyway, this seems to answer the original question in this thread. As far as I can see, fin 2 is (or more precisely can be made into) a perfectly good canonically_ordered_comm_semiring which isn't an ordered_semiring as far as mathlib is concerned. Do people agree?

[Eric Wieser]

Kevin Buzzard said:

(this is not Z/n, this is the stupid addition where big+big=n-1)

I thought addition on fin was defeq to addition on zmod, even though we discussed changing it

[Kevin Buzzard]

sure, maybe, but right now I'm talking about the stupid addition

[Kevin Buzzard]

(my view on this is that fin n shouldn't really even have an addition, if you're adding things in fin n then you're not thinking about fin n correctly and should be using another type)

[Johan Commelin]

Yakov is working on a refactor that will give fin n the absorbing addition.

[Damiano Testa]

absorbing means max?

[Johan Commelin]

I think it makes sense to have that structure in mathlib. I don't care how it's called.

[Kevin Buzzard]

no it means "add, but if it's bigger than n-1 then just let it be n-1"

[Damiano Testa]

ah, max min (a+b) (n-1), then?

[Johan Commelin]

min?

[Kevin Buzzard]

same for mul. It's the quotient of the semiring $\N$ by the relation $n-1=n=n+1+...$

[Kevin Buzzard]

This relation preserves + and * but does not come from an ideal.

[Damiano Testa]

Ok, so the consensus seems to be to avoid ordered_semiring, right? If so, then I might go with Johan's proof for linear_ordered_semiring. Does this seem like a good choice?

[Damiano Testa]

The relevant PR is #6031: I should have mentioned this earlier...

[Damiano Testa]

(Johan, since this is your proof, feel free to make your own PR, if you prefer!)

[Kevin Buzzard]

It seems to me that the current status of the questions on this thread are: (1) I am claiming that fin n with this absorbing structure will be a canonically ordered comm_semiring which isn't an ordered_semiring in mathlib's sense, answering the original question. (2) The definition of ordered semiring in mathlib seems to have no reference, and contains le_of_add_le_add_left. In the literature I cannot find any examples of where le_of_add_le_add_left is an axiom for ordered semirings (indeed it's hard to find many mentions of ordered semirings in the literature; note that le_of_add_le_add_left is not unreasonable for ordered rings because we have additive inverses so it's implied by a<=b->a+c<=b+c, which is a reasonable axiom). (3) Mathlib's ordered semirings are hence arguably pathological objects so it's perhaps not worth wasting time asking questions about them right now until (2) is resolved, thus both the original question in this thread, and asking whether add_le_mul is true for mathlib's ordered semirings, are pathological questions right now (and don't deserve attention until we have some evidence that le_of_add_le_add_left is a relevant axiom), and (4) we still don't know the answer to whether add_le_mul is true in what people on the internet think an ordered_semiring is but I have sketched what I think is an approach which will lead to a counterexample above. On the other hand add_le_mul is true for canonically ordered semirings and totally ordered semirings, and given that mathlib's ordered semirings are pathological right now, this resolves all the non-pathological questions that can be asked about mathlib's structures right now.

[Johan Commelin]

@Damiano Testa If you are making other PRs in this area, please include it. I'm too busy with teaching :see_no_evil:

[Kevin Buzzard]

The literature on ordered semirings is sparse and, in stark contrast to the usual conventions, no two definitions of an ordered semiring in the literature coincide. Gan and Jiang (Journal of Math Research and Exposition, in 2011 -- I've never heard of this journal BTW) define it but have as one of their axioms 0<=c for all c. Faible and Peis (2006, random preprint on internet so approach with caution) define it but demand that ab<=a (they're thinking about lattices). Ayutthaya and Pibaljommee give the definition which I expect in an article in 2015 in International Journal of Maths and Maths Sciences (another journal I don't think I've heard of) , i.e. a<=b implies a+x<=b+x, ax<=bx and xa<=xb (oh -- they don't demand x>=0 for the latter so probably they have 0 as their minimal element again) , but don't demand a 1 (or this cancellation axiom). Rao, Kumar, Venkateswarlu and Kumar (Mathematica Maravica 2018, never heard of it either) give a related definition of ordered Gamma-semiring with three axioms, two of which are identical, and none of which involve cancellation. Tentative conclusions are that the mathematical community doesn't have a standard convention for what an ordered semiring is, but nowhere in the literature (such as it is) can I find any mention of cancellation for + and <=.

[Kevin Buzzard]

https://github.com/leanprover/lean/commit/362f972edab4bc4fdb5e3085c2f1f4f32abee096

So Leo added them in 2016, extending ordered_mul_cancel_comm_monoid and then renaming mul to add (so the assumption was there right from the start).

[Damiano Testa]

Thanks for this, Kevin!

In the meanwhile, I proved that ordered_semiring has char_zero: turns out, it was almost already there!

import algebra.char_zero

instance char_zero_ordered_semiring {R : Type*} [ordered_semiring R] [nontrivial R] :
  char_zero R :=
{ cast_injective := injective_of_increasing (λ (a b : ℕ), a < b)  (λ (a b : R), a < b) coe
    (λ x y xy, nat.cast_lt.mpr xy) }

[Damiano Testa]

The nontrivial PR just got merged, so now we can start removing assumptions still! :grinning_face_with_smiling_eyes:

[Eric Wieser]

I think that instance might be bad, because there might be a docs#char_zero.nontrivial instance that forms a loop?

[Damiano Testa]

I was not planning of making a PR with this instance, but I would like to understand what would be the issue with nontrivial. What is it that would form a loop?

The link you sent does not work for me.

[Kevin Buzzard]

Char 0 implies non-trivial, and if this is also an instance then you might end up with the type class inference system (the thing which looks at the instances) finding an ordered semiring and then going into a loop constantly proving non-trivial -> char_zero -> non-trivial -> char_zero -> ... when trying to do something else. But my understanding of the actual computer program which runs the type class inference system (it's a C++ program in core Lean) is very poor, so I don't know whether this kind of thing is likely to happen or not.

[Damiano Testa]

Ah, I see! I understand now what the potential issue could be.

Do you think that this might explain why the instance is not there?

[Eric Wieser]

I think you could certainly add it as a lemma

[Kevin Buzzard]

There's no harm in making it a lemma (you could try library_search to see if it's already there) but Eric is pointing out that there might be a problem with it being an instance (which is nothing more than a def or lemma plus an @[instance] tag).

[Eric Wieser]

docs#injective_of_increasing (λ (a b : ℕ), a < b) (λ (a b : R), a < b) coe (λ x y xy, nat.cast_lt.mpr xy looks like it might be a strict_monotone statement that already exists somewhere

[Damiano Testa]

import algebra.char_zero

lemma char_zero_ordered_semiring {R : Type*} [ordered_semiring R] [nontrivial R] :
  char_zero R :=
{ cast_injective := nat.strict_mono_cast.injective }

[Eric Wieser]

nat.strict_mono_cast.injective

[Damiano Testa]

Updated!

[Damiano Testa]

However, I am not sure whether to PR this, partly since I would not know where to put it: the ordered_semiring file does not import char_zero and in char_zero there are no examples...

[Eric Wieser]

Right next to docs#linear_ordered_semiring.to_char_zero would make sense

[Eric Wieser]

Indeed, src#linear_ordered_semiring.to_char_zero has exactly your proof, so probably it makes senes to add lemma ordered_semiring.to_char_zero, and redefine instance linear_ordered_semiring.to_char_zero := semiring.to_char_zero

[Damiano Testa]

PR #6038!

[Yakov Pechersky]

Regarding refactoring fin, first we have to rip out the fin ops definitions in core. They're used to define unsigned, which is what makes all of expr naming work. When lean#527 is merged, the actual mathlib refactor of fin can start.

[Bhavik Mehta]

I think I've got a construction of a ordered_semiring in which 2a <= 2b -> a <= b fails, I'm trying to check it in Lean at the moment

[Damiano Testa]

In the meanwhile, I also pushed Johan's proof: PR #6043.

[Bhavik Mehta]

Yeah, I've got a ordered_comm_semiring in which 2a <= 2b -> a <= b fails

[Bhavik Mehta]

I think I can make it into a canonically ordered one too

[Riccardo Brasca]

Is it fin n as suggested above?

[Bhavik Mehta]

No

[Bhavik Mehta]

@[derive [comm_semiring]]
def K : Type := subsemiring.closure ({1.5} : set ℚ)

instance : has_coe K ℚ := ⟨λ x, x.1⟩

instance : preorder K :=
{ le := λ x y, x = y ∨ (x : ℚ) + 1 ≤ (y : ℚ),
  le_refl := λ x, or.inl rfl,
  le_trans := λ x y z xy yz,
  begin
    rcases xy with (rfl | _), { apply yz },
    rcases yz with (rfl | _), { right, apply xy },
    right,
    linarith
  end }

[Bhavik Mehta]

I can post a full gist if that's convenient, but it's not particularly interesting; that's the semiring structure and the partial order structure, the counterexample is a = 1, b = 1.5

[Bhavik Mehta]

In particular this is cancellative

[Bhavik Mehta]

I've upgraded it to a canonically_ordered_comm_semiring now, (thanks Kevin!)

[Julian Külshammer]

I wonder whether mathlib should at some point also start collecting such counterexamples.

[Kevin Buzzard]

The example I like best right now is $A=\{x\in\mathbb{R}\,|\,x=0\lor x\geq1\}$ with the rather bizarre $\leq$ defined by $a\leq b$ in $A$ iff $a=b$ or $a+1\leq b$ in $\mathbb{R}$.

[Kevin Buzzard]

So again $1\leq 1.5$ is false, but doubling it it's true

[Bhavik Mehta]

Kevin Buzzard said:

The example I like best right now is $A=\{x\in\mathbb{R}\,|\,x=0\lor x\geq1\}$ with the rather bizarre $\leq$ defined by $a\leq b$ in $A$ iff $a=b$ or $a+1\leq b$ in $\mathbb{R}$.

Yeah, this was my upgraded example

[Johan Commelin]

Julian Külshammer said:

I wonder whether mathlib should at some point also start collecting such counterexamples.

I think it should. But I don't yet know what the best way is to organize this. They shouldn't be scattered all over the place, I guess.

[Johan Commelin]

And ideally they would be tagged in some way, so that automation such as slim_check (or similar stuff, I don't know) can take advantage of them.

[Riccardo Brasca]

These remarks deserve definitely to be mentioned at least in the doc string... especially for not so well known notions

[Patrick Massot]

Yes, I think mathlib should contain counter-examples. They also act as sanity checks for the definitions.

[Julian Külshammer]

For me this naively sounds like a version of inhabited where instead of supplying one example one should supply a non-example which is an example of the things it extends.

[Patrick Massot]

I meant something more general, not only when extending structures.

[Mario Carneiro]

Late to the party, but my general sense is that a typeclass like ordered_semiring shouldn't have anything "cancellative" about it. ordered_cancel_add_comm_monoid seems named well enough, but it shouldn't be an ancestor of ordered_semiring, which should admit fin n with saturating add as an example

[Mario Carneiro]

I don't think the counter examples need to be formally stated or proved, though

[Mario Carneiro]

For me the main thing I learn from counterexamples is to not attempt a certain theorem, and for that formality in the counterexample is not needed

[Mario Carneiro]

They could be in the docstrings, though of what exactly I'm not sure

[Eric Wieser]

Slim_check seems like a particularly good motivation for this type of pathological typeclass instance to be in mathlib somewhere

[Eric Wieser]

Having a collection of examples that satisfy a typeclass A but not a derived typeclass B would allow a slim-check-like tactic to say "this is false for A but if you strengthen your requirement to B it might not be

[Damiano Testa]

I really like these examples: thank you all who contributed them!

I also think that counterexamples are fundamental to maths and therefore should find their way into mathlib. However, I am not sure what the best approach is.

[Mario Carneiro]

By the way, I think it is safe to assume that class A implies class B iff there is an instance that says so; if there is no instance then most likely it's false, because mathlib tries to be complete about such things

[Damiano Testa]

Just to make sure that I understand correctly: \N + zmod 2 without (0,1) and comparing elements just based on their \N coordinate, provided they are at least 1 away is another version of the same example as above, right? It is canonically ordered and an ordered semiring, where (1,0) and (1,1) are not comparable, but their doubles are actually equal.

Am I missing some further assumption?

[Kevin Buzzard]

This looks like it should work to me, but it's always safest to formalise the argument ;-)

[Damiano Testa]

In case people find it useful, I pushed a counterexamples branch to mathlib. I am trying to formalize the example that I mentioned above, but if someone wants to add other (counter)examples, feel free to do so!

[Bhavik Mehta]

Note that I think we don't have a counterexample to the original 2 <= a -> 2 <= b -> a + b <= a * b question (I think) for ordered-semirings. As far as I can tell, amongst the semirings we've found which fail 2a <= 2b -> a <= b, I don't think any of them contradict the original problem

[Damiano Testa]

I agree with you: so far, I do not know if 2 ≤ a v 2 ≤ b implies a + b ≤ a * b in an ordered (commutative) semiring.

[Kevin Buzzard]

I thought that we didn't know if 2<=a and 2 <=b implied a+b<=a*b in the pathological structure which is an ordered_semiring, but we did know it wasn't true in what the literature calls an ordered semiring.

[Kevin Buzzard]

oh maybe we never finished the proof

[Kevin Buzzard]

Today's idea: let the semiring be {0,1,2,3,4,a,b,a+b,ab,a+1,a+2,b+1,b+2,2a, 2b, a^2, b^2, BIG}

[Kevin Buzzard]

where I'm thinking of a=2+epsilon and b=2+delta and BIG means "5 or more" (so e.g 3+a=BIG etc)

[Kevin Buzzard]

Now look at the ordering generated by 0<1<2<3<4, everything <= BIG and 2<=a, 2<=b

[Kevin Buzzard]

close under ordered semiring axioms and it will either turn into a counterexample or a proof

[Kevin Buzzard]

but I am not talking about mathlib ordered semirings here, note that 3+4<=2+4 is true but 3<=2 is false.

[Damiano Testa]

I think that I agree with you, but, to be honest, the axioms of ordered semirings are so strange that I really need to write them down to understand what the implications of "close under the axioms" are.

[Kevin Buzzard]

I'm talking about literature ordered semirings. I think the axiom should be removed. I suspect Leo just added it randomly

[Kevin Buzzard]

Damiano I think the definition of ordered semiring in Lean 3 is wrong and there is no point investing any time investigating it. It's like deleting additive associativity from the axioms of a ring and then asking questions about the resulting pathological structure -- it's not worth investing time in it.

[Damiano Testa]

Ok, fair enough!

[Kevin Buzzard]

Nowhere in the literature is this cancellation axiom, it is an embarrassment that our definition of ordered semiring has this axiom in.

[Kevin Buzzard]

With the axiom removed I think my sketch above will get to the bottom of it and I strongly suspect that the boring answer will be that the ring above is a counterexample.

[Kevin Buzzard]

A more interesting question would be to see what happens if the lemma is removed from the definition of ordered semiring. I doubt anything will break, and furthermore you'll be able to prove that a canonically ordered comm semiring is an ordered semiring

[Damiano Testa]

This could be a fun experiment, I agree!

[Damiano Testa]

Somehow, I suspect that something will break down, but maybe not much.

[Kevin Buzzard]

Note that for linear_ordered semirings the axiom can be proved

[Damiano Testa]

And in that case, Johan proved add_le_mul. Maybe that one is the important axiom? Ahaha

[Damiano Testa]

It would be funny to mix add and mul like that...

[Damiano Testa]

Anyway, if I get a chance, I will try to remove the axiom and see what happens.. but not tonight!

[Damiano Testa]

Kevin, I think that your idea does indeed construct a counterexample. Here is an attempt at an explanation: actually formalizing it seems very long for me!

Make zmod 2 × zmod 2 intro an ordered ring by defining the three non-zero elements to be all incomparable and all greater than (0, 0). Intuitively, we have three rays, all starting at zero, but incomparable with one another.

The actual ring is ℕ × zmod 2 × zmod 2 with its normal (component-wise) addition and multiplication. For the order, let m, n : ℕ and a, b : zmod 2 × zmod 2. We set (m, a) ≤ (n, b) if and only if

• m < n, or
• m = n and a ≤ b.

This is the "lexicographic preorder". From each natural number, sprout out 3 incomparable directions.

Now, (2, (1, 0)) and (2, (0, 1)) are both at least 2 * (1, (1, 1)) = (2, (0, 0)). However,

• their sum (2, (1, 0)) + (2, (0, 1)) = (4, (1, 1)) and
• their product (2, (1, 0)) * (2, (0, 1)) = (4, (0, 0))

are comparable, but the inequality is the wrong one!

[Mario Carneiro]

I don't think that's an ordered ring. (0, 0) <= (0, 1) but if you add (1, 0) on both sides you get (1, 0) <= (1, 1) which fails

[Damiano Testa]

Ah, your example is taking place in zmod 2 × zmod 2, right? Hmm, I need to think more about this!

[Kevin Buzzard]

If a=2+e and b=2+f with e,f>=0 then a+b+(e+f+ef)=ab so you have to avoid this

[Kevin Buzzard]

My impression with Bhavik's {0} union {x>=1} example where a<=b in the ring if a=b or a+1<=b in the reals is that you can, if you're lucky, drop various <=s and preserve ordered ring axioms, this is why maybe building up a weird finite counterexample might work

[Bhavik Mehta]

I've been playing with the semiring

@[derive [comm_semiring]]
def K : Type := mv_polynomial bool ℕ

inductive K_le : K → K → Prop
| zero_le_one : K_le 0 1
| refl (x) : K_le x x
| trans (x y z) : K_le x y → K_le y z → K_le x z
| add_le_add_left (x y z) : K_le x y → K_le (x + z) (y + z)
| mul_le_mul_left (x y z) : K_le x y → K_le (x * z) (y * z)
| le_of_add_le_add_left (x y z) : K_le (x + z) (y + z) → K_le x y
| two_le_tt : K_le 2 (X tt)
| two_le_ff : K_le 2 (X ff)

based off your finite example (though I'm trying to make it into a mathlib ordered semiring mostly because I think it's a fun puzzle), I think the difficulty here is in showing that the ordering generated by the ordered semiring axioms isn't obviously antisymmetric - curiously enough including le_of_add_le_add_left in there makes it a little easier - but I still can't complete the antisymmetry proof. Perhaps in the finite case you mention it's easier though, since you could probably just case bash.

[Kevin Buzzard]

I was thinking that it might just be easier to do the finite example with Andrej Bauer's tool.

[Alex J. Best]

I tried this now and it doesn't seem any finite models exist for the canonically ordered comm semiring. I could be encoding it incorrectly still, I can't quite get alg to recognize the canonically ordered property well, I don't see the reason why it should be infinite from the axioms.

[Mario Carneiro]

well that's false

instance : canonically_ordered_comm_semiring unit :=
by refine { add := λ _ _, (),
  zero := (),
  le := λ _ _, true,
  lt := λ _ _, false,
  lt_iff_le_not_le := dec_trivial,
  bot := (),
  mul := λ _ _, (),
  one := (),
  .. }; dec_trivial

[Kevin Buzzard]

Well obviously the trivial ring works, Alex is a mathematician so he is obviously excluding all trivial counterexamples to any statement he makes.

[Kevin Buzzard]

Is this not in punit_instances btw?

[Kevin Buzzard]

Is 0<=1 an axiom in these wretched things? If not then any ring with <= := = works right (finite or not). If so then either 0=1 giving the example too trivial for us mathematicians to care about, or 0<1<2<3<...

[Mario Carneiro]

I don't think you can set <= to = in a canonically ordered whatever because the canonical order thing characterizes exactly what <= is

[Mario Carneiro]

(unless it's the trivial ring, of course)

[Mario Carneiro]

0 <= x is a theorem in canonically ordered monoids

[Mario Carneiro]

You don't know that x |-> a + x is injective, so you can't deduce x < y -> a + x < a + y so the infinite chain 0<1<2<... doesn't work

[Mario Carneiro]

it seems like fin n should be an instance

[Mario Carneiro]

instance : canonically_ordered_comm_semiring bool :=
by refine { add := bor,
  zero := ff,
  le := λ a b, a → b,
  bot := ff,
  mul := band,
  one := tt,
  .. }; dec_trivial

[Bhavik Mehta]

Alex J. Best said:

I tried this now and it doesn't seem any finite models exist for the canonically ordered comm semiring. I could be encoding it incorrectly still, I can't quite get alg to recognize the canonically ordered property well, I don't see the reason why it should be infinite from the axioms.

I might be missing something, but I thought a+b <= a*b always holds in canonically ordered comm semirings for 2 <= a and 2 <= b - don't we always have 0 <= x, and then Damiano's original proof basically works

[Adam Topaz]

I haven't been following this thread at all, but isn't nnreal such an object?

[Adam Topaz]

Oh, nevermind, I missed the inequalities with 2

[Alex J. Best]

Cool, there must be a problem with the translation to alg then

Constant 0 1 _.
Binary + *.
Relation <=.
Relation <.

Axiom plus_commutative: x + y = y + x.
Axiom plus_associative: (x + y) + z = x + (y + z).
Axiom zero_neutral_left: 0 + x = x.
Axiom mult_associative: (x * y) * z = x * (y * z).
Axiom mult_comm: x * y = y * x.
Axiom one_unit_left: 1 * x = x.
Axiom one_unit_right: x * 1 = x.
Axiom distrutivity_right: (x + y) * z = x * z + y * z.
Axiom distributivity_left: x * (y + z) = x * y + x * z.

# Consequences of axioms that make alg run faster:

Axiom zero_neutral_right: x + 0 = x.
Axiom mult_zero_left: 0 * x = 0.
Axiom mult_zero_right: x * 0 = 0.


# order axioms
Axiom reflexivity: x <= x.
Axiom transitivity: x <= y /\ y <= z -> x <= z.
Axiom antisymmetry: x <= y /\ y <= x -> x = y.
Axiom canon: forall x y, exists z, x + z = y -> x <= y.
Axiom canon: forall x y, x <= y -> exists z, y = x + g.
Axiom totality: x <= y \/ y <= x.

Axiom : x <= y -> x + z <= y + z.
Axiom eq_zero_or_eq_zero_of_mul_eq_zero: x * y = 0 -> x = 0 \/ y = 0.
Axiom lt_iff_le_not_le: x < y <-> x <= y /\ not y <= x.
Axiom bot_le: _ <= x.

[Alex J. Best]

I think the issue must be what the exists is quantifying over in the canon axioms

[Alex J. Best]

But if I try to bracket it I get an error message when parsing.

[Alex J. Best]

Kevin Buzzard said:

Well obviously the trivial ring works, Alex is a mathematician so he is obviously excluding all trivial counterexamples to any statement he makes.

I wish this was what happened :smile:, once again my mental model has 0, 1 separate so I didn't even consider a 1-element example

[Bhavik Mehta]

"Axiom canon: forall x y, x <= y -> exists z, y = x + g." looks dubious to me - surely you want y = x + z on the rhs

[Alex J. Best]

oops thats a copy paste error!

[Bhavik Mehta]

Oh also you have totality - you don't want to assume totality for these, an ordered semiring only needs a partial order structure

[Bhavik Mehta]

I also wonder if it runs faster if you don't include < in the definition, since it can be inferred just from the definition of <=

[Damiano Testa]

Damiano Testa said:

import algebra.char_zero

lemma char_zero_ordered_semiring {R : Type*} [ordered_semiring R] [nontrivial R] :
  char_zero R :=
{ cast_injective := nat.strict_mono_cast.injective }

Alex, I am not sure whether this will answer your question, but nontrivial ordered_semirings have characteristic zero, so they are never finite.

[Alex J. Best]

Yeah I got that (slowly during the discussion the other day) I'm thinking of the canonical ordered version now, and wondering why I can't convince alg to find finite ones (which as mario observed certainly exist).

[Alex J. Best]

Or maybe I don't get it, Mario's one is trivial after all!

[Alex J. Best]

Nevertheless my alg code is wrong as it doesn't even find the trivial one

[Damiano Testa]

Ah, ok! I thought that the question was about ordered_semirings that were also canonically ordered! I find the names really confusing! I never remember whether a canonically_ordered_semiring is also an ordered_semiring...

[Damiano Testa]

I need to think more about Mario's bool example of a canonically ordered semiring of non-zero characteristic.

[Bhavik Mehta]

Kevin Buzzard said:

Today's idea: let the semiring be {0,1,2,3,4,a,b,a+b,ab,a+1,a+2,b+1,b+2,2a, 2b, a^2, b^2, BIG}

I've shown that this semiring is a semiring, and that it has a partial order structure satisfying x <= y -> x+z <= y+z and x <= y -> xz <= yz, is there anything else left to check for this to be an example of the literature definition of an ordered semiring which doesn't have a+b <= a*b?

[Kevin Buzzard]

I guess commutativity of * (or else you're missing x<= y implies zx<=zy) but this looks good to me. Does the cancellation axiom fall?

[Bhavik Mehta]

Oops yeah I should have said comm semiring. Cancellation fails for exactly the reason you suggested it should, 3+2 >= 4+2 but 3 < 4