Bugzilla – Full Text Bug Listing
|Summary:||'Recursive definition of [...] is ill-formed.' on 'Defined.' after 'Proof completed'|
|Attachments:||A script triggering the bug. Comments point to the problem.|
Description sielenk 2011-06-19 10:01:43 CEST
The attached code contains a Fixpoint definition (term21') which fails to save after Coq has reported 'Proof complete'. A minor change in the development of the propositional part of the definition fixes the problem: If I replace a direct case analysis on an equality (via 'destruct') by an indirect one (via 'rewrite'), the definition can be saved.
Comment 1 sielenk 2011-06-19 10:03:40 CEST
Created attachment 260 [details] A script triggering the bug. Comments point to the problem.
Comment 2 Pierre Boutillier 2011-06-19 16:48:54 CEST
Welcome in the nightmare of defining fixpoints by tactics. Your problem here is that whereas rewrite only rewrites the goal, destruct rewrites all the hypotheses too. Consequently, it rewrites also the fixpoint definition (that you don't need anymore !) and then the guard condition complains about a wrong (and useless) use of the fixpoint ! Telling I don't need the fixpoint anymore by "clear term21' ; destruct H3a." would have done the job too...