search

coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
https://coq.inria.fr/
GNU Lesser General Public License v2.1
4.83k stars 646 forks source link

Anomaly: Not an unfoldable reference. Please report. #2955

Closed coqbot closed 11 years ago

coqbot commented 11 years ago

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#2955 From: Ludovic Patey <ludovic.patey@gmail.com> Reported version: 8.4 CC: @herbelin, @letouzey

coqbot commented 11 years ago

Comment author: Ludovic Patey <ludovic.patey@gmail.com>

Created attachment 382 Minimal example generating the error.

Hello,

I'm currently proving semantics preservation of a monadic translation in Coq, and I encounter this error everywhere. It happens while trying to apply the simpl tactic on an expression involving a mutually-dependendant inductive definition defined in another module.

I already had this problem with version 8.3, and it is still there in 8.4. I enclosed a minimal example.

Best, Ludovic

PS: I also have other bugs occuring in the same situation, with rewrite tactic: If H: A.foo n = 0 H0: A.foo = foo making rewrite H0 in H says "nothing to rewrite" And I've got to do remember (A.foo) as b ; clear Heqb ; subst ; clear b. to make rewriting. An example is given in the file.

Attached file: Test.v (text/x-verilog, 860 bytes) Description: Minimal example generating the error.

coqbot commented 11 years ago

Comment author: @herbelin

Bug of simpl is now fixed in branches v8.3 (r16179) and v8.4 (r16178). Bug was already fixed in trunk (thanks to "monomorphization" commit r15994 by Pierre-Marie Pédrot).

The second issue is more discutable. It is certainly counterintuitive that the rewrite tactic refuses to rewrite a constant name by an alias of this constant name, but it is unclear whether it is worth changing the code (*) so that rewrite does not complain, knowing that the two constants are indeed "equal" as names. Further opinions on this question are welcome.

(*) Technical comment: Changing the code would mean for rewrite not using eq_constr to test progress but to use instead a variant of it that does not equate constants having the same canonical name though coming from different modules.

coqbot commented 11 years ago

Comment author: @letouzey

Concerning the rewrite failure on modularly equivalent terms, I agree with Hugo: the behavior might be surprising and the error message could be improved, but I think this issue is relatively minor, and improving the behavior or the error message won't be particularly easy. So I'm afraid this won't change soon, sorry. Meanwhile, instead of rewrite, I suggest using "change" here which works fine.

Side remark : for separate issues, please submit separate bugs, it's easier to handle them later...

Summary: part I : RESOLVED part II : WONTFIX (at least now)

If you disagree with the WONTFIX, feel free to reopen a separate bug report concerning this part...

Best regards, Pierre Letouzey

coqbot commented 11 years ago

Comment author: Ludovic Patey <ludovic.patey@gmail.com>

I'm convinced by the argument of Hugo and am totally satisfied by the fix for the first part. Sorry for having posted multiple issues in the same report. I thought they were related.

Best, Ludovic Patey