The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 09/25/2012 01:46 PM, Daniel Schepler wrote:
> 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.
>    

The trick in this context is that there is no need to build completely 
general tactics.  You could build a monster per assigned homework 
problem, for doing every step you don't want to ask students to do, and 
it would still be fine from an educational perspective!