The Coq mailing list

[andré hirschowitz <ah AT unice.fr>]

Hi all,

Although it is not so clearly related to Adam's original question, here 
is a short report on my activity on teaching proofs to freshmen in 
mathematics.

My activity until 2007 is roughly reported in the slides already mentioned here http://math.unice.fr/~ah/div/bghp.pdf .





At that time, my friend Loic Pottier was tired of programming Coqweb and
 decided to stop, and I found nobody else interested in going ahead.
While,
 until then, I had tried to teach proofs within a regular calculus or 
algebra course, from 2008 on, I was committed to give a regular course 
on logic for freshmen. I was given full freedom, except one condition: 
not to use Coq(web)! This interdiction, formulated by an essentially 
normal chairman, reflected the standard receptivity of the mathematical 
community to our new tools.

In order to fill the gap between students, standard colleagues, and 
the coq-like way of thinking, I have progressively elaborated a 
presentation of proofs not too far from Coq, but sticking to the basic 
tactics, left and right introductions for And Or Imply Forall Exist, 
plus the minimum extra needed. Poor French slides of these courses are 
available on my web page (http://math.unice.fr/~ah/ens/MD.html).
 Another main feature of my approach is that I have systematically 
treated (or asked to treat) statements from standard calculus. The third
 main feature is that I have proposed (only) exercises on Wims: there 
students give (by drag and drop) a list of tactics which is 
machine-checked (the list can be partially ok).


As a sample, here is the statement of a typical exercise :

%%%%%%%%%%%%%%%%
Here is a statement found on the web (www.math.univ-toulouse.fr/~yak/Suites-Poly.pdf , p.45),  together with its proof :



Every convergent sequence is Cauchy.

Proof. Let u be a convergent sequence and let L be its limit. We know that
$\forall \epsilon >0, \exists N(\epsilon ): \NN, \forall n \ge N(\epsilon), |u_n -L|  \le  \epsilon$.



We deduce that, for all  n and m bigger than   $N(\frac{\epsilon}{2})$, we have 
$ |u_n -u_m| =  |u_n - L - (u_m -L)| \le  |u_n - L|+|u_m -L| \le \epsilon$,
which proves that u is Cauchy.
Qed.

This proof suggests a sequence of tactics. Give the corresponding subsequence of ten Forall_L Forall_R Exist_L Exist_R tactics. 



%%%%%%%%%%%%%%%%%%%

Of course, it is a pity that such exercises cannot (yet) be performed through a tool like Coqweb.

ah

2012/9/20 Julien Narboux <jnarboux AT narboux.fr>

HI Adam,

In France, André Hirschowitz and Loic Pottier and Xiao Gang have performed some experiments about using Coq to teach mathematics.

see:http://math.unice.fr/~ah/div/bghp.pdf

Christophe Raffalli is also using his own tool called Phox to teach maths:
http://www.lama.univ-savoie.fr/~raffalli/?page=cours&lang=fr

Cheers,

Julien

2012/9/17 Adam Chlipala <adamc AT csail.mit.edu>

I'm interested in applying Coq in teaching university students mathematical subjects, including the theory underlying computing.  This message is meant to get a sense of who out there is interested in collaborating to build the necessary tool support.

A bit of my personal context: I teach at MIT, which has a newish initiative MITx, for running online classes, with opportunities to apply the same technology to augment traditional in-person education.  Automatic grading is a central part of the approach, and one of the biggest scaling challenges has been grading assignments where students write mathematical proofs.  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.  I'm doing some initial work in this direction with students, but I think this is an idea that could really benefit from a broad community effort.

So, I have two primary questions to ask:

1. Would any Coq experts be interested in spending some time at MIT as postdocs or research scientists, building the support for applying Coq in early university classes relevant to computer science?  Please let me know if so!

2. Could we as a community create an open platform for contributing Coq libraries relevant to different modules of different courses?  A nice user interface would be crucial, and it wouldn't be any good for each university to roll its own.  I would like to see a web-based interface, with bonus points (from my perspective) if it uses my language Ur/Web <http://www.impredicative.com/ur/>. :)  I also feel that we need course-specific tactic libraries, to allow proofs to be written at the right levels of abstraction, without overwhelming students.