This repository contains an extensive formalisation of a dependent type theory (MLT with one universe and a number of type formers: Π, Σ, ℕ, Id). It contains:
- a proof by logical relations, inspired by the approach of Abel et al. (described in Decidability of conversion for Type Theory in Type Theory, 2018), and ideas by Loïc Pujet on removing induction-recursion from it;
- a formalisation of multiple conversion-checking algorithms (type-directed and term-directed) and a bidirectional type system, all fully verified.
Parts of the formalisation has been described in the following papers:
- Martin-Löf à la Coq presents the core of the project;
- What does it take to certify conversion? focuses more on the verification of the properties of the algorithms, including the term-directed one.
The project has also been used as a base for the following work:
- “Upon This Quote I Will Build My Church Thesis”, which extends the type system with primitives for quoting;
- Continuity in Type Theory, Chapter 4, which extends the system with sheaf-like conditions to obtain continuity properties.
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.