Singleton notation

Stream: mathlib4

[Dan Velleman]

Consider these example:

import Mathlib

example (x : Nat) : x ∈ {x} := Eq.refl _

example (x : Nat) : x ∈ ({x} : Set Nat) := Eq.refl _

The second one works, but the first gives the error "typeclass instance problem is stuck". It seems that Lean can't figure out the type of {x}. But it knows that x has type Nat. Shouldn't that be enough information for it to figure out that {x} has type Set Nat?

[Yury G. Kudryashov]

It can be Finset Nat as well.

[Yury G. Kudryashov]

In x ∈ s, Lean can find the type of x from the type of s, not vice versa.

[Dan Velleman]

Oh, I see.

[Kevin Buzzard]

This is a common gotcha and it became annoying from the moment mathlib3 was extended to allow {x,y,...} notation for finsets, but at the end of the day you can see the logic and I just got used to it.

[Mario Carneiro]

Aha, but lean 4 has a new trick up its sleeve for this situation:

import Mathlib.Data.Finset.Basic

attribute [default_instance] Set.instSingletonSet

example (x : Nat) : x ∈ {x} := Eq.refl _ -- look ma, no type ascription
example (x : Nat) : x ∈ ({x} : Finset Nat) := Finset.mem_singleton_self _ -- still works

[Chris Hughes]

Is this necessarily a good thing? People can accidentally change the statement of a theorem by changing its proof.

[Mario Carneiro]

no, the two are elaborated separately. The following does not typecheck:

example (x : Nat) : x ∈ {x} := Finset.mem_singleton_self _

[Dan Velleman]

Thanks Mario, that's very helpful. Now, what's going on here:

import Mathlib

attribute [default_instance] Set.instSingletonSet

example (x : Nat) : x ∈ {x} := Eq.refl _    --this works

example (x : Nat) : x ∈ {x} := by
  have h : x ∈ {x} := Eq.refl _    --error
  exact h

The first example works, but the second doesn't. The error is:

type mismatch
  Eq.refl ?m.692
has type
  ?m.692 = ?m.692 : Prop
but is expected to have type
  x ∈ ?m.645 : Prop