The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I have python scripts on my github called coq-bug-finder which were written for exactly this kind of problem.  They now successfully handle non-flat directory structures and require-without-import.  If you can turn the misbehavior into an error (e.g., simple; unfold f. Fail progress simpl. => command has not failed (when unfolding helps, which it shouldn't)), find-bug.py will inline dependencies, and start trimming your file while making sure the error doesn't disappear.  If you want any help running it, let me know.  (Warning: the script misbehaves on windows, in my experience.  Help understanding why coqtop's output never makes it to my script (or why my script's commands never make it to coqtop) would be appreciated.)

-Jason

On Apr 24, 2014 11:47 PM, "Abhishek Anand" <abhishek.anand.iitg AT gmail.com> wrote:

I'm having a strange issue with the simpl tactic.

I have a function (Say f) defined using the Fixpoint keyword.

When f is defined outside any section, simpl happily reduces

f whenever the  structure of its recursive argument is known.

As soon as I move f into a section

where some of its arguments 

become section variables, simpl stops reducing f in

*other* sections even

when the  structure of its recursive argument is known.

I can unfold f, and then successfully do simpl. However, that leaves a 

large fix _expression_ after the reduction step.

I cannot reproduce this problem on a small enough example.

In all of the toy examples I tried to write, simpl works just fine.

 

Does someone know what could be going wrong?

I can share the source files required to reproduce the issue

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/