coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.0cat MyFile.v | coqtopworks like a charm (so does running it in proof general)but then coqc MyFile.v fails withFile "./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 systemIs 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
- [Coq-Club] coqc and coqtop differ in what they can prove., Alexandre Pilkiewicz, 11/20/2016
- Re: [Coq-Club] coqc and coqtop differ in what they can prove., Alexandre Pilkiewicz, 11/20/2016
- Re: [Coq-Club] coqc and coqtop differ in what they can prove., Jonathan Leivent, 11/20/2016
- Re: [Coq-Club] coqc and coqtop differ in what they can prove., Alexandre Pilkiewicz, 11/20/2016
Archive powered by MHonArc 2.6.18.