Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 17:55):

Try simp only [h]

view this post on Zulip 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

view this post on Zulip Reid Barton (Jul 10 2020 at 17:58):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 18:01):

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

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 18:01):

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

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 18:02):

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

view this post on Zulip Reid Barton (Jul 10 2020 at 18:02):

seems like a missing lemma

view this post on Zulip 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:

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 18:02):

Try congr

view this post on Zulip Carl Friedrich Bolz-Tereick (Jul 10 2020 at 18:02):

but "ext, simp" does :sweat_smile:

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 18:03):

I think finset is subsingleton data

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 18:04):

Blame the computer scientists

view this post on Zulip Reid Barton (Jul 10 2020 at 18:04):

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

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 18:04):

Does congr or congr' work?

view this post on Zulip Carl Friedrich Bolz-Tereick (Jul 10 2020 at 18:05):

nope

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 18:05):

Am I right in thinking that finset is subsingleton data?

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 18:06):

finset x has type Type but is a subsingleton?

view this post on Zulip Carl Friedrich Bolz-Tereick (Jul 10 2020 at 18:06):

I don't know what subsingleton is

view this post on Zulip Johan Commelin (Jul 10 2020 at 18:06):

A type with at most 1 term

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 18:07):

Does to_finset use the fintype type class?

view this post on Zulip Reid Barton (Jul 10 2020 at 18:07):

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

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 18:07):

Right

view this post on Zulip Carl Friedrich Bolz-Tereick (Jul 10 2020 at 18:08):

@Kevin Buzzard yes, and fintype is subsingleton

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip Reid Barton (Jul 10 2020 at 18:09):

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

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 18:10):

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

view this post on Zulip Reid Barton (Jul 10 2020 at 18:10):

wait, maybe not?

view this post on Zulip Reid Barton (Jul 10 2020 at 18:10):

oh it's a fintype on the coerced set

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 18:11):

Try convert

view this post on Zulip Reid Barton (Jul 10 2020 at 18:11):

you can put it near src#set.to_finset_univ

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 18:12):

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

view this post on Zulip Carl Friedrich Bolz-Tereick (Jul 10 2020 at 18:12):

cfbolz

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 18:12):

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

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 18:12):

Is it a simp lemma?

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 18:13):

So convert should do it

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 18:13):

But then I'm surprised congr didn't work

view this post on Zulip Carl Friedrich Bolz-Tereick (Jul 10 2020 at 18:14):

I don't have write access yet

view this post on Zulip 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

view this post on Zulip Carl Friedrich Bolz-Tereick (Jul 10 2020 at 18:15):

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

view this post on Zulip Reid Barton (Jul 10 2020 at 18:17):

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

view this post on Zulip Carl Friedrich Bolz-Tereick (Jul 10 2020 at 18:17):

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

view this post on Zulip Carl Friedrich Bolz-Tereick (Jul 10 2020 at 18:19):

should I pull request it?

view this post on Zulip 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

view this post on Zulip Carl Friedrich Bolz-Tereick (Jul 10 2020 at 18:19):

thanks a lot

view this post on Zulip Reid Barton (Jul 10 2020 at 18:20):

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

view this post on Zulip Reid Barton (Jul 10 2020 at 18:20):

does convert try assumption or something?

view this post on Zulip 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?)

view this post on Zulip 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

view this post on Zulip Carl Friedrich Bolz-Tereick (Jul 10 2020 at 18:22):

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

view this post on Zulip 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?

view this post on Zulip 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