PCUICAst defines the syntax of terms of PCUIC: term.
Utility functions on this syntax can be found in
PCUICAstUtils, while PCUICInduction
provides induction principles on the syntax, while taking care of special
constructors like tCase (pattern-maching), tFix (fixed points) and
tCoFix (co-fixed points) which take lists of terms as arguments.
PCUICLiftSubst defines renaming, lifting and susbtitution.
PCUICUnivSubst defines universe substitution (for universe
polymorphism).
PCUICReflect contains the definition of the ReflectEq type
class, coming with boolean equality eqb which reflects equality, and give
many instances of that class.
Typing in PCUIC is defined in PCUICTyping, it also comes
with the definition of reduction, conversion and cumulativity.
Some results about reduction (including the definition of parallel reduction)
can be found in PCUICReduction.
In PCUICPosition, we define the notion of position in a
term, as well as the notion of stack, how they are related and a
well-founded order on positions (in a given term).
In PCUICNameless we define a notion of nameless terms
(without any pretty-printing annotations) and the nl function to remove
such names in a term.
Weakening on environments is done in PCUICWeakeningEnv.
The notion of closed terms is defined in PCUICClosed.
In PCUICSigmaCalculus we show type
preservation for σ-calculus instantiation.
Then PCUICWeakening contains the weakening lemma.
Some properties on cumulativity are proven in
PCUICCumulativity, it also includes some other
properties about eq_term but they can mainly be found in
PCUICEquality.
PCUICSubstitution contains the substitution lemma.
All inversion lemmata on typing are in PCUICInversion.
PCUICGeneration on the other hand is about admissibility
lemmata on typing, for instance typing of n-ary application mkApps.
PCUICParallelReduction and
PCUICParallelReductionConfluence have
self-explanatory names, they define parallel reduction and show it is confluent
as a stepping stone to prove confluence of the "usual" reduction in
PCUICConfluence.
We prove principality (if a term has two types, it can be typed with a subtype
of both) in PCUICPrincipality.
PCUICUnivSubstitution contains more universe
substitution lemmata.
PCUICValidity allows us to show that every type A
such that Γ ⊢ t : A is valid, meaning it is sorted or a well-formed
arity.
Subject reduction is addressed in PCUICSR.
PCUICWcbvEval defines the weak head call by value
evaluation strategy.
PCUICMetaTheory sums up the meta-theory? (probably outdated)
PCUICChecker contains a fueled type checker for PCUIC
whose completeness can be found in
PCUICCheckerCompleteness.
PCUICRetyping provides a type_of function to get the
type of well-typed expression, it doesn't check again that the term is
well-typed, so it can go faster.
TemplateToPCUIC, as the name implies, contains a translation from TemplateCoq syntax to PCUIC syntax. TemplateToPCUICCorrectness shows that this translation is type-preserving.
PCUICErasedTerm contains the AST for the erased terms (proofs are identified). PCUICElimination defines information about elimination of proofs.
In PCUICNormal we define the notion of (weak head) neutral and
normal terms.
PCUICSafeLemmata mostly contains lemmata that should be
moved, but also the definition of welltyped and wellformed which are
Prop variants of typing, stating that a term is well typed (or is an arity
in the case of wellformed). The file includes lemmata about it.
PCUICSN defines the normalisation axiom as well-foundedness
of the co-reduction, as well as related lemmata.