Zulip Chat Archive

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:

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

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?

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

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

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

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

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

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

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

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?

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

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):

Do you already have write access to non master branches of mathlib?

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

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

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?)

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

Yes
https://leanprover-community.github.io/contribute/index.html
https://github.com/leanprover-community/lean/blob/master/doc/commit_convention.md

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: Dec 20 2023 at 11:08 UTC