finset.univ_eq_set_univ_to_finset

Stream: new members

[Alex Zhang]

I wrote

variables (I : Type*) [fintype I]
lemma finset.univ_eq_set_univ_to_finset :
finset.univ = (@set.univ I).to_finset :=
by {simp [finset.univ, set.to_finset], ext, simp, exact fintype.complete a}

Should this be a simplification lemma? If so, which direction is the right direction to simply?

[Eric Wieser]

Did you try by library_search to see if we already have this?

[Eric Wieser]

docs#set.to_finset_univ or docs#set.univ_to_finset would be my immediate guess

[Eric Wieser]

So yes, this should be and already is a simp lemma

[Eric Wieser]

I think your mistake here was simplifying away the definitions before asking lean if the result was already proven

[Alex Zhang]

I think they are not the same thing actually,

lemma finset.univ_eq_set_univ_to_finset :
finset.univ = (@set.univ I).to_finset :=
set.to_finset_univ.symm

won't able to close the goal.

[Eric Wieser]

With what error?

[Alex Zhang]

type mismatch, term
  set.to_finset_univ.symm
has type
  @finset.univ ?m_1 ?m_2 =
    @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)
but is expected to have type
  @finset.univ I _inst_1 = @set.to_finset I (@set.univ I) (@set.fintype_univ I _inst_1)

[Eric Wieser]

Can you give a mwe with imports?

[Eric Wieser]

It might succeed / fail depending on what you have imported

[Eric Wieser]

by convert set.to_finset_univ.symm may also close it

[Alex Zhang]

That is weird, Eric. Why should this happen? @Eric Wieser
If I do

import tactic
import data.fintype.card
variables (I : Type*) [fintype I]
lemma finset.univ_eq_set_univ_to_finset :
finset.univ = (@set.univ I).to_finset :=
set.to_finset_univ.symm

then it fails, but it will succeed if I remove the import tactic.

[Eric Wieser]

Can you narrow down the import that makes it fail?

[Eric Wieser]

import tactic imports tactic.default, which is just a file full of imports

[Eric Wieser]

You can paste those all in, and delete them one at a time until it works

[Kyle Miller]

tactic imports data.set.finite, which provides the instance fintype_univ, which conflicts with subtype.fintype for set.univ.

[Kyle Miller]

import tactic
import data.fintype.card

local attribute [-instance] set.fintype_univ
lemma finset.univ_eq_set_univ_to_finset (I : Type*) [h : fintype I] :
finset.univ = (@set.univ I).to_finset :=
set.to_finset_univ.symm

[Kyle Miller]

Maybe set.to_finset_univ should be changed to take a [fintype set.univ] instance

[Eric Wieser]

Is there any reason for docs#set.fintype_univ to exist?

[Eric Wieser]

If not, it seems easier to remove it than to add that argument

[Kyle Miller]

I don't see why set.fintype_univ exists, since set.univ is a decidable predicate. Only thing I can think of is that subtype.fintype breaks the set API slightly, since it treats sets as predicates directly.

(Though it still might be worth fixing set.to_finset_univ, since it breaks the ideal rule that instances used in a lemma should all be given as arguments.)

[Eric Wieser]

I thought I fixed docs#subtype.fintype to not abuse the set API

[Kyle Miller]

@Alex Zhang The reason by convert works is that it makes use of the fact that fintype is a subsingleton (if you have two fintype instances, while they might not be definitionally equal, they are at least provably equal). There are two instances for fintype (@set.univ I) floating around, and set.to_finset_univ has picked up on a different instance than (@set.univ I).to_finset.

Just for completeness, here is how to get it to work (better to not mess around with removing attributes):

import tactic
import data.fintype.card

lemma finset.univ_eq_set_univ_to_finset (I : Type*) [h : fintype I] :
  finset.univ = (@set.univ I).to_finset :=
by convert set.to_finset_univ.symm

[Kyle Miller]

@Eric Wieser I'm not sure what counts as abuse exactly. I was just going on the fact that p here is not a set:

