Zulip Chat Archive

Stream: Lean for teaching

Topic: teaching algebraic structures


Rob Lewis (Oct 27 2021 at 17:16):

I'm about to introduce my class to groups, rings, and fields. Mathlib's implementations have a lot of noise, for forgetful inheritance reasons. I don't want to introduce my students to this notion yet. So we'll start by defining group on our own, but very quickly I want all the group theorems in mathlib, so we'll have to switch.

How have others dealt with this dissonance? I'll tell them "there are a lot of fields you see when you #print group that you can really just ignore." But it's really ugly, and I don't think there's a clean way to see only the necessary fields of a structure, is there?

Rob Lewis (Oct 27 2021 at 17:17):

In particular, using the hole command to generate a skeleton structure shows you all the junk.

Rob Lewis (Oct 27 2021 at 17:18):

If you start with an empty structure { } the error messages "field ... was not provided" only cover the necessary stuff, which is good. But this isn't a great way to display it and it's annoying to have to go through them one by one.

Kevin Buzzard (Oct 27 2021 at 17:36):

I absolutely agree with you. I've only dealt with groups in one-off lectures, not in classes, and since the nsmul stuff appeared I've been rolling my own. You even see this problem with preorder, where using the hole command generates lt even though it's :=... and lt_iff_le_not_le even though it's ... . order_laws_tac. I would just switch, under the pretence that "we spent an hour proving theorems about groups but clearly we don't want to go through all x thousand lines of code in mathlib about group theory, oh by the way, here's a custom constructor I just made which enables us to make mathlib groups using exactly the same axioms as we used to make those hand-rolled groups last time"

Johan Commelin (Oct 27 2021 at 17:36):

Can meta programming detect which fields have default args?

Kevin Buzzard (Oct 27 2021 at 17:37):

you want to detect default args and args which are filled in with default tactics

Kevin Buzzard (Oct 27 2021 at 17:38):

"don't look at the definition of a group, it's not what you think it is" is no different to "don't look at the definition of a compact space, it's not something about open covers having finite subcovers despite the fact that this is the definition in every math textbook ever"

Johan Commelin (Oct 27 2021 at 17:40):

fair enough

Filippo A. E. Nuccio (Oct 27 2021 at 17:41):

@Kevin Buzzard When teaching your class last Spring (the formalising_mathematics repo), did this problem occur often? I am asking because I will need to teach a course next year and wanted to draw inspiration from yours.

Kevin Buzzard (Oct 27 2021 at 17:43):

My course was 8 independent short stories. So in the group theory short story I rolled my own groups and subgroups, and then we put them away and never used them again; later on when we needed groups I used mathlib's groups.

Filippo A. E. Nuccio (Oct 27 2021 at 17:45):

Ah OK, I see. And did you do a "pilot Episode 0" telling students the basics or was Episode 1 the true beginning, with them already in front of some Lean Code?

Kevin Buzzard (Oct 27 2021 at 17:51):

I demanded that everyone install Lean/VS Code etc beforehand, and then I just put episode 1 in front of them, and it was way way way too much material to cover in 2 hours. My current attempt on how to start a Lean course for mathematicians is here

Kevin Buzzard (Oct 27 2021 at 17:52):

I will be getting 1st years to beta test it next week

Rob Lewis (Oct 27 2021 at 17:52):

I'm ready to handwave it away for now, but some of my students will do math-y final projects and I don't want them to use a handrolled group for that. I trust them to figure it out more or less after I explain the handwaving. But this is a big-ish UI hiccup.

Rob Lewis (Oct 27 2021 at 17:52):

Metaprogramming can detect default tactics but not default args, afaik

Filippo A. E. Nuccio (Oct 27 2021 at 17:53):

Thanks! I have also seen you will be teaching in Term 2 to more advanced students. I guess I will try to steal a lot of ideas, is it allowed :angel: ?

Rob Lewis (Oct 27 2021 at 17:53):

We should definitely update that hole command to omit as many provided fields as we can detect.

Kevin Buzzard (Oct 27 2021 at 17:54):

@Rob: I've got used to it now. You roll your own natural numbers / groups / whatever, you maybe give them silly names like xena.group or my_group, you play around with them, and then you say "but of course we need 1000 lemmas so we're going to have to use mathlib's official ones now"

Kevin Buzzard (Oct 27 2021 at 17:55):

@Filippo I'm going to start preparing teaching materials for final year UGs in November and it will all be publically available.

Filippo A. E. Nuccio (Oct 27 2021 at 17:56):

Great! I will then ask for the link. I think that finding a balance in what you're currently discussing with Rob will be a hard point for a novice teacher.

Kevin Buzzard (Oct 27 2021 at 17:57):

@Rob the mantra I always push is "don't unfold -- use the API", but your audience will be different to mine; probably a bit less scared about computers but also I suspect far happier to take on board the idea that there can be more than one implementation of a structure and that it's not for them to worry about how the devs actually did it as long as they can use it.

Filippo A. E. Nuccio (Oct 27 2021 at 17:59):

Ah, one more question: from your experience, would you recommend having the students be in front of their PC trying to code 100% of the time, or would it be better to have some balance between me showing/coding/teaching "classically" and them trying/coding/getting frustrated?

Adam Topaz (Oct 27 2021 at 18:23):

Getting frustrated is the only way to learn (in my opinion)

Filippo A. E. Nuccio (Oct 27 2021 at 18:24):

I basically agree, but wouldn't you think that a bit of balance might help? I am happy I haven't been confronted to prismatic cohomology before simplicial one... But sure, you're right: a good deal of frustration helps.

Adam Topaz (Oct 27 2021 at 18:25):

The issue with groups is not just about the weird fields like gpow_..., but also because the first definition students see for groups is "A set GG with a binary operation such that blah blah blah". I introduced lean to a few of my group theory students this term, and the fact that ()1(-)^{-1} is defined as part of the data of a group was also confusing for them.

Filippo A. E. Nuccio (Oct 27 2021 at 18:26):

I see; do you have a public repo with your material?

Adam Topaz (Oct 27 2021 at 18:27):

there is no repo. I am not actually teaching any lean, this was just some optional components that some students found interesting.

Adam Topaz (Oct 27 2021 at 18:31):

Rob Lewis said:

We should definitely update that hole command to omit as many provided fields as we can detect.

Is this really a good idea? I would prefer to delete the fields myself if I want the default.

Adam Topaz (Oct 27 2021 at 18:31):

Is there a way to indicate that a certain field is optional?


Last updated: Dec 20 2023 at 11:08 UTC