# Zulip Chat Archive

## 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 `ennreal`

s? 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 :=
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 (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