This repo contains formalisation work on implementing a logical relation over MLTT with one universe. This formalisation follows the work done by Abel et al. (described in Decidability of conversion for Type Theory in Type Theory, 2018), and Loïc Pujet's work on removing induction-recursion from the previous formalization, making it feasible to translate it from Agda to Coq.
The definition of the logical relation (LR) ressembles Loïc's in many ways, but also had to be modified for a few reasons :
- Because of universe constraints and the fact that functors cannot be indexed by terms in Coq whereas it is possible in Agda, the relevant structures had to be parametrized by a type level and a recursor, and the module system had to be dropped out entirely.
- Since Coq and Agda's positivity checking for inductive types is different, it turns out that LR's definition, even though it does not use any induction-induction or induction-recursion in Agda, is not accepted in Coq. As such, the predicate over Π-types for LR has been modified compared to Agda. You can find a MWE of the difference in positivity checking in the two systems in Positivity.v and Positivity.agda.
In order to avoid some work on the syntax, this project uses the AutoSubst project to generate syntax-related boilerplate.
The project builds with Coq version 8.19.0. It needs the opam package coq-smpl. Once these have been installed, you can simply issue make in the root folder.
The make depgraph recipe can be used to generate the dependency graph.
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-ocaml.
It can be re-generated using the make autosubst recipe, once autosubst-ocaml has been installed. Note that we include modified versions of the core and unscoped files, which fix their dependency inclusion. Thus, when the recipe offers to overwrite these, one should choose not to, and only let AutoSubst overwrite Ast.v.
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.