The Coq mailing list

[David Aspinall <David.Aspinall AT ed.ac.uk>]

Dear Coq'ers,

Interesting this has been raised.  Although you may be able to simulate
both cases with a proof control command (Abort) or using a false
axiom(!), I think it would be an excellent idea to extend the vernacular
to make these important cases explicit.   In particular, this would help
not only readers of your scripts but also tools concerned with
generating and analysing proof scripts (something we are looking at in
the Proof General Kit project).

For comparison, Isabelle's Isar language uses the words "oops" to stop
the proof attempt and forget theorem, and "sorry" to stop the 
proof attempt and retain the theorem --- morally there is a proof
obligation in this second case, although there is no way to 
discharge the obligation later apart from rewriting the script
(as far as I know).
 
 - David.
    
-- 
David Aspinall 
<David.Aspinall AT ed.ac.uk>

Attachment: signature.asc
Description: This is a digitally signed message part