## Stream: new members

### Topic: motive is not type-correct when proving simple fintype lemma

#### Carl Friedrich Bolz-Tereick (Jul 10 2020 at 17:45):

I am doing some stuff with sets/finsets/fintypes and was running into this error that I don't understand. mwe:

import tactic
import tactic.find
import tactic.suggest
import data.fintype.basic
import data.setoid.partition

variables {α : Type} {β : Type} {γ : Type}

open_locale classical
open_locale big_operators

lemma minimal (s1 s2 : set α) [fintype α] (h : s1 ∩ s2 = ∅) : (s1 ∩ s2).to_finset = ∅ :=
begin
--fails with:
-- rewrite tactic failed, motive is not type correct
-- λ (_a : set α), (s1 ∩ s2).to_finset = ∅ = (_a.to_finset = ∅)
rw h,
end


Any hints why this happens?

#### Kevin Buzzard (Jul 10 2020 at 17:55):

Try simp only [h]

#### Kevin Buzzard (Jul 10 2020 at 17:57):

It happens because the rewrite tactic is not powerful enough to do the rewrite you want. There is a hidden proof that s1 cap s2 has some property, and the rewrite didn't change it into a proof that the empty set had the property

#### Reid Barton (Jul 10 2020 at 17:58):

you can also probably avoid it by doing whatever you were planning to do next first

#### Carl Friedrich Bolz-Tereick (Jul 10 2020 at 18:00):

simp only [h] gives me the goal "∅.to_finset = ∅"
I hoped refl would close this, but somehow doesn't in this situation

#### Kevin Buzzard (Jul 10 2020 at 18:01):

Maybe simp finishes it, it looks like a good simp lemma

#### Kevin Buzzard (Jul 10 2020 at 18:01):

If it does then simp [h] probably does the proof in one line

#### Kevin Buzzard (Jul 10 2020 at 18:02):

You can unfold everything to find out why refldoesn't work

#### Reid Barton (Jul 10 2020 at 18:02):

seems like a missing lemma

#### Carl Friedrich Bolz-Tereick (Jul 10 2020 at 18:02):

no, if I put "∅.to_finset = ∅" into its own lemma, then refl proves it. but in the context of my strange "minimal" thing, neither simp nor refl do :thinking:

Try congr

#### Carl Friedrich Bolz-Tereick (Jul 10 2020 at 18:02):

but "ext, simp" does :sweat_smile:

#### Kevin Buzzard (Jul 10 2020 at 18:03):

I think finset is subsingleton data

#### Kevin Buzzard (Jul 10 2020 at 18:04):

Blame the computer scientists

#### Reid Barton (Jul 10 2020 at 18:04):

∅.to_finset = ∅ needs induction on the fintype I think

#### Kevin Buzzard (Jul 10 2020 at 18:04):

Does congr or congr' work?

nope

#### Kevin Buzzard (Jul 10 2020 at 18:05):

Am I right in thinking that finset is subsingleton data?

#### Kevin Buzzard (Jul 10 2020 at 18:06):

finset x has type Type but is a subsingleton?

#### Carl Friedrich Bolz-Tereick (Jul 10 2020 at 18:06):

I don't know what subsingleton is

#### Johan Commelin (Jul 10 2020 at 18:06):

A type with at most 1 term

#### Kevin Buzzard (Jul 10 2020 at 18:07):

I'm sure I'm trying to ask something but I haven't got it straight yet

#### Kevin Buzzard (Jul 10 2020 at 18:07):

Does to_finset use the fintype type class?

#### Reid Barton (Jul 10 2020 at 18:07):

finset α is not a subsingleton, it's like set α + a subsingleton

Right

#### Carl Friedrich Bolz-Tereick (Jul 10 2020 at 18:08):

@Kevin Buzzard yes, and fintype is subsingleton

#### Reid Barton (Jul 10 2020 at 18:08):

to_finset is basically "go through the list of everything that exists and keep the ones that belong to this set"

#### Kevin Buzzard (Jul 10 2020 at 18:09):

