The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

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