The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

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.
-- 
Daniel Schepler