Zulip Chat Archive

Stream: maths

Topic: Lifting a finite set to a finset


view this post on Zulip Ryan Lahfa (Apr 01 2020 at 19:32):

I'm trying to lift a finite set to a finset using some hypothesis of finiteness.

import data.set
import data.set.finite
import data.finset

variable {X: Type}

open set
open classical
local attribute [instance] prop_decidable

set_option trace.app_builder true

lemma finite_set_has_greatest_element [preorder X] (S: set X):
  S.finite   x  S, is_greatest S x := begin
  intro Hf,
  lift S to finset using Hf,
  end

But this is failing with:

[app_builder] failed to create an 'can_lift'-application, failed to solve unification constraint for #2 argument (Type ? =?= Type ? → Type ?)
app_builder_exception, more information can be obtained using command `set_option trace.app_builder true`

But, I'm not sure I understand why https://leanprover-community.github.io/mathlib_docs/data/set/finite.html#set.can_lift does not get picked up by Lean.

view this post on Zulip Kevin Buzzard (Apr 01 2020 at 19:37):

finset X not finset

view this post on Zulip Ryan Lahfa (Apr 01 2020 at 19:38):

… Thanks, sorry for the stupid question!

view this post on Zulip Kevin Buzzard (Apr 01 2020 at 19:38):

Thanks for that question! I had no idea about that whole machinery. I remember noticing that some trick to go from int to nat landed in Lean but I'd not realised it was so powerful.

view this post on Zulip Kevin Buzzard (Apr 01 2020 at 19:39):

I just learnt about how far it all went from your question.

view this post on Zulip Ryan Lahfa (Apr 01 2020 at 19:39):

Happy to make this very cool API more attention then, because it sounds really useful for heavy coercions :)

view this post on Zulip Ryan Lahfa (Apr 01 2020 at 19:40):

I guessed that lift S to finset using Hf could guess that finset has some holes and fill them itself by reusing the fact that S: set α and then trying to make some finset α too, but it's not obvious I guess

view this post on Zulip Ryan Lahfa (Apr 01 2020 at 19:41):

Putting a hole, i.e. lift S to (finset _) using Hf makes the error a lot more user friendly.


Last updated: May 10 2021 at 07:15 UTC