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.
In case you are not familiar with Coq's module system: we implemented this formalization as a library for people to use. A "Module Type" specifies a signature that a user needs to implement; "Parameter"s within that module type are the specific things a user needs to provide/proof. Once a user instantiated a module type in a module of their own, they can use that to instantiate our "Module"s, which provide the extended systems/proofs based on the user's input.
This file contains only the signatures of the various components of our proof, but for each file (.v), there is a link at the beginning of the section corresponding to that file that leads to the coqdoc for the full file including the actual proof code. The .v-files themselves are also included and can be used to verify the proofs in Coq. The files should be compiled in the order in which they appear in this file.
The following table gives an outline of the parts of our paper and where to find their corresponding counterpart in this formalization:
Concept from PaperCorresponding Proof PartComment
Literals & TypesTyp.T in Common.vGeneralized to arbitrary types, all user-provided
User-Defined Subtyping RulesRules.Con, Rules.Req, Rules.Ass in Common.v
Declarative Subtyping RulesTraditional.TransRefl.TRCon etc. in Tradition.vin our original formalization, we used the term "Traditional" instead of "Declarative"
Reductive Subtyping Rulessee User-Defined Typing RulesWhile Declarative Rules add reflexivity and transitivity, Reductive Rules are all user-supplied in this more general framework
Requirement 1: Syntax-DirectednessDecidableRules.finite_con in Decide.v
Requirement 2: Well-FoundednessDecidableRules.wf in Decide.v
Requirement 3: Literal ReflexivityDecidableRules.refl in Decide.vSince everything is a literal/type, this captures all types
Subtyping Rules with AssumptionsProofPV.ProofPV etc. in Common.v
Requirement 4: R-to-D Literal ConversionConverter.decidable_traditional_R in Convert.v
Requirement 5: D-to-R Literal ConversionConverter.traditional_decidable_R in Convert.v
Requirement 6: Literal TransitivityDecidableRules.Red in Decide.vSee also Reduction.Reduction in Common.v
Decidability of Declarative Subtyping TheoremConversion.decidable_traditional and Conversion.traditional_decidable in Convert.vTogether with Decider.decider in Decide.v
Extended SubtypingExtension.Con and ExtendedRules.ECon etc. in Extend.v
Intersector/IntegratorComonad.i in Preprocess.vSince everything is a literal/type, there is no distinction between intersector and integrator
Requirement 7: Intersector CompletenessEquivocator.iextended in Equate.v
Requirement 8: Intersector SoundnessEquivocator.unit in Equate.v
Lemma 1: Integrated SoundnessEquivalence.ipreprocessing_extended in Equate.v
Requirement 9: Measure PreservationWellFoundedComonad.i_wf in Preprocess.vRequires full well-foundedness proof instead of measure preservation
Lemma 2: Integrated DecidabilityDecider.decider in Preprocess.v
Requirement 10: Literal DerelictionComonad.counit in Preprocess.v
Lemma 3: DerelictionComonad.counit in Preprocess.vSame as Requirement 10 due to missing type/literal distinction
Intersected PredicateComonad.Preprocessed in Preprocess.v
Requirement 11: Intersector IntegratedComonad.i_Preprocessed in Preprocess.v
Lemma 4: Integrator IntegratedComonad.i_Preprocessed in Preprocess.vSame as Requirement 11 due to missing type/literal distinction
Requirement 12: Literal PromotionComonad.i_promote_R in Preprocess.v
Lemma 5: PromotionPreprocessing.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 PromotionPreprocessing.promote in Preprocess.v
Lemma 9: Integrated ReflexivityComonad.derelict and Comonad.refl in Preprocess.v
Lemma 10: D-to-I Literal ConversionEquivalence.iadmitst in Equate.v
Lemma 11: Integrated TransitivityPreprocessing.itrans in Preprocess.v
Lemma 12: Integrated CompletenessEquivalence.extended_ipreprocessing in Equate.v
Decidability of Extended Subtyping TheoremEquivalence.decider in Equate.v
All of this was generated using coqdoc, whose approach to links in the face of modules is not the most helpful one. However, other syntax highlighting features depend on the same information as link generation, so the code should still be a lot more readable than without links. We made sure that links in standard HTML rendering (blue underlined) lead to where they should, and most of the links should get you at least closer to where the definition you wanted to was.

This page has been generated by coqdoc