Zulip Chat Archive

Stream: general

Topic: subsingleton instances


view this post on Zulip Chris Hughes (Mar 03 2018 at 15:22):

I'm struggling with the following proof

α : Type u_1,
s : set α,
_inst_1 : fintype s,
h : s = 
 card s = 0

the trouble is that rw h` does not work because it has to rewrite the fintype instance at the same time. I'm having trouble in general with lean not recognizing two terms as equal because the fintype instances are different. Is there a nice way of dealing with this. I can use congr to prove that two terms with different fintype instances are equal, but this seems quite messy.

view this post on Zulip Gabriel Ebner (Mar 03 2018 at 15:43):

Does simp [h] work by chance?

view this post on Zulip Chris Hughes (Mar 03 2018 at 16:07):

no

view this post on Zulip Kevin Buzzard (Mar 03 2018 at 18:05):

import data.fintype
universe u


example (α : Type u) (s : set α) [fintype s] (h : s = ∅) : fintype.card ↥s = 0 := begin
rw ←fintype.card_empty,
rw fintype.card_eq,
rw h,
show nonempty ({x : α // false} ≃ empty),
refine ⟨_⟩,
refine ⟨_,_,_,_⟩,
exact λ x, false.elim x.property,
intro x,cases x,
intro x,exact false.elim x.property,
intro x,cases x,
end

view this post on Zulip Kevin Buzzard (Mar 03 2018 at 18:07):

kind of a comical proof because I never used these types before, so most of it is me experimenting with what is there. Obviously this can be shortened a lot.

view this post on Zulip Chris Hughes (Mar 03 2018 at 18:11):

rw ← set.empty_card; congr; assumption is also a slightly shorter proof, but I was hoping there was an easy way.

view this post on Zulip Patrick Massot (Mar 03 2018 at 18:20):

Are students allowed to be that insolent in England?

view this post on Zulip Gabriel Ebner (Mar 03 2018 at 18:32):

I think this is a more idiomatic solution:

import data.fintype
universe u

@[simp] lemma fintype.card_emptyset (α : Type u) [fintype.{u} ( : set α)] :
    fintype.card ( : set α) = 0 :=
begin
simp [fintype.card], apply finset.ext.mpr, intros, cases a, cases a_property
end

local attribute [-simp] set.set_coe_eq_subtype -- bad simp lemma

example (α : Type u) (s : set α) [fintype s] (h : s = ) :
    fintype.card s = 0 :=
by simp [h]

view this post on Zulip Chris Hughes (Mar 03 2018 at 19:32):

the lemma fintype.card_emptyset already exists, it's called set.empty_card in data/set/finite. However it doesn't require a fintype instance as an argument, because it uses a different proof that the empty set is finite.

view this post on Zulip Gabriel Ebner (Mar 03 2018 at 19:56):

That's the core of the misunderstanding: fintype is not a proof, it is data. So you need to write all lemmas with generic fintype arguments, otherwise they won't match. We have a very similar problem with decidability instances actually.

view this post on Zulip Gabriel Ebner (Mar 03 2018 at 19:58):

One solution is to use E-matching in the SMT mode. This would transparently ignore the different subsingleton instances. However the SMT mode is abandoned and does not have a clear future.

view this post on Zulip Gabriel Ebner (Mar 03 2018 at 20:05):

I'm not sure if I see a good and general solution. The same issue applies not just to simp, but pretty much all tactics and also term-mode proof construction. A somewhat clean approach that works in all those cases would be to post-process the types of lemmas, and generalize non-dependent subsingleton subterms. Maybe we could do this automatically with more powerful user attributes, or user commands once the new parser lands.

view this post on Zulip Kevin Buzzard (Mar 03 2018 at 21:06):

Are students allowed to be that insolent in England?

Ha ha :-) Chris knows a lot more about these finite types than I do. He's been doing stuff with finite groups -- I've never used them at all. Chris -- why not PR some stuff to xena? Or just email it me if you can't be bothered? I'd be interested to see what you've been doing.

view this post on Zulip Chris Hughes (Mar 03 2018 at 21:30):

Just made a PR to xena. It's quite an incomplete file with a few sorries, but there's lagrange in there, which is good.

view this post on Zulip Patrick Massot (Mar 04 2018 at 09:05):

What's the point of proving Lagrange without developing group actions? If you want to do more group theory you won't be able to bypass them much longer.

view this post on Zulip Patrick Massot (Mar 04 2018 at 09:05):

@Scott Morrison what happened to your student who was doing group theory?

view this post on Zulip Patrick Massot (Mar 04 2018 at 09:06):

@Chris Hughes what happened to your analysis PRs?

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 12:09):

What's the point of proving Lagrange without developing group actions? If you want to do more group theory you won't be able to bypass them much longer.

There's a danger here that you can argue that there's no point doing anything because someone did something more general. Chris is a first year undergraduate who just learnt Lagrange's theorem and we don't teach group actions until the 3rd year, so his view of the subject is very different to yours. I completely appreciate your point of view but the answer is that Chris is using Lean to teach himself the material that he's going to be examined on in the summer.

view this post on Zulip Chris Hughes (Mar 04 2018 at 12:13):

@Patrick Massot I'm waiting for a PR on Cauchy Sequence limits to be merged, and then I'll merge some more stuff. There was a bit of discussion about the best way to implement the exponential function, about whether to do it using Johannes definition of a limit, or Mario's simpler definition of a limit. I'm not going to work on making it mathlib ready until that discussion is resolved.

The answer to your other question was pretty much the same as @Kevin Buzzard 's answer. I've no idea if my group theory stuff is useful, given that I've formalised most of what I know, it's unlikely I'll have defined things in the most useful manner.

view this post on Zulip Patrick Massot (Mar 04 2018 at 17:29):

I agree that aiming for the greatest generality is not a good idea. My point is that, if you continue finite group theory, then you will encounter group actions really soon (for instance if you go for Sylow).

view this post on Zulip Patrick Massot (Mar 04 2018 at 17:29):

Maybe I'm confused about what you know because Kevin teaches the concept of rigorous proofs, schemes, and perfectoid spaces in the same year.

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:30):

I teach several different courses/classes I guess

view this post on Zulip Patrick Massot (Mar 04 2018 at 17:31):

No, you teach schemes to Kenny and you mentioned teaching perfectoid spaces to first years on March 11th or something

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:31):

That's right but these are different things

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:31):

There's my normal course for 220 first years

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:31):

there is xena

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:32):

there is an undergraduate conference

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:32):

I am also teaching a graduate course

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:33):

oh golly

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:33):

he pushed them to mine

view this post on Zulip Patrick Massot (Mar 04 2018 at 17:34):

yes

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:34):

OK I merged.

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:34):

Should I just push to mathlib?

view this post on Zulip Patrick Massot (Mar 04 2018 at 17:36):

Nah

view this post on Zulip Patrick Massot (Mar 04 2018 at 17:36):

You should do something to my pending review

view this post on Zulip Patrick Massot (Mar 04 2018 at 17:37):

Otherwise Chris cannot see it

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:39):

I can't figure out how to do that

view this post on Zulip Patrick Massot (Mar 04 2018 at 17:39):

Hum, maybe the fact that you merged is not helping here

view this post on Zulip Patrick Massot (Mar 04 2018 at 17:40):

Or maybe it's my fault

view this post on Zulip Patrick Massot (Mar 04 2018 at 17:41):

yes it was

view this post on Zulip Patrick Massot (Mar 04 2018 at 17:41):

I forgot to hit some button to submit my review

view this post on Zulip Patrick Massot (Mar 04 2018 at 17:41):

It should be visible now

view this post on Zulip Patrick Massot (Mar 04 2018 at 17:41):

@Chris Hughes could you have a look at https://github.com/kbuzzard/mathlib/pull/1/ ?

view this post on Zulip Kevin Buzzard (Mar 04 2018 at 17:42):

OK I can now see it

view this post on Zulip Scott Morrison (Mar 04 2018 at 19:08):

@Patrick Massot they are getting a PR ready. We met on Friday to discuss, and I'm now travelling all this week (actually doing some maths...), so I'm not sure when it will happen.

I think his plan is to send an initial PR covering subgroups, normal subgroups, centers, and kernels, and then a second PR with quotient groups and the first isomorphism theorem.


Last updated: May 15 2021 at 02:11 UTC