Pierre Rousselin (Sep 12 2023 at 14:29): Pierre Rousselin (Sep 12 2023 at 14:29):Has anyone tried to teach undergraduate students some form of "Set theory" with Coq?
My previous attempt at the subject is a bit messy and not very satisfying. We use some type A and A -> Prop, see here the draft in french if you want : second part of this.
I think this does not really add more than plain predicate calculus (and we do not use fancy notations).
Of course there are many ways to formalize sets in Coq.
Would you have some suggestions?
Pierre Roux (Sep 12 2023 at 14:32):Never tried but coq-mathcomp-classical (subpackage of MathComp Analysis) has a classical_sets.v file about classical set theory https://github.com/math-comp/analysis/blob/master/classical/classical_sets.v if it can be of any interest
Karl Palmskog (Sep 12 2023 at 17:35):@Paolo Giarrusso as resident Std++ expert (user), isn't there a way to use classical sets via Std++? (https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/stdpp/sets.v is the closest I see)
Karl Palmskog (Sep 12 2023 at 17:37):in my experience, using/teaching MathComp is all or nothing, so people teaching [with] Coq could probably use some alternative
Paolo Giarrusso (Sep 12 2023 at 19:37):@Karl Palmskog Require Import stdpp.propset + Coq stdlib LEM
Paolo Giarrusso (Sep 12 2023 at 19:39):at least propset gives you not-necessarily-finite sets defined via predicates, while still plugging into stdpp
Paolo Giarrusso (Sep 12 2023 at 19:44):In particular, set_solver should still be able to turn ≡ on propset into first-order logic problems and then use a first-order solver. You can plug sauto, tho in my quick experiments it was even solver than stdpp naive_solver... regardless, this is probably good enough for teaching, especially if the teacher can write a "prelude" hiding any complexities (say, plugging set_solver and sauto together)
Pierre Rousselin (Sep 13 2023 at 07:51):stdpp looks very utf8 heavy. Do you use specific tools for this? At the beginning, I used utf8 for my course, but it proved to be yet another thing to digest for the students so I abandoned it.
Pierre Rousselin (Sep 13 2023 at 07:58):Karl Palmskog said:
Paolo Giarrusso as resident Std++ expert (user), isn't there a way to use classical sets via Std++? (https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/stdpp/sets.v is the closest I see)
The math-comp or not math-comp question will probably arise very often... I think it's good to take any ideas, even if in the end math-comp is not used and serves mostly as an inspiration.
Paolo Giarrusso (Sep 13 2023 at 08:58):@Pierre Rousselin here are the docs on configuring editors for stdpp — even if configs there include iris symbols: https://gitlab.mpi-sws.org/iris/iris/-/blob/master/docs/editor.md?ref_type=heads
Paolo Giarrusso (Sep 13 2023 at 09:04):I agree one might want non-unicode notations; one can add that on top but some work is needed https://github.com/bedrocksystems/BRiCk/blob/614b303aa6370ecfcb354ec9715e65a5a5a28630/theories/prelude/notations.v
djao (Sep 13 2023 at 09:42):For sufficiently advanced undergraduates, I've done literal ZFC set theory with Coq. See https://proofassistants.stackexchange.com/a/2169/2148
Pierre Rousselin (Sep 13 2023 at 12:43):djao said:
For sufficiently advanced undergraduates, I've done literal ZFC set theory with Coq. See https://proofassistants.stackexchange.com/a/2169/2148
That's interesting. Where did you go after this? Did you push all the way to natural numbers?
djao (Sep 13 2023 at 22:44):Pierre Rousselin said:
That's interesting. Where did you go after this? Did you push all the way to natural numbers?
I have in fact gone all the way to real numbers and quadratic reciprocity (but not with undergraduates).
Pierre Rousselin (Sep 14 2023 at 04:57):I would be very curious to see how the proofs go. Are they long and/or complicated?
djao (Sep 14 2023 at 05:09):https://github.com/davidjao/zfc-coq have at it.
Last updated: Oct 13 2024 at 01:02 UTC