Zulip Chat Archive

Stream: mathlib4

Topic: Singleton notation


Dan Velleman (Jan 28 2023 at 22:24):

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 (Jan 28 2023 at 22:26):

It can be Finset Nat as well.

Yury G. Kudryashov (Jan 28 2023 at 22:26):

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

Dan Velleman (Jan 28 2023 at 22:26):

Oh, I see.

Kevin Buzzard (Jan 29 2023 at 00:20):

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 (Jan 29 2023 at 13:44):

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 (Jan 29 2023 at 20:17):

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

Mario Carneiro (Jan 29 2023 at 20:36):

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

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

Dan Velleman (Jan 29 2023 at 22:17):

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

Last updated: Dec 20 2023 at 11:08 UTC