## Stream: general

### Topic: norm_num for ennreal

#### Yury G. Kudryashov (Feb 23 2021 at 03:36):

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 (Feb 23 2021 at 04:19):

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 (Feb 23 2021 at 04:22):

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

#### Mario Carneiro (Feb 23 2021 at 04:22):

but it's not implemented for le and lt

#### Mario Carneiro (Feb 23 2021 at 04:23):

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 (Feb 23 2021 at 04:30):

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

#### Mario Carneiro (Feb 23 2021 at 04:33):

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

#### Yury G. Kudryashov (Feb 23 2021 at 06:12):

For le theorems the answer is "yes".

#### Mario Carneiro (Feb 23 2021 at 06:24):

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

#### Mario Carneiro (Feb 23 2021 at 06:25):

But we need an algebraic class that captures this

#### Mario Carneiro (Feb 23 2021 at 06:26):

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 :=
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 (Feb 23 2021 at 06:28):

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 (Feb 23 2021 at 06:29):

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 (Feb 23 2021 at 06:30):

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

#### Mario Carneiro (Feb 23 2021 at 06:39):

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 (Feb 23 2021 at 19:18):

Thank you for an explanation.

#### Kevin Buzzard (Feb 23 2021 at 20:41):

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 (Feb 23 2021 at 21:27):

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 (Feb 23 2021 at 21:28):

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

#### Kevin Buzzard (Feb 23 2021 at 21:42):

Ennreal isn't a ring, hopefully you mean semiring

#### Yury G. Kudryashov (Feb 24 2021 at 02:32):

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 (Feb 24 2021 at 02:32):

BTW, what does norm_num do with negation?

#### Yury G. Kudryashov (Feb 24 2021 at 02:33):

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

#### Yury G. Kudryashov (Feb 24 2021 at 02:34):

But we have subtraction.

#### Kevin Buzzard (Feb 24 2021 at 10:33):

norm_num works on naturals, right?

#### Mario Carneiro (Feb 24 2021 at 11:55):

There is a norm_num extension specifically for handling nat.sub

#### Mario Carneiro (Feb 24 2021 at 11:56):

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

Last updated: May 15 2021 at 23:13 UTC