documentation and clean-up

README.md

@@ -1,66 +1,25 @@
 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.]((https://github.com/mr-ohman/logrel-mltt/)) (described in [Decidability of conversion for Type Theory in Type Theory, 2018](https://dl.acm.org/doi/10.1145/3158111)), and [Loïc Pujet's work](https://github.com/loic-p/logrel-mltt) on removing induction-recursion from the previous formalization, making it feasible to translate it from Agda to Coq.
+This repo contains the formalisation work accompangy the paper *Definitional Functoriality for Dependent (Sub)Types*.
 
-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](https://github.com/uds-psl/autosubst-ocaml) project to generate syntax-related boilerplate.
+The formalisation follows a similar [Agda formalization]((https://github.com/mr-ohman/logrel-mltt/)) (described in [*Decidability of conversion for Type Theory in Type Theory*, 2018](https://dl.acm.org/doi/10.1145/3158111)). In order to avoid some work on the syntax, this project uses the [AutoSubst](https://github.com/uds-psl/autosubst-ocaml) project to generate syntax-related boilerplate. It also includes code from Winterhalter's [partial-fun](https://github.com/TheoWinterhalter/coq-partialfun) library to handle the definition of partial functions.
 
 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 syntax has been generated using AutoSubst OCaml with the options `-s ucoq -v ge813 -allfv` (see the [AutoSubst OCaml documentation](https://github.com/uds-psl/autosubst-ocaml) for installation instructions for it). Currently, this package works only with older version of Coq (8.13), so we cannot add a recipe to the MakeFile for automatically
-re-generating the syntax.
+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. Apart from a few harmless warnings, the build should report on the assumptions of our main theorems:
+- `typing_SN` in [Normalisation](./theories/Normalisation.v), states that reduction on well-typed terms is (strongly) normalizing; this is phrased in a constructively acceptable way, as accessibility of every well-typed term under reduction, i.e. as well-foundation of the reduction relation.
+- `algo_typing_sound` in [BundledAlgorithmicTyping](./theories/BundledAlgorithmicTyping.v) says that algorithmic typing (assuming its inputs are well-formed), is sound with respect to declarative typing, and `algo_typing_complete` in [AlgorithmicTypingProperties](./theories/AlgorithmicTypingProperties.v) says that it is complete.
+- `check_full` in file [Decidability](./theories/Decidability.v), says that typing is decidable.
 
-**In order to regenerate the syntax**, install autosubst paying attention to [this issue](https://github.com/uds-psl/autosubst-ocaml/issues/1) -- in an opam installation do a `cp -R $OPAM_SWITCH_PREFIX/share/coq-autosubst-ocaml $OPAM_SWITCH_PREFIX/share/autosubst`--, modify the syntax file `AutoSubst/PiUniv.sig`, run autosubst on it (`autosubst -s ucoq -v ge813 -allfv PiUniv.sig -o Ast.v`) and patch the resulting files using the checked in patch (`git apply -R autosubst-patch.diff`).
+The first three are axiom-free, while `check_full`
+only requires a dependently-typed version of the function extensionality axiom. This harmless axiom is introduced by Equations for the definition of the functions.
 
 Browsing the Development
 ==================
 
-The development, rendered using `coqdoc`, can be [browsed online](https://coqhott.github.io/logrel-coq/coqdoc/toc.html).
-
-Getting Started
-=================
-
-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](https://math-classes.github.io/) 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:
-
-``` coq-lang
-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.
+The development, rendered using the [coqdoc](https://coq.inria.fr/refman/using/tools/coqdoc.html) utility, can be generated using `make coqdoc`, and then browed offline (as html files). To start navigating the sources, the best entry point is probably the [the table of content](./docs/coqdoc/toc.html). A [short description of the file contents](./docs/index.md) is also provided to make the navigation easier.
 
 [Utils]: ./theories/Utils.v
 [BasicAst]: ./theories/BasicAst.v

_CoqProject

@@ -17,7 +17,6 @@ theories/Notations.v
 theories/NormalForms.v
 theories/Weakening.v
 theories/UntypedReduction.v
-theories/UntypedValues.v
 theories/GenericTyping.v
 
 theories/DeclarativeTyping.v
@@ -59,10 +58,10 @@ theories/Substitution/Introductions/Sigma.v
 theories/Substitution/Introductions/List.v
 theories/Fundamental.v
 
-theories/AlgorithmicTyping.v
 theories/DeclarativeSubst.v
 theories/TypeConstructorsInj.v
 theories/Normalisation.v
+theories/AlgorithmicTyping.v
 theories/BundledAlgorithmicTyping.v
 theories/AlgorithmicConvProperties.v
 theories/AlgorithmicTypingProperties.v