gds (gds) wrote,

coq, reversed lists

Взял несложную (как казалось) задачку, потыкал в неё палочкой, отчаялся, дошёл до #coq irc, изложил проблему, но не помогли. Зато теперь есть изложение этой проблемы:

[14:19] == gdsfh [1f1f0ba0@gateway/web/freenode/ip.] has joined #coq
[14:38] <gdsfh> Hello. I'm learning coq (already can prove simple things with tactics and sometimes even with direct proof construction), but I'm trying to make something closer to practice.
[14:38] <gdsfh> I've took as example the task that requires compile-time elimination of Prop-typed values to generate some ocaml code, but failed.
[14:39] <gdsfh> I don't know whether my code has any sence at all, so I'll be glad to hear any critique (including notes about my dumbness).
[14:39] <gdsfh> I'm trying to use the "reverted" property of lists in compile-time only, and then I want to generate code that uses only List.rev_map, List.rev, List.rev_append to work with lists.
[14:39] <gdsfh> (the practical part of this task is the exclusion of non-tail-rec functions in some pieces of code; btw I know about extlib/batteries for real tasks, it's just a toy example.)
[14:39] <gdsfh> The code is: , I'm trying to get rid of runtime manipulations with type "dir", but when I'm declaring it to be in Prop (line 3), the function "to_list" (line 75) becomes unacceptable, since I'm trying to destruct "dir" to produce "real values" (of type Set, I guess).
[14:39] <gdsfh> When the code uses "dir : Set", the extracted ocaml source has runtime work with "dir".
[14:40] <gdsfh> What should I do to solve similar problems (with compile-time propagation of values)? Is it possible at all?
[14:50] <vsiles> gdsfh: if I got it right, you want to_list to take a listr d and build a regular list depending on d ?
[14:51] <gdsfh> vsiles: yes!
[14:52] <vsiles> so you expect Coq to do some magic and get completely rid of d in the extracted code ?
[14:53] <gdsfh> vsiles: yes, maybe. Some things Coq can eliminate (proofs, for example), so maybe I can somehow tell Coq to eliminate "d". But maybe it's impossible. I'm newbie, I don't know.
[14:55] <vsiles> d is not a proof
[14:55] <vsiles> it can't be
[14:55] <vsiles> it has computational content
[14:57] <vsiles> you can't hide "if b then do foo1 else do foo2"
[14:57] <gdsfh> yes, it has. so, this task (work with listr and then converting them to regular list, in compile-time) is impossible?
[14:58] <gdsfh> i've heard that dependent types can be used to do some metaprogramming (here -- converting listr_functions to List.functions).
[14:59] <vsiles> hmmm I start to understand what you want to do
[14:59] <vsiles> I'm not sure this is possible in ocaml
[15:00] <vsiles> maybe with phantom types...
[15:00] <vsiles> sgnb: ^^^^ any idea ?
[15:00] <gdsfh> I know about ocaml's limitations very well, so that's why I'm trying to use Coq.
[15:01] <gdsfh> phantom types are good in the ocaml itself, but here they won't help, anyway I'll need some "dir" in runtime. (I'm thinking so.)
[15:02] <vsiles> you can't expect Coq to extract some code that you can't yourself
[15:02] <vsiles> I mean, if it's not posible in ocaml
[15:02] <vsiles> coq won't make it magically possible
[15:04] <gdsfh> but maybe I'll can prove with Coq that the whole work with "listr" gives a list in Forward order (and maybe this will require the last result's reversal), and Coq just generate the code based on List.rev*, dropping "d" (since I proved that last list has Forw direction).
[15:05] <gdsfh> I don't know what Coq can and what can't, that's why I'm asking for your help.
[15:06] <vsiles> sorry, can't help you with that, it's not my speciality :)
[15:07] <gdsfh> vsiles: ok, no problem. this is not so easy question (it is not described in popular manuals), and not every coq professional should know about these things.

Может, у вас будут идеи?

Подсказали. Definition my_list_rev_mapped := Eval compute in предыдущее_определение. И всё, что оно может, оно вычисляет в compile time. Как же мне это нравится!
  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded