This repo contains the formalisation work accompanying the paper “Upon This Quote I Will Build My Church Thesis”.
The formalization is based on a previous work by Adjej et al (Martin-Löf à la Coq, CPP'24), which itself follows a similar Agda formalization (described in Decidability of conversion for Type Theory in Type Theory, 2018). In order to avoid some work on the syntax, this project uses the AutoSubst project to generate syntax-related boilerplate.
- Install opam through your favourite means.
- Double-check that no Coq-related environment variables like COQBIN or COQPATH are set.
- Launch the following commands in the folder of this development.
opam switch create . --empty
eval $(opam env)
opam install ocaml-base-compiler=4.11.2
opam repo --this-switch add coq-released https://coq.inria.fr/opam/released
opam install . --deps-only
make
The coqdocjs subfolder is not part of this development, but an independent project vendored here for simplicity of the build process. The upstream repository can be found at https://github.com/coq-community/coqdocjs/.
The project builds with Coq version 8.20.0, and depends on the smpl and Equations libraries.
If you already have an opam set-up, dependencies can be installed by simply using opam install . --deps-only.
Once the dependencies have been installed, you can simply issue make in the root folder to
build the whole development.
The make depgraph recipe can be used to generate the dependency graph.
The project uses the AutoSubst tool to generate syntax-related boilerplate, although it is not necessary to install it to build the project (see below for how to use it).
The development, rendered using coqdoc, can be browsed online. A dependency graph for the project is available here.
For simplicity, we include the syntax file (Ast.v) generated using AutoSubst.
It can be re-generated using the make autosubst recipe, once autosubst-ocaml (version >= 1.1) has been installed.
Note that we include modified versions of the core and unscoped files, which fix their dependencies, so one should pass the -no-static option to AutoSubst to avoid overwriting them.
A few things to get accustomed to if you want to use the development.
In a style somewhat similar to the Math Classes project,
generic notations for typing, conversion, renaming, etc. are implemented using type-classes.
While some care has been taken to try and respect the abstractions on which the notations are
based, they might still be broken by carefree reduction performed by tactics. In this case,
the refold tactic can be used, as the name suggests, to refold all lost notations.
The development relies on large, mutually-defined inductive relations. To make proofs by induction
more tractable, functions XXXInductionConcl are provided. These take the predicates
to be mutually proven, and construct the type of the conclusion of a proof by mutual induction.
Thus, a typical induction proof looks like the following:
Section Foo.
Let P := … .
…
Theorem Foo : XXXInductionConcl P … .
Proof.
apply XXXInduction.
End Section.
The names of the arguments printed when querying About XXXInductionConcl should make it clear
to which mutually-defined relation each predicate corresponds.