Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] coqc and coqtop differ in what they can prove.

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] coqc and coqtop differ in what they can prove.


Chronological Thread 
  • From: Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] coqc and coqtop differ in what they can prove.
  • Date: Sun, 20 Nov 2016 20:36:44 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=dapilki AT gmail.com; spf=Pass smtp.mailfrom=dapilki AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f44.google.com
  • Ironport-phdr: 9a23:qi21IBexLSMI/Q6/3FHfZCqmlGMj4u6mDksu8pMizoh2WeGdxc65ZR7h7PlgxGXEQZ/co6odzbGH6Oa6AydZuMfJ8ChbNscTB1ld0YRetjdjKfDGIHWzFOTtYS0+EZYKf35e1Fb/D3JoHt3jbUbZuHy44G1aMBz+MQ1oOra9QdaK3Iyfntq/8JzLYghOmCH1IfYrdE33/k3tsZw9hpIqAaIswFOdqXxRPu9S2GlAJFSJnh+66N3mr7B59CEFkvYs58dGXb/3N5w5Sb9ZASsnOHJ9sMTvuAnKSweV6z0EU2EVkxdXAgPXxAn9WobtvyD6sOtkxSTcOtf5G+NnEQ++5rtmHUe7wBwMMCQ0pSSO0pR9

After figuring it out that I can print goals with Print. and fail right after, I found out the difference.
The tactic
autounfold with autounfold in *.
does less unfolding in coqc. In particular, it does not unfold in coqc (but does in coqtop) a function defined like this:

Definition Pol_In v (pol: Polyhedron) :=
  list_forall (satisfy_constraint v) pol.

I manually unfold it and the proof now passes in both, but it still is quite weird.

Alex

On Sun, Nov 20, 2016 at 8:09 PM, Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org> wrote:
All,

I am fixing an old Coq development, and I'm hitting a snag: one file compiles fine in coqtop but fails with coqc, and I don't understand why, nor do I know how to debug.

coqc --version and coqtop --version return the same thing.

The Coq Proof Assistant, version 8.5pl3 (November 2016)
compiled on Nov 19 2016 16:24:18 with OCaml 4.03.0

cat MyFile.v | coqtop
works like a charm (so does running it in proof general)

but then coqc MyFile.v fails with

File "./MyFile.v", line 161, characters 2-5:
In nested Ltac calls to "lia" and "xlia", last call failed.
Error: Tactic failure:  Cannot find witness.

If I replace lia with omega, it still works with coqtop, still fails with coqc, so it's not just a lia issue.

Error: Omega can't solve this system

Is this a common thing (maybe they use different environment variables or something)?

Is there a way to ask coqc to tell me what is the current state of the goal (-verbose does not help)

Thanks in advance!

Alex






Archive powered by MHonArc 2.6.18.

Top of Page