Pierre Rousselin (Nov 08 2023 at 08:52): Pierre Rousselin (Nov 08 2023 at 08:52):This fifth session (out of 6) was in two parts:
@Hugo Herbelin (please do not hesitate to add things I forgot) was here.
It's probably the session the students struggled the most with.
Most of the issues are pedagogical, some of them raise Coq questions, others are
related with the user interface (Coq/jscoq).
About classical logic: The students have used intuitionistic logic from the
first day, now we give them classic as an axiom. It's the first time I've
written a separate file about classical logic. Seeing them struggling with De
Morgan's law was surprising. On the other hand it's not that easy: with
intuitionistic logic the path is clearer; the excluded middle can happen at any
point. For propositional logic, we could tell them to just use the excluded
middle for every occurring proposition and use a kind of "truth table"
reasoning, but I'm not sure it would really be a good thing.
Some students tried to destruct P, with P : Prop.
I think I still want more from Coq.Logic.Classical, with tactics like:
by_casesby_contradictionby_contrapositionpush_negAbout real numbers: This first file's philosophy is that the students are given
progressively some axioms and they have to "unlock" new lemmas from these.
A first issue is that nothing actually prevents them from proving, say,
Rplus_0_r with an imported Rplus_0_r. For this I would like to have some
kind of selective Import; but maybe I could also write the file differently.
Many students wanted to use the names from Nat (e.g. add_0_l), so this
goes in the direction of a current discussion about Reals.
At this point forward reasoning would probably be more natural, however, I
only introduced apply in and rewrite in. Using assert at this point
would probably be better. But then, maybe what we really want is some form of
Lean's calc.
Again we had some hidden parentheses issues. There is Set Printing
Parentheses but this adds too much. Something like Set Printing Parentheses
for "+" or something like that would be good (or something in the IDE).
About basic tactics: I did not write down yet a tactics cheat sheet, it is my
fault. In general, I feel that I need simpler and more predictable tactics. But
first I need to write down clearly what I expect of each tactic in this course,
which is not that simple.
About the UI: All the students (except one duo using CoqIDE) use jscoq. Some
UI problems are related to Coq, others are related to jscoq.
Error messages: there is room from improvement in terms of readability. The
"cannot unify" messages use some hard to read variables like ?M1034. I
already mentioned the "no product, even after head reduction" message.
Ideally, I would also like multilingual support.
The auto-completion list in jscoq is nice but too big. I don't know if it is a
Coq issue or a jscoq issue, though.
The other problems, I have already mentioned: need to load/save documents and
an easier way for the teacher to provide her own library instead of being
restricted to the stdlib (or other libraries). I won't try more things this
year since it's almost the end, but I hope this will be available in the
future.
Concluding thoughts: this is still very enjoyable to see how active the students
are. The need to have a "Coq document" (here HTML with Coq snippets, but it
could be something else) is clear and jscoq provides it nicely. I have listed
things for which IMHO, there is room from improvement, but let's not forget also
that the biggest difficulty here is mathematics. The students are first year
undergraduate, so it's the first time they reason at such an abstract level. A
proof assistant makes it possible.
Julio Di Egidio (Nov 08 2023 at 15:32):Pierre Rousselin said:
On the other hand it's not that easy: with intuitionistic
logic the path is clearer; the excluded middle can happen
at any point. For propositional logic, we could tell them
to just use the excluded middle for every occurring
proposition and use a kind of "truth table" reasoning, but
I'm not sure it would really be a good thing.
Not sure if this is relevant, I have been thinking about similar issues, though for my own programming "patterns".
At some point I have decided (for the time being, of course) I won't use classical axioms unless and until strictly necessary (and singling out the use, at least in documentation if not also in the naming of the theorems affected), not so much re intuitionistic but re constructive logic: but my requirement indeed is that decidability and computability are primary. (Makes sense?)
As for the classical side, of course I cant' say, but FWIW "truth tables" sounds pretty reasonable to me and possibly amenable to quite some automation: I am just not sure how it would play with my previous point, i.e. in a scenario where classical is to be kept "under control".
Last updated: Oct 13 2024 at 01:02 UTC