Pierre Rousselin (Sep 26 2023 at 14:29): Pierre Rousselin (Sep 26 2023 at 14:29):So, my first lecture with Coq for undergraduates went well, so I noticed some (not that important) pedagogical issues with some basic tactics. These are, maybe, easily fixed with a little bit of Ltac.
intros for both variables and hypotheses can be a little bit disturbing for the students. Maybe some custom fix and assume tactics would do a better job for the first lecture.apply to have a very clear semantics (one applies an implication), the fact that it subsumes exact in particular, could be also a bit disturbing (I like that apply is strong in my own proofs but not with the students).destruct H. to finish a proof when H is a proof of False. Karl Palmskog (Sep 26 2023 at 14:31):I hope someone will do some experiment at some point of working "modulo SAT" with Coq at some point, i.e., the only allowed tactics are (1) first-order stuff or more powerful/domain-specific and (2) SAT solving. intros is actually doing first-order stuff, so it would be allowed.
Théo Winterhalter (Sep 26 2023 at 15:03):For False, we show our students exfalso first. We also showed apply but not exact.
Théo Zimmermann (Sep 26 2023 at 15:18):destruct is indeed way too powerful. Students try it at random and get used to it doing useful stuff (e.g., it can perform a rewrite), but then they do not notice when they apply it on something that just makes hypotheses disappear without making the goal progress.
Emilio Jesús Gallego Arias (Sep 26 2023 at 15:26):@Théo Zimmermann indeed destruct does way too much, I've actually had a bit more success on my short courses going the lower-level way case: $gpat ; this mimics the convoy pattern actually, and opens the door to move advanced case analysis using dependent indexes.
Emilio Jesús Gallego Arias (Sep 26 2023 at 15:26):Moreover destruct will, for my taste, manipulate the context too much, I find this to be fragile so even when not using ssr I tend to prefer the more primitive case tactic.
Pierre Rousselin (Sep 26 2023 at 15:30):Théo Winterhalter said:
For
False, we show our studentsexfalsofirst. We also showedapplybut notexact.
Hmm... ok, maybe next year I will just show exfalso; exact H.
The nice thing about exact (for pedagogical purposes) is that it does not unify silently. So there is less magic involved during the first hours.
Pierre Rousselin (Sep 26 2023 at 15:37):Théo Zimmermann said:
destructis indeed way too powerful. Students try it at random and get used to it doing useful stuff (e.g., it can perform a rewrite), but then they do not notice when they apply it on something that just makes hypotheses disappear without making the goal progress.
Since this lecture does not really much talks about Inductive types and props, we reduce the roles of destruct to :
I think it's okish as long as they don't try too many random things.
Maybe for this lecture, everything could be wrapped in separate tactics.
We also show them (more this year) intro patterns with brackets.
Huỳnh Trần Khanh (Sep 26 2023 at 15:38):one thing that I'd caution all of you against is creating new tactics specifically for your course or changing the behavior of existing tactics. on the Lean side many people learning Lean through Natural Number Game struggle to adapt to actual Lean because of the differences. encouraging the use of more granular tactics might be OK though
Théo Zimmermann (Sep 26 2023 at 15:40):I think it's okish as long as they don't try too many random things.
In my experience it's ok for the first few lessons, but as they learn more and more tactics, they forget about which ones they should use in which case and they start trying them randomly. And there, everything breaks loose because instead of immediately failing, the tactics actually do stuff on their goals, even if this is outside the scope of what was seen in class.
Pierre Rousselin (Sep 26 2023 at 15:40):Huỳnh Trần Khanh said:
one thing that I'd caution all of you against is creating new tactics specifically for your course or changing the behavior of existing tactics. on the Lean side many people learning Lean through Natural Number Game struggle to adapt to actual Lean because of the differences. encouraging the use of more granular tactics might be OK though
Yes, there are definitely some downsides to customizing too much. For the moment I'm ok with destruct but seriously considering alternatives to intros in further experiments (but not this year since there is no "undo" in real life).
Pierre Rousselin (Sep 26 2023 at 16:21):Théo Zimmermann said:
I think it's okish as long as they don't try too many random things.
In my experience it's ok for the first few lessons, but as they learn more and more tactics, they forget about which ones they should use in which case and they start trying them randomly. And there, everything breaks loose because instead of immediately failing, the tactics actually do stuff on their goals, even if this is outside the scope of what was seen in class.
Yes, you're right, I forgot how it is at the end of the course. OTOH I think it's also ok to teach them that trying things at random is not really a good method :D
Pierre Rousselin (Oct 03 2023 at 16:38):Small update after today's second 3-hour session.
destruct on hypotheses of type P -> False (I don't really know what it does, but it got them stuck). The sad thing is that the students wasted quite some time on this.Lemma impl3': forall (P Q R : Prop), (P -> Q -> R) -> P -> Q -> R.
using
imp_refl: forall (P : Prop), P -> P.
and unification. The student tought of:
exact (imp_refl _ -> _ -> _).
but then there was a universe inconsistency issue. Filling one of the holes solved it, but it was surprising.
->. Right associativity of -> is not that easy for first year undergraduate Emilio Jesús Gallego Arias (Oct 03 2023 at 16:51):It would be nice if it was easy to print all lemmas and theorems defined in the current file.
coq-lsp does provide the outline view (at least emacs and vscode clients do show it) , jsCoq 2.0 hopefully will be able to display it too. I do agree that's a very useful feature to have.
Pierre Roux (Oct 03 2023 at 19:47):Pierre Rousselin said:
- Print Parentheses with
->. Right associativity of->is not that easy for first year undergraduate
In Coq master:
Set Printing Parentheses.
Check nat -> nat -> nat.
(* nat -> (nat -> nat) *)
Print Parentheses is immensely useful for teaching (and was introduced for this purpose)
Théo Zimmermann (Oct 04 2023 at 07:25):It cannot be set by default even when teaching because it clutters goals too much, but knowing how to use it is a useful thing to teach students.
Karl Palmskog (Oct 04 2023 at 07:28):on the other hand, isn't it good practice to teach people to add parentheses? One can validate by looking at printing that the added parentheses "disappeared"
Théo Zimmermann (Oct 04 2023 at 07:29):Sure, but also it's a much less obvious process, isn't it?
Karl Palmskog (Oct 04 2023 at 07:32):I guess it's a teaching style thing in the end
Théo Winterhalter (Oct 04 2023 at 07:39):It depends a lot on whether they are used to, say, OCaml before.
Théo Zimmermann (Oct 04 2023 at 07:43):Even for students used to OCaml before, Set Printing Parentheses has been useful, e.g., to make obvious which associativity rules are used for +.
Théo Winterhalter (Oct 04 2023 at 07:45):Oh right. I meant for arrows, but indeed, this can be very helpful!
Pierre Rousselin (Oct 04 2023 at 09:55):This does not seem to work (with arrows) in CoqIDE. Tested with 8.16, 8.17 and 8.18. Neither does this work with jsCoq (at least version "1", that is wacoq 0.16).
Pierre Roux (Oct 04 2023 at 09:59):Yep, this was recently fixed in Master, will work with 8.19.
Pierre Rousselin (Oct 10 2023 at 15:17):Today (3rd lecture) was mostly (depending on the students) about
About natural numbers, rewriting with associativity is one of the main difficulties, it is made harder by hidden parentheses. I would have liked to print parentheses just for +. At this point, it is also important that they learn to instantiate their rewrites. Maybe (with on option), it would be nice for beginners if rewrite suggests to use rewrite <- if appropriate. I have told them to avoid simpl in favor of rewrite and they mostly follow this advice (this prepares lessons about real numbers). Again I also express the need of searching in lemmas proved (or admitted) in the current file _at this point_.
Predicate calculus is, as expected, difficult. I have not introduced the excluded middle yet, so there is only one way to prove an existential formula. Still, the students have a tendency to choose a witness too early (same thing for left, right and \/). Also the students forget things from the earlier sessions (e.g. destruct on nat) and start to confuse rewrite and apply.
Pierre Rousselin (Oct 10 2023 at 16:31):I think I will have to write a cheatsheet with the tactics and their expected semantics.
grianneau (Oct 10 2023 at 16:53):Pierre Rousselin said:
I think I will have to write a cheatsheet with the tactics and their expected semantics.
There is a cheatsheet (with SSReflect tactics) made available by Enrico there:
https://github.com/gares/math-comp-school-2022
I was happy to find this source code for a Coq cheatsheet :) I've just modified it today for a tutorial.
Pierre Rousselin (Oct 17 2023 at 17:23):To keep on with my weekly reports.
This is the fourth 3h hands-on session (no courses) out of 6. Most students are between Predicate calculus and classical logic here.
At this point the students really struggle and mix everything because it starts being more maths than Coq.
discriminate. It doesn't really correspond to anything in maths so it feels weird. Maybe with more time I could explain more constructors and injection, but I think they view it as a magic thing.Classical is not good enough... I think we need more than destruct (classic ...).Nat.le and Nat.divide. They have a link to this forum (beginners questions welcome).All in all, I have mixed feelings today. I've worked a lot on the material, this course is really hard to write and every little detail counts. The students are still active but I can feel some discouragement too.
Last updated: Oct 13 2024 at 01:02 UTC