The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 20.09.2012 01:04, schrieb Kristopher Micinski:
> On Wed, Sep 19, 2012 at 6:56 PM, Jonas Oberhauser 
> <s9joober AT gmail.com>
>  wrote:
> > Am 17.09.2012 19:47, schrieb Adam Chlipala:
> >
> > >    I think Coq is the secret weapon for addressing this challenge, but I
> > > also think we need some new tool and library support to present Coq in a way
> > > that doesn't send first-year university students running and screaming.
> >
> > Although this does not address your issues directly, I took a course
> > covering Coq in my second semester and to much benefit, as I feel. I have
> > also urged other students to do the same and could convince at least two
> > other second semester students to take that course. Although the course was
> > slightly different from when I took it, the feedback from the other second
> > semester students was positive. (I have also received feedback from other
> > students I urged to take the course and the feedback was ... mixed).
> >
> > For me working with Coq gave me a lot more structure my thoughts and a more
> > analytical view on proving and mathematics as a whole.
> > I hope that if such classes could be established, other students can profit
> > in the same way. While I was a tutor I have seen how some students approach
> > proving and I was shocked.
> May I ask the range of topics covered?  I think the consensus here is that:
>
>    -- Coq provides a great interactive (and more importantly,
> *accountable*) style for learning formal mathematics.
>    -- Being based on type theoretic concepts, it's natural to teach
> things that look like (can be encoded easily in) type theory using it.
>    -- Doing so with freshmen / sophomore classes requires careful
> planning so as not to force students to battle these topics directly.
>    -- A first start to this will be identifying a good base set of
> material that can be formalized (definitions written, theorems proved,
> tactics provided, book written) for teaching a first / second year
> class.
>
> I've been looking and thinking about how you would introduce freshmen
> to discrete math using Coq, and again looking at the Gries and
> Schneider book "A Logical Approach to Discrete Math," I rather like
> it...
>
> kris

The course is not aimed at freshmen. It is a course usually taken in the 
fourth or sixth semester of bachelors or masters.

Modulo my lossy memory (and taking into consideration the table of 
contents), the course first introduced us to Coq syntax, how to use Coq 
to define inductive datastructures and operators on these 
datastructures, how to prove simple properties using tactics, etc. After 
we had that basic knowledge we were introduced to reduction and typing 
rules (also confluence and termination), the curry-howard isomorphism, 
dependent types and matches, sum and sigma types. Then we formalized 
boolean logic and quantified boolean logic; in this context we also 
learned about the tableau method and how to simulate it in Coq. Then we 
learned the crude basics of: intuitionistic vs classical logic, 
extension vs intension, proof irrelevance. After I took a couple of 
courses in philosophy I felt cheated by that last chapter.

If you are interested in the details, i.e. the covered proofs etc, 
here's the script: 
http://www.ps.uni-saarland.de/courses/cl-ss11/script/icl.pdf

Cheers,
jonas