coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] body is hidden -- why and how to reveal it?

From: Dmitry Grebeniuk <gdsfh1 AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] body is hidden -- why and how to reveal it?
Date: Thu, 1 Aug 2013 14:44:56 +0300

Hello.

I'm trying to write and prove some code about files and buffers (I
need some special buffering in OCaml code), but I failed to write
bugless imperative code. But I want to stick with imperative features
now. So I'm going to prove code in Coq and then translate it manually
to OCaml.

My code: https://gist.github.com/gdsfh/74ac36c8f8dbf46d2373 (it's
lame, but I want to check will it work at all, and only then I'll add
glamour).

My current problem is: definition of ba', added with "refine (let
ba' := <body> in _)", appears in hypotheses just as "ba' : array", the
body is hidden, but the body is required to prove current goal.

I've tried to ask for help in #coq irc, but without any success.

Two questions:

1. Why the body is hidden?

2. How to "reveal" it? I suspect I need to change the way I introduce
ba', but I can't find the correct way to do it.

[Coq-Club] body is hidden -- why and how to reveal it?, Dmitry Grebeniuk, 08/01/2013
- Re: [Coq-Club] body is hidden -- why and how to reveal it?, Stéphane Glondu, 08/01/2013
  - Re: [Coq-Club] body is hidden -- why and how to reveal it?, Dmitry Grebeniuk, 08/01/2013
    - Re: [Coq-Club] body is hidden -- why and how to reveal it?, Arnaud Spiwack, 08/02/2013