Zulip Chat Archive

Stream: general

Topic: norm_num for ennreal


view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Feb 23 2021 at 04:22):

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

view this post on Zulip Mario Carneiro (Feb 23 2021 at 04:22):

but it's not implemented for le and lt

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 23 2021 at 04:33):

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

view this post on Zulip Yury G. Kudryashov (Feb 23 2021 at 06:12):

For le theorems the answer is "yes".

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 23 2021 at 06:25):

But we need an algebraic class that captures this

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Feb 23 2021 at 19:18):

Thank you for an explanation.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Feb 23 2021 at 21:42):

Ennreal isn't a ring, hopefully you mean semiring

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Feb 24 2021 at 02:32):

BTW, what does norm_num do with negation?

view this post on Zulip Yury G. Kudryashov (Feb 24 2021 at 02:33):

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

view this post on Zulip Yury G. Kudryashov (Feb 24 2021 at 02:34):

But we have subtraction.

view this post on Zulip Kevin Buzzard (Feb 24 2021 at 10:33):

norm_num works on naturals, right?

view this post on Zulip Mario Carneiro (Feb 24 2021 at 11:55):

There is a norm_num extension specifically for handling nat.sub

view this post on Zulip 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