norm_num on ennreal

Stream: metaprogramming / tactics

[Yakov Pechersky]

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]

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]

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

[Yakov Pechersky]

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]

the one that matters in this case is le_one_bit0 I think

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

this is what prove_nat_uncast does

[Yakov Pechersky]

Could we do this for rat.cast?

[Mario Carneiro]

there's also a version for rat

[Yakov Pechersky]

Ah, it doesn't embed

[Mario Carneiro]

no it does

[Mario Carneiro]

the nonnegative rats do

[Mario Carneiro]

prove_rat_uncast_nonneg

[Mario Carneiro]

oh, but it might not be a division_ring

[Yakov Pechersky]

So would you stick it into eval_ineq?

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

more nat_cast and int_cast data fields :upside_down:

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

the nat_uncast stuff makes that explicit

[Mario Carneiro]

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]

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)