The Coq mailing list

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

On 09/25/2012 02:07 PM, Daniel Schepler wrote:
> On Tue, Sep 25, 2012 at 10:53 AM, Adam 
> Chlipala<adamc AT csail.mit.edu>
>   wrote:
>    
> > 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!
> >      
> OK, then I'm not sure how you'd avoid giving away the answer on one
> hand, and also restricting the possible solutions on the other hand.
> For example, suppose the problem was "give an example of bounded
> sequences (a_n) and (b_n) where sup(a_n + b_n)<  sup(a_n) + sup(b_n),
> strictly", and then the tactics you give prove that (-1)^n +
> (-1)^(n+1) = 0, sup 0 = 0, sup((-1)^n) = sup((-1)^(n+1)) = 1.
>    

My idea would be to give one tactic that proves all of the above and 
more, without listing out its domain as documentation.  It's certainly 
tricky to get right, but I can also imagine the course staff working to 
add support for new reasonable facts that students wind up needing.