# Coq Proof Script Visualiser

Copyright 2019-2020 Mario Frank mario.frank@uni-potsdam.de

## Project Members

• Mario Frank - Developer and maintainer.
• Sebastian Böhne - Tool idea/concept and advice (e.g. functionality and layout of the output).

## Synopsis

This tool provides the functionality to visualise Coq proof scripts in a form that is understandable without using Coq.
It currently should be seen as a proof-of-concept and is in an early beta phase (version number 0.5).
So, errors may occur. If you have technical difficulties or just want to give feedback, do not hesitate to contact me.
If you stumble over an exception that states that you should report the error to the Coq bug tracker,
please report it to me as the error will probably be on my side and not on the Coq side.
The error messages are generated by Coq functionality and thus point to the Coq resources.
I will hopefully get that corrected, soon.

Status of Coq support:

• Coq version 8.11 : Currently unsupported due to significant changes in Coq-internal data structures. We are working on it!
• Coq version 8.10 : Supported
• Coq version < 8.10 : Unsupported, definitely not working.

Supported output Formats are:

• LaTeX proof table (cmd-line-option -t latex-table)
• Complete LaTeX document (cmd-line-option -t latex)
• PDF (cmd-line-option -t pdf)

## 1.1 Dependencies

Coq-psv has the following dependencies

• opam at least 2.0
• Coq 8.10
• ocaml at least 4.02 and above
• dune at least 1.6.0

## 1.2 Preparation

In order to install coq-psv, you need the current version of coq, i.e. coq 8.10.

You can install coq with

opam install coq.8.10.0

Those who wish to work with coqide, have to install it with

opam install coqide.8.10.0

Nevertheless, coq-psv does not need nor use coqide.

After the installation of coq is finished, you can go on to the installation of coq-psv.

## 1.3 From our Opam Repository

If you want to have it as easy as possible, add our opam repository on the command line with

opam repo add up_cs_thi_soft https://www.cs.uni-potsdam.de/~mafrank/public/opam/

and install coq-psv with

opam install coq-psv

### 1.4 From source

If you want to install this plugin from source, you first have to compile it. The source code will be published in the near future but is already provided when the tool is installed from the opam repository.

For the compilation, you have to make sure that dune is installed. If it is not, call

opam install dune

on the command line.

Then, you can compile coq-psv being in the root directory of the package with

dune build

and install it with

dune install

## 2 Usage

After successful installation, the program coq_psv is available. And you can use both the tool and its output.

First, we will describe the supported command line options and then, the way, you can use the tool and its output.

## 2.1 Command Line Options

The tool supports the usual options as coqtop does. Additionally, we provide the following options:

Output file options:

• -t <fmt> : Defines the output file format.
• latex-table : Only the LaTeX table is generated. This option is useful if you want to include the generated file into an existing document.
• latex : A complete standalone LaTeX document is generated (default).
• pdf : A complete standalone LaTeX document and the respective PDF are generated.
• -out-fmt <fmt> : (idem)
• -generate-stub-files : Defines that for every input file, an output file should be generated, even if it does not contain proofs. The default behaviour is to ignore files without proofs.
• -one-file-per-proof : If this flag is set, a separate output file File_proof_name.tex will be generated for each proof in the file File.v

Output file content options:

• -psit-style <style> : Sets the proof situation (hyps and goal(s)) column
• coq : The proof situation as is shown as frac as in Coq. (default) Invariant hypotheses are hidden by default.
• sequent : The proof situation is shown as in sequent calculus style. Invariant hypotheses are shown by default.
• -hide-inv-hyps [yes|no] : Defines whether invariant hypotheses shall be hidden in output.
• -hide-branch-psits : If this flag is set, the proof situations resulting from a tactic are not printed in the step of a tactic if they are handled by bullets later on. However, Each bullet has it’s proof situation in it’s proof situation column.
• -show-all-sequence-psits : Defines that, if a tactic is applied in a situation with multiple proof situations (Sequence node), all proof situations should be shown. The default is to show only the first and note, how many exist additionally.

