0 as a member of Icc 0 1

Stream: new members

[Matias Heikkilä]

I would like to identify 0 as a member of the closed interval [0, 1] (see below)

theorem thm : true := by
  let x : Set.Icc (0 : ℝ) 1 := 0
  sorry

This does not work due to some type issues I don't understand well enough to fix it. Any pointers to help me understand what's going on?

[Alex J. Best]

What imports do you have? I get no errors when I use your code with import Mathlib (this is why we ask for imports in #mwe)

[Alex J. Best]

That said Set.Icc is a Set not a type so when you write what you have there you are coercing it to be the type of all elements contained in that set, which may or may not be what you need, it depends on the context.
To use it as a set you would make statements like

  have : 0 ∈  Set.Icc (0 : ℝ) 1 := by simp

[Alex J. Best]

Which says the real number 0 is contained in the subset of reals between 0 and 1

[Matias Heikkilä]

Thanks @Alex J. Best, afk for a bit. I’ll update the example and list the imports when I’m back

[Matias Heikkilä]

@Alex J. Best so the thing is I was preparing a small mathlib4 PR for submission, and I'm working on the file Mathlib/Topology/StoneCech.lean. With my current imports, the following should be an #mwe

import Mathlib.Topology.Bases
import Mathlib.Topology.DenseEmbedding
import Mathlib.Topology.UrysohnsLemma

theorem thm : true := by
  let x : Set.Icc (0 : ℝ) 1 := 0
  sorry

What I get is

failed to synthesize instance
  OfNat (↑(Icc 0 1)) 0

While this example doesn't really make sense on its own, it should succesfully isolate the issue I'm currently stuck with in the proof.

[Matias Heikkilä]

(deleted)

[Patrick Massot]

This too minimized. Maybe you would benefit from reading #xy.

[Patrick Massot]

We could define the instance Lean asks, but this is almost surely not what you should be doing.

[Matias Heikkilä]

Thanks, I guess my question really is, what is Lean trying to tell me here? And more generally, how to understand these kinds of errors better?

[Patrick Massot]

It is trying to tell you that the instance database that Lean is using when trying to go from a number literal to a Lean object of a given type does not contain any entry explaining how to take a 0 literal to an object with type ↑(Icc 0 1)

[Patrick Massot]

And again the root cause is that you probably want to use Icc 0 1 as a set and not as a type.

[Matias Heikkilä]

Thanks, this actually also helped me to understand the comment by Alex above

[Eric Wieser]

Patrick Massot said:

It is trying to tell you that the instance database that Lean is using when trying to go from a number literal to a Lean object of a given type does not contain any entry explaining how to take a 0 literal to an object with type ↑(Icc 0 1)

I think Alex's point is that the database does contain this information, but you only imported some of the database