0 < 2

Stream: lean4

[Jeremy Avigad]

Is it possible to prove (0 : ℝ) < 2 in Lean 4 with the mathlib3 binport? In full, the goal is here:

⊢ @LT.lt.{0} Real Real.hasLt (@OfNat.ofNat.{0} Real 0 (@Zero.toOfNat0.{0} Real Real.hasZero))
    (@OfNat.ofNat.{0} Real 2 (@AddMonoidₓ.instOfNat.{0} Real 2 Real.addMonoid Real.hasOne))

@Gabriel Ebner @Mario Carneiro

[Mario Carneiro]

I would try to prove that 0 and 2 are equal to nat.cast 0 and nat.cast 2 and then use nat.cast_lt to reduce it to something norm_num / dec_trivial can do

[Mario Carneiro]

Oh wait, it's already in that form

[Mario Carneiro]

I'm not quite sure how you got ofNat in your terms given that this is from mathlib, maybe binport is doing it? But see if you can apply Nat.cast_lt or whatever it's called

[Jeremy Avigad]

rw [Nat.cast_lt] and apply Nat.cast_lt.mpr don't seem to work. E.g. the first gives:

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
(fun a b [self : HasLiftT a b] => self.1) ℕ ?m.310 ?m.313 < (fun a b [self : HasLiftT a b] => self.1) ℕ ?m.310 ?m.314
⊢ 0 < 2

[Alexander Bentkamp]

Mario Carneiro said:

I'm not quite sure how you got ofNat in your terms given that this is from mathlib, maybe binport is doing it?

It's probably because we have this instance in our code:

noncomputable instance : CoeHTCT ℕ ℝ where coe := AddMonoidWithOneₓ.natCast

Is there a better way to get real numerals?

[Alexander Bentkamp]

Oh, maybe

noncomputable instance : CoeHTCT ℕ ℝ where coe := Nat.cast

? I'll try that tomorrow.

[Ramon Fernández Mir]

I proved it. But it's not pretty...

example : (0 : ℝ) < 2 := by
  have h1 : 0 = ((fun a b [self : HasLiftT a b] => self.1) ℕ ℝ 0) := by rfl
  have h2 : 2 = ((fun a b [self : HasLiftT a b] => self.1) ℕ ℝ 2) := by rfl
  rw [h1, h2]
  apply Nat.cast_lt.mpr
  norm_cast

[Jeremy Avigad]

It looks beautiful to me!

[Jeremy Avigad]

Interestingly, these give error messages:

example : (0 : ℝ) < 2 := by
  have : ((fun a b [self : HasLiftT a b] => self.1) ℕ ℝ 0) < ((fun a b [self : HasLiftT a b] => self.1) ℕ ℝ 2) := by
     sorry
  exact this

example : (0 : ℝ) < 2 := by
  show ((fun a b [self : HasLiftT a b] => self.1) ℕ ℝ 0) < ((fun a b [self : HasLiftT a b] => self.1) ℕ ℝ 2)

[Mario Carneiro]

I would assume that the < is being interpreted differently in those examples?

[Jeremy Avigad]

I think it's a matter of type inference having a hard time finding the instance when it is buried under a lambda. I tried helping it out with more information:

example : (0 : ℝ) < 2 := by
  have : @LT.lt.{0} Real Real.hasLt ((fun (a b : Type) [self : HasLiftT a b] => self.1) ℕ ℝ 0 : ℝ) ((fun (a b : Type) [self : HasLiftT a b] => self.1) ℕ ℝ 2 : ℝ) := by
    apply Nat.cast_lt.mpr
    norm_cast
  exact this

But still:

type mismatch
this
has type
@LT.lt.{0} Real Real.hasLt
((@fun (a b : Type) [self : HasLiftT.{?u.1608, ?u.1607} a b] => @HasLiftT.lift.{?u.1611, ?u.1610} a b self) Nat Real
?m.1620 (@OfNat.ofNat.{0} ?m.1622 0 ?m.1623))
((@fun (a b : Type) [self : HasLiftT.{?u.1804, ?u.1803} a b] => @HasLiftT.lift.{?u.1807, ?u.1806} a b self) Nat Real
?m.1814 (@OfNat.ofNat.{0} ?m.1816 2 ?m.1817)) : Prop
but is expected to have type
@LT.lt.{0} Real Real.hasLt (@OfNat.ofNat.{0} Real 0 (@Zero.toOfNat0.{0} Real Real.hasZero))
(@OfNat.ofNat.{0} Real 2 (@AddMonoidₓ.instOfNat.{0} Real 2 Real.addMonoid Real.hasOne)) : Prop