instance subtype.fintype (p : α → Prop) [decidable_pred p] [fintype α] : fintype {x // p x} :=
fintype.subtype (univ.filter p) (by simp)

(If this is an abuse, I think it's an ok one, but that's just my opinion. I think the fact that sets are predicates is a fundamental fact about them.)

[Eric Wieser]

Doesn't it infer that with p = (∈ s)?

[Eric Wieser]

Interestingly we have docs#set_fintype right below that, but it's not an instance

[Kyle Miller]

Eric Wieser said:

Doesn't it infer that with p = (∈ s)?

Oh, my mistake -- thanks.

[Alex Zhang]

Eric Wieser said:

I thought I fixed docs#subtype.fintype to not abuse the set API

Eric, what do you mean by "not abuse the set API" here?

[Eric Wieser]

A lot of stuff used to behave the way you were claiming though - I changed it in the last week or so.

[Eric Wieser]

By abuse, I mean using s x instead x ∈ s when s : set α

[Alex Zhang]

So is the current solution for working on relevant things to block an instance?

[Alex Zhang]

Is local attribute [-instance] set.fintype_univ the right thing supposed to do now?

[Alex Zhang]

and also do local attribute [instance] set_fintype perhas?

[Alex Zhang]

@Eric Wieser @Kyle Miller

[Alex Zhang]

I asked how to block things in another post as I had felt that something was going wrong at that point before encounter this specific issue when working on my own project.

[Kyle Miller]

Alex Zhang said:

Is local attribute [-instance] set.fintype_univ the right thing supposed to do now?

No, you should use by convert like in the code block in one of my last comments (at least until these overlapping instances are possibly fixed).

[Alex Zhang]

There is no mismatch of instances constructed between set_fintype and subtype.fintype right? @Kyle Miller

[Kyle Miller]

@Alex Zhang Correct, those are definitionally equal.

[Alex Zhang]

I note there is one mismatch : set_fintype uses [_inst_1 : decidable_pred p], subtype.fintype uses [_inst_1 : decidable_pred p]. I suggest to match them.
Which condition is a better form?

[Eric Wieser]

Did you mean to type those as the same in both cases?

[Alex Zhang]

Yes!

[Eric Wieser]

Then in what way are they a mismatch?

[Alex Zhang]

sorry, there is a typo, I fixed it.

[Eric Wieser]

decidable_pred expects a p : α → Prop, but s : set α. To get the right type, we need (∈ s) : α → Prop.

[Eric Wieser]

Using decidable_pred s directly is telling lean to unfold set, which you should never do

[Alex Zhang]

What I am saying is that subtype.fintype uses [_inst_1 : decidable_pred p] as a condition, I suggest to rewrite it to [_inst_2 : decidable_pred (λ (_x : α), _x ∈ s)]

[Eric Wieser]

But subtype.fintype has no s argument, so that second version doesn't make sense!

[Alex Zhang]

You use p.

[Eric Wieser]

You can't use ∈ on p because it's not a set

[Alex Zhang]

Oh, that's sad..

[Eric Wieser]

Why?

[Alex Zhang]

If you have [_inst_2 : decidable_pred (λ (_x : α), _x ∈ s)], can lean infer [_inst_1 : decidable_pred s]?

[Eric Wieser]

The latter is nonsense, because it implies using s x on a set

[Eric Wieser]

Lean happens to accept it, but you don't want to do it

[Eric Wieser]

Because there are no lemmas about s x but lots of lemmas about x ∈ x

[Eric Wieser]

#8211 tried to clean this sort of mess up

[Kyle Miller]

Alex Zhang said:

Oh, that's sad..

Just FYI, set_of is how you convert a predicate into a set. The subtype.fintype instance will convert the set into a predicate (via (λ (x : α), x ∈ s) through a couple of nice coincidences.

[Eric Wieser]

docs#set_of aka {x | p x}

[Eric Wieser]

As I understand it, the only reason that lean doesn't define set as structure set := (mem : α → Prop) is so that both (∈ {x | p x}) = p and {x | x ∈ s} = s are true definitionally; if it were a structure, the second statement would require extensionality to prove as lean does not perform eta reduction.

[Yakov Pechersky]

BTW, to answer the first question, docs#set.to_finset_univ is in the desired direction. An alright rule of thumb for simp lemmas is that the RHS term should have fewer terms.

[Yakov Pechersky]

On the LHS, you have both set.univ and set.to_finset. The RHS only have finset.univ