Video tutorials for the Coq proof assistant
- 22 February 2011
- General
Next week I am going to a meeting where I am supposed to give a tutorial on the Coq proof assistant. Inspired by the Catsters, I decided to prepare the material in the form of screencasts. You can find the first few tutorials on Youtube in my “Coq tutorials” playlist. So far I have:
- Obtaining and installing the Coq proof assistant
- How to use CoqIDE
- How to use Coq with Proof General
- A first proof with Coq (Frobenius rule)
- The dual Frobenius rule, part 1
- The dual Frobenius rule, part 2
- Currying and uncurrying, part 1
- Currying and uncurrying, part 2
You should turn on the high quality HD stream when you watch these. Feedback is welcome (and easy to provide on Youtube). I find it very, very difficult to listen to my own voice. I hope to have many more lectures soon, but I am starting to feel out of my depth, so if anyone wants to help they are welcome!
I am making screencasts with
Screenium on my Mac, which is just one of many available options. Preparation of a screencast takes less time than preparation of equivalent written notes or slides, as long as one is not obsessed with making everything perfect. In fact, I think it is important not to make tutorials perfect. In a screencast the viewer can see how I make mistakes and, more importantly, how I discover and fix them. It still takes me two or three takes before I am happy with a screencast, but all in all the process is becoming more streamlined with each next tutorial.
I have learnt a couple of tricks. The “pause” button is my friend when the phone rings or I need to think for a moment what to say next. It takes less time to start over than to try to edit out mistakes afterwards. A screen cast must be short. There must be a central message, but often I find it convenient to explain “on the side” various details which do not easily fit anywhere.
Somehow the whole process feels organic. There is less global planning than in teaching a course, but some planning is still needed. There are non-traditional ways of organizing tutorials into playlists. For example, other people can combine screencasts from various sources and create their own tracks. I think there is a lot of potential.
Screencasts are ok for computer-sciency themes, such as Coq and programming, but for real math, I will have to make videos of handwriting. The Catsters stand in front of a blackboard in their videos, but I would like to try pencil and paper with our departmental document camera. We will see how that goes.
andrejbauer@mathstodon.xyz, I will
gladly respond.
You are also welcome to contact me directly.
Comments
That's one great tutorial. Thank you!
Thanks for the nice videos! I should try this some time. Maybe you can provide the .v files somewhere?
Nice tutorials!
I have experimented with videos too, in particular with video/slideshow hybrids. The idea is that some people don't like watching videos because they are hard to skim and navigate. Feel free to drop me a line in case you'd like to "steal" anything, I'm happy to make this open source etc.
For real math, a pen tablet works quite well; I simply copied the style of Khan Academy. The 90€ purchase is easily justified with the observation that "professional mathematicians need professional tools". I think that blackboard or paper don't work so well because the visual quality tends to be rather poor. CCD noise, compression artifacts etc. That said, it is a tad easier for me to do nice handwriting on paper.
Concerning hearing your own voice, I have found that applying an audio plugin that simulates light reverb / room ambience can help.
Ayn recommendations on a tablet (for Mac)?
I bought a Wacom Bamboo Fun. Works flawlessly with my Mac. Highly configurable, too.
Note that the Bamboo Fun has (had?) two different sizes: a smaller S version and a larger M version. (The website only shows the larger version.) I bought the smaller version, whose pen sensitive area has the size of a postcard. If I were to buy again and if I had sufficient funds, I would buy the larger version, though, because that leaves more room for handwriting.
Andrej, the tutorials are great. Can you please add one more that has some structural induction? I would like to see how you prove this:
Theorem map_id : forall ls, map id ls = ls.
Cheers! Dan
I managed to do it myself eventually. (Theorem map_id : forall ls, map id ls = ls.) It's great stuff this Coq.
... and you do have a tutorial on recursion and induction, just that it's not linked from this page. Dan.
Great screencast!
[...] Video tutorials for the Coq proof assistant [...]
[…] There were some things I recognized, but also a lot of things that were foreign. I found these video tutorials for Coq by Andrej Bauer, which were very helpful. I tried following along, but I didn’t get very far […]
[…] There were some things I recognized, but also a lot of things that were foreign. I found these video tutorials for Coq by Andrej Bauer, which were very helpful. I tried following along, but I didn’t get very far […]
Thanks a lot for the helpful videos! Without them, I couldn't have gotten started with Coq. You're doing a very nice job.
Very nice videos. Thank you for posting!
These tutorials are brilliant. Terse enough to keep you interested, and the examples are appropriate too. Thank you!
[…] Video Tutorials (Andrej Bauer) […]
Great tutorial. One issue: I wasn't sure of the logical context from which Coq starts. Is it intuitionist logic? That might have been made clear.