coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, (continued)
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Jonas Oberhauser, 09/20/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Kristopher Micinski, 09/20/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Wolfram Kahl, 09/20/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Freek Wiedijk, 09/20/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Jonas Oberhauser, 09/20/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Wolfram Kahl, 09/20/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Kristopher Micinski, 09/20/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Julien Narboux, 09/20/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Daniel Schepler, 09/24/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, bertot, 09/25/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Daniel Schepler, 09/25/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Adam Chlipala, 09/25/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Daniel Schepler, 09/25/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Adam Chlipala, 09/26/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Daniel Schepler, 09/25/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Adam Chlipala, 09/25/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Adam Chlipala, 09/26/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Jason Gross, 09/27/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Daniel Schepler, 09/25/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Andrej Bauer, 09/27/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Daniel Schepler, 09/28/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Andrej Bauer, 09/28/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Daniel Schepler, 09/28/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, bertot, 09/25/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Adam Chlipala, 09/26/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Daniel Schepler, 09/24/2012
- Re: [Coq-Club] Interest in Coq-based mathematics classes?, Jonas Oberhauser, 09/20/2012
Archive powered by MHonArc 2.6.18.