Mechanically Verified Proofs from "Empowering Union and Intersection Types with Integrated Subtyping"
Preface
This is not the artifact that was evaluated during the OOPSLA 2018 Artifact Evaluation process, rather it is an improvement on that artifact. For archival purposes, the outdated artifact that was evaluated is provided in outdated_artifact.zip. However, the outdated artifact does not directly support the claims stated in the paper, and the section of the paper that discussed what claims it did support has been removed, so we strongly discourage referencing the outdated artifact. The artifact presented here, although it was not evaluated, has been developed to the same or higher quality than the one that was, and was made to directly support the claims in the paper.Introduction
This document gives an overview of the Coq formalization we have created for our paper. It formalizes every requirement and claim in Sections 3 - 5. It is meant to be read along with the paper and largely tries to follow the flow of the paper exactly, with the exception that for engineering reasons, the requirements of each section are all stated together, followed by the Lemmas and Theorems of that section.Outline
The following outline of the proofs shows the items that correspond to something in the paper:- Section 3: Formalizing Traditional Union and Intersection Subtyping
- Literals (Lit; in many cases an (implicit) parameter)
- Types (Notation T := UIType Lit)
- Declarative Subtyping with Assumptions (dsuba)
- Reductive Subtyping with Assumptions (rsubam; see explanation at definition)
- Declarative Literal Subtyping Rules (DRule and DPremise)
- Declarative Subtyping (dsub based on dsuba and dsubf)
- Reductive Literal Subtyping Rules (RRule and RPremise)
- Reductive Subtyping (rsub based on uisub, lsub, and rsubf)
- Requirements
- Requirement 1: Syntax-Directedness (SyntaxDirectedness_Rules and SyntaxDirectedness_Premises)
- Requirement 2: Well-Foundedness (m, M, mlt, mltwf, m_ui_l, m_ui_r, and m_lit)
- Requirement 3: Literal Reflexivity (LiteralReflexivity)
- Requirement 4: R-to-D Literal Conversion (RRuleToDProof)
- Requirement 5: D-to-R Literal Conversion (DRuleToRProof)
- Requirement 6: Literal Transitivity (LiteralTransitivity)
- Decidability of Declarative Subtyping Theorem (DecidabilityOfDeclarativeSubtyping)
- Section 4: Empowering Unions and Intersections
- Integrator DNFc (Integrate)
- Integrated Predicate dnfφ/dnfφ∩ (Integrated and Integrated_int)
- Extension Axioms (extension)
- Extended Subtyping (esub)
- Intersector (⊓) (intersect)
- Intersected Predicate (φ) (intersected)
- Requirements
- Requirement 7: Intersector Completeness (IntersectorCompleteness)
- Requirement 8: Intersector Soundness (IntersectorSoundness)
- Requirement 9: Measure Preservation (MeasurePreservation)
- Requirement 10: Literal Dereliction (LiteralDereliction)
- Requirement 11: Intersector Integrated (IntersectorIntegrated)
- Requirement 12: Literal Promotion (LiteralPromotion)
- Proofs
- Lemma 1: Integrated Soundness (IntegratedSoundness)
- Lemma 2: Integrated Decidability (IntegratedDecidability)
- Lemma 3: Dereliction (Dereliction)
- Lemma 4: Integrator Integrated (IntegratorIntegrated)
- Lemma 5: Promotion (Promotion)
- Lemma 6: Integrated Monotonicity (IntegratedMonotonicity)
- Lemma 7: Integrated Assumptions (IntegratedAssumptions)
- Lemma 8: Integrated Promotion (IntegratedPromotion)
- Lemma 9: Integrated Reflexivity (IntegratedReflexivity)
- Lemma 10: D-to-I Literal Conversion (DeclarativeToIntegratedLiteralConversion)
- Lemma 11: Integrated Transitivity (IntegratedTransitivity)
- Lemma 12: Integrated Completeness (IntegratedCompleteness)
- Decidability of Extended Subtyping Theorem (DecidabilityOfExtendedSubtyping and OptimizedDecidabilityOfExtendedSubtyping)
- Section 5: Composability
- Requirement 13: Intersected Preservation (IntersectedPreservation)
- Intersector Composability Theorem (Module Composition)
Paper Concept Index
The following table gives an outline of the parts of our paper and where to find their corresponding counterpart in this formalization:Concept from Paper | Corresponding Definitions/Lemmas/Theorems | Comment |
---|---|---|
Literals | Lit in Section3_Requirements.v | Also an implicit parameter in many global definitions |
Types | Notation T := UIType Lit defined almost everywhere | UIType is defined in Section3_Requirements.v |
Declarative Literal Subtyping Rules | DRule and DPremise in Section3_Requirements.v | |
Declarative Subtyping | dsub in Section3_Requirements.v | Based on dsuba and dsubf in Section3_Requirements.v |
Reductive Literal Subtyping Rules | RRule and RPremise in Section3_Requirements.v | |
Reductive Subtyping | rsub in Section3_Requirements.v | Based on uisub, lsub, and rsubf in Section3_Requirements.v |
Requirement 1: Syntax-Directedness | SyntaxDirectedness_Rules and SyntaxDirectedness_Premises in Section3_Requirements.v | |
Requirement 2: Well-Foundedness | m, M, mlt, mltwf, m_ui_l, m_ui_r, and m_lit in Section3_Requirements.v | |
Requirement 3: Literal Reflexivity | LiteralReflexivity in Section3_Requirements.v | |
Declarative Subtyping with Assumptions | dsuba in Section3_Requirements.v | |
Reductive Subtyping with Assumptions | rsubam in Section3_Requirements.v | Also includes Monotonicity, which makes the proof stronger than in the paper (see explanation at definition) |
Requirement 4: R-to-D Literal Conversion | RRuleToDProof in Section3_Requirements.v | |
Requirement 5: D-to-R Literal Conversion | DRuleToRProof in Section3_Requirements.v | |
Requirement 6: Literal Transitivity | LiteralTransitivity in Section3_Requirements.v | |
Decidability of Declarative Subtyping Theorem | DecidabilityOfDeclarativeSubtyping in Section3_Proofs.v | |
Extension Axioms | extension in Section4_Requirements.v | |
Extended Subtyping | esub in Section4_Requirements.v | Based on dsubda and extension in Section4_Requirements.v |
Integrator (DNFc) | Integrate in Section4_Requirements.v | |
Intersector (⊓) | intersect in Section4_Requirements.v | |
Requirement 7: Intersector Completeness | IntersectorCompleteness in Section4_Requirements.v | |
Requirement 8: Intersector Soundness | IntersectorSoundness in Section4_Requirements.v | |
Lemma 1: Integrated Soundness | IntegratedSoundness in Section4_Proofs.v | |
Requirement 9: Measure Preservation | MeasurePreservation in Section4_Requirements.v | |
Lemma 2: Integrated Decidability | IntegratedDecidability in Section4_Proofs.v | |
Requirement 10: Literal Dereliction | LiteralDereliction in Section4_Requirements.v | |
Lemma 3: Dereliction | Dereliction in Section4_Proofs.v | |
Intersected Predicate (φ) | intersected in Section4_Requirements.v | |
Integrated Predicate (dnfφ/dnfφ∩) | Integrated and Integrated_int in Section4_Requirements.v | |
Requirement 11: Intersector Integrated | IntersectorIntegrated in Section4_Requirements.v | |
Lemma 4: Integrator Integrated | IntegratorIntegrated in Section4_Proofs.v | |
Requirement 12: Literal Promotion | LiteralPromotion in Section4_Requirements.v | |
Lemma 5: Promotion | Promotion in Section4_Proofs.v | |
Lemma 6: Integrated Monotonicity | IntegratedMonotonicity in Section4_Proofs.v | Actually mostly proved together in integrated_assumptions' in Section4_Proofs.v |
Lemma 7: Integrated Assumptions | IntegratedAssumptions in Section4_Proofs.v | |
Lemma 8: Integrated Promotion | IntegratedPromotion in Section4_Proofs.v | |
Lemma 9: Integrated Reflexivity | IntegratedReflexivity in Section4_Proofs.v | |
Lemma 10: D-to-I Literal Conversion | DeclarativeToIntegratedLiteralConversion in Section4_Proofs.v | |
Lemma 11: Integrated Transitivity | IntegratedTransitivity in Section4_Proofs.v | |
Lemma 12: Integrated Completeness | IntegratedCompleteness in Section4_Proofs.v | |
Decidability of Extended Subtyping Theorem | DecidabilityOfExtendedSubtyping and OptimizedDecidabilityOfExtendedSubtyping in Section4_Proofs.v | |
Requirement 13: Intersected Preservation | IntersectedPreservation in Section5.v | |
Intersector Composability Theorem | Module Composition in Section5.v | Defines its intersect and extension as described in the paper and satisfies the Intersector module type and hence all the Lemmas and Theorems above. |
Section 3: Formalizing Traditional Union and Intersection Subtyping (Section3_Requirements.v)
This section contains the formalization of Section 3 of the paper, i.e. the traditional formalization of subtyping in the presence of union and intersection types.Inductive UIType {Lit : Type} : Type :=
| TTop : UIType
| TBot : UIType
| TUni (l r : UIType) : UIType
| TIsect (l r : UIType) : UIType
| TLit (l : Lit) : UIType
.
Declarative Subtyping
Next, we define declarative subtyping with assumptions (dsuba) as in Figure 3; standard declarative subtyping from Figure 1 (dsubf) is defined as dsuba with empty assumptions. Both dsuba and dsubf are parameterized over a set of declarative literal subtyping rules DRule, as in the paper, and a relation on pairs of types for each rule (DPremise) specifying the premises of each rule. The additional parameter Assumed in dsuba models the set of assumptions, as in Figure 3.
Section DSub.
Variable Lit : Type.
Notation T := (UIType Lit).
Variable DRule : Lit -> Lit -> Type.
Variable DPremise : forall (l r : Lit), DRule l r -> T -> T -> Prop.
Inductive dsuba {Assumed : T -> T -> Prop} : T -> T -> Prop :=
| dsuba_refl : forall t : T, dsuba t t
| dsuba_trans : forall tl tm tr : T, dsuba tl tm -> dsuba tm tr -> dsuba tl tr
| dsuba_assume : forall tl tr : T, Assumed tl tr -> dsuba tl tr
| dsuba_lit : forall {ll lr : Lit} (r : DRule ll lr), (forall ptl ptr : T, DPremise ll lr r ptl ptr -> dsuba ptl ptr) -> dsuba (TLit ll) (TLit lr)
| dsuba_top : forall t : T, dsuba t TTop
| dsuba_bot : forall t : T, dsuba TBot t
| dsuba_uni_l : forall tl tr t : T, dsuba tl t -> dsuba tr t -> dsuba (TUni tl tr) t
| dsuba_uni_rl : forall tl tr : T, dsuba tl (TUni tl tr)
| dsuba_uni_rr : forall tl tr : T, dsuba tr (TUni tl tr)
| dsuba_int_r : forall t tl tr : T, dsuba t tl -> dsuba t tr -> dsuba t (TIsect tl tr)
| dsuba_int_ll : forall tl tr : T, dsuba (TIsect tl tr) tl
| dsuba_int_lr : forall tl tr : T, dsuba (TIsect tl tr) tr
.
Definition dsubf : T -> T -> Prop :=
dsuba (fun _ _ => False).
End DSub.
Variable Lit : Type.
Notation T := (UIType Lit).
Variable DRule : Lit -> Lit -> Type.
Variable DPremise : forall (l r : Lit), DRule l r -> T -> T -> Prop.
Inductive dsuba {Assumed : T -> T -> Prop} : T -> T -> Prop :=
| dsuba_refl : forall t : T, dsuba t t
| dsuba_trans : forall tl tm tr : T, dsuba tl tm -> dsuba tm tr -> dsuba tl tr
| dsuba_assume : forall tl tr : T, Assumed tl tr -> dsuba tl tr
| dsuba_lit : forall {ll lr : Lit} (r : DRule ll lr), (forall ptl ptr : T, DPremise ll lr r ptl ptr -> dsuba ptl ptr) -> dsuba (TLit ll) (TLit lr)
| dsuba_top : forall t : T, dsuba t TTop
| dsuba_bot : forall t : T, dsuba TBot t
| dsuba_uni_l : forall tl tr t : T, dsuba tl t -> dsuba tr t -> dsuba (TUni tl tr) t
| dsuba_uni_rl : forall tl tr : T, dsuba tl (TUni tl tr)
| dsuba_uni_rr : forall tl tr : T, dsuba tr (TUni tl tr)
| dsuba_int_r : forall t tl tr : T, dsuba t tl -> dsuba t tr -> dsuba t (TIsect tl tr)
| dsuba_int_ll : forall tl tr : T, dsuba (TIsect tl tr) tl
| dsuba_int_lr : forall tl tr : T, dsuba (TIsect tl tr) tr
.
Definition dsubf : T -> T -> Prop :=
dsuba (fun _ _ => False).
End DSub.
Reductive Subtyping
As in the paper, we formalize reductive subtyping rules, which do not have reflexivity or transitivity. We split up subtyping a little bit more here: uisub, which formalizes the subtyping rules for union and intersection types, takes an arbitrary relation on literals to decide literal subtyping. Usually, this relation will be some instantiation of lsub, which is parameterized by reductive literal subtyping rules and a premise relation for them, similar to the declarative subtyping rules, and in addition a relation on literals that is used to decide whether the premises hold. In most cases, this will be some instantiation of uisub again. For instance, rsubf recursively combines uisub and lsub given some literal type, reductive literal subtyping rules and a premise relation.
Section RSub.
Variable Lit : Type.
Notation T := (UIType Lit).
Variable RRule : Lit -> Lit -> Type.
Variable RPremise : forall (l r : Lit), RRule l r -> T -> T -> Prop.
Inductive uisub {R : Lit -> Lit -> Prop} : T -> T -> Prop :=
| ui_lit (ll lr : Lit) : R ll lr -> uisub (TLit ll) (TLit lr)
| ui_top (tl : T) : uisub tl TTop
| ui_int_ll (il ir tr : T) : uisub il tr -> uisub (TIsect il ir) tr
| ui_int_lr (il ir tr : T) : uisub ir tr -> uisub (TIsect il ir) tr
| ui_int_r (tl il ir : T) : uisub tl il -> uisub tl ir -> uisub tl (TIsect il ir)
| ui_bot (tr : T) : uisub TBot tr
| ui_uni_rl (tl ul ur : T) : uisub tl ul -> uisub tl (TUni ul ur)
| ui_uni_rr (tl ul ur : T) : uisub tl ur -> uisub tl (TUni ul ur)
| ui_uni_l (ul ur tr : T) : uisub ul tr -> uisub ur tr -> uisub (TUni ul ur) tr
.
Inductive lsub (R : T -> T -> Prop) (ll lr : Lit) : Prop :=
| Lsub (r : RRule ll lr) : (forall tl tr : T, RPremise ll lr r tl tr -> R tl tr) -> lsub R ll lr
.
Inductive rsubf : T -> T -> Prop :=
| Rsubf (tl tr : T) : uisub (lsub (rsubf)) tl tr -> rsubf tl tr
.
Variable Lit : Type.
Notation T := (UIType Lit).
Variable RRule : Lit -> Lit -> Type.
Variable RPremise : forall (l r : Lit), RRule l r -> T -> T -> Prop.
Inductive uisub {R : Lit -> Lit -> Prop} : T -> T -> Prop :=
| ui_lit (ll lr : Lit) : R ll lr -> uisub (TLit ll) (TLit lr)
| ui_top (tl : T) : uisub tl TTop
| ui_int_ll (il ir tr : T) : uisub il tr -> uisub (TIsect il ir) tr
| ui_int_lr (il ir tr : T) : uisub ir tr -> uisub (TIsect il ir) tr
| ui_int_r (tl il ir : T) : uisub tl il -> uisub tl ir -> uisub tl (TIsect il ir)
| ui_bot (tr : T) : uisub TBot tr
| ui_uni_rl (tl ul ur : T) : uisub tl ul -> uisub tl (TUni ul ur)
| ui_uni_rr (tl ul ur : T) : uisub tl ur -> uisub tl (TUni ul ur)
| ui_uni_l (ul ur tr : T) : uisub ul tr -> uisub ur tr -> uisub (TUni ul ur) tr
.
Inductive lsub (R : T -> T -> Prop) (ll lr : Lit) : Prop :=
| Lsub (r : RRule ll lr) : (forall tl tr : T, RPremise ll lr r tl tr -> R tl tr) -> lsub R ll lr
.
Inductive rsubf : T -> T -> Prop :=
| Rsubf (tl tr : T) : uisub (lsub (rsubf)) tl tr -> rsubf tl tr
.
The relation rsubam is the reductive subtyping relation with assumptions and monotonicity.
This relation is a super-relation of reductive subtyping with assumptions as defined in Figure 4, which defines reductive subtyping rules that additionally admit subtypings in the given set of assumptions.
The additional relations come from the monotonicity rules ram_mono, which lets one compose rsubam proofs with proofs without assumptions or monotonicity on the left and right.
rsubam is used internally in some of our proofs and replaces the simple reductive subtyping with assumptions in our requirements, making the requirements here weaker than in the paper, as any subtyping proof just with assumptions is also a subtyping proof with assumptions and monotonicity.
This comes in handy in modelling Minimal Relevant Logic as discussed in Section 7.
Inductive rsubam {Assumed : T -> T -> Prop} : T -> T -> Prop :=
| ram_assumption (tl tr : T) : Assumed tl tr -> rsubam tl tr
| ram_mono (tl tl' tr' tr : T) : rsubf tl tl' -> rsubam tl' tr' -> rsubf tr' tr -> rsubam tl tr
| ram_lit (ll lr : Lit) (r : RRule ll lr) : (forall pl pr : T, RPremise ll lr r pl pr -> rsubam pl pr) -> rsubam (TLit ll) (TLit lr)
| ram_top (tl : T) : rsubam tl TTop
| ram_int_ll (il ir tr : T) : rsubam il tr -> rsubam (TIsect il ir) tr
| ram_int_lr (il ir tr : T) : rsubam ir tr -> rsubam (TIsect il ir) tr
| ram_int_r (tl il ir : T) : rsubam tl il -> rsubam tl ir -> rsubam tl (TIsect il ir)
| ram_bot (tr : T) : rsubam TBot tr
| ram_uni_rl (tl ul ur : T) : rsubam tl ul -> rsubam tl (TUni ul ur)
| ram_uni_rr (tl ul ur : T) : rsubam tl ur -> rsubam tl (TUni ul ur)
| ram_uni_l (ul ur tr : T) : rsubam ul tr -> rsubam ur tr -> rsubam (TUni ul ur) tr
.
End RSub.
Requirements
The requirements of Section 3 (Requirements 1 - 6) are collected in the module type Traditional. A user of our framework instantiates this module type to provide the type of literals Lit and the other required components and the Lemmas about them.Inductive subui {Lit : Type} : UIType Lit -> UIType Lit -> Prop :=
| sub_uni_l : forall (t tr : UIType Lit) , subui t (TUni t tr)
| sub_uni_r : forall (t tl : UIType Lit) , subui t (TUni tl t)
| sub_isect_l : forall (t tr : UIType Lit) , subui t (TIsect t tr)
| sub_isect_r : forall (t tl : UIType Lit) , subui t (TIsect tl t)
.
Module Type Traditional.
This is where a user of our framework defines the type of literals Lit, usually recursively using UIType Lit in some cases.
Also defined here are the relations for declarative and reductive subtyping rules (DRule, RRule) and their premises (DPremise, RPremise) as described above.
We also define the notations dsub and rsub for the declarative and reductive subtyping relations with the respective premises, respectively, which are now exactly modelling the relations defined in Figures 1 and 2.
Parameter Lit : Type.
Notation T := (UIType Lit).
Parameter DRule : Lit -> Lit -> Type.
Parameter DPremise : forall {l r : Lit}, DRule l r -> T -> T -> Prop.
Notation dsub := (dsubf (@DPremise)).
Parameter RRule : Lit -> Lit -> Type.
Parameter RPremise : forall {l r : Lit}, RRule l r -> T -> T -> Prop.
Notation rsub := (rsubf (@RPremise)).
Requirement 1: Syntax-Directedness
For every pair of literals ll and lr, the set of applicable rules RRule ll lr must be computable and finite (SyntaxDirectedness_Rules). For every rule r, the set of premises RPremise r must be computable and finite (SyntaxDirectedness_Premises).Parameter SyntaxDirectedness_Rules : forall ll lr : Lit, { rrules : list (RRule ll lr) | forall r : RRule ll lr, In r rrules }.
Parameter SyntaxDirectedness_Premises : forall {ll lr : Lit} (r : RRule ll lr), { rpremises : list (prod T T) | forall pl pr : T, RPremise r pl pr <-> In (pair pl pr) rpremises }.
Requirement 2: Well-Foundedness
There exists a function m from pairs of types to some set M with a well-founded (mltwf) relation mlt satisfying the following inequalities: m_ui_l, m_ui_r, and m_lit.Parameter M : Type.
Parameter mlt : M -> M -> Prop.
Parameter mltwf : well_founded mlt.
Parameter m : T -> T -> M.
Parameter m_ui_l : forall (tl tl' tr : T), subui tl tl' -> (clos_refl_trans M mlt) (m tl tr) (m tl' tr).
Parameter m_ui_r : forall (tl tr tr' : T), subui tr tr' -> (clos_refl_trans M mlt) (m tl tr) (m tl tr').
Parameter m_lit : forall {ll lr : Lit} (r : RRule ll lr), forall pl pr : T, RPremise r pl pr -> mlt (m pl pr) (m (TLit ll) (TLit lr)).
Requirement 3: Literal Reflexivity
For each literal l, there exists an RRule l l such that all premises have the same type on the left- and right-hand side.Parameter LiteralReflexivity : forall l : Lit, exists r : RRule l l, forall pl pr : T, RPremise r pl pr -> pl = pr.
Requirement 4: Reductive-to-Declarative Literal Conversion
Each reductive subtyping rule can be converted into a declarative subtyping proof where the premises of the reductive subtyping rule are assumed.Parameter RRuleToDProof : forall {ll lr : Lit} (r : RRule ll lr), dsuba (@DPremise) (RPremise r) (TLit ll) (TLit lr).
Requirement 5: Declarative-to-Reductive Literal Conversion
Each declarative subtyping rule can be converted into a reductive subtyping proof where the premises of the reductive subtyping rule are assumed and monotonicity holds.Parameter DRuleToRProof : forall {ll lr : Lit} (r : DRule ll lr), rsubam (@RPremise) (DPremise r) (TLit ll) (TLit lr).
Requirement 6: Literal Transitivity
For each pair of reductive literal rules rl rr that share a middle (right-hand in rl, left-hand in rr) literal lm, there exists a combined rule r between the left-hand literal of rl and the right-hand literal of rr, and each of the premises can be proven assuming local transitivity of the premises of rl and rr. Due to contravariance, it is possible that the premises of rl and rr might be composed in the opposite order.Parameter LiteralTransitivity : forall {ll lm lr : Lit} (rl : RRule ll lm) (rr : RRule lm lr),
exists r : RRule ll lr,
forall pl pr : T, RPremise r pl pr ->
exists pm : T, (rsubam (@RPremise) (RPremise rl) pl pm /\ rsubam (@RPremise) (RPremise rr) pm pr) \/ (rsubam (@RPremise) (RPremise rr) pl pm /\ rsubam (@RPremise) (RPremise rl) pm pr).
End Traditional.
Infrastructure
At this point, there are a few definitions and lemmas that are not central to understanding the proofs and in some sense self-explanatory, and therefore omitted from this document. Please see Section3_Infrastructure.v for those definitions and lemmas.Proof of Decidability of Subtyping (Section3_Proofs.v)
The single theorem of Section 3 is as follows: For every set of literals Lit, set of declarative rules (DRule, DPremise), and set of reductive rules (RRule, RPremise) satisfying Requirements 1 through 6, proof search for reductive subtyping as defined in Figure 2 (rsub) is a decision procedure for declarative subtyping as defined in Figure 1 (dsub).- We prove that rsub is decidable (rsub_dec)
- We prove that rsub is reflexive (rsub_refl) and transitive (rsub_trans)
- We prove that rsub is equivalent to dsub (rsub_dsub)
- We prove that dsub is decidable by using the decidability of rsub and its equivalence to dsub (DecidabilityOfDeclarativeSubtyping)
Deciability of rsub
The decidability of rsub is established using a well-founded measure and proving that every recursive step of rsub reduces the size of that measure. The particular measure used here, progress_measure, is based on the lexicographic ordering of the measure mlt (or more precisely, its transitive closure mltt) provided by the user and the syntactic depth of literals within a given type (syntactic_literal_depth). The former guarantees that the measure is reduced when recursively stepping into the premises of the literal subtyping rule, whereas the latter guarantees that the measure is reduced when union or intersection rules are applied, where mlt is only required to be less-than-or-equal. We first define the measure and its components, establish its well-foundedness (progress_measure_wf) and transitivity (progress_measure_trans, for convenience), and finally prove that rsubf is decidable for any set of premises that reduce the measure in the literal step (rsubf_dec). This is then easily applied to rsub, because RPremise by Requirement 2 (in particular, m_lit) has this property, which gives us rsub_dec.Module TraditionalDec (M_Traditional : Traditional).
Module M_Infrastructure := UIType_Infrastructure(M_Traditional).
Fixpoint syntactic_literal_depth (t : T) :=
match t with
| TTop => 0
| TBot => 0
| TUni l r => 1 + (max (syntactic_literal_depth l) (syntactic_literal_depth r))
| TIsect l r => 1 + (max (syntactic_literal_depth l) (syntactic_literal_depth r))
| TLit l => 0
end.
Definition mltt: M -> M -> Prop := clos_trans M mlt.
Definition mltt_wf : well_founded mltt := wf_clos_trans M mlt mltwf.
Lemma mltt_trans : forall ml mm mr : M, mltt ml mm -> mltt mm mr -> mltt ml mr.
Definition PM : Type := M * nat.
Definition pm (tp : T * T) : PM := (m (fst tp) (snd tp), ((syntactic_literal_depth (fst tp)) + (syntactic_literal_depth (snd tp)))).
Definition pmlt (pml pmr : PM) : Prop := mltt (fst pml) (fst pmr) \/ (fst pml = fst pmr /\ snd pml < snd pmr).
Definition progress_measure (tpl tpr : T * T) : Prop := pmlt (pm tpl) (pm tpr).
Lemma lt_Acc_pmlt_acc : forall pmr : PM, (forall pml : PM, mltt (fst pml) (fst pmr) -> Acc pmlt pml) -> Acc lt (snd pmr) -> Acc pmlt pmr.
Lemma mltt_Acc_pmlt_acc : forall pmr : PM, Acc mltt (fst pmr) -> Acc pmlt pmr.
Lemma pmlt_wf : well_founded pmlt.
Lemma progress_measure_wf : well_founded progress_measure.
Lemma progress_measure_trans : forall tpl tpm tpr : T * T, progress_measure tpl tpm -> progress_measure tpm tpr -> progress_measure tpl tpr.
Lemma rsubf_dec {Premise : forall ll lr : Lit, RRule ll lr -> T -> T -> Prop} (Hpremsd : forall {ll lr : Lit} (r : RRule ll lr), { rpremises : list (prod (T) (T)) | forall pl pr : T, Premise ll lr r pl pr <-> In (pair pl pr) rpremises }) (HMlit : forall {ll lr : Lit} (r : RRule ll lr) (tl tr : T), Premise ll lr r tl tr -> progress_measure (tl, tr) (TLit ll, TLit lr)) : forall tl tr : T, {rsubf Premise tl tr} + {~ rsubf Premise tl tr}.
Lemma rsub_dec : forall tl tr : T, {rsub tl tr} + {~ rsub tl tr}.
An induction principle and Reflexivity
Next, we use the progress_measure to prove a mutual induction principle on types T and literals Lit: uirec_alt. The only part of it that so far has not been mentioned is the predicate uirec, defined in Section3_Infrastructure.v, which specifies that, for two given types, a given relation on Literals holds for all pairs of literals contained in the cross product of the literals contained somewhere in each of the two types. This induction principle is used to prove most of the following Lemmas, starting with reflexivity (rsub_refl), which is otherwise straightforward, using Requirement 3 LiteralReflexivity.Lemma uirec_alt (RL : Lit -> Lit -> Prop) (RT : T -> T -> Prop) : (forall {ll lr : Lit} , (forall (r : RRule ll lr) (tl tr : T), RPremise r tl tr -> (RT tl tr)) -> RL ll lr) -> (forall (tl tr : T), uirec RL tl tr -> RT tl tr) -> forall (tl tr : T), RT tl tr.
Lemma rsub_refl : forall t : T, rsub t t.
Transitivity
First, it is relatively easy to see that the rules for union and intersection types alone (i.e. uisub) are transitive if the literal subtyping relation they use is transitive (see uisub_trans). That last part, however, depends on being able to build a reductive subtyping proof using Requirement 6 (LiteralTransitivity). Requirement 6 is specified using reductive subtyping proofs with assumptions and monotonicity (rsubam), which are not easily translated to regular subtyping proofs. The key trick in the proof here is defining the relation rsubt, which is essentially like rsub, except that it has an explicit transitivity rule. The nice thing about this relation is that it exactly expresses transitivity of rsub and has a nice translation from rsubam (rsubam_rsubt), which we can use to compose the assumptions given by Requirement 6 and therefore proof that rsubt implies rsub (rsubt_rsub) and therefore rsub is transitive (rsub_trans).Lemma uisub_trans {R R' R'' : Lit -> Lit -> Prop} (Htrans: forall ll lm lr : Lit, R ll lm -> R' lm lr -> R'' ll lr) : forall tl tm tr : T, uisub R tl tm -> uisub R' tm tr -> uisub R'' tl tr.
Inductive rsubt : T -> T -> Prop :=
| rt_transitivity (tl tm tr : T) : rsubt tl tm -> rsubt tm tr -> rsubt tl tr
| rt_lit (ll lr : Lit) (r : RRule ll lr) : (forall pl pr : T, RPremise r pl pr -> rsubt pl pr) -> rsubt (TLit ll) (TLit lr)
| rt_top (tl : T) : rsubt tl TTop
| rt_int_ll (il ir tr : T) : rsubt il tr -> rsubt (TIsect il ir) tr
| rt_int_lr (il ir tr : T) : rsubt ir tr -> rsubt (TIsect il ir) tr
| rt_int_r (tl il ir : T) : rsubt tl il -> rsubt tl ir -> rsubt tl (TIsect il ir)
| rt_bot (tr : T) : rsubt TBot tr
| rt_uni_rl (tl ul ur : T) : rsubt tl ul -> rsubt tl (TUni ul ur)
| rt_uni_rr (tl ul ur : T) : rsubt tl ur -> rsubt tl (TUni ul ur)
| rt_uni_l (ul ur tr : T) : rsubt ul tr -> rsubt ur tr -> rsubt (TUni ul ur) tr.
Lemma rsub_rsubt : forall tl tr : T, rsub tl tr -> rsubt tl tr.
Lemma rsubam_rsubt (A : T -> T -> Prop) : (forall tl tr : T, A tl tr -> rsubt tl tr) -> forall tl tr : T, rsubam (@RPremise) A tl tr -> rsubt tl tr.
Lemma rsubt_rsub : forall tl tr : T, rsubt tl tr -> rsub tl tr.
Lemma rsub_trans : forall tl tm tr : T, rsub tl tm -> rsub tm tr -> rsub tl tr.
Two corollaries of rsub's transitivity are that proofs with assumptions and monotonicity can be converted into regular subtyping proofs if the assumptions can be proven (rsubam_rsub), and that literal subtyping proofs can be composed when the relation used for the premises is rsub (lsub_rsub_trans)
Lemma rsubam_rsub {A : T -> T -> Prop}: (forall tl tr: T, A tl tr -> rsub tl tr) -> forall tl tr : T, rsubam (@RPremise) A tl tr -> rsub tl tr.
Lemma lsub_rsub_trans : forall ll lm lr : Lit, lsub (@RPremise) rsub ll lm -> lsub (@RPremise) rsub lm lr -> lsub (@RPremise) rsub ll lr.
Lemma lsub_rsub_trans : forall ll lm lr : Lit, lsub (@RPremise) rsub ll lm -> lsub (@RPremise) rsub lm lr -> lsub (@RPremise) rsub ll lr.
Equivalence
Since rsub has been shown reflexive (rsub_refl) and transitive (rsub_trans), we can now show that declarative and reductive subtyping are equivalent. The reflexivity and transitivity rules are already taken care of, the rules for unions, intersections, top and bottom are trivial, and the rules for literals can be proven equivalent using Requirements 4 (RRuleToDProof) and 5 (DRuleToRProof).Theorem : Decidability of Declarative Subtyping
Now we just stitch the previous lemmas together. Given two types, we use the decider for rsub to see whether they are subtypes under reductive subtyping, and then use the equivalence of reductive and declarative subtyping to produce the corresponding result for declarative subtyping.Theorem DecidabilityOfDeclarativeSubtyping : forall tl tr : T, {dsub tl tr} + {~ dsub tl tr}.
End TraditionalDec.
Section 4: Empowering Unions and Intersections (Section4_Requirements.v)
With the proofs of decidability of traditional declarative subtyping in hand, we now turn to Section 4. We start with a few auxiliary definitions:- Intersect just takes a list of literals and returns a UIType that just consists of nested intersections of those literals. It is meant to mostly represent the big intersection operator on lists of literals from the paper, except that the big intersection operator is not mean to prescribe a particular nesting.
- Integrate is the function DNFc from Figure 6.
- Integrated_int and Integrated are the functions dnfφ∩ and dnfφ from Figure 8, respectively.
- Exists_intersection is like Integrated, except that it only demands that the predicate on lists of literals is true for some intersection in a type that is in DNF instead of all of them. This is used to express the Literal Promotion requirement, see below.
- sig2T essentially lets us hide two type arguments from a dependent type. In particular, recall that RRules are dependent on the literals in their conclusion. sig2T RRule is a type that lets us have lists of rules that are not necessarily between the same literals. proj2T1, proj2T2, and proj2V are just accessor functions that return the LHS argument, the RHS argument, and the specific dependent value packaged in the sig2T, respectively.
- dsubda is Declarative Subtyping with Distributivity and Assumptions, i.e. just dsuba plus a distributivity rule, as in Figure 5 (the user-provided set of extensions behaves like assumptions).
Section Integrator.
Variable Lit : Type.
Notation T := (UIType Lit).
Variable DRule : Lit -> Lit -> Type.
Variable DPremise : forall (l r : Lit), DRule l r -> T -> T -> Prop.
Definition Intersect : list Lit -> T
:= fold_right (fun l => TIsect (TLit l)) TTop.
Fixpoint Integrate (intersect : list Lit -> T) (t : T) : T :=
match t with
| TBot => TBot
| TTop => intersect []
| TUni tl tr => TUni (Integrate intersect tl) (Integrate intersect tr)
| TIsect tl tr => Integrate (fun l => Integrate (fun l' => intersect (l ++ l')) tr) tl
| TLit l => intersect [l]
end.
Fixpoint Integrated_int (intersected : list Lit -> Prop) (t : T) : Prop :=
match t with
| TBot => False
| TTop => intersected []
| TUni tl tr => False
| TIsect tl tr => Integrated_int (fun l => Integrated_int (fun l' => intersected (l ++ l')) tr) tl
| TLit l => intersected [l]
end.
Fixpoint Integrated (intersected : list Lit -> Prop) (t : T) : Prop :=
match t with
| TBot => True
| TTop => intersected []
| TUni tl tr => (Integrated intersected tl) /\ (Integrated intersected tr)
| TIsect tl tr => Integrated_int intersected (TIsect tl tr)
| TLit l => intersected [l]
end.
Fixpoint Exists_Intersection (P : list Lit -> Prop) (t : T) : Prop :=
match t with
| TBot => False
| TTop => P []
| TUni tl tr => (Exists_Intersection P tl) \/ (Exists_Intersection P tr)
| TIsect tl tr => Integrated_int P (TIsect tl tr)
| TLit l => P [l]
end.
Inductive sig2T {A B : Type} {C : A -> B -> Type} : Type :=
exist2T (a : A) (b : B) (c : C a b).
Definition proj2T1 {A B : Type} {C : A -> B -> Type} (s : sig2T C) : A :=
match s with exist2T a _ _ => a end.
Definition proj2T2 {A B : Type} {C : A -> B -> Type} (s : sig2T C) : B :=
match s with exist2T _ b _ => b end.
Definition proj2V {A B : Type} {C : A -> B -> Type} (v : sig2T C) : C (proj2T1 v) (proj2T2 v).
Defined.
Inductive dsubda {Assumed : T -> T -> Prop} : T -> T -> Prop :=
| dsubda_refl : forall t : T, dsubda t t
| dsubda_trans : forall tl tm tr : T, dsubda tl tm -> dsubda tm tr -> dsubda tl tr
| dsubda_assume : forall tl tr : T, Assumed tl tr -> dsubda tl tr
| dsubda_lit : forall {ll lr : Lit} (r : DRule ll lr), (forall ptl ptr : T, DPremise ll lr r ptl ptr -> dsubda ptl ptr) -> dsubda (TLit ll) (TLit lr)
| dsubda_top : forall t : T, dsubda t TTop
| dsubda_bot : forall t : T, dsubda TBot t
| dsubda_uni_l : forall tl tr t : T, dsubda tl t -> dsubda tr t -> dsubda (TUni tl tr) t
| dsubda_uni_rl : forall tl tr : T, dsubda tl (TUni tl tr)
| dsubda_uni_rr : forall tl tr : T, dsubda tr (TUni tl tr)
| dsubda_int_r : forall t tl tr : T, dsubda t tl -> dsubda t tr -> dsubda t (TIsect tl tr)
| dsubda_int_ll : forall tl tr : T, dsubda (TIsect tl tr) tl
| dsubda_int_lr : forall tl tr : T, dsubda (TIsect tl tr) tr
| dsubda_dist : forall tl trl trr : T, dsubda (TIsect tl (TUni trl trr)) (TUni (TIsect tl trl) (TIsect tl trr))
.
End Integrator.
Requirements
The user-provided defintions and requirements of Section 4 (Requirements 7 - 12) are collected in the module type Intersector (based on definitions provided by an instantiation of Traditional). A user of our framework first instantiates the module type Traditional to provide the basic proofs about the type system, and then uses that to instantiate Intersector to provide our framework with proofs of the necessary requirements to prove the Lemmas and Theorems of Section 4.Declarative Subtyping Extension
extension represents the set of additional subtyping axioms used for the definition of Extended Subtyping in Figure 5. As mentioned above, extension will be used as the set of assumptions for dsubda such that dsubda (@DPremise) extension is the definition of Extended Subtyping.Requirement 7: Intersector Completeness
The integrator Integrate intersect incorporates all the extensions in extension into traditional declarative subtyping.Parameter IntersectorCompleteness : forall tl tr : T, extension tl tr -> dsub (Integrate intersect tl) tr.
Requirement 8: Intersector Soundness
The intersector intersect integrates nothing more than what the extensions in extension can deduce via extended subtyping.Requirement 9: Measure Preservation
The integrator Integrate intersect preserves the termination measure. The paper technically only implies that the reflexive closure of mlt can be used here, so allowing the reflexive transitive closure here is a weaker requirement than in the paper.Parameter MeasurePreservation : forall tl tr : T, clos_refl_trans M mlt (m (Integrate intersect tl) tr) (m tl tr).
Requirement 10: Literal Dereliction
The intersector 'adds information' to a type, i.e. the result of applying the intersector to a list of literals is a traditional reductive subtype of the straightforward intersection of of those literals.The Intersected Predicate
intersected is the intersected predicate φ, as in the paper (Section 4.5.2).Requirement 11: Intersector Integrated
The result of applying the intersector to a list of literals counts as Integrated using the provided intersected predicate.Requirement 12: Literal Promotion
For every two lists of literals ls and ls', and list of reductive literal subtyping rules rs ⊆ RRule such thatParameter LiteralPromotion : forall (ls ls' : list Lit) (rs : list (sig2T RRule)), Forall (fun l' : Lit => Exists (fun r : (sig2T RRule) => proj2T2 r = l') rs) ls' -> incl (map proj2T1 rs) ls -> intersected ls -> exists rs' : list (sig2T RRule), Exists_Intersection (fun ls'' => ls'' = map proj2T2 rs' /\ incl (map proj2T1 rs') ls /\ Forall (fun r' : sig2T RRule => forall tl tr :T, RPremise (proj2V r') tl tr -> rsubam (@RPremise) (fun tl' tr' => Exists (fun r => RPremise (proj2V r) tl' tr') rs) tl tr) rs') (intersect ls').
End Intersector.
Sums of Products
The core component of our proof of the main Lemmas and Theorems in this paper is an adjunction based on a sums-of-products representation of types in disjunctive normal form. Here, (in UIType potentially nested) intersections (products) of literals are represent just as lists of literals, and unions (sums) of those intersections are just lists of them, i.e. lists of lists of literals, called sops. Then, the bottom type is represented by the empty union, i.e. [], and the top type is represented by an empty intersection, which has to be wrapped in a singleton union, i.e. [[]].Section SumOfProducts.
Variable Lit : Type.
Notation T := (UIType Lit).
Notation sop := (list (list Lit)).
Fixpoint SopIntegrate (intersect : list Lit -> sop) (t : T) : sop :=
match t with
| TBot => []
| TTop => intersect []
| TUni tl tr => (SopIntegrate intersect tl) ++ (SopIntegrate intersect tr)
| TIsect tl tr => SopIntegrate (fun l => SopIntegrate (fun l' => intersect (l ++ l')) tr) tl
| TLit l => intersect [l]
end.
Definition SopIntegrated (intersected : list Lit -> Prop) : sop -> Prop :=
Forall intersected.
We can convert between Ts and sops using ui2sop and sop2ui.
Since all sops are in disjunctive normal form, but not necessarily all Ts are, ui2sop is essentially implemented as (sop-)dnf using the identity function on lists of literals.
sop2ui on the other hand simply creates some biased equivalent of a sop by first biasing the intersections using Intersect and then unioning the results.
The predicate ProductOfLiterals holds for a given t : T if that t is just a nesting of intersections with either TTop or some literal at all of its leaves.
Similarly, the predicate SumOfProducts holds for a given t : T if that t is a nesting of unions of either TBot or types for which ProductOfLiterals holds.
Definition ui2sop : T -> sop :=
SopIntegrate (fun i => [i]).
Definition sop2ui : sop -> T
:= fold_right (fun i => TUni (Intersect i)) TBot.
Inductive ProductOfLiterals : T -> Prop :=
| POL_top : ProductOfLiterals TTop
| POL_lit : forall l : Lit, ProductOfLiterals (TLit l)
| POL_int : forall tl tr : T, ProductOfLiterals tl -> ProductOfLiterals tr -> ProductOfLiterals (TIsect tl tr)
.
Inductive SumOfProducts : T -> Prop :=
| SOP_bot : SumOfProducts TBot
| SOP_uni : forall tl tr : T, SumOfProducts tl -> SumOfProducts tr -> SumOfProducts (TUni tl tr)
| SOP_prod : forall t: T, ProductOfLiterals t -> SumOfProducts t
.
While for any sop s, ui2sop (sop2ui s) = s (proven as Lemma ui2sop_sop2ui in the infrastructure file later), the converse is not true for sop2ui (ui2sop t) for all t : Ts, not even when SumOfProducts (or ProductOfLiterals) holds for t.
The reason is that even if t is already in DNF, it is (a) not necessarily balanced in the same way as the the output of sop2ui, and (b) may contain superfluous leaves of TTop and TBot that are eliminated during DNF-ing.
Hence, the predicates polof and sopof relate lists of literals and sops with all Ts that might convert to them and are ProductOfLiterals or SumOfProducts, respectively (i.e. the equivalence is still syntactic in that the order and number of literals is preserved, but superfluous TTops and TBots are ignored).
Inductive polof : list Lit -> T -> Prop :=
| polof_lit (l : Lit) : polof [l] (TLit l)
| polof_top : polof [] TTop
| polof_int (lsl lsr : list Lit) (tl tr : T) : polof lsl tl -> polof lsr tr -> polof (lsl ++ lsr) (TIsect tl tr)
.
Inductive sopof : sop -> T -> Prop :=
| sopof_pol (ls : list Lit) (t : T) : polof ls t -> sopof [ls] t
| sopof_bot : sopof [] TBot
| sopof_uni (sl sr : sop) (tl tr : T) : sopof sl tl -> sopof sr tr -> sopof (sl ++ sr) (TUni tl tr)
.
While ui2sop based on SopIntegrate is a nice instantiation of SopIntegrate, it is sometimes a little bit unwieldy.
Another possible way of just getting the DNF of a type is to do it recursively, and using a meet function to intersect two existing sops.
ui2sop_meet is equivalent to ui2sop (proven in Section4_Infrastructure.v).
Definition meet (sl sr : sop) : sop := flat_map (fun ls => map (fun ls' => ls ++ ls') sr) sl.
Fixpoint ui2sop_meet (t : T) : sop :=
match t with
| TTop => [[]]
| TBot => []
| TUni tl tr => (ui2sop_meet tl) ++ (ui2sop_meet tr)
| TIsect tl tr => meet (ui2sop_meet tl) (ui2sop_meet tr)
| TLit l => [[l]]
end.
Lastly, we define a sop-only version of uisub (ssub), and mixed versions of uisub and uirec (ruisub/suisub and ruirec/suirec, respectively).
Definition ssub (R : Lit -> Lit -> Prop) (sl sr : sop) : Prop :=
Forall (fun il => Exists (fun ir => Forall (fun lr => Exists (fun ll => R ll lr) il) ir) sr) sl.
Inductive ruisub {P : Lit -> Prop} : T -> Prop :=
| rui_lit (l : Lit) : P l -> ruisub (TLit l)
| rui_top : ruisub TTop
| rui_int (tl tr : T) : ruisub tl -> ruisub tr -> ruisub (TIsect tl tr)
| rui_uni_l (tl tr : T) : ruisub tl -> ruisub (TUni tl tr)
| rui_uni_r (tl tr : T) : ruisub tr -> ruisub (TUni tl tr).
Definition suisub (R : Lit -> Lit -> Prop) (sl : sop) (tr : T) :=
Forall (fun il => ruisub (fun lr => Exists (fun ll => R ll lr) il) tr) sl.
Definition ruirec (P : Lit -> Prop) (t : T) : Prop := Forall P (lits t).
Definition suirec (R : Lit -> Lit -> Prop) (sl : sop) (tr : T) :=
Forall (fun il => ruirec (fun lr => Forall (fun ll => R ll lr) il) tr) sl.
End SumOfProducts.
Infrastructure
At this point, there are a few definitions and lemmas that are not central to understanding the proofs and in some sense self-explanatory, and therefore omitted from this document. In particular, there are many relatively obvious equivalences and other relationships between previously defined functions and predicates on Ts and their sop-equivalents. Please see Section4_Infrastructure.v for those definitions and lemmas.Proof of Decidability of Extended Subtyping (Section4_Proofs.v)
The main Theorem of this section (Decidability of Extended Subtyping) is proven along the path set out in the paper, though due to the use of the SOP representation the formulation of some of the intermediate Lemmas has changed (all Lemmas in the paper are proven here, but they may not be part of the final proof in their form in the paper). The proof proceeds roughly as follows:- We define sop versions of most things given by an Intersector module
- We prove induction principles for sops that include integrating the LHS of premises of literal rules.
- We define integrated subtyping and prove Lemmas similar to those in the paper about it
- We prove equivalence of integrated subtyping and extended subtyping
- We prove decidability of integrated subtyping
- We prove that if an equivalent decidable relation exists, extended subtyping is decidable, and instantiate this lemma with integrated subtyping and the above proofs, proving the main Theorem.
SOP Intersectors
We define sopintersect as simply the user-defined intersector combined with ui2sop. Because any result of intersect is required to be in DNF, we can proof that the sopof relation holds between the results of sopintersect and intersect (sopintersect_sopof_intersect). Several intermediate lemmas build up to suisub_SopIntegrate_sopintersect_uisub_Integrate_intersect, which lets us translate subtyping proofs involving the SOP Integrator to subtyping proofs involving the Integrator as presented in the paper, and vice versa. This is a quite central part of moving between the two representations in the rest of this section's proofs.Module Integrated (M_traditional : Traditional) (M_intersector : Intersector M_traditional).
Module M_sopinfrastructure := SOP_Infrastructure M_traditional.
Definition sopintersect : list Lit -> list (list Lit) := fun ls => ui2sop (intersect ls).
Lemma sopintersect_sopof_intersect : forall ls : list Lit, sopof (sopintersect ls) (intersect ls).
Lemma suisub_sopof_uisub (R : Lit -> Lit -> Prop) : forall (sl : sop) (tl t : T), sopof sl tl -> (suisub R sl t <-> uisub R tl t).
Lemma SopIntegrate_sopof_Integrate (f : list Lit -> sop) (g : list Lit -> T) (Hfg : forall ls : list Lit, sopof (f ls) (g ls)) : forall t : T, sopof (SopIntegrate f t) (Integrate g t).
Lemma suisub_SopIntegrate_uisub_Integrate (R : Lit -> Lit -> Prop) (f : list Lit -> sop) (g : list Lit -> T) (Hfg : forall ls : list Lit, sopof (f ls) (g ls)) : forall (tl t : T), suisub R (SopIntegrate f tl) t <-> uisub R (Integrate g tl) t.
Lemma suisub_SopIntegrate_sopintersect_uisub_Integrate_intersect (R : Lit -> Lit -> Prop) : forall tl t : T, suisub R (SopIntegrate sopintersect tl) t <-> uisub R (Integrate intersect tl) t.
Lemma SopIntersectorCompleteness : forall tl tr : T, extension tl tr -> dsub (sop2ui (SopIntegrate sopintersect tl)) tr.
Lemma rssub_refl : forall s : sop, ssub (lsub (@RPremise) rsub) s s.
Lemma SopIntersectorSoundness : forall ls : list Lit, esub (Intersect ls) (sop2ui (sopintersect ls)).
Requirement 9: Measure Preservation (No SOP Version)
The requirements on the behavior of the measure function m are very weak - we expect that in most cases, the measures of unions and intersections will be joins of the measures of their components, but that is not required. Hence, the connections of measures of a type in DNF with their original are hard to establish, even more so if additionally, and intersector mangles types. We can avoid all of this by simply using the original measure preservation requirement whenever we need to prove that some recursion terminates.Requirement 10: Literal Derelicton (SOP Version)
Lemma SopLiteralPromotion : forall ls : list Lit, intersected ls -> forall rs : list (sig2T RRule), incl (map proj2T1 rs) ls -> Exists (fun ls' => Forall (fun lr => Exists (fun ll => lsub (@RPremise) (rsubam (@RPremise) (fun tl tr : T => Exists (fun r => RPremise (proj2V r) tl tr) rs)) ll lr) ls) ls') (sopintersect (map proj2T2 rs)).
Lemma suirec_suisub_suisub (R R' R'' : Lit -> Lit -> Prop) (sl : sop) (tr : T) : (forall ll lr : Lit, R ll lr -> R' ll lr -> R'' ll lr) -> suirec R sl tr -> suisub R' sl tr -> suisub R'' sl tr.
Induction Principles
Next, we prove the induction principles irec and irec_alt. irec is really only used to prove irec_alt, which is simliar to uirec_alt, except that it includes the Integrator and is (partially) about sops. As sops make it easy to recurse down to pairings of literals, the measure litlt we use to prove these induction principles is a measure between pairs of literals; and essentially defined as the restriction of (the transitive closure of) mlt to just the literal cases. Since lrec and irec are defined largely using a mixed sop/T relation, we define the intermediate lemma mlt_recurse, which, together with a number of other straightforward lemmas about the relationship between InType and sops also lets us drill down to the literal cases in Ts.
Definition litlt (lpl lpr : Lit * Lit) : Prop := mltt (m (TLit (fst lpl)) (TLit (snd lpl))) (m (TLit (fst lpr)) (TLit (snd lpr))).
Lemma litlt_wf : well_founded litlt.
Lemma mlt_recurse : forall (tl tr : T) (tl' tr' : T), InType tl' tl -> InType tr' tr -> clos_refl_trans M mlt (m tl' tr') (m tl tr).
Lemma irec (R : Lit -> Lit -> Prop) : (forall ll lr : Lit, (forall (r : RRule ll lr) (tl tr : T), RPremise r tl tr -> suirec R (SopIntegrate sopintersect tl) tr) -> R ll lr) -> forall ll lr : Lit, R ll lr.
Lemma irec_alt (RL : Lit -> Lit -> Prop) (RT : sop -> T -> Prop) : (forall ll lr : Lit, (forall (r : RRule ll lr) (tl tr : T), RPremise r tl tr -> RT (SopIntegrate sopintersect tl) tr) -> RL ll lr) -> (forall (sl : sop) (tr : T), suirec RL sl tr -> RT sl tr) -> forall (sl : sop) (tr : T), RT sl tr.
Lemma litlt_wf : well_founded litlt.
Lemma mlt_recurse : forall (tl tr : T) (tl' tr' : T), InType tl' tl -> InType tr' tr -> clos_refl_trans M mlt (m tl' tr') (m tl tr).
Lemma irec (R : Lit -> Lit -> Prop) : (forall ll lr : Lit, (forall (r : RRule ll lr) (tl tr : T), RPremise r tl tr -> suirec R (SopIntegrate sopintersect tl) tr) -> R ll lr) -> forall ll lr : Lit, R ll lr.
Lemma irec_alt (RL : Lit -> Lit -> Prop) (RT : sop -> T -> Prop) : (forall ll lr : Lit, (forall (r : RRule ll lr) (tl tr : T), RPremise r tl tr -> RT (SopIntegrate sopintersect tl) tr) -> RL ll lr) -> (forall (sl : sop) (tr : T), suirec RL sl tr -> RT sl tr) -> forall (sl : sop) (tr : T), RT sl tr.
Integrated Subtyping
The recursive part of Integrated Subtyping in the paper is defined to be like reductive subtyping, except that the literal rule applies the Integrator to the LHS of every premise. We model this by giving rsubf a different Premise argument, IPremise, which applies the Integrator to the LHS of every RPremise. isub' is therefore the recursive part of Integrated Subtyping (≤⊓), and isub the outer part (≤⊓). rssub and issub are the sop counterparts of rsub and isub', respectively.Inductive IPremise {ll lr : Lit} (r : RRule ll lr) : T -> T -> Prop :=
ipremise (tl tr : T) : RPremise r tl tr -> IPremise r (Integrate intersect tl) tr.
Definition isub' : T -> T -> Prop :=
rsubf (@IPremise).
Definition isub (tl : T) : T -> Prop :=
isub' (Integrate intersect tl).
Definition rssub : sop -> sop -> Prop :=
ssub (lsub (@RPremise) (rsub)).
Definition issub : sop -> sop -> Prop :=
ssub (lsub (@IPremise) isub').
Lemma 1: Integrated Soundness
Integrated Subtyping implies Extended Subtyping (proven using helper Lemma IntegratorSoundness, which in turn extends the IntersectorSoundness Requirement to Integrators)Lemma IntegratorSoundness : forall t : T, esub t (Integrate intersect t).
Lemma IntegratedSoundness : forall tl tr : T, isub tl tr -> esub tl tr.
Lemma 2: Integrated Decidability
The Integrated Subtyping Relation relation ≤⊓ is decidable.Lemma 3: Dereliction
The result of integrating a type is a subtype of the original type. After a few straightforward intermediate Lemmas, we first proof dereliction on sops (sopdereliction, and then based on that, the Dereliction Lemma as in the paper.Lemma suisub_uisub_trans (Rl Rm Rr : Lit -> Lit -> Prop) {sl : sop} (tm : T) {tr : T} : (forall ll lm lr : Lit, Rl ll lm -> Rr lm lr -> Rm ll lr) -> suisub Rl sl tm -> uisub Rr tm tr -> suisub Rm sl tr.
Lemma dereliction_lits : forall (ls ls' : list Lit), rssub [ls] [ls'] -> suisub (lsub (@RPremise) rsub) (sopintersect ls) (sop2ui [ls']).
Lemma sopdereliction (tl tr : T) : rsub tl tr -> rsub (sop2ui (SopIntegrate sopintersect tl)) tr.
Lemma Dereliction (tl tr : T) : rsub tl tr -> rsub (Integrate intersect tl) tr.
Lemma 4: Integrator Integrated
Proofs of both the sop and regular version of Lemma 4. None of these proofs depend on each other, but we mostly use the sop version in the rest of the proof.Lemma SopIntegratorIntegrated : forall (t : T), SopIntegrated intersected (SopIntegrate sopintersect t).
Lemma IntegratorIntegrated : forall t : T, Integrated intersected (Integrate intersect t).
Lemma 5: Promotion
If the LHS of a reductive subtyping proof is Integrated, then the reductive subtyping also holds after Integrating the RHS.Lemma LiteralPromotion' : forall ls : list Lit, intersected ls -> forall rs : list (sig2T RRule), incl (map proj2T1 rs) ls -> rsubam (@RPremise) (fun pl pr => Exists (fun r => match r with exist2T rl rr r => RPremise r pl pr end) rs) (Intersect ls) (sop2ui (sopintersect (map proj2T2 rs))).
Lemma ssub_isects_litrules : forall (lsl lsr : list Lit), rssub [lsl] [lsr] -> exists lrt : list (sig2T RRule), map proj2T2 lrt = lsr /\ incl (map proj2T1 lrt) lsl /\ Forall (fun rt => forall tl tr : T, RPremise (proj2V rt) tl tr -> rsub tl tr) lrt.
Lemma sui_promotion (sl : sop) (tr : T) : SopIntegrated intersected sl -> suisub (lsub (@RPremise) (rsub)) sl tr -> ssub (lsub (@RPremise) (rsub)) sl (SopIntegrate sopintersect tr).
Lemma Promotion : forall tl tr : T, Integrated intersected tl -> rsub tl tr -> rsub tl (Integrate intersect tr).
Lemmas 6 and 7: Integrated Monotonicity and Integrated Assumptions
The first three lemmas ssub_suisub_trans, lsub_rsubam_rsubf_trans, and lsub_rsubf_rsubam_trans are concerned with composing subtyping proofs, of various kinds, which is necessary for proving Monotonicity. Since rsubam is reductive subtyping with Assumptions and Monotonicity, integrated_assumptions' and IntegratedAssumptions already integrate the Integrated Monotonicity Lemma; thus the surface-level Lemma IntegratedMonotonicity follows from IntegratedAssumptions in this proof, while at the core, monotonicity is required to prove IntegratedAssumptions.Lemma ssub_suisub_trans (Rl Rm Rr : Lit -> Lit -> Prop) {sl : sop} (sm : sop) {tr : T} : (forall ll lm lr : Lit, Rl ll lm -> Rr lm lr -> Rm ll lr) -> ssub Rl sl sm -> suisub Rr sm tr -> suisub Rm sl tr.
Lemma lsub_rsubam_rsubf_trans (A : T -> T -> Prop) (ll lm lr : Lit) : lsub (@RPremise) (rsubam (@RPremise) A) ll lm -> lsub (@RPremise) (rsub) lm lr -> lsub (@RPremise) (rsubam (@RPremise) A) ll lr.
Lemma lsub_rsubf_rsubam_trans (A : T -> T -> Prop) (ll lm lr : Lit) : lsub (@RPremise) (rsub) ll lm -> lsub (@RPremise) (rsubam (@RPremise) A) lm lr -> lsub (@RPremise) (rsubam (@RPremise) A) ll lr.
Lemma integrated_assumptions' (A : T -> T -> Prop) (sl : sop) (tl tr : T) : SopIntegrated intersected sl -> rsub (sop2ui sl) tl -> rsubam (@RPremise) A tl tr -> (forall tl tr : T, A tl tr -> isub tl tr) -> isub' (sop2ui sl) tr.
Lemma IntegratedAssumptions (A : T -> T -> Prop) (tl tr : T) : rsubam (@RPremise) A tl tr -> (forall tl tr : T, A tl tr -> isub tl tr) -> isub tl tr.
Lemma IntegratedMonotonicity : forall t1 t2 t3 t4 : T, rsub t1 t2 -> isub t2 t3 -> rsub t3 t4 -> isub t1 t4.
Lemma 8: Integrated Promotion
If Integrated Subtyping holds between two types, it also holds after applying the Integrator to the RHS.Lemma issub_promotion (sl sr : sop) : Forall intersected sl -> issub sl sr -> issub sl (flat_map sopintersect sr).
Lemma isuisub_promotion (sl : sop) (tr : T) : Forall intersected sl -> suisub (lsub (@IPremise) isub') sl tr -> issub sl (SopIntegrate sopintersect tr).
Lemma integrated_promotion (tl tr : T) : isub tl tr -> isub tl (sop2ui (SopIntegrate sopintersect tr)).
Lemma uisub_dnf_r {R : Lit -> Lit -> Prop}: forall tl tr : T, uisub R tl (sop2ui (ui2sop tr)) -> uisub R tl tr.
Lemma IntegratedPromotion : forall tl tr : T, isub tl tr -> isub tl (Integrate intersect tr).
Lemma 10: Declarative-to-Integrated Literal Conversion
Straightforward proof based on IntegratedAssumptions.Lemma DeclarativeToIntegratedLiteralConversion : forall {ll lr : Lit} (r : DRule ll lr), (forall tl tr : T, DPremise r tl tr -> isub tl tr) -> isub (TLit ll) (TLit lr).
Lemma 11: Integrated Transitivity
As before, we need to be able to compose assumptions of literal subtyping. The complication here is that the the LHS of the RHS premise is integrated, while the RHS of the LHS premise is not. Thus, we need to promote the LHS premise. Lastly, IntegratedAssumptions lets us convert the rsubam proofs of LiteralTransitivity into the isub proofs we need.Lemma 12: Integrated Completeness
Mostly applying the previous lemmas, some extra work to cover distributivity.Equivalence of Integrated and Extended Subtyping
Simply combines IntegratedSoundness and IntegratedCompleteness.MAIN THEOREM, Part 1: Decidability of Extended Subtyping
We first prove the Lemma dsub_ext_dec, which says that if there is a relation that is equivalent to Extended Subtyping and decidable, then Extended Subtyping is decidable. We instantiate this Lemma with isub in dsuba_ext_dec_isub' and use that to prove the main theorem, namely that Integrated Subtyping provides a decision procedure for Extended Subtyping.Lemma dsuba_ext_dec : forall (R : T -> T -> Prop), (forall tl tr : T, R tl tr <-> esub tl tr) -> (forall tl tr : T, {R tl tr} + {~ R tl tr}) -> forall tl tr : T, {esub tl tr} + {~ esub tl tr}.
Definition dsuba_ext_dec_isub' : forall tl tr : T, {esub tl tr} + {~ esub tl tr} := dsuba_ext_dec isub isub_esub IntegratedDecidability.
Theorem DecidabilityOfExtendedSubtyping : forall tl tr : T, {esub tl tr} + {~ esub tl tr}.
Beginning of MAIN THEOREM, Part 2: Optimized Decision Procedure for Extended Subtyping
The decision procedure for isub is somewhat inefficient. As it is defined, it first tries to recurse down into the LHS type as far as possible before ever touching the RHS type. However, it is well-known that a subtyping algorithm for union and intersection types can prioritize certain rules over others. In particular, the LHS-union and RHS-intersection rules can (and should) always be applied before any other rules, because none of these rules makes a choice that might have to be back-tracked later. The LHS-intersection and RHS-union rules, on the other hand, need to make a choice and might have to back-track later because we tried the wrong subtyping first. This means that normally, one might have to try out all four combinations of of potential subtypings if one needs to decide whether τ1∩τ2 <: τ3∪τ4. However, because we know that the LHS is in DNF, we know that all we can do on the LHS is to find a number of matching Literals for whatever is on the RHS. That is, there is no way that the proof search will branch in a way such that different branches will choose differently between τ3 and τ4 on the RHS. This means that we can prioritize the RHS-union rule in those cases. The result is a deterministic algorithm that minimizes the search space for subtyping proofs.- ouisub says all subtyping proofs need to descend through all unions on the LHS down to either bottom or a ProductOfLiterals (i.e. a TIsect, TTop, or TLit) first.
- Then, ouisub_r says all subtyping proofs needs to descend through the RHS down to either a TTop or a literal TLit
- Only then, ouisub_l allows recursing through intersections on the LHS until we find a literal that is in a literal subtyping relation with an RHS literal
Inductive ouisub_l {R : Lit -> Lit -> Prop} : T -> Lit -> Prop :=
| oui_lit (ll lr : Lit) : R ll lr -> ouisub_l (TLit ll) lr
| oui_int_l (tl tr : T) (l : Lit) : ouisub_l tl l -> ouisub_l (TIsect tl tr) l
| oui_int_r (tl tr : T) (l : Lit) : ouisub_l tr l -> ouisub_l (TIsect tl tr) l
.
Inductive ouisub_r {R : Lit -> Lit -> Prop} : T -> T -> Prop :=
| oui_poll (tl : T) (lr : Lit) : ouisub_l R tl lr -> ouisub_r tl (TLit lr)
| oui_top (t : T) : ouisub_r t TTop
| oui_int (t tl tr : T) : ouisub_r t tl -> ouisub_r t tr -> ouisub_r t (TIsect tl tr)
| oui_uni_l (t tl tr : T) : ouisub_r t tl -> ouisub_r t (TUni tl tr)
| oui_uni_r (t tl tr : T) : ouisub_r t tr -> ouisub_r t (TUni tl tr)
.
Inductive ouisub {R : Lit -> Lit -> Prop} : T -> T -> Prop :=
| oui_polr (tl tr : T) : ProductOfLiterals tl -> ouisub_r R tl tr -> ouisub tl tr
| oui_bot (t : T) : ouisub TBot t
| oui_uni (tl tr t : T) : ouisub tl t -> ouisub tr t -> ouisub (TUni tl tr) t
.
Inductive orsubf (RPremise : forall ll lr : Lit, RRule ll lr -> T -> T -> Prop) : T -> T -> Prop :=
| ORsubf : forall tl tr : T, ouisub (lsub RPremise (orsubf RPremise)) tl tr -> orsubf RPremise tl tr
.
orsubf_ouisub is equivalent to rsubf_uisub
Lemma orsubf_ouisub {RPremise : forall ll lr : Lit, RRule ll lr -> T -> T -> Prop} : forall tl tr : T, orsubf RPremise tl tr -> ouisub (lsub RPremise (orsubf RPremise)) tl tr.
Some helper Lemmas
Lemma ouisub_int_l {R : Lit -> Lit -> Prop} : forall tl tr t : T, ouisub R (TIsect tl tr) t -> ouisub_r R (TIsect tl tr) t.
Lemma ouisub_top_l {R : Lit -> Lit -> Prop} : forall t : T, ouisub R TTop t -> ouisub_r R TTop t.
Lemma ouisub_r_top_lit {R : Lit -> Lit -> Prop} : forall l : Lit, ouisub_r R TTop (TLit l) -> False.
Lemma ouisub_r_uni_l {R : Lit -> Lit -> Prop} : forall tl tr t : T, ouisub_r R (TUni tl tr) t -> ouisub_r R tl t /\ ouisub_r R tr t.
Lemma ouisub_uni_l {R : Lit -> Lit -> Prop} : forall tl tr t : T, ouisub R (TUni tl tr) t -> ouisub R tl t /\ ouisub R tr t.
Lemma ouisub_ProductOfLiterals {R : Lit -> Lit -> Prop} : forall tl tr : T, ProductOfLiterals tl -> ouisub R tl tr -> ouisub_r R tl tr.
Lemma ouisub_r_lit_r {R : Lit -> Lit -> Prop} : forall (tl : T) (lr : Lit), ouisub_r R tl (TLit lr) -> ouisub_l R tl lr.
The definition of ouisub_dec follows the prioritized proof-search method description above.
Recursive calls have the form (destruct IH _ _ _), and prioritize in order
In the last case, there are inner recursions to go over all possible rules between the two literals, and for each such rule (while no applicable one has been found), all of its premses.
For a somewhat easier-to-read version of the algorithm, check the result of extracting this function to ML, listed below (or check "OptimizedSubtyping.ml" after compiling/running this file once).
Definition ouisub_dec {Premise : forall ll lr : Lit, RRule ll lr -> T -> T -> Prop} (premises_for_rule : forall {ll lr : Lit} (r : RRule ll lr), { rpremises : list (prod (T) (T)) | forall pl pr : T, Premise ll lr r pl pr <-> In (pair pl pr) rpremises }) (HMlit : forall {ll lr : Lit} (r : RRule ll lr) (tl tr : T), Premise ll lr r tl tr -> progress_measure (tl, tr) (TLit ll, TLit lr) /\ SumOfProducts tl) : forall tl tr : T, SumOfProducts tl -> {orsubf Premise tl tr} + {~ orsubf Premise tl tr}.
Defined.
Extraction Language Ocaml.
Extraction "OptimizedSubtyping.ml" ouisub_dec.
The result of the above extraction is shown below (check "OptimizedSubtyping.ml" after compiling/running this file once).
The inner recursive function that is defined on pairs because that is how the recursion principle works - the pair consists of the two arguments to the subtyping algorithm.
What we can see in this definition is that we first match on the left argument and then potentially match on the right argument, recursing into first Unions on the left, then Unions and Intersections on the right, and finally Intersections on the right, until we either find an easy case involving Top or Bottom or two Literals.
In the latter case, we find all the rules that might apply for the two literals in question, and try to see if we can find one for which all premises hold.
The return values Left and Inleft _ here represent true, while the return values Right and Inright represent false.
Similar to the definition of isub based on rsubf, we define oisub based on orsubf, and prove it's decidability (oisub_dec).
let ouisub_dec premises_for_rule tl tr = let rec fix_F = function | Pair (tl0, tr0) -> (match tl0 with | TTop -> (match tr0 with | TTop -> Left | TUni (trl, trr) -> let s = fix_F (Pair (TTop, trl)) in (match s with | Left -> Left | Right -> fix_F (Pair (TTop, trr))) | TIsect (trl, trr) -> let s = fix_F (Pair (TTop, trl)) in (match s with | Left -> fix_F (Pair (TTop, trr)) | Right -> Right) | _ -> Right) | TBot -> Left | TUni (tll, tlr) -> let s = fix_F (Pair (tll, tr0)) in (match s with | Left -> fix_F (Pair (tlr, tr0)) | Right -> Right) | TIsect (tll, tlr) -> (match tr0 with | TTop -> Left | TBot -> Right | TUni (trl, trr) -> let s = fix_F (Pair ((TIsect (tll, tlr)), trl)) in (match s with | Left -> Left | Right -> fix_F (Pair ((TIsect (tll, tlr)), trr))) | TIsect (trl, trr) -> let s = fix_F (Pair ((TIsect (tll, tlr)), trl)) in (match s with | Left -> fix_F (Pair ((TIsect (tll, tlr)), trr)) | Right -> Right) | TLit lr -> let s = fix_F (Pair (tll, (TLit lr))) in (match s with | Left -> Left | Right -> fix_F (Pair (tlr, (TLit lr))))) | TLit ll -> (match tr0 with | TTop -> Left | TBot -> Right | TUni (trl, trr) -> let s = fix_F (Pair ((TLit ll), trl)) in (match s with | Left -> Left | Right -> fix_F (Pair ((TLit ll), trr))) | TIsect (trl, trr) -> let s = fix_F (Pair ((TLit ll), trl)) in (match s with | Left -> fix_F (Pair ((TLit ll), trr)) | Right -> Right) | TLit lr -> let x0 = M_traditional.coq_SyntaxDirectedness_Rules ll lr in let exists_applicable_rule = let rec f = function | Nil -> Inright | Cons (y, l0) -> let x1 = premises_for_rule ll lr y in let all_premises_hold = let rec f0 = function | Nil -> Left | Cons (y0, l2) -> let current_premise_holds = fix_F y0 in (match current_premise_holds with | Left -> f0 l2 | Right -> Right) in f0 x1 in (match all_premises_hold with | Left -> Inleft y | Right -> f l0) in f x0 in (match exists_applicable_rule with | Inleft _ -> Left | Inright -> Right))) in fix_F (Pair (tl, tr))
Definition oisub (tl tr : T) := orsubf (@IPremise) (Integrate intersect tl) tr.
Lemma oisub_dec : forall tl tr : T, {oisub tl tr} + {~ oisub tl tr}.
If the LHS type is in DNF, uisub and ouisub are equivalent (uisub_ouisub).
This is a helper lemma for proving the equivalence of isub and oisub in oisub_isub
Lemma uisub_ouisub {R : Lit -> Lit -> Prop} : forall tl tr : T, SumOfProducts tl -> (uisub R tl tr <-> ouisub R tl tr).
Lemma oisub_isub : forall tl tr : T, oisub tl tr <-> isub tl tr.
From the equivalence of oisub and isub, and the equivalence of isub and esub, it follows that oisub and esub are equivalent, too
Actual MAIN THEOREM, Part 2: Optimized Decidability of Extended Subtyping
As oisub is decidable and equivalent to esub, esub is decidable.Theorem OptimizedDecidabilityOfExtendedSubtyping : forall tl tr : T, {esub tl tr} + {~ esub tl tr}.
End Integrated.
Composability (Section5.v)
Some Intersectors can be easily composed. The criterion for this composability is IntersectedPreservation, i.e. that, given two Intersectors, the second Intersector's intersect function does not invalidate the intersectedness predicate of the first Intersector. The module type Composability lets a user provide a proof of that for a given pair of Intersectors.Module Type Composability (M_traditional : Traditional) (M_intersector_l M_intersector_r : Intersector M_traditional).
Parameter IntersectedPreservation : forall ls : list Lit, M_intersector_l.intersected ls -> Integrated M_intersector_l.intersected (M_intersector_r.intersect ls).
End Composability.
Composition
Given two Intersectors Il and Ir and a proof of IntersectedPreservation (i.e. Composability) between the two, this module proves all the necessary Requirements for a new Intersector module where intersect is defined as Integrate Ir.intersect (Il.intersect ls) and extension tl tr is defined as Il.extension tl tr \/ Ir.extension tl tr. Requirements 1 - 6 are already proven by Traditional and do not change when Intersectors are composed. Requirements 7 - 12 are proved here for the new definitions of intersect, intersected and extension. This satisfies the "Intersector Composability" Theorem in the paper.Module Composition (M_traditional : Traditional) (M_intersector_l M_intersector_r : Intersector M_traditional) (M_composability : Composability M_traditional M_intersector_l M_intersector_r) <: Intersector M_traditional.
Module M_traditional_dec := TraditionalDec M_traditional.
Module Intl := Integrated M_traditional M_intersector_l.
Module Intr := Integrated M_traditional M_intersector_r.
Module Il := M_intersector_l.
Module Ir := M_intersector_r.
Definitions of ⊓, φ, and extension
Straightfoward composition of their respective counterparts in the two given Intersector modules, as described in the paper.Definition intersect (ls : list Lit) := Integrate Ir.intersect (Il.intersect ls).
Definition intersected (ls : list Lit) := Il.intersected ls /\ Ir.intersected ls.
Definition extension (tl tr : T) : Prop := Il.extension tl tr \/ Ir.extension tl tr.
Lemma IntersectorCompleteness : forall tl tr : T, extension tl tr -> dsub (Integrate intersect tl) tr.
Lemma rsubfi_refl : forall t : T, rsubf (@IPremise) t t.
Lemma IntersectorSoundness : forall ls : list Lit, dsubda (@DPremise) extension (Intersect ls) (intersect ls).
Lemma MeasurePreservation : forall tl tr : T, clos_refl_trans M mlt (m (Integrate intersect tl) tr) (m tl tr).
Lemma LiteralPromotion : forall (ls ls' : list Lit) (rs : list (sig2T RRule)), Forall (fun l' : Lit => Exists (fun r : (sig2T RRule) => proj2T2 r = l') rs) ls' -> incl (map proj2T1 rs) ls -> intersected ls -> exists rs' : list (sig2T RRule), Exists_Intersection (fun ls'' => ls'' = map proj2T2 rs' /\ incl (map proj2T1 rs') ls /\ Forall (fun r' : sig2T RRule => forall tl tr :T, RPremise (proj2V r') tl tr -> rsubam (@RPremise) (fun tl' tr' => Exists (fun r => RPremise (proj2V r) tl' tr') rs) tl tr) rs') (intersect ls').
End Composition.
Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (311 entries) |
Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |
Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10 entries) |
Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (86 entries) |
Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (97 entries) |
Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (28 entries) |
Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (20 entries) |
Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (9 entries) |
Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (38 entries) |
Global Index
C
Composability [module, in Section5]Composability.IntersectedPreservation [axiom, in Section5]
Composition [module, in Section5]
Composition.extension [definition, in Section5]
Composition.Il [module, in Section5]
Composition.intersect [definition, in Section5]
Composition.intersected [definition, in Section5]
Composition.IntersectorCompleteness [lemma, in Section5]
Composition.IntersectorIntegrated [lemma, in Section5]
Composition.IntersectorSoundness [lemma, in Section5]
Composition.Intl [module, in Section5]
Composition.Intr [module, in Section5]
Composition.Ir [module, in Section5]
Composition.LiteralDereliction [lemma, in Section5]
Composition.LiteralPromotion [lemma, in Section5]
Composition.MeasurePreservation [lemma, in Section5]
Composition.M_traditional_dec [module, in Section5]
Composition.rsubfi_refl [lemma, in Section5]
D
DSub [section, in Section3_Requirements]dsuba [inductive, in Section3_Requirements]
dsuba_int_lr [constructor, in Section3_Requirements]
dsuba_int_ll [constructor, in Section3_Requirements]
dsuba_int_r [constructor, in Section3_Requirements]
dsuba_uni_rr [constructor, in Section3_Requirements]
dsuba_uni_rl [constructor, in Section3_Requirements]
dsuba_uni_l [constructor, in Section3_Requirements]
dsuba_bot [constructor, in Section3_Requirements]
dsuba_top [constructor, in Section3_Requirements]
dsuba_lit [constructor, in Section3_Requirements]
dsuba_assume [constructor, in Section3_Requirements]
dsuba_trans [constructor, in Section3_Requirements]
dsuba_refl [constructor, in Section3_Requirements]
dsubda [inductive, in Section4_Requirements]
dsubda_dist [constructor, in Section4_Requirements]
dsubda_int_lr [constructor, in Section4_Requirements]
dsubda_int_ll [constructor, in Section4_Requirements]
dsubda_int_r [constructor, in Section4_Requirements]
dsubda_uni_rr [constructor, in Section4_Requirements]
dsubda_uni_rl [constructor, in Section4_Requirements]
dsubda_uni_l [constructor, in Section4_Requirements]
dsubda_bot [constructor, in Section4_Requirements]
dsubda_top [constructor, in Section4_Requirements]
dsubda_lit [constructor, in Section4_Requirements]
dsubda_assume [constructor, in Section4_Requirements]
dsubda_trans [constructor, in Section4_Requirements]
dsubda_refl [constructor, in Section4_Requirements]
dsubf [definition, in Section3_Requirements]
DSub.DPremise [variable, in Section3_Requirements]
DSub.DRule [variable, in Section3_Requirements]
DSub.Lit [variable, in Section3_Requirements]
E
Exists_Intersection [definition, in Section4_Requirements]exist2T [constructor, in Section4_Requirements]
I
Integrate [definition, in Section4_Requirements]Integrated [module, in Section4_Proofs]
Integrated [definition, in Section4_Requirements]
Integrated_int [definition, in Section4_Requirements]
Integrated.DecidabilityOfExtendedSubtyping [lemma, in Section4_Proofs]
Integrated.DeclarativeToIntegratedLiteralConversion [lemma, in Section4_Proofs]
Integrated.Dereliction [lemma, in Section4_Proofs]
Integrated.dereliction_lits [lemma, in Section4_Proofs]
Integrated.dsuba_ext_dec_isub' [definition, in Section4_Proofs]
Integrated.dsuba_ext_dec [lemma, in Section4_Proofs]
Integrated.IntegratedAssumptions [lemma, in Section4_Proofs]
Integrated.IntegratedCompleteness [lemma, in Section4_Proofs]
Integrated.IntegratedDecidability [lemma, in Section4_Proofs]
Integrated.IntegratedMonotonicity [lemma, in Section4_Proofs]
Integrated.IntegratedPromotion [lemma, in Section4_Proofs]
Integrated.IntegratedReflexivity [lemma, in Section4_Proofs]
Integrated.IntegratedSoundness [lemma, in Section4_Proofs]
Integrated.IntegratedTransitivity [lemma, in Section4_Proofs]
Integrated.integrated_promotion [lemma, in Section4_Proofs]
Integrated.integrated_assumptions' [lemma, in Section4_Proofs]
Integrated.IntegratorIntegrated [lemma, in Section4_Proofs]
Integrated.IntegratorSoundness [lemma, in Section4_Proofs]
Integrated.ipremise [constructor, in Section4_Proofs]
Integrated.IPremise [inductive, in Section4_Proofs]
Integrated.irec [lemma, in Section4_Proofs]
Integrated.irec_alt [lemma, in Section4_Proofs]
Integrated.issub [definition, in Section4_Proofs]
Integrated.issub_promotion [lemma, in Section4_Proofs]
Integrated.isub [definition, in Section4_Proofs]
Integrated.isub_esub [lemma, in Section4_Proofs]
Integrated.isub' [definition, in Section4_Proofs]
Integrated.isuisub_promotion [lemma, in Section4_Proofs]
Integrated.LiteralPromotion' [lemma, in Section4_Proofs]
Integrated.litlt [definition, in Section4_Proofs]
Integrated.litlt_wf [lemma, in Section4_Proofs]
Integrated.lsub_rsubf_rsubam_trans [lemma, in Section4_Proofs]
Integrated.lsub_rsubam_rsubf_trans [lemma, in Section4_Proofs]
Integrated.mlt_recurse [lemma, in Section4_Proofs]
Integrated.M_sopinfrastructure [module, in Section4_Proofs]
Integrated.oisub [definition, in Section4_Proofs]
Integrated.oisub_esub [lemma, in Section4_Proofs]
Integrated.oisub_isub [lemma, in Section4_Proofs]
Integrated.oisub_dec [lemma, in Section4_Proofs]
Integrated.OptimizedDecidabilityOfExtendedSubtyping [lemma, in Section4_Proofs]
Integrated.ORsubf [constructor, in Section4_Proofs]
Integrated.orsubf [inductive, in Section4_Proofs]
Integrated.orsubf_ouisub [lemma, in Section4_Proofs]
Integrated.ouisub [inductive, in Section4_Proofs]
Integrated.ouisub_dec [definition, in Section4_Proofs]
Integrated.ouisub_r_lit_r [lemma, in Section4_Proofs]
Integrated.ouisub_ProductOfLiterals [lemma, in Section4_Proofs]
Integrated.ouisub_uni_l [lemma, in Section4_Proofs]
Integrated.ouisub_r_uni_l [lemma, in Section4_Proofs]
Integrated.ouisub_r_top_lit [lemma, in Section4_Proofs]
Integrated.ouisub_top_l [lemma, in Section4_Proofs]
Integrated.ouisub_int_l [lemma, in Section4_Proofs]
Integrated.ouisub_r [inductive, in Section4_Proofs]
Integrated.ouisub_l [inductive, in Section4_Proofs]
Integrated.oui_uni [constructor, in Section4_Proofs]
Integrated.oui_bot [constructor, in Section4_Proofs]
Integrated.oui_polr [constructor, in Section4_Proofs]
Integrated.oui_uni_r [constructor, in Section4_Proofs]
Integrated.oui_uni_l [constructor, in Section4_Proofs]
Integrated.oui_int [constructor, in Section4_Proofs]
Integrated.oui_top [constructor, in Section4_Proofs]
Integrated.oui_poll [constructor, in Section4_Proofs]
Integrated.oui_int_r [constructor, in Section4_Proofs]
Integrated.oui_int_l [constructor, in Section4_Proofs]
Integrated.oui_lit [constructor, in Section4_Proofs]
Integrated.Promotion [lemma, in Section4_Proofs]
Integrated.rssub [definition, in Section4_Proofs]
Integrated.rssub_refl [lemma, in Section4_Proofs]
Integrated.sopdereliction [lemma, in Section4_Proofs]
Integrated.SopIntegrate_sopof_Integrate [lemma, in Section4_Proofs]
Integrated.SopIntegratorIntegrated [lemma, in Section4_Proofs]
Integrated.sopintersect [definition, in Section4_Proofs]
Integrated.SopIntersectorCompleteness [lemma, in Section4_Proofs]
Integrated.SopIntersectorIntegrated [lemma, in Section4_Proofs]
Integrated.SopIntersectorSoundness [lemma, in Section4_Proofs]
Integrated.sopintersect_sopof_intersect [lemma, in Section4_Proofs]
Integrated.SopLiteralDereliction [lemma, in Section4_Proofs]
Integrated.SopLiteralPromotion [lemma, in Section4_Proofs]
Integrated.ssub_suisub_trans [lemma, in Section4_Proofs]
Integrated.ssub_isects_litrules [lemma, in Section4_Proofs]
Integrated.suirec_suisub_suisub [lemma, in Section4_Proofs]
Integrated.suisub_uisub_trans [lemma, in Section4_Proofs]
Integrated.suisub_SopIntegrate_sopintersect_uisub_Integrate_intersect [lemma, in Section4_Proofs]
Integrated.suisub_SopIntegrate_uisub_Integrate [lemma, in Section4_Proofs]
Integrated.suisub_sopof_uisub [lemma, in Section4_Proofs]
Integrated.sui_promotion [lemma, in Section4_Proofs]
Integrated.uisub_ouisub [lemma, in Section4_Proofs]
Integrated.uisub_dnf_r [lemma, in Section4_Proofs]
Integrator [section, in Section4_Requirements]
Integrator.DPremise [variable, in Section4_Requirements]
Integrator.DRule [variable, in Section4_Requirements]
Integrator.Lit [variable, in Section4_Requirements]
Intersect [definition, in Section4_Requirements]
Intersector [module, in Section4_Requirements]
Intersector.esub [abbreviation, in Section4_Requirements]
Intersector.extension [axiom, in Section4_Requirements]
Intersector.intersect [axiom, in Section4_Requirements]
Intersector.intersected [axiom, in Section4_Requirements]
Intersector.IntersectorCompleteness [axiom, in Section4_Requirements]
Intersector.IntersectorIntegrated [axiom, in Section4_Requirements]
Intersector.IntersectorSoundness [axiom, in Section4_Requirements]
Intersector.LiteralDereliction [axiom, in Section4_Requirements]
Intersector.LiteralPromotion [axiom, in Section4_Requirements]
Intersector.MeasurePreservation [axiom, in Section4_Requirements]
Introduction [library]
L
Lsub [constructor, in Section3_Requirements]lsub [inductive, in Section3_Requirements]
M
meet [definition, in Section4_Requirements]P
polof [inductive, in Section4_Requirements]polof_int [constructor, in Section4_Requirements]
polof_top [constructor, in Section4_Requirements]
polof_lit [constructor, in Section4_Requirements]
POL_int [constructor, in Section4_Requirements]
POL_lit [constructor, in Section4_Requirements]
POL_top [constructor, in Section4_Requirements]
ProductOfLiterals [inductive, in Section4_Requirements]
proj2T1 [definition, in Section4_Requirements]
proj2T2 [definition, in Section4_Requirements]
proj2V [definition, in Section4_Requirements]
R
ram_uni_l [constructor, in Section3_Requirements]ram_uni_rr [constructor, in Section3_Requirements]
ram_uni_rl [constructor, in Section3_Requirements]
ram_bot [constructor, in Section3_Requirements]
ram_int_r [constructor, in Section3_Requirements]
ram_int_lr [constructor, in Section3_Requirements]
ram_int_ll [constructor, in Section3_Requirements]
ram_top [constructor, in Section3_Requirements]
ram_lit [constructor, in Section3_Requirements]
ram_mono [constructor, in Section3_Requirements]
ram_assumption [constructor, in Section3_Requirements]
RSub [section, in Section3_Requirements]
rsubam [inductive, in Section3_Requirements]
Rsubf [constructor, in Section3_Requirements]
rsubf [inductive, in Section3_Requirements]
RSub.Lit [variable, in Section3_Requirements]
RSub.RPremise [variable, in Section3_Requirements]
RSub.RRule [variable, in Section3_Requirements]
ruirec [definition, in Section4_Requirements]
ruisub [inductive, in Section4_Requirements]
rui_uni_r [constructor, in Section4_Requirements]
rui_uni_l [constructor, in Section4_Requirements]
rui_int [constructor, in Section4_Requirements]
rui_top [constructor, in Section4_Requirements]
rui_lit [constructor, in Section4_Requirements]
S
Section3_Proofs [library]Section3_Requirements [library]
Section4_Requirements [library]
Section4_Proofs [library]
Section5 [library]
sig2T [inductive, in Section4_Requirements]
sop [abbreviation, in Section4_Requirements]
SopIntegrate [definition, in Section4_Requirements]
SopIntegrated [definition, in Section4_Requirements]
sopof [inductive, in Section4_Requirements]
sopof_uni [constructor, in Section4_Requirements]
sopof_bot [constructor, in Section4_Requirements]
sopof_pol [constructor, in Section4_Requirements]
SOP_prod [constructor, in Section4_Requirements]
SOP_uni [constructor, in Section4_Requirements]
SOP_bot [constructor, in Section4_Requirements]
sop2ui [definition, in Section4_Requirements]
ssub [definition, in Section4_Requirements]
subui [inductive, in Section3_Requirements]
sub_isect_r [constructor, in Section3_Requirements]
sub_isect_l [constructor, in Section3_Requirements]
sub_uni_r [constructor, in Section3_Requirements]
sub_uni_l [constructor, in Section3_Requirements]
suirec [definition, in Section4_Requirements]
suisub [definition, in Section4_Requirements]
SumOfProducts [inductive, in Section4_Requirements]
SumOfProducts [section, in Section4_Requirements]
SumOfProducts.Lit [variable, in Section4_Requirements]
T
T [abbreviation, in Section3_Requirements]T [abbreviation, in Section3_Requirements]
T [abbreviation, in Section4_Requirements]
T [abbreviation, in Section4_Requirements]
TBot [constructor, in Section3_Requirements]
TIsect [constructor, in Section3_Requirements]
TLit [constructor, in Section3_Requirements]
Traditional [module, in Section3_Requirements]
TraditionalDec [module, in Section3_Proofs]
TraditionalDec.DecidabilityOfDeclarativeSubtyping [lemma, in Section3_Proofs]
TraditionalDec.lsub_rsub_trans [lemma, in Section3_Proofs]
TraditionalDec.lt_Acc_pmlt_acc [lemma, in Section3_Proofs]
TraditionalDec.mltt [definition, in Section3_Proofs]
TraditionalDec.mltt_Acc_pmlt_acc [lemma, in Section3_Proofs]
TraditionalDec.mltt_trans [lemma, in Section3_Proofs]
TraditionalDec.mltt_wf [definition, in Section3_Proofs]
TraditionalDec.M_Infrastructure [module, in Section3_Proofs]
TraditionalDec.pm [definition, in Section3_Proofs]
TraditionalDec.PM [definition, in Section3_Proofs]
TraditionalDec.pmlt [definition, in Section3_Proofs]
TraditionalDec.pmlt_wf [lemma, in Section3_Proofs]
TraditionalDec.progress_measure_trans [lemma, in Section3_Proofs]
TraditionalDec.progress_measure_wf [lemma, in Section3_Proofs]
TraditionalDec.progress_measure [definition, in Section3_Proofs]
TraditionalDec.rsubam_rsub [lemma, in Section3_Proofs]
TraditionalDec.rsubam_rsubt [lemma, in Section3_Proofs]
TraditionalDec.rsubf_dec [lemma, in Section3_Proofs]
TraditionalDec.rsubt [inductive, in Section3_Proofs]
TraditionalDec.rsubt_rsub [lemma, in Section3_Proofs]
TraditionalDec.rsub_dsub [lemma, in Section3_Proofs]
TraditionalDec.rsub_trans [lemma, in Section3_Proofs]
TraditionalDec.rsub_rsubt [lemma, in Section3_Proofs]
TraditionalDec.rsub_refl [lemma, in Section3_Proofs]
TraditionalDec.rsub_dec [lemma, in Section3_Proofs]
TraditionalDec.rt_uni_l [constructor, in Section3_Proofs]
TraditionalDec.rt_uni_rr [constructor, in Section3_Proofs]
TraditionalDec.rt_uni_rl [constructor, in Section3_Proofs]
TraditionalDec.rt_bot [constructor, in Section3_Proofs]
TraditionalDec.rt_int_r [constructor, in Section3_Proofs]
TraditionalDec.rt_int_lr [constructor, in Section3_Proofs]
TraditionalDec.rt_int_ll [constructor, in Section3_Proofs]
TraditionalDec.rt_top [constructor, in Section3_Proofs]
TraditionalDec.rt_lit [constructor, in Section3_Proofs]
TraditionalDec.rt_transitivity [constructor, in Section3_Proofs]
TraditionalDec.syntactic_literal_depth [definition, in Section3_Proofs]
TraditionalDec.uirec_alt [lemma, in Section3_Proofs]
TraditionalDec.uisub_trans [lemma, in Section3_Proofs]
Traditional.DPremise [axiom, in Section3_Requirements]
Traditional.DRule [axiom, in Section3_Requirements]
Traditional.DRuleToRProof [axiom, in Section3_Requirements]
Traditional.dsub [abbreviation, in Section3_Requirements]
Traditional.Lit [axiom, in Section3_Requirements]
Traditional.LiteralReflexivity [axiom, in Section3_Requirements]
Traditional.LiteralTransitivity [axiom, in Section3_Requirements]
Traditional.m [axiom, in Section3_Requirements]
Traditional.M [axiom, in Section3_Requirements]
Traditional.mlt [axiom, in Section3_Requirements]
Traditional.mltwf [axiom, in Section3_Requirements]
Traditional.m_lit [axiom, in Section3_Requirements]
Traditional.m_ui_r [axiom, in Section3_Requirements]
Traditional.m_ui_l [axiom, in Section3_Requirements]
Traditional.RPremise [axiom, in Section3_Requirements]
Traditional.RRule [axiom, in Section3_Requirements]
Traditional.RRuleToDProof [axiom, in Section3_Requirements]
Traditional.rsub [abbreviation, in Section3_Requirements]
Traditional.SyntaxDirectedness_Premises [axiom, in Section3_Requirements]
Traditional.SyntaxDirectedness_Rules [axiom, in Section3_Requirements]
Traditional.T [abbreviation, in Section3_Requirements]
TTop [constructor, in Section3_Requirements]
TUni [constructor, in Section3_Requirements]
U
uisub [inductive, in Section3_Requirements]UIType [inductive, in Section3_Requirements]
ui_uni_l [constructor, in Section3_Requirements]
ui_uni_rr [constructor, in Section3_Requirements]
ui_uni_rl [constructor, in Section3_Requirements]
ui_bot [constructor, in Section3_Requirements]
ui_int_r [constructor, in Section3_Requirements]
ui_int_lr [constructor, in Section3_Requirements]
ui_int_ll [constructor, in Section3_Requirements]
ui_top [constructor, in Section3_Requirements]
ui_lit [constructor, in Section3_Requirements]
ui2sop [definition, in Section4_Requirements]
ui2sop_meet [definition, in Section4_Requirements]
Module Index
C
Composability [in Section5]Composition [in Section5]
Composition.Il [in Section5]
Composition.Intl [in Section5]
Composition.Intr [in Section5]
Composition.Ir [in Section5]
Composition.M_traditional_dec [in Section5]
I
Integrated [in Section4_Proofs]Integrated.M_sopinfrastructure [in Section4_Proofs]
Intersector [in Section4_Requirements]
T
Traditional [in Section3_Requirements]TraditionalDec [in Section3_Proofs]
TraditionalDec.M_Infrastructure [in Section3_Proofs]
Variable Index
D
DSub.DPremise [in Section3_Requirements]DSub.DRule [in Section3_Requirements]
DSub.Lit [in Section3_Requirements]
I
Integrator.DPremise [in Section4_Requirements]Integrator.DRule [in Section4_Requirements]
Integrator.Lit [in Section4_Requirements]
R
RSub.Lit [in Section3_Requirements]RSub.RPremise [in Section3_Requirements]
RSub.RRule [in Section3_Requirements]
S
SumOfProducts.Lit [in Section4_Requirements]Library Index
I
IntroductionS
Section3_ProofsSection3_Requirements
Section4_Requirements
Section4_Proofs
Section5
Lemma Index
C
Composition.IntersectorCompleteness [in Section5]Composition.IntersectorIntegrated [in Section5]
Composition.IntersectorSoundness [in Section5]
Composition.LiteralDereliction [in Section5]
Composition.LiteralPromotion [in Section5]
Composition.MeasurePreservation [in Section5]
Composition.rsubfi_refl [in Section5]
I
Integrated.DecidabilityOfExtendedSubtyping [in Section4_Proofs]Integrated.DeclarativeToIntegratedLiteralConversion [in Section4_Proofs]
Integrated.Dereliction [in Section4_Proofs]
Integrated.dereliction_lits [in Section4_Proofs]
Integrated.dsuba_ext_dec [in Section4_Proofs]
Integrated.IntegratedAssumptions [in Section4_Proofs]
Integrated.IntegratedCompleteness [in Section4_Proofs]
Integrated.IntegratedDecidability [in Section4_Proofs]
Integrated.IntegratedMonotonicity [in Section4_Proofs]
Integrated.IntegratedPromotion [in Section4_Proofs]
Integrated.IntegratedReflexivity [in Section4_Proofs]
Integrated.IntegratedSoundness [in Section4_Proofs]
Integrated.IntegratedTransitivity [in Section4_Proofs]
Integrated.integrated_promotion [in Section4_Proofs]
Integrated.integrated_assumptions' [in Section4_Proofs]
Integrated.IntegratorIntegrated [in Section4_Proofs]
Integrated.IntegratorSoundness [in Section4_Proofs]
Integrated.irec [in Section4_Proofs]
Integrated.irec_alt [in Section4_Proofs]
Integrated.issub_promotion [in Section4_Proofs]
Integrated.isub_esub [in Section4_Proofs]
Integrated.isuisub_promotion [in Section4_Proofs]
Integrated.LiteralPromotion' [in Section4_Proofs]
Integrated.litlt_wf [in Section4_Proofs]
Integrated.lsub_rsubf_rsubam_trans [in Section4_Proofs]
Integrated.lsub_rsubam_rsubf_trans [in Section4_Proofs]
Integrated.mlt_recurse [in Section4_Proofs]
Integrated.oisub_esub [in Section4_Proofs]
Integrated.oisub_isub [in Section4_Proofs]
Integrated.oisub_dec [in Section4_Proofs]
Integrated.OptimizedDecidabilityOfExtendedSubtyping [in Section4_Proofs]
Integrated.orsubf_ouisub [in Section4_Proofs]
Integrated.ouisub_r_lit_r [in Section4_Proofs]
Integrated.ouisub_ProductOfLiterals [in Section4_Proofs]
Integrated.ouisub_uni_l [in Section4_Proofs]
Integrated.ouisub_r_uni_l [in Section4_Proofs]
Integrated.ouisub_r_top_lit [in Section4_Proofs]
Integrated.ouisub_top_l [in Section4_Proofs]
Integrated.ouisub_int_l [in Section4_Proofs]
Integrated.Promotion [in Section4_Proofs]
Integrated.rssub_refl [in Section4_Proofs]
Integrated.sopdereliction [in Section4_Proofs]
Integrated.SopIntegrate_sopof_Integrate [in Section4_Proofs]
Integrated.SopIntegratorIntegrated [in Section4_Proofs]
Integrated.SopIntersectorCompleteness [in Section4_Proofs]
Integrated.SopIntersectorIntegrated [in Section4_Proofs]
Integrated.SopIntersectorSoundness [in Section4_Proofs]
Integrated.sopintersect_sopof_intersect [in Section4_Proofs]
Integrated.SopLiteralDereliction [in Section4_Proofs]
Integrated.SopLiteralPromotion [in Section4_Proofs]
Integrated.ssub_suisub_trans [in Section4_Proofs]
Integrated.ssub_isects_litrules [in Section4_Proofs]
Integrated.suirec_suisub_suisub [in Section4_Proofs]
Integrated.suisub_uisub_trans [in Section4_Proofs]
Integrated.suisub_SopIntegrate_sopintersect_uisub_Integrate_intersect [in Section4_Proofs]
Integrated.suisub_SopIntegrate_uisub_Integrate [in Section4_Proofs]
Integrated.suisub_sopof_uisub [in Section4_Proofs]
Integrated.sui_promotion [in Section4_Proofs]
Integrated.uisub_ouisub [in Section4_Proofs]
Integrated.uisub_dnf_r [in Section4_Proofs]
T
TraditionalDec.DecidabilityOfDeclarativeSubtyping [in Section3_Proofs]TraditionalDec.lsub_rsub_trans [in Section3_Proofs]
TraditionalDec.lt_Acc_pmlt_acc [in Section3_Proofs]
TraditionalDec.mltt_Acc_pmlt_acc [in Section3_Proofs]
TraditionalDec.mltt_trans [in Section3_Proofs]
TraditionalDec.pmlt_wf [in Section3_Proofs]
TraditionalDec.progress_measure_trans [in Section3_Proofs]
TraditionalDec.progress_measure_wf [in Section3_Proofs]
TraditionalDec.rsubam_rsub [in Section3_Proofs]
TraditionalDec.rsubam_rsubt [in Section3_Proofs]
TraditionalDec.rsubf_dec [in Section3_Proofs]
TraditionalDec.rsubt_rsub [in Section3_Proofs]
TraditionalDec.rsub_dsub [in Section3_Proofs]
TraditionalDec.rsub_trans [in Section3_Proofs]
TraditionalDec.rsub_rsubt [in Section3_Proofs]
TraditionalDec.rsub_refl [in Section3_Proofs]
TraditionalDec.rsub_dec [in Section3_Proofs]
TraditionalDec.uirec_alt [in Section3_Proofs]
TraditionalDec.uisub_trans [in Section3_Proofs]
Constructor Index
D
dsuba_int_lr [in Section3_Requirements]dsuba_int_ll [in Section3_Requirements]
dsuba_int_r [in Section3_Requirements]
dsuba_uni_rr [in Section3_Requirements]
dsuba_uni_rl [in Section3_Requirements]
dsuba_uni_l [in Section3_Requirements]
dsuba_bot [in Section3_Requirements]
dsuba_top [in Section3_Requirements]
dsuba_lit [in Section3_Requirements]
dsuba_assume [in Section3_Requirements]
dsuba_trans [in Section3_Requirements]
dsuba_refl [in Section3_Requirements]
dsubda_dist [in Section4_Requirements]
dsubda_int_lr [in Section4_Requirements]
dsubda_int_ll [in Section4_Requirements]
dsubda_int_r [in Section4_Requirements]
dsubda_uni_rr [in Section4_Requirements]
dsubda_uni_rl [in Section4_Requirements]
dsubda_uni_l [in Section4_Requirements]
dsubda_bot [in Section4_Requirements]
dsubda_top [in Section4_Requirements]
dsubda_lit [in Section4_Requirements]
dsubda_assume [in Section4_Requirements]
dsubda_trans [in Section4_Requirements]
dsubda_refl [in Section4_Requirements]
E
exist2T [in Section4_Requirements]I
Integrated.ipremise [in Section4_Proofs]Integrated.ORsubf [in Section4_Proofs]
Integrated.oui_uni [in Section4_Proofs]
Integrated.oui_bot [in Section4_Proofs]
Integrated.oui_polr [in Section4_Proofs]
Integrated.oui_uni_r [in Section4_Proofs]
Integrated.oui_uni_l [in Section4_Proofs]
Integrated.oui_int [in Section4_Proofs]
Integrated.oui_top [in Section4_Proofs]
Integrated.oui_poll [in Section4_Proofs]
Integrated.oui_int_r [in Section4_Proofs]
Integrated.oui_int_l [in Section4_Proofs]
Integrated.oui_lit [in Section4_Proofs]
L
Lsub [in Section3_Requirements]P
polof_int [in Section4_Requirements]polof_top [in Section4_Requirements]
polof_lit [in Section4_Requirements]
POL_int [in Section4_Requirements]
POL_lit [in Section4_Requirements]
POL_top [in Section4_Requirements]
R
ram_uni_l [in Section3_Requirements]ram_uni_rr [in Section3_Requirements]
ram_uni_rl [in Section3_Requirements]
ram_bot [in Section3_Requirements]
ram_int_r [in Section3_Requirements]
ram_int_lr [in Section3_Requirements]
ram_int_ll [in Section3_Requirements]
ram_top [in Section3_Requirements]
ram_lit [in Section3_Requirements]
ram_mono [in Section3_Requirements]
ram_assumption [in Section3_Requirements]
Rsubf [in Section3_Requirements]
rui_uni_r [in Section4_Requirements]
rui_uni_l [in Section4_Requirements]
rui_int [in Section4_Requirements]
rui_top [in Section4_Requirements]
rui_lit [in Section4_Requirements]
S
sopof_uni [in Section4_Requirements]sopof_bot [in Section4_Requirements]
sopof_pol [in Section4_Requirements]
SOP_prod [in Section4_Requirements]
SOP_uni [in Section4_Requirements]
SOP_bot [in Section4_Requirements]
sub_isect_r [in Section3_Requirements]
sub_isect_l [in Section3_Requirements]
sub_uni_r [in Section3_Requirements]
sub_uni_l [in Section3_Requirements]
T
TBot [in Section3_Requirements]TIsect [in Section3_Requirements]
TLit [in Section3_Requirements]
TraditionalDec.rt_uni_l [in Section3_Proofs]
TraditionalDec.rt_uni_rr [in Section3_Proofs]
TraditionalDec.rt_uni_rl [in Section3_Proofs]
TraditionalDec.rt_bot [in Section3_Proofs]
TraditionalDec.rt_int_r [in Section3_Proofs]
TraditionalDec.rt_int_lr [in Section3_Proofs]
TraditionalDec.rt_int_ll [in Section3_Proofs]
TraditionalDec.rt_top [in Section3_Proofs]
TraditionalDec.rt_lit [in Section3_Proofs]
TraditionalDec.rt_transitivity [in Section3_Proofs]
TTop [in Section3_Requirements]
TUni [in Section3_Requirements]
U
ui_uni_l [in Section3_Requirements]ui_uni_rr [in Section3_Requirements]
ui_uni_rl [in Section3_Requirements]
ui_bot [in Section3_Requirements]
ui_int_r [in Section3_Requirements]
ui_int_lr [in Section3_Requirements]
ui_int_ll [in Section3_Requirements]
ui_top [in Section3_Requirements]
ui_lit [in Section3_Requirements]
Axiom Index
C
Composability.IntersectedPreservation [in Section5]I
Intersector.extension [in Section4_Requirements]Intersector.intersect [in Section4_Requirements]
Intersector.intersected [in Section4_Requirements]
Intersector.IntersectorCompleteness [in Section4_Requirements]
Intersector.IntersectorIntegrated [in Section4_Requirements]
Intersector.IntersectorSoundness [in Section4_Requirements]
Intersector.LiteralDereliction [in Section4_Requirements]
Intersector.LiteralPromotion [in Section4_Requirements]
Intersector.MeasurePreservation [in Section4_Requirements]
T
Traditional.DPremise [in Section3_Requirements]Traditional.DRule [in Section3_Requirements]
Traditional.DRuleToRProof [in Section3_Requirements]
Traditional.Lit [in Section3_Requirements]
Traditional.LiteralReflexivity [in Section3_Requirements]
Traditional.LiteralTransitivity [in Section3_Requirements]
Traditional.m [in Section3_Requirements]
Traditional.M [in Section3_Requirements]
Traditional.mlt [in Section3_Requirements]
Traditional.mltwf [in Section3_Requirements]
Traditional.m_lit [in Section3_Requirements]
Traditional.m_ui_r [in Section3_Requirements]
Traditional.m_ui_l [in Section3_Requirements]
Traditional.RPremise [in Section3_Requirements]
Traditional.RRule [in Section3_Requirements]
Traditional.RRuleToDProof [in Section3_Requirements]
Traditional.SyntaxDirectedness_Premises [in Section3_Requirements]
Traditional.SyntaxDirectedness_Rules [in Section3_Requirements]
Inductive Index
D
dsuba [in Section3_Requirements]dsubda [in Section4_Requirements]
I
Integrated.IPremise [in Section4_Proofs]Integrated.orsubf [in Section4_Proofs]
Integrated.ouisub [in Section4_Proofs]
Integrated.ouisub_r [in Section4_Proofs]
Integrated.ouisub_l [in Section4_Proofs]
L
lsub [in Section3_Requirements]P
polof [in Section4_Requirements]ProductOfLiterals [in Section4_Requirements]
R
rsubam [in Section3_Requirements]rsubf [in Section3_Requirements]
ruisub [in Section4_Requirements]
S
sig2T [in Section4_Requirements]sopof [in Section4_Requirements]
subui [in Section3_Requirements]
SumOfProducts [in Section4_Requirements]
T
TraditionalDec.rsubt [in Section3_Proofs]U
uisub [in Section3_Requirements]UIType [in Section3_Requirements]
Section Index
D
DSub [in Section3_Requirements]I
Integrator [in Section4_Requirements]R
RSub [in Section3_Requirements]S
SumOfProducts [in Section4_Requirements]Abbreviation Index
I
Intersector.esub [in Section4_Requirements]S
sop [in Section4_Requirements]T
T [in Section3_Requirements]T [in Section3_Requirements]
T [in Section4_Requirements]
T [in Section4_Requirements]
Traditional.dsub [in Section3_Requirements]
Traditional.rsub [in Section3_Requirements]
Traditional.T [in Section3_Requirements]
Definition Index
C
Composition.extension [in Section5]Composition.intersect [in Section5]
Composition.intersected [in Section5]
D
dsubf [in Section3_Requirements]E
Exists_Intersection [in Section4_Requirements]I
Integrate [in Section4_Requirements]Integrated [in Section4_Requirements]
Integrated_int [in Section4_Requirements]
Integrated.dsuba_ext_dec_isub' [in Section4_Proofs]
Integrated.issub [in Section4_Proofs]
Integrated.isub [in Section4_Proofs]
Integrated.isub' [in Section4_Proofs]
Integrated.litlt [in Section4_Proofs]
Integrated.oisub [in Section4_Proofs]
Integrated.ouisub_dec [in Section4_Proofs]
Integrated.rssub [in Section4_Proofs]
Integrated.sopintersect [in Section4_Proofs]
Intersect [in Section4_Requirements]
M
meet [in Section4_Requirements]P
proj2T1 [in Section4_Requirements]proj2T2 [in Section4_Requirements]
proj2V [in Section4_Requirements]
R
ruirec [in Section4_Requirements]S
SopIntegrate [in Section4_Requirements]SopIntegrated [in Section4_Requirements]
sop2ui [in Section4_Requirements]
ssub [in Section4_Requirements]
suirec [in Section4_Requirements]
suisub [in Section4_Requirements]
T
TraditionalDec.mltt [in Section3_Proofs]TraditionalDec.mltt_wf [in Section3_Proofs]
TraditionalDec.pm [in Section3_Proofs]
TraditionalDec.PM [in Section3_Proofs]
TraditionalDec.pmlt [in Section3_Proofs]
TraditionalDec.progress_measure [in Section3_Proofs]
TraditionalDec.syntactic_literal_depth [in Section3_Proofs]
U
ui2sop [in Section4_Requirements]ui2sop_meet [in Section4_Requirements]
Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (311 entries) |
Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |
Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10 entries) |
Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (86 entries) |
Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (97 entries) |
Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (28 entries) |
Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (20 entries) |
Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (9 entries) |
Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (38 entries) |
This page has been generated by coqdoc