Bump README

Author: ppedrot

README.md

@@ -1,94 +1,63 @@
 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 accompanying the paper "In Cantor Space No One Can Hear You Stream".
 
-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].
+The formalization is based on a [previous work](https://github.com/coqhott/logrel-coq/) by Adjej et al ([*Martin-Löf à la Coq*, CPP'24](https://arxiv.org/abs/2310.06376)), which itself 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.
 
-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.
+TL;DR HOWTO INSTALL
+===================
+
+- 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.14.3
+opam repo --this-switch add coq-released https://coq.inria.fr/opam/released
+opam install . --deps-only
+make
+```
+
+IMPORTANT NOTE
+==============
+
+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/.
 
 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 project builds on Coq version `8.19.2`, see the [opam](./opam) file for complete dependencies. Since they are not available as opam packages, [coqdocjs](https://github.com/coq-community/coqdocjs/) is simply included.
+
+Once the dependencies have been installed, you can simply issue `make` in the root folder. The development should build within 10 minutes (around 3 minutes on a modern laptop).
 
-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.
+Apart from a few harmless warnings, and the output of some examples, the build reports on the assumptions of our main theorems, using `Print Assumptions`.
 
-**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`).
+For simplicity, the html documentation built using `coqdoc` is included in the artefact. It can be built again by invoking `make coqdoc`.
 
-Browsing the Development
+Browsing the development
 ==================
 
-The development, rendered using `coqdoc`, can be [browsed online](https://coqhott.github.io/logrel-coq/coqdoc/toc.html).
+The development, rendered using the [coqdoc](https://coq.inria.fr/refman/using/tools/coqdoc.html) utility, can be then browsed (as html files). To start navigating the sources, the best entry point is probably the [the table of content](https://ppedrot.github.io/quote-mltt-lics24/coqdoc/toc.html). A [short description of the file contents](https://ppedrot.github.io/quote-mltt-lics24/index.md) is also provided to make the navigation easier.
 
-Getting Started
+Files of interest
 =================
 
-A few things to get accustomed to if you want to use the development.
+Definitions
+--------
 
-Notations and refolding
------------
+The abstract syntax tree of terms is in [Ast](https://ppedrot.github.io/quote-mltt-lics24/coqdoc/LogRel.AutoSubst.Ast.html), the declarative typing and conversion predicates are in [DeclarativeTyping](https://ppedrot.github.io/quote-mltt-lics24/coqdoc/LogRel.DeclarativeTyping.html), reduction is in [UntypedReduction](https://ppedrot.github.io/quote-mltt-lics24/coqdoc/LogRel.UntypedReduction.html).
 
-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.
+The logical relation is defined with respect to a generic notion of typing, given in [GenericTyping](https://ppedrot.github.io/quote-mltt-lics24/LogRel.GenericTyping.html).
 
-Induction principles
+Proofs
 ----------
 
-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:
+The toplevel results are exposed in a standalone file [Main](https://ppedrot.github.io/quote-mltt-lics24/coqdoc/LogRel.Main.html).
 
-``` coq-lang
-Section Foo.
+The logical relation is defined in [LogicalRelation](https://ppedrot.github.io/quote-mltt-lics24/coqdoc/LogRel.LogicalRelation.html). It is first defined component by component, before the components are all brought together by inductive `LR` at the end of the file. The fundamental lemma of the logical relation, saying that every well-typed term is reducible, is in [Fundamental](https://ppedrot.github.io/quote-mltt-lics24/coqdoc/LogRel.Fundamental.html).
 
-Let P := … .
-…
+Injectivity and no-confusion of type constructor, and subject reduction, are proven in [TypeConstructorsInj](https://ppedrot.github.io/quote-mltt-lics24/coqdoc/LogRel.TypeConstructorsInj.html).
 
-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.
-
-[Utils]: ./theories/Utils.v
-[BasicAst]: ./theories/BasicAst.v
-[Context]: ./theories/Context.v
-[AutoSubst/]: ./theories/AutoSubst/
-[AutoSubst/Extra]: ./theories/AutoSubst/Extra.v
-[Notations]: ./theories/Notations.v
-[Automation]: ./theories/Automation.v
-[NormalForms]: ./theories/NormalForms.v
-[UntypedReduction]: ./theories/UntypedReduction.v
-[GenericTyping]: ./theories/GenericTyping.v
-[DeclarativeTyping]: ./theories/DeclarativeTyping.v
-[Properties]: ./theories/Properties.v
-[DeclarativeInstance]: ./theories/DeclarativeInstance.v
-[LogicalRelation]: ./theories/LogicalRelation.v
-[Induction]: ./theories/LogicalRelation/Induction.v
-[Escape]: ./theories/Escape.v
-[Reflexivity]: ./theories/Reflexivity.v
-[Irrelevance]: ./theories/Irrelevance.v
-[ShapeView]: ./theories/ShapeView.v
-[Positivity.v]: ./theories/Positivity.v
-[Weakening]: ./theories/Weakening.v
-[Substitution]: ./theories/Substitution.v
-[AlgorithmicTyping]: ./theories/AlgorithmicTyping.v
-[AlgorithmicConvProperties]: ./theories/AlgorithmicConvProperties.v
-[AlgorithmicTypingProperties]: ./theories/AlgorithmicTypingProperties.v
-[LogRelConsequences]: ./theories/LogRelConsequences.v
-[BundledAlgorithmicTyping]: ./theories/BundledAlgorithmicTyping.v
-
-[autosubst-ocaml]: https://github.com/uds-psl/autosubst-ocaml
-[Positivity.agda]: ./theories/Positivity.agda
+Consistency and canonicity are derived in [Consequences](https://ppedrot.github.io/quote-mltt-lics24/coqdoc/LogRel.Consequences.html).