Coq (Rocq) and Other Proof Assistants in Org Mode

Emacs
1

Hi! My name is Danny, this is my first time starting a thread in the System Crafters forum. I am starting to try org-babel, and one of my intentions is to use it to learn how to write mechanized proofs, with Coq (or Rocq Prover, as it is now renamed). Currently I am stuck at setting up org-babel + coq; as I browse along the way, it seems that the org-babel support for Coq has become incomplete.

I wish to use this thread to keep track of the status of coq (rocq) support in org babel, and also to seek advice on integrating proof assistants in general with org mode. Any suggestion on using proof assistants, learning type theory, or setting up org-mode + a proof assistant is greatly appreciated. Thanks in advance! If this is rather vague, please ask me to be more specific.

Also, I should mention that I have not systematically studied type theory, and have only begun playing with Coq since yesterday.

1 Like
2

Hello @ANoobyBird, and welcome to the wonderful world of starting discussions. Not an easy feat, congratulations[1].

As I’m not a coq user, but an org-babel user, I wonder how you would use ob-coq. How would an Org-mode file look like in this case? Do you need :session or :noweb support? How should the resulting export look like?

  1. I’m well aware that this sounds like sarcasm, but it isn’t, it’s genuine. It took me ~400 answers till I finally felt comfortable/brave enough to ask a single question on StackOverflow. ↩︎

3

Hi, @ashraz ! Thank you for the warm welcome, it really lifted the invisible weight which was usually there when I interact with people. :laughing:

Do you need :session or :noweb support?

Um, actually I only began to use both coq and babel the day before yesterday, so I apologize for any misconceptions. Right now I am assuming, or going on with the impression, that:

  1. ob-<lang-identifier> is the file org-babel looks for when trying to evaluate a source block written in <lang-identifier>;
  2. :session: and :noweb are separate ways to keep objects defined or states updated in different blocks in sync; in particular, sessions seem to genuinely maintain global states by creating separate processes of some kind, but noweb seems to be doing simple replacements of text. So I think right now, conceptually, I prefer sessions.

With these impressions, I think you do need heavy amounts of sessions when hypothetically using a complete ob-coq in order to maintain the types you’ve constructed. AFAIK, with proof assistants like coq, a theorem is internally a particular type, and proofs are internally members or terms of that type, so it should be safe to say that the checking of proof correctness is essentially type checking. And there is a lot of types and proofs to be “remembered” when you nest stuff in different code blocks, so yeah, one would need session support for ob-coq. By very briefly glancing through the comments in the related repositories, I believe that to maintain such sessions is what coq-inferior (in the old ob-coq) and inf-coq.el (in the new ob-coq) are for.

How should the resulting export look like?

For simple evaluations, say Check nat. (which tells coq to print the definition of the type of natural numbers), the results would ideally look something like this:

#+RESULTS:
: Inductive nat : Set := O : nat | S : nat -> nat

Though I haven’t yet learned how to do more complicated stuff in coq, I believe that the results emitted should be similar in nature, as it all amounts to type checking in the end. And the :session should quickly come in handy when you define types upon types upon types.

So in a way, I guess things should look quite similar to:

#+BEGIN_SRC python :session :result output
  type("string")
#+END_SRC

#+RESULTS:
: <class 'str'>
4

Addendum regarding

How would an Org-mode file look like in this case?

and

How should the resulting export look like?

After glancing through a section of Coq documentation (here for Coq 8.18.0, and here for Rocq 9.0.0) and playing with the Coq repl (rocq top in shell) a bit, I feel the need to add the following:

Certain aspects of the Coq repl appear to be unique to Coq, in that one can enter the proof mode by using the Proof. command, and exit the proof mode by entering the Qed. command. And the proof mode itself has “proof states”. This behavior seems to be what makes Coq interactive, and could be the harder part for org-mode and a hypothetical ob-coq to emulate.

Fortunately, according to the docs, going through a proof mode is not the only way to construct and verify proofs in Coq, instead one can just feed Coq an entire proof term and ask it to check the correctness for you. I think that, for a hypothetical ob-coq, feeding an entire proof term in a coq source block and evaluating the result is the more fundamental feature, and the more feasible thing to do. The interactive proof mode somehow embedded in org-mode would be a nice bonus, but may not be necessary.

I am still learning very slowly how to write proofs using Coq, and may append pieces of information if they appear to be related to some implementation of, or the ideal ob-coq. :grinning_face:

Also, in case this becomes useful to others, when using Emacs but not using org-mode in particular, a good way of interacting with Coq and other proof assistants is the package Proof General.

In Proof General or the CoqIDE, one can just type in an entire chunk:

Theorem true_is_true: True.
Proof.
  exact I.
Qed.

(example extracted from Ilya Sergey’s coq tutorial.)

and evaluate this, which enters and then exits the proof mode. There seems to be no output if the proof is correct, and complaints if there are errors. So actually, there is no extra difficulty to enter and exit proof mode in org-mode as long as it is all wrapped up in an entire chunk and evaluated as a whole. Excuse me for the frequent edits to make the phrasing more accurate.

5

Hi! This is a minor update.

  • I tried the new ob-coq using straight.el with the following recipe '(:type git :host github :repo "sp1ff/ob-coq"), which does install it but with some warnings. After that, applying C-c C-c on a Coq source block no longer make Emacs complain that it cannot find ob-coq, but the new complaint seems to be from the new ob-coq itself, informing me that “Parsing Coq output as values not supported, yet”, even though I have set the header to be :session :result output. The next step would be to look into this. (This could indicate something wrong with the repo itself, but could also be how I installed it.)
  • The new ob-coq repo does not support Rocq 9.0.0, but only older versions like Coq 8.18.0. It looks for the command coqtop for processing Coq source blocks, not rocq top.
  • Also, to correct a huge mistake in one of my previous replies: Check nat. does not ask for the definition of nat, but for the type of nat (which is Set); instead, Print nat. does ask for the definition.

OK, so I did more looking up, found out that I can debug a function using debug-on-entry, and applied this to ob-coq-evaluate (in the ob-coq repos). Based on the backtrace which I do not fully understand, I suspected that the problem lies with the handling of header arguments. By luck I changed :result output to :results output, and then the coq block evaluation produced the desired results. Then I applied the debug function to the evaluation of other source blocks and found out that indeed it is :results which changes the result type, not :result. That I should put :results instead of :result is the whole point here :rofl:. Though this is a stupid mistake, I think I have learned a lot through the process. Maybe now I understand how babel works a bit more.

The conclusion so far is that you can set up the new ob-coq as long as you restrict yourself to certain kinds of results and pay attention to its requirements. Of course I hope that the features of this package be gradually enriched.

Finally, @ashraz , if you’d like to know, I would like to share with you the result produced by a minimal theorem proving:

#+BEGIN_SRC coq :session :results output
  Theorem true_is_true: True.
  Proof.
    exact I.
  Qed.
#+END_SRC

#+RESULTS:
: 1 goal
:   
:   ============================
:   True
: 
: No more goals.

I think that similar results are displayed if you feed it an incomplete proof, or more complicated theorems and proofs, in that it informs you of your current proof state (if I am using this terminology correctly) if you enter (and later exit, or not) the proof mode. I may be speaking too soon about many things, though, having only barely set up the environment just now and not grown familiar with everything involved.

6

That’s exactly why I asked about your org-mode file, e.g. input and expected output. Glad that you worked it out on your own :slight_smile:

7

Thank you :smiley: knowing myself, I really would have lingered on and on speculating instead of actually doing, were it not for your prompt.