So if you prove the lemma independently and give it a name like empty_to_finset and PR to mathlib

#### Reid Barton (Jul 10 2020 at 18:09):

I think it's a decidable instance that causes the original error?

#### Kevin Buzzard (Jul 10 2020 at 18:10):

Then will convert empty_to_finset do it? Oh -- not if the proof is refl

wait, maybe not?

#### Reid Barton (Jul 10 2020 at 18:10):

oh it's a fintype on the coerced set

#### Carl Friedrich Bolz-Tereick (Jul 10 2020 at 18:10):

@Kevin Buzzard trying that makes me more confused:

import tactic
import tactic.find
import tactic.suggest
import data.fintype.basic
import data.setoid.partition

variables {α : Type} {β : Type} {γ : Type}

open_locale classical
open_locale big_operators

--set_option pp.all true

lemma empty_to_finset : (∅ : set α).to_finset = ∅ :=
begin
refl, -- works
end

lemma minimal (s1 s2 : set α) [fintype α] (h : s1 ∩ s2 = ∅) : (s1 ∩ s2).to_finset = ∅ :=
begin
simp [h], -- now the goal is ∅.to_finset = ∅
apply empty_to_finset, -- fails to unify :-(
end


Try convert

#### Reid Barton (Jul 10 2020 at 18:11):

you can put it near src#set.to_finset_univ

#### Kevin Buzzard (Jul 10 2020 at 18:12):

Prove it in term mode with rfl and make a PR. What's your GitHub userid?

cfbolz

#### Reid Barton (Jul 10 2020 at 18:12):

Because one has the global instance of fintype ∅ and the other has the one that comes from being a subset

#### Kevin Buzzard (Jul 10 2020 at 18:12):

Is it a simp lemma?

#### Kevin Buzzard (Jul 10 2020 at 18:13):

So convert should do it

#### Kevin Buzzard (Jul 10 2020 at 18:13):

But then I'm surprised congr didn't work

#### Carl Friedrich Bolz-Tereick (Jul 10 2020 at 18:14):

I don't have write access yet

#### Reid Barton (Jul 10 2020 at 18:14):

I'm not surprised that Lean needs this kind of help to see what combination of definitional rewriting + subsingleton will do the trick

#### Carl Friedrich Bolz-Tereick (Jul 10 2020 at 18:15):

(and nope, I couldn't get convert to do it either)

#### Reid Barton (Jul 10 2020 at 18:17):

simp [h], convert empty_to_finset works for me (as expected)

#### Carl Friedrich Bolz-Tereick (Jul 10 2020 at 18:17):

ah! that convert I didn't try, thank you :-)

#### Carl Friedrich Bolz-Tereick (Jul 10 2020 at 18:19):

should I pull request it?

#### Bryan Gin-ge Chen (Jul 10 2020 at 18:19):

@Carl Friedrich Bolz-Tereick I've sent you an invitation https://github.com/leanprover-community/mathlib/invitations

thanks a lot

#### Reid Barton (Jul 10 2020 at 18:20):

also simply convert empty_to_finset works for me too, not as expected

#### Reid Barton (Jul 10 2020 at 18:20):

does convert try assumption or something?

#### Carl Friedrich Bolz-Tereick (Jul 10 2020 at 18:20):

is there a document how to contribute (I am familiar with git/github, but stuff like conventions for commit messages etc?)

#### Carl Friedrich Bolz-Tereick (Jul 10 2020 at 18:22):

thank you. I might have a few other small finset lemmas later

#### Carl Friedrich Bolz-Tereick (Jul 10 2020 at 19:16):

hm, in mathlib rfl doesn't prove the lemma (maybe because of the lack of open_locale classical?). but I can prove it analogously to to_finset_univ. should to_finset_empty be a @[simp] lemma too?

#### Carl Friedrich Bolz-Tereick (Jul 10 2020 at 19:29):

I guessed yes and opened a pull request: https://github.com/leanprover-community/mathlib/pull/3361

Last updated: May 13 2021 at 19:20 UTC