The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Tue, Sep 25, 2012 at 2:27 AM, bertot 
<Yves.Bertot AT inria.fr>
 wrote:
> - We don't need to restrict to discrete maths.  Reasoning about real numbers
> is a good playground for learning mathematics. Epsilon-delta proofs, as can
> be seen in elementary calculus are a good example of where rigor is provided
> by the proof system.

I doubt that would work well in practice.  For my Topology contrib, I
did a limited number of epsilon-delta proofs (trying to keep them
minimal and split them as much as possible by invoking continuity
principles).  Almost always, the basic structure didn't take that long
to lay out; but actually proving the inequalities I needed became
extremely tedious and detailed.  Even with the help of the fourier
tactic, which only goes so far.

So, my fear would be that inexperienced students would get bogged down
in the details of the inequalities, and miss out on the big picture of
how the proofs are structured.

(Note that the Topology contrib is pretty much laid out in reverse
order of how you'd typically teach the subject in an undergraduate
course.  Where you'd usually start with the example of R^n, then
generalize to metric spaces, then to general topological spaces, my
contrib first defines topological space, and specializes to metric
spaces, and then proves the metric topology on R agrees with the order
topology -- and I take the order topology as the definition.  The
contrib also introduces nets and filters early and uses them for some
basic proofs where in a normal class you'd use proofs "closer to the
metal", and put off nets and filters until much later if you include
them at all.)

I guess what I'm trying to say is that analysis proofs seem to have a
higher ratio of formal proof to informal proof lengths than in things
like algebra or combinatorics.  At least in my experience.  (Another
area that I found somehow had a comparatively high ratio: proofs using
Zorn's Lemma.)

I do admit it was quite a thrill when I finally removed the last
"admit" from my formalization of Urysohn's Lemma, then executed Print
Assumptions on it and saw only things like classic, choice, functional
extensionality, etc.
-- 
Daniel Schepler