coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] ProofObject and Definitions

From: Benoît Viguier <beviguier AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] ProofObject and Definitions
Date: Sun, 16 Jul 2017 06:55:53 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=beviguier AT gmail.com; spf=Pass smtp.mailfrom=beviguier AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f182.google.com
Ironport-phdr: 9a23:aLINHhSmQ/cbLLWUomYTKysH8Npsv+yvbD5Q0YIujvd0So/mwa69YhyN2/xhgRfzUJnB7Loc0qyN4v+mATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSijewZbF/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/n/XhMJtj6xVrhyuqBNjzIPPb4GZKOBzcKTBcd4UR2dMWNtaWSxbAoO7aosCF/cMMvher4n6qUMOsQOxCgatBOPg1z9Ih2H53bcn2OkmCg7JwhIgH9MBsHTJrdX6Kr0SXPu6zKnN1zrDbvdW1S3h54jPdxAsuPeBVq9+f8rWzEkgDQLFjlOIpIz7PjOV2fkNs2mF4Op6T+6vjWonpgdsqTas3schkpfFip4Rx1ze9ih0wJw5KcOlREN6e9KoDZhduz+CO4drTc4vTHtktDsnxrAFo5K3YicHxZU9yxLCZPGLbY6F6Q/5WumLOzd3nndldaq/hxms9UigzfXxVsyu31ZLqipJi8DMtmwR2xDK5MiLV/hw8lm71TaA0ADT7e5EIUQqmqbBN5EhxbswmoISsUTFACD2hF37gLGKekgg4OSl6OTqbq/4qpOBNoJ4kBzyP6cwlsCnBOQ3KAkOX2yV+eSm073j+FX0T65Ugf0ok6nZv43aJcUFqa6jGAJV3YMj5Ay+DzeiytgXgX4HLFdddBKdk4fpI03OIOz/Dfqnn1usly5ry+naMb3lH5XCNWPOkKzhfLZ4805T0hA/zdFZ55JOC7EOOuj/WkHrtI+QMhhsOAuthu3jFd9V14UEWGvJDLXKHrnVtAqi6+QopfW7Wo4apTfwMbBx7fPwjHAkmFIHVaas1JoTLnu/G6I1cA2ifXPwj4JZQi8xtQ0kQbmyhQ==

Dear Coq-club

If we have :
Lemma answer : answer(Q) = 42.
Proof.
apply Answer_to_the_Ultimate_Question_of_Life_the_Universe_and_Everything.
Qed.
And then do:
Print answer.
We get a proof object that we can use to rebuild the proof and lemma:
Definition answer := fun x => blablabla.

My problem is as follow. When I do the Print answer I get a really big ProofObject (nothing wrong with that) but when I want to use that proof object to directly feed it into another definition, I get the following error:

Syntax error: [constr:lconstr] expected after ':' (in [constr:open_binders]).

This is due to in the line that some "..." that appeared. A few lines later I also have this chunk of code :

   (fun e : ℕ =>
     match ... with
     | ... False
     | ... False
     | ... False
     | ... False
     | ... False
     | ... False
     | ... False
     | ... True
     | ... False
     end) I 16%nat Ha'7

Which I'm pretty sure won't be parsed (this does not look like correct Galina).

How can I make sure that the proof term that I get will be correct (The proof term is 20 000 character long) ?
Or in other word how to print the full Proof Object ?

----------------------------------------------------------------------------------------------------------------------------------------

The motivation of this approach is as follow :

All the 'apply/eapply', 'repeat', 'match' are building the proof term. But finding the right lemma with eauto etc is long and slow.
The time to typecheck a Proof with the QED is decently faster.

Thus what about using the proofobject directly as a definition and skip the whole "building proof via tactial" step
and feed it to the typechecker.

-- 
Kind regards,

Benoît Viguier
Software Engineer - PhD Student | Cryptography & Formal Methods
Radboud University | Mercator 1, room 03.17, Toernooiveld 212
6525 EC Nijmegen, the Netherlands | www.viguier.nl

--------------------------------------------------------------------------
This message (and any attachments) is intended solely for the addressee(s)
and may contain confidential information. If you are not the addressee, do
not copy this message (and any attachments), forward or share this message
with third parties. You are requested to notify the sender immediately and
delete this message.

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] ProofObject and Definitions, Benoît Viguier, 07/16/2017
- Re: [Coq-Club] ProofObject and Definitions, Pierre Courtieu, 07/16/2017