coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- 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?, Stéphane Glondu, 08/01/2013
Archive powered by MHonArc 2.6.18.