coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq Proof Assistant Question

From: Tej Chajed <tchajed AT mit.edu>
To: coq-club <coq-club AT inria.fr>
Cc: "Dr. Damian Dechev" <dechev AT cs.ucf.edu>
Subject: Re: [Coq-Club] Coq Proof Assistant Question
Date: Tue, 9 Aug 2016 12:27:07 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tchajed AT mit.edu; spf=Pass smtp.mailfrom=tchajed AT mit.edu; spf=None smtp.helo=postmaster AT dmz-mailsec-scanner-1.mit.edu
Ironport-phdr: 9a23:3FVaURSuZcPSUTmCqEuOAhdJZ9psv+yvbD5Q0YIujvd0So/mwa64bBSN2/xhgRfzUJnB7Loc0qyN4vmmATVLucjJ8ChbNscdD1ld0YRetjdjKfbNMVf8Iv/uYn5yN+V5f3ghwUuGN1NIEt31fVzYry76xzcTHhLiKVg9fbytScbshsi6n9q/54fUK10RwmHsOPUqdV7u802R7pBQ2to6bP5pi1PgmThhQ6xu32RmJFaezV7Xx/yb29pdyRlWoO8r7MVaUK/3LOwSRL1cCyk6YShuvJW4/TGKdwaE52MdX2MKiVIIRlGdtFCpFqv25yD9r6923DSQdZn9SqlxUjC/5Y9qTgXpgWEJLWhq3nvQj5lMgaATixKopRFzi9rIa4GcNvdyVqbcYZUXSXcXDZUZbDBIHo7pN9hHNOEGJ+sN6tCl/1Y=

Hi Christina,

In your example it looks like all you need is unfold program1.

Note though that if you run simpl on your original goal it computes everything to 1 = 1. Even if head were not computable (you can test this with the command Opaque head) you get head 0 [1; 2; 3; 4] = 1, which seems like what you wanted.

Best,
Tej

On Tue, Aug 9, 2016 at 11:31 AM, Christina Peterson <clp8199 AT knights.ucf.edu> wrote:

Hello,

I am working with a record in the Coq Proof Assistant and would like to be able to access and display elements of the record in the proof environment so that I can apply formal logic to them. I have attached the file Example.v which is a simple reproducible example of the problem.

Sincerely,

Christina

[Coq-Club] Coq Proof Assistant Question, Christina Peterson, 08/09/2016
- Re: [Coq-Club] Coq Proof Assistant Question, Asya Bergal, 08/09/2016
- Re: [Coq-Club] Coq Proof Assistant Question, Tej Chajed, 08/09/2016