set.card_to_finset_univ

Stream: Is there code for X?

[Kyle Miller]

I've found I've wanted this lemma before for direct conversion between fintype.card and set.univ.to_finset.card. Does it already exist somewhere? Any reason for it not to exist?

lemma set.card_to_finset_univ [fintype α] :
  (set.univ : set α).to_finset.card = fintype.card α :=
by rw [set.to_finset_univ, finset.card_univ]

(I ask because it's currently in #5698.)

[Eric Wieser]

Not every pair of lemmas chained together is worthy of its own lemma (otherwise this strategy for adding lemmas recurses forever!). When do you need this combination?

[Kyle Miller]

Yeah, that's the motivation for asking about this. It would be a counterpart to docs#set.to_finset_card for set.univ, and you can use these two lemmas in reverse to turn all the fintype.cards in an expression into to_finset.card, which then you manipulate using the set.finite module.

It's not essential to have this shortcut lemma, but I usually forget which pair of lemmas are needed to do the transformation.

[Oliver Nash]

Can this be simp? If so that would be a good reason to have it.

[Kyle Miller]

I wonder if there's a reason docs#finset.card_univ isn't a simp lemma already.

[Eric Rodriguez]

#7230

[Eric Wieser]

I think that might be worth reviving

[Kevin Buzzard]

Maybe if you're mostly dealing with fintype.card then you want it as a simp lemma and if you're mostly dealing with finset.card then you don't. This sort of thing can happen, right? For example when making an API for the complex numbers you really want complex.ext_iff as a simp lemma because when checking the axioms to show C is a ring you want to prove all equalities by equating real and imaginary parts and then using ring for the corresponding real equations. But in general when working with complex numbers as more conceptual objects e.g. when doing complex analysis you probably don't want this.

[Kyle Miller]

It's still running through CI, but I've made a PR (#11174) that addresses what is probably the underlying issue that made we want set.card_to_finset_univ, which is that set.to_finset_univ does not have fully general fintype arguments.

[Kyle Miller]

(A way I've used things like set.card_to_finset_univ in the past is to close goals by convert.)

[Kyle Miller]

It still doesn't seem like it's properly general -- it would be nice if a lemma could take implicit arguments that are elaborated as typeclass arguments if they don't end up being solved for via unification.

To do things "right" without that, it seems like we need variants of each lemma where instances for the left-hand side of an expression come from implicit arguments, and instances on the right-hand side come from typeclasses. That way when rewriting the left-hand side has greater freedom to match, but the right-hand side still is able to use typeclass search to fill in instances that the implicit argument system can't determine.

[Kyle Miller]

To illustrate the issue that #11174 is solving more clearly:

example [hα : fintype α] :
  (set.univ : set α).to_finset = finset.univ := by simp -- fails

example [hα : fintype α] :
  (set.univ : set α).to_finset = finset.univ := set.to_finset_univ --fails
-- `set.univ.to_finset = finset.univ` and `set.univ.to_finset = finset.univ` have different types
-- due to different instance arguments.

example [hα : fintype α] :
  (set.univ : set α).to_finset = finset.univ := by convert set.to_finset_univ -- OK

-- New lemma:
@[simp] lemma set.to_finset_univ' {hu : fintype (set.univ : set α)} [fintype α] :
  @set.to_finset _ (set.univ : set α) hu = finset.univ :=
by { ext, simp only [set.mem_univ, finset.mem_univ, set.mem_to_finset] }

example [hα : fintype α] :
  (set.univ : set α).to_finset = finset.univ := by simp -- OK

[Kyle Miller]

The PR leaves the original version of docs#set.to_finset_univ because it's still useful if you want to rw ← set.to_finset_univ, since it will synthesize the fintype set.univ instance.

[Eric Wieser]

What's the conflicting pair of instances?

[Kyle Miller]

@Eric Wieser subtype.fintype and set.fintype_univ

type mismatch, term
  set.to_finset_univ
has type
  @set.to_finset ?m_1 (@set.univ ?m_1)
      (@subtype.fintype ?m_1 (λ (x : ?m_1), x ∈ @set.univ ?m_1) (λ (a : ?m_1), @set.univ_decidable ?m_1 a) ?m_2) =
    @finset.univ ?m_1 ?m_2
but is expected to have type
  @set.to_finset α (@set.univ α) (@set.fintype_univ α hα) = @finset.univ α hα

[Eric Wieser]

src#set.fintype_univ

[Eric Wieser]

That instance seems pointless if the other one matches it

[Kyle Miller]

Also, I believe I've misunderstood how simp interacts with instance arguments. It seems to already treat them as implicit arguments first? Otherwise, these examples wouldn't all work:

@[simp] lemma set.to_finset_univ' [hu : fintype (set.univ : set α)] [fintype α] :
  @set.to_finset _ (set.univ : set α) hu = finset.univ :=
by { ext, simp only [set.mem_univ, finset.mem_univ, set.mem_to_finset] }

example [fintype α] :
  @set.to_finset _ (set.univ : set α) (subtype.fintype _) = finset.univ := by simp

example [fintype α] :
  @set.to_finset _ (set.univ : set α) set.fintype_univ = finset.univ := by simp

example (hu : fintype (set.univ : set α)) (hα : fintype α)  :
  @set.to_finset _ (set.univ : set α) hu = @finset.univ _ hα:= by simp

example [fintype α] :
  (@set.to_finset _ (set.univ : set α) (subtype.fintype _)).card = finset.univ.card := by simp

example [fintype α] :
  (@set.to_finset _ (set.univ : set α) set.fintype_univ).card = finset.univ.card := by simp

example (hu : fintype (set.univ : set α)) (hα : fintype α)  :
  (@set.to_finset _ (set.univ : set α) hu).card = (@finset.univ _ hα).card := by simp

[Anne Baanen]

Indeed, after matching with the goal, simp processes arguments to its lemmas left-to-right, if the value of the argument derives from the unification it uses that, otherwise it will use typeclass inference, or if it's a Prop, recursively call simp on that argument. (Notably, this means out_params of instances do not get inferred correctly by simp.)

[Oliver Nash]

Does any of the interesting discussion above deserve being added to this page: https://leanprover-community.github.io/extras/simp.html ?

[Anne Baanen]

I'm hoping to fix the out_param issue soon, so let's wait a bit before we do so :)

[Kyle Miller]

There seems to be an elaboration bug with this:

@[simp] lemma set.to_finset_univ [fintype (set.univ : set α)] [fintype α] :
  (set.univ : set α).to_finset = finset.univ :=
by { ext, simp only [set.mem_univ, mem_univ, set.mem_to_finset] }

Here's the full error using set_option pp.implicit true:

1303:35: kernel failed to type check declaration 'set.to_finset_univ' this is usually due to a buggy tactic or a bug in the builtin elaborator
elaborated type:
  ∀ {α : Type u_1} [_inst_1 : fintype ↥(@set.univ α)] [_inst_2 : fintype α],
    @set.to_finset α (@set.univ α)
        (@subtype.fintype α (λ (x : α), x ∈ @set.univ α) (λ (a : α), @set.univ_decidable α a) _inst_2) =
      @univ α _inst_2
elaborated value:
  λ {α : Type u_1} [_inst_1 : fintype ↥(@set.univ α)] [_inst_2 : fintype α],
    @ext α
      (@set.to_finset α (@set.univ α)
         (@subtype.fintype α (λ (x : α), x ∈ @set.univ α) (λ (a : α), @set.univ_decidable α a) _inst_2))
      (@univ α _inst_2)
      (λ (a : α),
         (@id
            ((a ∈
                    @set.to_finset α (@set.univ α)
                      (@subtype.fintype α (λ (x : α), x ∈ @set.univ α) (λ (a : α), @set.univ_decidable α a)
                         _inst_2) ↔
                  a ∈ @univ α _inst_2) =
               (true ↔ true))
            ((λ (a a_1 : Prop) (e_1 : a = a_1) (b b_1 : Prop) (e_2 : b = b_1),
                @congr Prop Prop (iff a) (iff a_1) b b_1 (@congr_arg Prop (Prop → Prop) a a_1 iff e_1) e_2)
               (a ∈
                  @set.to_finset α (@set.univ α)
                    (@subtype.fintype α (λ (x : α), x ∈ @set.univ α) (λ (a : α), @set.univ_decidable α a)
                       _inst_2))
               true
               ((@propext
                   (a ∈
                      @set.to_finset α (@set.univ α)
                        (@subtype.fintype α (λ (x : α), x ∈ @set.univ α) (λ (a : α), @set.univ_decidable α a)
                           _inst_2))
                   (a ∈ @set.univ α)
                   (@set.mem_to_finset α (@set.univ α)
                      (@subtype.fintype α (λ (x : α), x ∈ @set.univ α) (λ (a : α), @set.univ_decidable α a)
                         _inst_2)
                      a)).trans
                  (@propext (a ∈ @set.univ α) true
                     (@(λ {α : Type u_1} (x : α), @iff_true_intro (x ∈ @set.univ α) (@set.mem_univ α x)) α a)))
               (a ∈ @univ α _inst_2)
               true
               (@propext (a ∈ @univ α _inst_2) true
                  (@(λ {α : Type u_1} [_inst_1 : fintype α] (x : α),
                      @iff_true_intro (x ∈ @univ α _inst_1) (@mem_univ α _inst_1 x))
                     α
                     _inst_2
                     a)))).mpr
           (iff.refl true))
nested exception message:
type mismatch at application
  fintype ↥(@set.univ α)
term
  ↥(@set.univ α)
has type
  Type u_1
but is expected to have type
  Type u_2

[Kyle Miller]

I'm not sure whether I'd expect it or not, but it also chooses the subtype.fintype instance for set.to_finset rather than the one given as an argument.

[Eric Wieser]

You need to add a coe_sort arrow I think

[Kyle Miller]

That does fix it here, but what's going on exactly? The error message shows that Lean's inserting the coe_sort automatically -- my only guess is that somehow it causes the elaborator to fail to unify some universe (meta)variables, so when metavariables are replaced by variables, once the kernel gets ahold of it they're accidentally different.

I think this explains also why typeclass inference isn't picking up on the instance, since it seems to be fintype.{u_2} (↥(@set.univ α) : Type u_1).

[Kyle Miller]

Indeed, explicit universes fixes it:

@[simp] lemma set.to_finset_univ {α : Type u}
  [fintype.{u} ((set.univ : set α) : Type u)] [fintype α] :
  (set.univ : set α).to_finset = finset.univ :=
by { ext, simp only [set.mem_univ, mem_univ, set.mem_to_finset] }

Edit: Hmm, even this is enough to get it to work:

@[simp] lemma set.to_finset_univ
  [fintype ((set.univ : set α) : Type*)] [fintype α] :
  (set.univ : set α).to_finset = finset.univ :=
by { ext, simp only [set.mem_univ, mem_univ, set.mem_to_finset] }

[Kyle Miller]

But this does fix it, too:

@[simp] lemma set.to_finset_univ {α : Type u}
  [fintype.{u} (set.univ : set α)] [fintype α] :
  (set.univ : set α).to_finset = finset.univ :=
by { ext, simp only [set.mem_univ, mem_univ, set.mem_to_finset] }

[Kyle Miller]

Anyway, assuming this is a bug, #11247 puts the lemma into this last form while adding a TODO.

[Kyle Miller]

Does it seem like a bug? Should I submit a lean issue?

Here's a mathlib-free mwe:

universes u
variables {α : Type u}

instance : has_coe_to_sort (set α) (Type*) := ⟨λ s, {x // x ∈ s}⟩

-- OK
lemma ex1 [inhabited α] : true := trivial

-- Not OK
lemma ex2 [inhabited (set.univ : set α)] : true := trivial
/-
kernel failed to type check declaration 'ex2' this is usually due to a buggy tactic or a bug in the builtin elaborator
elaborated type:
  ∀ {α : Type u} [_inst_1 : inhabited ↥set.univ], true
elaborated value:
  λ {α : Type u} [_inst_1 : inhabited ↥set.univ], trivial
nested exception message:
type mismatch at application
  inhabited ↥set.univ
term
  ↥set.univ
has type
  Type u
but is expected to have type
  Sort u_1
-/

-- OK
lemma ex3 [inhabited.{u+1} (set.univ : set α)] : true := trivial

-- OK
lemma ex4 [inhabited ↥(set.univ : set α)] : true := trivial

-- OK
lemma ex5 (s : set α) [inhabited s] : true := trivial

[Rob Lewis]

This definitely seems like an elaborator bug.

example : inhabited (set.univ : set α) → true := sorry

fails,

example : inhabited (set.univ : set α) := sorry

works

[Eric Wieser]

Definitely open a lean issue, because then you can reference it from a comment.

[Kyle Miller]

I wonder if it's the same underlying issue as lean#474