adelon/naproche-zf

Experimental natural theorem prover with a controlled natural language as input language and proof automation powered by automated theorem provers

Naproche/ZF

Naproche/ZF is an experimental proof assistant based on set theory (and classical logic). It uses a controlled language embedded into subset of LaTeX as input format, supporting literate formalization.

Example

\begin{theorem}[Cantor]\label{cantor}
    There exists no surjection from $A$ to $\pow{A}$.
\end{theorem}
\begin{proof}
    Suppose not.
    Consider a surjection $f$ from $A$ to $\pow{A}$.
    Let $B = \{a \in A \mid a\notin f(a)\}$.
    Then $B\in\pow{A}$.
    Take an element $a'$ of $A$ such that $f(a') = B$ by \cref{surj}.
    Now $a' \in B$ iff $a' \notin f(a') = B$.
    Contradiction.
\end{proof}

Development

Prerequisites

We rely on automated theorem provers like Vampire and E to discharge proof tasks.

Obtaining Vampire

The default prover is Vampire and the included library is written against a specific release of Vampire. Currently the library uses Vampire 4.7.

On non-Linux platforms you may need to install Vampire by compiling from source. Download the source code release and follow the instructions in Vampire’s README.md and make sure that the resulting binary is available as vampire on your $PATH. If you have multiple versions of Vampire installed, you can export the $NAPROCHE_VAMPIRE environment variable to choose a specific version, e.g. by adding

export NAPROCHE_VAMPIRE="/absolute/path/to/vampire_4.7"

to your shell configuration.

Obtaining E

You can usually install a reasonably up-to-date version of E via your system’s package manager (e.g. via apt-get install eprover on Ubuntu and brew install eprover on macOS). Alternatively, you can build E from source. By default whichever eprover is on your $PATH will be used, but you can override the default executable using the NAPROCHE_EPROVER environment variable.

Building

This project uses Stack to manage Haskell libraries and GHC. You can install Stack and other Haskell tooling using GHCup. Follow the GHCup install instructions and then use ghcup tui to install Stack. Stack should install the correct GHC version when you first try to build the software. You can also use GHCup to install the Haskell Language Server, which enables IDE features in some text editors. For VS Code you also need to install the Haskell extension.

You can build the project using stack build in the root directory of this project.

Supported platforms are Linux x86-64 and macOS AArch64/x86-64. Support for Windows is currently untested, but using WSL2 may work.

Checking individual files

After running stack build you can run the program with stack exec zf -- <FILENAME> in the root directory of this project. The double hyphens -- separate the arguments of stack from the arguments of the proof checker. Here's an example invocation:

stack exec zf -- library/set.tex --log --uncached

For a list of all options run stack exec zf -- --help.

Checking the entire standard library

Run make lib to check the file library/everything.tex.

Compiling the PDF of the standard library

cd latex && xelatex stdlib.tex

Setting up other formalization environments

When looking for imported files, the following list of base directories is considered (in descending priority):

• the current working directory in the command line
• the user library directory, set with the environment variable NAPROCHE_LIB, defaulting to ~/formalizations
• the source code library directory, set with the environment variable NAPROCHE_SCR_LIB, defaulting to ~/code/zf/library
• the source code examples directory, set with the environment variable NAPROCHE_SCR_EXAMPLES, defaulting to ~/code/zf/examples

Running the tests

There are a few golden tests that compare the output of the program to previously accepted output. You can run the tests with stack test, which will fail if the output differs from the existing golden files. Run

make test

or, equivalently

stack test --test-arguments "--accept"

to update the golden files.

Building Haskell documentation

Running stack haddock will build the project together with its documentation, placing the rendered HTML files into haddocks/.

Profiling

The following makes sure that stack uses a dedicated directory to cache the profiled version of all dependencies. Otherwise switching between profiled and unprofiled builds will cause lots of recompilation.

stack --work-dir .stack-work-profile --profile build

Basic time profiling:

stack --work-dir .stack-work-profile exec --profile zf -- library/ordinal.tex --uncached +RTS -p

If you have ghc-prof-flamegraph installed (e.g. after running cabal install ghc-prof-flamegraph), you can generate an interactive zf.prof.svg from the .prof file by running the following:

ghc-prof-flamegraph zf.prof

Debugging

If verification fails, then the failed TPTP encoded task is dumped to stderr. You can redirect that output to a file to experiment with it.

stack exec zf -- file-that-fails.tex 2> debug/fail.p

You can then run provers manually on that file.

eprover --auto --soft-cpu-limit=10  --memory-limit=5000 --silent --proof-object debug/fail.p

vampire --mode casc debug/fail.p

You can also dump all prover task by passing, e.g. --dump ./dump (the .gitignore is set up to ignore files in this specific directory).