coercion from nnreal to ennreal

Stream: new members

[Jason KY.]

Hi! I'm trying to coerce a nonnegative real to a ennreal using a coercion

import data.real.ennreal

open_locale nnreal ennreal

variables (a : ℝ≥0) (b : ℝ) (hb : 0 ≤ b)

#check (a : ℝ≥0∞) -- works

#check (⟨b, hb⟩ : ℝ≥0) -- works

#check ((⟨b, hb⟩ : ℝ≥0) : ℝ≥0∞)
/- invalid type ascription, term has type
  {r // 0 ≤ r}
but is expected to have type
  ℝ≥0∞
-/

I have no clue why the third #check doesn't work

[Alex J. Best]

If you put two type ascriptions in a row with nothing else lean sometimes just ignores the first one, so its trying to interpret ⟨b, hb⟩ as a ℝ≥0∞, you can force lean to do what you intend by adding a docs#id as in

#check ((id ⟨b, hb⟩ : ℝ≥0) : ℝ≥0∞)

but what the actual fix is depends on what you are trying to do.

[Jason KY.]

I would like to address the comment from here: https://github.com/leanprover-community/mathlib/pull/8597#discussion_r685779359 though I don't know if its worth using id just to force a coercion instead of using some since they are all defeq

[Alex J. Best]

Looks a bit funny but making the coe explicitly works, and looks like it gives the right definition

import data.real.ennreal

open_locale nnreal ennreal

variables (a : ℝ≥0) (b : ℝ) (hb : 0 ≤ b)

#check (a : ℝ≥0∞) -- works

#check (⟨b, hb⟩ : ℝ≥0) -- works

def t : ennreal := @coe nnreal ennreal _ ⟨b, hb⟩
#print t
set_option pp.all true
#print t

[Yury G. Kudryashov]

When you write ((⟨b, hb⟩ : ℝ≥0) : ℝ≥0∞), Lean verifies that ⟨b, hb⟩ has type defeq to nnreal but continues to treat it as {r // 0 ≤ r}. There are a few workarounds: (1) add id; (2) use @coe nnreal ennreal so that Lean expects an nnreal when it parses ⟨b, hb⟩; (3) use show nnreal, from ⟨b, hb⟩.

[Kevin Buzzard]

(3) and (1) are the same IIRC

[Eric Wieser]

2 is best in lemma statements