Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Interest in Coq-based mathematics classes?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Interest in Coq-based mathematics classes?


Chronological Thread 
  • From: Daniel Schepler <dschepler AT gmail.com>
  • To: Adam Chlipala <adamc AT csail.mit.edu>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Interest in Coq-based mathematics classes?
  • Date: Tue, 25 Sep 2012 11:07:46 -0700

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



Archive powered by MHonArc 2.6.18.

Top of Page