Bug 2558

Summary:	'Recursive definition of [...] is ill-formed.' on 'Defined.' after 'Proof completed'
Product:	Coq	Reporter:	sielenk
Component:	Main	Assignee:	nobody <coq-bugs-redist>
Status:	NEW ---
Severity:	normal	CC:	pierre.boutillier, sebastien.mondet+coq
Priority:	P5
Version:	trunk
Target Milestone:	---
Hardware:	PC
OS:	Linux
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...

Comment 3 Pierre Boutillier 2011-08-31 12:09:21 CEST

*** Bug 2585 has been marked as a duplicate of this bug. ***