norm_num for ennreal

Stream: general

[Yury G. Kudryashov]

Hi, would it be hard to make norm_num work for ennreals? E.g., the following fails:

import data.real.ennreal

example : (1 : ennreal) ≤ 3 := by norm_num

[Mario Carneiro]

Method 1 requires a linear_ordered_semiring. (PS: why does one_lt_bit1 need nontrivial and linear_ordered_semiring? One implies the other)

[Mario Carneiro]

Method 2 requires only semiring for the casting part, and char_zero for lifting not equal

[Mario Carneiro]

but it's not implemented for le and lt

[Mario Carneiro]

Do these theorems hold for ennreal?

theorem le_one_bit0 {α} [linear_ordered_semiring α] (a : α) (h : 1 ≤ a) : 1 ≤ bit0 a :=
le_of_lt (lt_one_bit0 _ h)
-- deliberately strong hypothesis because bit1 0 is not a numeral
theorem le_one_bit1 {α} [linear_ordered_semiring α] (a : α) (h : 0 < a) : 1 ≤ bit1 a :=
le_of_lt (lt_one_bit1 _ h)
theorem le_bit0_bit0 {α} [linear_ordered_semiring α] (a b : α) : a ≤ b → bit0 a ≤ bit0 b :=
bit0_le_bit0.2
theorem le_bit0_bit1 {α} [linear_ordered_semiring α] (a b : α) (h : a ≤ b) : bit0 a ≤ bit1 b :=
le_of_lt (lt_bit0_bit1 _ _ h)
theorem le_bit1_bit0 {α} [linear_ordered_semiring α] (a b : α) (h : a + 1 ≤ b) : bit1 a ≤ bit0 b :=
le_of_lt (lt_bit1_bit0 _ _ h)
theorem le_bit1_bit1 {α} [linear_ordered_semiring α] (a b : α) : a ≤ b → bit1 a ≤ bit1 b :=
bit1_le_bit1.2

[Mario Carneiro]

The constraints on ordered_semiring are too strict for ennreal, it requires a < b → 0 < c → c * a < c * b

[Mario Carneiro]

wikipedia also does not attest the lt-version of this theorem

[Yury G. Kudryashov]

For le theorems the answer is "yes".

[Mario Carneiro]

hm, that might be enough; the mutual recursion is mostly between le and sle (a + 1 <= b) theorems

[Mario Carneiro]

But we need an algebraic class that captures this

[Mario Carneiro]

These are the lt theorems:

theorem lt_one_bit0 {α} [linear_ordered_semiring α] (a : α) (h : 1 ≤ a) : 1 < bit0 a :=
lt_of_lt_of_le one_lt_two (bit0_le_bit0.2 h)
theorem lt_one_bit1 {α} [linear_ordered_semiring α] (a : α) (h : 0 < a) : 1 < bit1 a :=
one_lt_bit1.2 h
theorem lt_bit0_bit0 {α} [linear_ordered_semiring α] (a b : α) : a < b → bit0 a < bit0 b :=
bit0_lt_bit0.2
theorem lt_bit0_bit1 {α} [linear_ordered_semiring α] (a b : α) (h : a ≤ b) : bit0 a < bit1 b :=
lt_of_le_of_lt (bit0_le_bit0.2 h) (lt_add_one _)
theorem lt_bit1_bit0 {α} [linear_ordered_semiring α] (a b : α) (h : a + 1 ≤ b) : bit1 a < bit0 b :=
lt_of_lt_of_le (by simp [bit0, bit1, zero_lt_one, add_assoc]) (bit0_le_bit0.2 h)
theorem lt_bit1_bit1 {α} [linear_ordered_semiring α] (a b : α) : a < b → bit1 a < bit1 b :=
bit1_lt_bit1.2

I think they are all true for ennreal as well

[Mario Carneiro]

That is, bit0 is injective on ennreal, although that's definitely not true for all ordered semirings in the weak sense, for example saturating fin n does not have that property

[Mario Carneiro]

That said I really don't expect the generic norm_num method to work to prove things like (1 : fin 15) < (17 : fin 15)

[Mario Carneiro]

since it doesn't really have any concept of "characteristic", it thinks all numbers act the same in the target ring

[Mario Carneiro]

I'm not going to work on this right now, but I will say that norm_num is using the weakest available class that supports these theorems; if you refactor things so that there is a weaker class supporting these it should be a drop in replacement.

[Yury G. Kudryashov]

Thank you for an explanation.

[Kevin Buzzard]

IIRC linarith doesn't work on random total orders. Is there a similar list of lemmas which have to be satisfied? One could go the other way and make a minimal is_normnummable class and then make instances as required. Could one do the same for linarith?

[Mario Carneiro]

Sure, is_normnummable would do just fine, although I hope that it boils down to less than the laundry list of lemmas above, so the class has some independent usefulness and it's not dead weight in the typeclass system.

[Mario Carneiro]

I think something like a linear order + ring + le versions of the ordered ring axioms + 0 < 1 should suffice

[Kevin Buzzard]

Ennreal isn't a ring, hopefully you mean semiring

[Yury G. Kudryashov]

is_normnummable won't get in the way of the rest of the typeclass system if we have no instances assuming [is_normnummable.

[Yury G. Kudryashov]

BTW, what does norm_num do with negation?

[Yury G. Kudryashov]

(ignore, we have no unary - on (e)nnreal)

[Yury G. Kudryashov]

But we have subtraction.

[Kevin Buzzard]

norm_num works on naturals, right?

[Mario Carneiro]

There is a norm_num extension specifically for handling nat.sub

[Mario Carneiro]

It pretty much has to be that way since the instance that provides nat.sub is not a special case of any existing typeclass other than has_sub