General options:

• -v : Print the coq_psv version and exit
• --version : (idem)
• -print-version : Print coq_psv version in easy to parse format and exit. The format is psv-version Coq-version Ocaml-version.
• -h : Print this list of options
• -help : (idem)
• --help : (idem)

## 2.2 Extracting Proofs From one Coq File

To extract all proofs from file numbers.v, you can for example call

coq_psv -l numbers.v 

which will generate the file numbers.tex

Note that this mode currently only works if the numbers.v only imports modules from the Coq library or already compiled. In other cases, the project extraction mode should be used (as described in the following subsection).

## 2.3 Extracting Proofs From Complete Coq Projects

To enable coq-psv to process complete Coq projects, you currently have to add the following lines to the CoqMakefile.in template provided by Coq. This file can be found in your opam directory, which is usually in your home directory. The usual location of the template is

~/.opam/default/lib/coq/tools/CoqMakefile.in

COQPSV   ?= "$(COQBIN)coq_psv" to the section annotated with # Coq binaries Also, you have to replace the lines $(VOFILES): %.vo: %.v
$(SHOW)COQC$<
$(HIDE)$(TIMER) $(COQC)$(COQDEBUG) $(TIMING_ARG)$(COQFLAGS) $(COQLIBS)$< $(TIMING_EXTRA) with $(VOFILES): %.vo: %.v
$(SHOW)COQPSV$<
$(HIDE)$(TIMER) $(COQPSV)$(COQFLAGS) $(COQLIBS)$(COQPSVOPTS) -l $<$(SHOW)COQC $<$(HIDE)$(TIMER)$(COQC) $(COQDEBUG)$(TIMING_ARG) $(COQFLAGS)$(COQLIBS) $<$(TIMING_EXTRA) 

Furthermore, you need a _CoqProject file for your project. You then first have to generate the Makefile for processing your project with

coq_makefile -o CoqMakefile _CoqProject

You also should clean your project with

make -f CoqMakefile clean

After that, you can start the processing of your project with

make -f CoqMakefile COQPSVOPTS="-hide-branch-psits -one-file-per-proof"

which will generate the proof table files in the directories where the referenced Coq files are located. For other options, please refer to the command line options.

## 2.4 Using the Output Files

To include the generated LaTeX files, make sure that you define at least

\usepackage{tabularx} % general table support
\usepackage[mathletters]{ucs} % UTF8 symbol support
\usepackage[utf8x]{inputenc} % UTF8 symbol support
\usepackage{unicode} % UTF8 symbol support
\usepackage{multirow} % support of multirows in tables
\usepackage{longtable, array} % Support for multipage-tables

If you generated the file numbers_my_proof.tex, you can input this file in your own LaTeX document with

\input{numbers_my_proof.tex}

In your document, you can reference the proof with

\ref{Proofs:numbers:Theorem:my-theorem-name}

Please note that the name of the input file and theorem are not allowed to have underscores in the label. Thus, underscores are replaced by minus symbols.

All generated LaTeX files use default table and cell spaces.

You can override the following commands for spacing and widths:

• \stepcolwidth The width of the justification/Coq step column (default is set to 20 % of the table width)
• \rulewidth The width of the rule in frac/default style (default is set to 100% of the cell text width)
• \rulethickness The thickness of the rule in frac/default style (default is set to 0.2 mm)


## 2.5 Example output files

We provide some example output files for a non-trivial proof in Coq as PDF files. The layout is far from being perfect and a small calculation bug currently leads to the command in Coq not always being centered.

The provided example files visualise the proof of the theorem: for all two lists of naturals L and K: If both lists are strictly ordered and both are "subsets" of each other, then they are identical.

## 3 Future Work

There are many possible improvements which includes

• HTML support
• Support for modules in Coq files (They are processed already but the generated labels do not respect them, so proofs with the same name being in the same file currently have the same label )
• Layout improvements
• Integration into Coq/coqdoc

## 4 Papers and Technical Reports

• Chris Dams for providing a standalone Coq file as test case for proof information extraction.