Awesome

Presentation

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.

Building

The project builds with Coq version 8.16.1. 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.

Browsing the development

The development, rendered using coqdoc, can be browsed online. A dependency graph for the project is available here.

Syntax (re)generation

The syntax boilerplate has been generated using AutoSubst OCaml from the root folder, with the options -s ucoq -v ge813 -no-static -p ./theories/AutoSubst/Ast_preamble (see the AutoSubst OCaml documentation for installation instructions). Currently, this package works only with older version of Coq (8.14), so we cannot add a recipe to the MakeFile for automatically re-generating the syntax.

If you wish to regenerate the syntax by hand, you need to install AutoSubst from source using Coq 8.14, and use it with the previous options.

Getting started with using the development

A few things to get accustomed to if you want to use the development.

Notations and refolding

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.

Induction principles

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.