Showing proof context

[tbelaire]

Hi, this is an idea I've had to use peacoq's existing work to generate annotated coq files to get things like

http://homes.cs.washington.edu/~jrw12/dep-destruct.html

where you can mouse over the proof in the post and read it.

Long term idea is to get that working on some sort of pastebin.

(*begin code *)
    Require Import Program.
(*context
  y : Fin 2
  ============================
   bool_to_Fin_2 (Fin_2_to_bool y) = y

<hr />
    dependent destruction y.

<hr />
  ============================
   bool_to_Fin_2 (Fin_2_to_bool (F1 1)) = F1 1

subgoal 2 (ID 140) is:
 bool_to_Fin_2 (Fin_2_to_bool (FS 1 y)) = FS 1 y
*)
    dependent destruction y.

Generating the *context sections automatically.

I'm just poking around, but if you have any ideas, that would be great.

[Ptival]

Sounds like a pretty good idea. I could see it work in two ways:

• one would be to just have the contexts statically. with the way the editor works now, this should be fairly simple, as you can already move your cursor around to see goals at different points in time.
• one would be to use something like jscoq to actually have dynamic code that you could alter and run. It would be a bit more work.

[tbelaire]

The problem I was aiming at was making it nicer to post problems in the irc channel and have people follow the proof state without needing to copy it to their local disk first. It would also be awesome for blogging about coq.

I'm leaning towards just statically generating the contexts by using peacoq as a library and just having a little command line tool step through the file, feeding it piece by piece to coqtop and recording the results.