The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Dear Michael,

Thanks for your message. Even if I haven't read SF yet, I've already heard about what you just said through the Stack Overflow question I linked above. Still, I'm uneasy encouraging students to do a proof using rewrite in this case. It's not the right way to conclude a proof where an hypothesis is absurd IMHO. At least, I try to show them then that there are two possible ways (I don't use SF for teaching but these kinds of situations come along often anyways).

Of course, I also understand what you explained: why you make sure to show them that the exercises are doable with what they just learned.

Best regards,

Théo

Le lun. 14 mai 2018 à 13:30, Soegtrop, Michael <michael.soegtrop AT intel.com> a écrit :

Dear Théo,

 

the question was about an exercise in the first file of SF where the only tactics discussed so far are intros, destruct, rewrite and reflexivity (not even apply). Teaching SF I frequently find that students are asking others and they say use this or that tactic and then they complain that the exercises are not doable with what they have learned so far. I just wanted to show that the exercise can be done with the tools already learned. Actually there are no exercises in SF which cannot be done with the things learned so far except 5 start exercises (which are intended to be done in a second pass).

 

Best regards,

 

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928