Proof of the more general integration process
Introduction
This document gives an overview of the Coq formalization we have created for our more general framework that handles Integrated Subtyping for general type systems, not just those with union and intersection types, as discussed in section 7 of the paper.Concept from Paper | Corresponding Proof Part | Comment |
---|---|---|
Literals & Types | Typ.T in Common.v | Generalized to arbitrary types, all user-provided |
User-Defined Subtyping Rules | Rules.Con, Rules.Req, Rules.Ass in Common.v | |
Declarative Subtyping Rules | Traditional.TransRefl.TRCon etc. in Tradition.v | in our original formalization, we used the term "Traditional" instead of "Declarative" |
Reductive Subtyping Rules | see User-Defined Typing Rules | While Declarative Rules add reflexivity and transitivity, Reductive Rules are all user-supplied in this more general framework |
Requirement 1: Syntax-Directedness | DecidableRules.finite_con in Decide.v | |
Requirement 2: Well-Foundedness | DecidableRules.wf in Decide.v | |
Requirement 3: Literal Reflexivity | DecidableRules.refl in Decide.v | Since everything is a literal/type, this captures all types |
Subtyping Rules with Assumptions | ProofPV.ProofPV etc. in Common.v | |
Requirement 4: R-to-D Literal Conversion | Converter.decidable_traditional_R in Convert.v | |
Requirement 5: D-to-R Literal Conversion | Converter.traditional_decidable_R in Convert.v | |
Requirement 6: Literal Transitivity | DecidableRules.Red in Decide.v | See also Reduction.Reduction in Common.v |
Decidability of Declarative Subtyping Theorem | Conversion.decidable_traditional and Conversion.traditional_decidable in Convert.v | Together with Decider.decider in Decide.v |
Extended Subtyping | Extension.Con and ExtendedRules.ECon etc. in Extend.v | |
Intersector/Integrator | Comonad.i in Preprocess.v | Since everything is a literal/type, there is no distinction between intersector and integrator |
Requirement 7: Intersector Completeness | Equivocator.iextended in Equate.v | |
Requirement 8: Intersector Soundness | Equivocator.unit in Equate.v | |
Lemma 1: Integrated Soundness | Equivalence.ipreprocessing_extended in Equate.v | |
Requirement 9: Measure Preservation | WellFoundedComonad.i_wf in Preprocess.v | Requires full well-foundedness proof instead of measure preservation |
Lemma 2: Integrated Decidability | Decider.decider in Preprocess.v | |
Requirement 10: Literal Dereliction | Comonad.counit in Preprocess.v | |
Lemma 3: Dereliction | Comonad.counit in Preprocess.v | Same as Requirement 10 due to missing type/literal distinction |
Intersected Predicate | Comonad.Preprocessed in Preprocess.v | |
Requirement 11: Intersector Integrated | Comonad.i_Preprocessed in Preprocess.v | |
Lemma 4: Integrator Integrated | Comonad.i_Preprocessed in Preprocess.v | Same as Requirement 11 due to missing type/literal distinction |
Requirement 12: Literal Promotion | Comonad.i_promote_R in Preprocess.v | |
Lemma 5: Promotion | Preprocessing.dpromote' in Preprocess.v | |
Lemma 6: Integrated Monotonicity | - | Helper Lemmas, established in various different forms in Preprocess.v |
Lemma 7: Integrated Assumptions | - | |
Lemma 8: Integrated Promotion | Preprocessing.promote in Preprocess.v | |
Lemma 9: Integrated Reflexivity | Comonad.derelict and Comonad.refl in Preprocess.v | |
Lemma 10: D-to-I Literal Conversion | Equivalence.iadmitst in Equate.v | |
Lemma 11: Integrated Transitivity | Preprocessing.itrans in Preprocess.v | |
Lemma 12: Integrated Completeness | Equivalence.extended_ipreprocessing in Equate.v | |
Decidability of Extended Subtyping Theorem | Equivalence.decider in Equate.v |
This page has been generated by coqdoc