Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Using ltac:(admit) to define terms.

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Using ltac:(admit) to define terms.


Chronological Thread 
  • From: Jonathan Leivent <jonikelee AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Using ltac:(admit) to define terms.
  • Date: Mon, 11 Jul 2016 14:20:39 -0400
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f170.google.com
  • Ironport-phdr: 9a23:io8+Mx+7q039mP9uRHKM819IXTAuvvDOBiVQ1KB90OkcTK2v8tzYMVDF4r011RmSDN2dsK8P1LSempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47AblHf6ke/8SQVUk2mc1EkfqKuR8WN0Yye7KObw9XreQJGhT6wM/tZDS6dikHvjPQQmpZoMa0ryxHE8TNicuVSwn50dxrIx06vrpT4wJk2+CNJ/vkl6sRoUKPgfq1+Q6YLIi4hNjUX48viqRnKS0Or63oCX2MK2k5KBA7E7xz+U5rZvS7zt+470y6fa56lBYsoUCivuv84ACTjjz0KYmY0



On 07/11/2016 02:07 PM, Jonathan Leivent wrote:
I think the point of the new way admit works is that there is no way to make

Definition exercise : nat := ltac:(admit).
work via direct usage of admit - because the result would be Defined instead of just Admitted. However, the error about not being able to infer an existential variable of type "nat" happens earlier than that - which means that any way of fixing that error will just run afoul of the Defined/Admitted issue.

BTW: if you do the following, you bypass the can't infer error and get the Defined/Admitted one:

Definition exercise : nat := ltac:(abstract admit).

Error: Attempt to save a proof with given up goals. If this is really what you want to do, use Admitted in place of
Qed. (in proof anonymous_subproof)

This is because admit is now a synonym for the give_up tactic.

FYI: many bikes were shed on coqdev over whether to do it this way or not ;-)

-- Jonathan


To get around this, you will have to define something that is Admitted or itself an axiom, then use that - which is IMHO what the new rules about admit are trying to force you to do - declare your intentions to leave something undefined instead of relying on the standard library to hide those intentions for you.

-- Jonathan


On 07/11/2016 01:53 PM, Arthur Azevedo de Amorim wrote:
Dear list,

In the Software Foundations textbook, we define an "admit" axiom that we
use to leave out parts of definitions in exercises:

Axiom admit : forall {T : Type}, T.
(* Replace "admit" with answer here *)
Definition exercise : nat := admit.

We were wondering whether we could remove this definition in favor of just
using ltac:(admit). Unfortunately, this causes Coq to complain about
existential variables:

Definition exercise : nat := ltac:(admit).
Toplevel input, characters 0-39:
Error: Cannot infer an existential variable of type "nat".
Is there anyway of making this work?






Archive powered by MHonArc 2.6.18.

Top of Page