Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: norm_num on ennreal


Yakov Pechersky (Aug 02 2022 at 23:40):

Is there a way to loosen the lemma requirements for norm_num to have it work for extended types? mwe:

import data.real.ennreal

example : (1 : ennreal)  2 :=
begin
  success_if_fail { norm_num },
  -- won't work because `norm_num` requires `linear_ordered_semiring`, which has
  -- `add_left_cancel : a + b = a + c → b = c`, which is not true for `a = ⊤`.
  refine ennreal.le_of_top_imp_top_of_to_nnreal_le _ _;
  norm_num
end

@Eric Rodriguez

Mario Carneiro (Aug 02 2022 at 23:43):

norm_num doesn't require that class, the theorems it uses do. If you can weaken the requirements on the lemmas then it should be fixed automatically

Mario Carneiro (Aug 02 2022 at 23:43):

but I would assume that the theorems are assuming the minimum requirements already

Yakov Pechersky (Aug 02 2022 at 23:44):

Sorry, I was fast and loose with the statement. Yes, its this collection of lemmas:

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

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

theorem sle_one_bit0 {α} [linear_ordered_semiring α] (a : α) : 1  a  1 + 1  bit0 a :=
bit0_le_bit0.2
theorem sle_one_bit1 {α} [linear_ordered_semiring α] (a : α) : 1  a  1 + 1  bit1 a :=
le_bit0_bit1 _ _
theorem sle_bit0_bit0 {α} [linear_ordered_semiring α] (a b : α) : a + 1  b  bit0 a + 1  bit0 b :=
le_bit1_bit0 _ _
theorem sle_bit0_bit1 {α} [linear_ordered_semiring α] (a b : α) (h : a  b) : bit0 a + 1  bit1 b :=
bit1_le_bit1.2 h
theorem sle_bit1_bit0 {α} [linear_ordered_semiring α] (a b : α) (h : a + 1  b) :
  bit1 a + 1  bit0 b :=
(bit1_succ a _ rfl).symm  bit0_le_bit0.2 h
theorem sle_bit1_bit1 {α} [linear_ordered_semiring α] (a b : α) (h : a + 1  b) :
  bit1 a + 1  bit1 b :=
(bit1_succ a _ rfl).symm  le_bit0_bit1 _ _ h

Mario Carneiro (Aug 02 2022 at 23:45):

the one that matters in this case is le_one_bit0 I think

Mario Carneiro (Aug 02 2022 at 23:46):

Actually I should take back what I said: I think these theorems are deliberately all using the same class for efficiency. So you would need a single class that implies all of them

Mario Carneiro (Aug 02 2022 at 23:48):

There is an alternative proof approach that norm_num uses for complex not-equal which could also apply here: if nat order-embeds in the target type, then it is possible to prove that both sides are equal to nat.cast of something and then do the proof on nat instead

Yakov Pechersky (Aug 02 2022 at 23:48):

Unfortunately, I don't think there is such a class

Mario Carneiro (Aug 02 2022 at 23:49):

this is what prove_nat_uncast does

Yakov Pechersky (Aug 02 2022 at 23:49):

Could we do this for rat.cast?

Mario Carneiro (Aug 02 2022 at 23:49):

there's also a version for rat

Yakov Pechersky (Aug 02 2022 at 23:49):

Ah, it doesn't embed

Mario Carneiro (Aug 02 2022 at 23:49):

no it does

Mario Carneiro (Aug 02 2022 at 23:49):

the nonnegative rats do

Mario Carneiro (Aug 02 2022 at 23:50):

prove_rat_uncast_nonneg

Mario Carneiro (Aug 02 2022 at 23:50):

oh, but it might not be a division_ring

Yakov Pechersky (Aug 02 2022 at 23:52):

So would you stick it into eval_ineq?

Mario Carneiro (Aug 02 2022 at 23:54):

no, prove_lt_nat would get a wrapper that checks for an instance of linear_ordered_semiring and otherwise uses this method

Mario Carneiro (Aug 02 2022 at 23:55):

Alternatively, and I haven't done this with other things before because I don't like to introduce typeclasses, you could just have a new typeclass for having an order embedding to nat / int / nonneg rat / rat

Yakov Pechersky (Aug 02 2022 at 23:56):

I see, you stick it in as deep as possible, relying on the nat-le/lt proving to be done "right" -- deferring the need for coercion as late as possible

Yakov Pechersky (Aug 02 2022 at 23:56):

more nat_cast and int_cast data fields :upside_down:

Mario Carneiro (Aug 02 2022 at 23:56):

no, this doesn't have to be a data carrying typeclass

Mario Carneiro (Aug 02 2022 at 23:57):

basically we're saying that casted naturals are in the "center" of the type

Mario Carneiro (Aug 02 2022 at 23:58):

when you prove theorems about bit0 and bit1 directly you don't have that fact available even though it's always going to be the case

Mario Carneiro (Aug 02 2022 at 23:58):

and that makes the lemmas have stronger hypotheses than you would like

Mario Carneiro (Aug 02 2022 at 23:58):

the nat_uncast stuff makes that explicit

Mario Carneiro (Aug 02 2022 at 23:59):

incidentally, in lean 4 this will trivially be available because numeric literals are defined like nat.cast instead of by recursive application of bit0 and bit1

Yakov Pechersky (Aug 03 2022 at 00:16):

Something like this?

meta def prove_nat_uncast_los (ic : instance_cache) (e : expr) :
  tactic (instance_cache × expr × option expr) := (do
  (ic, _)  ic.get `linear_ordered_semiring,
  pure (ic, e, none)) <|> do
  nc  mk_instance_cache `(),
  (ic, nc, e', p)  prove_nat_uncast ic nc e,
  pure (ic, e', some p)

Last updated: Dec 20 2023 at 11:08 UTC