Zulip Chat Archive

Stream: new members

Topic: Coercing "nested" types


AG (Jan 11 2022 at 04:39):

How does one coerce nested types in lean?

For example, I can coerce a finset to a set no problem…

def my_def (F : set α): Prop :=
  true

lemma my_lemma (F : finset α) : my_def F :=
  by trivial

But Lean throws an error when I try to coerce a finset of finsets to a set of sets…

def my_def' (F : set (set α)): Prop :=
  true

lemma my_lemma' (F : finset (finset α)) : my_def' F :=
  by trivial

The error says: Type mismatch at application my_def' F. Term F has type finset (finset α) but is expected to have type set (set α).

Johan Commelin (Jan 11 2022 at 07:01):

@AG You'll have to choose an intermediate step. Do you want to pass through finset (set α) or through set (finset α).
Anyway, I expect that coe '' F or F.image coe should work.

AG (Jan 12 2022 at 04:46):

Oh that makes sense, thank you. It seems I can get to the intermediary easily enough by writing it as (F : set (finset α)) or @coe (finset (finset α)) (set (finset α)) _ F, but how exactly do I use coe to get the inner type to be a set as well?

In particular, if I set parameter F : finset (finset α), then

  • #check @coe (finset (finset α)) (set (finset α)) _ F works fine
  • but #check @coe (finset (finset α)) (finset (set α)) _ F throws an error.

AG (Jan 12 2022 at 04:59):

Oh just got something that did it! Thank you again.

set.image (@coe (finset α) (set α) _) (F : set (finset α))

It turns out Lean can even go through the intermediary for you with

set.image (@coe (finset α) (set α) _) F

Last updated: Dec 20 2023 at 11:08 UTC