This file is a short explanation that links the manuscript to the .v files for PTSatr. ** Chapter 2.1: untyped PTSs ============================= * base.v: Basic assumptions for PTSs. * ut_term.v: Definition of the terms of PTSs in de Bruijn encoding, and the lemmas needed by this encoding (lift, substitution, ...) * ut_env.v: Definition of the contexts of PTSs and the useful lemmas to manipulate them. * ut_red.v: Definition of the beta-reduction for PTSs with congruences properties, Church-Rosser(Theorem Betas_diamond), Confluence (Theorem Betac_confl) and injectivity of Pi-types (Theorem PiInj). * ut_typ.v: Definition of the typing rules for PTSs with basic properties: - weakening, substitution - inversion lemmas (Lemma gen_sort, gen_var, ...) - type correctness (Theorem TypeCorrect). * ut_sr.v: Proof of Subject Reduction for PTSs, with some tools to manipulate context conversion (Theorem Beta_sound, Subject_Reduction, ...) * ut_strengh.v (not in the manuscript): formalization of Jutting's proof of strengthening for PTSs, based on its ''shape of type'' properties. ** Chapter 2.2: PTSs in Sequent Calculus ========================================= See http://www.lix.polytechnique.fr/~vsiles/coq/formalisation.html It has the same structure ** Chapter 3.1: PTSe ===================== * ut_typ_eq.v: Definition of PTSe with basic manipulation lemmas: - weakening, substitution - context conversion - TypeCorrectness and Reflexivity (Lemma TypeCorrect, TypeCorrect_eq, left_reflexivity, right_reflexivity). - First part of the equivalence: From PTSe -> PTS. * counter_ex.v: Proof of the counterexample of Strong Pi injectivity for PTSe ** Chapter 3.2: PTSatr ======================= * term.v/env.v/red.v: Same as their ut_*.v counterpart, but for annotated terms of PTSatr. * strip.v: Definition of the stripping operator | | that maps terms of PTSatr to terms of PTSs, with some properties of this operator. * typ_annot.v: Definition of the PTSatr systems and most of its properties (due to the complexity of the system, the order of lemmas differ from the usual order for PTSs): - weakening, context conversion (Lemma conv_in_env) - left reflexivity (Theorem red_refl_lt) and substitution (subst_gen) - right reflexivity (Theorem red_refl_gt). - inversion lemmas (Lemma pgen_sort, pgen_var, ...) - Type Correctness (Lemma typ_wf) - Exchange of Types (in the manuscript, Lemma 3.2.7: Theorem relocate) - Correct induction scheme "by hand" to be able to deal with the annotation Lemma typ_ind2. - Diamond Property (Theorem OSDiamond), Church-Rosser and Pi injectivity (Lemma ChurchRooser, Theorem Confluence, Theorem PiInj). - Congruence Lemmas (Lemma reds_La, reds_Pi, ...) - Subject Reduction (Theorem SR) ** Chapter 3.3: Validity of the annotations ============================================ * glue.v: Proof of several tools need for the final equivalence: - Lemma 3.3.2: Weak Shape of Types: Lemma weak_type_shape - Lemma 3.3.1: Erased Confluence: Lemma ErasedTermConfluence (be careful, this one is the worst technical piece of Coq ever). - Lemma 3.3.3: Erased Conversion: Lemma ErasedTypeConversion - Lemma 43_, 33, 33' and ErasedContextSwitch are tool to "glue" contexts that where annotated in different ways from the same basis in the proof of equivalence. * final_result.v: Final proof of the equivalence and its consequences: - From PTS to PTSatr - From PTSatr to PTS / PTSe ( - PTS <-> PTSe: Lemma PTS_equiv_PTSe) - Subject Reduction for PTSe: Lemma PTSe_SR - The definition of a Coq Module which embeds all the theory of PTS/PTSe/PTSatr * ut_typ_eq_inj.v: - Proof that weak PTSe equality enjoys Pi Injectivity - Complete Generation lemmas for PTSe - A direct Proof of Subject Reduction for PTSe if we assume Pi Injectivity for the weak equality.