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.
In case you are not familiar with Coq's module system: we implemented this formalization as a library for people to use. A "Module Type" specifies a signature that a user needs to implement; "Parameter"s within that module type are the specific things a user needs to provide/proof. Once a user instantiated a module type in a module of their own, they can use that to instantiate our "Module"s, which provide the extended systems/proofs based on the user's input.
This file contains only the signatures of the various components of our proof, but for each file (.v), there is a link at the beginning of the section corresponding to that file that leads to the coqdoc for the full file including the actual proof code. The .v-files themselves are also included and can be used to verify the proofs in Coq. The files should be compiled in the order in which they appear in this file.
All of this was generated using coqdoc, whose approach to links in the face of modules is not the most helpful one. However, other syntax highlighting features depend on the same information as link generation, so the code should still be a lot more readable than without links. We made sure that links in standard HTML rendering (blue underlined) lead to where they should, and most of the links should get you at least closer to where the definition you wanted to was.
We prove an example of how to instantiate the module types of Sections 3 and 4 in Example.v.

Outline

The following outline of the proofs shows the items that correspond to something in the paper:

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 PaperCorresponding Definitions/Lemmas/TheoremsComment
LiteralsLit in Section3_Requirements.vAlso an implicit parameter in many global definitions
TypesNotation T := UIType Lit defined almost everywhereUIType is defined in Section3_Requirements.v
Declarative Literal Subtyping RulesDRule and DPremise in Section3_Requirements.v
Declarative Subtypingdsub in Section3_Requirements.vBased on dsuba and dsubf in Section3_Requirements.v
Reductive Literal Subtyping RulesRRule and RPremise in Section3_Requirements.v
Reductive Subtypingrsub in Section3_Requirements.vBased on uisub, lsub, and rsubf in Section3_Requirements.v
Requirement 1: Syntax-DirectednessSyntaxDirectedness_Rules and SyntaxDirectedness_Premises in Section3_Requirements.v
Requirement 2: Well-Foundednessm, M, mlt, mltwf, m_ui_l, m_ui_r, and m_lit in Section3_Requirements.v
Requirement 3: Literal ReflexivityLiteralReflexivity in Section3_Requirements.v
Declarative Subtyping with Assumptionsdsuba in Section3_Requirements.v
Reductive Subtyping with Assumptionsrsubam in Section3_Requirements.vAlso includes Monotonicity, which makes the proof stronger than in the paper (see explanation at definition)
Requirement 4: R-to-D Literal ConversionRRuleToDProof in Section3_Requirements.v
Requirement 5: D-to-R Literal ConversionDRuleToRProof in Section3_Requirements.v
Requirement 6: Literal TransitivityLiteralTransitivity in Section3_Requirements.v
Decidability of Declarative Subtyping TheoremDecidabilityOfDeclarativeSubtyping in Section3_Proofs.v
Extension Axiomsextension in Section4_Requirements.v
Extended Subtypingesub in Section4_Requirements.vBased on dsubda and extension in Section4_Requirements.v
Integrator (DNFc)Integrate in Section4_Requirements.v
Intersector (⊓)intersect in Section4_Requirements.v
Requirement 7: Intersector CompletenessIntersectorCompleteness in Section4_Requirements.v
Requirement 8: Intersector SoundnessIntersectorSoundness in Section4_Requirements.v
Lemma 1: Integrated SoundnessIntegratedSoundness in Section4_Proofs.v
Requirement 9: Measure PreservationMeasurePreservation in Section4_Requirements.v
Lemma 2: Integrated DecidabilityIntegratedDecidability in Section4_Proofs.v
Requirement 10: Literal DerelictionLiteralDereliction in Section4_Requirements.v
Lemma 3: DerelictionDereliction 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 IntegratedIntersectorIntegrated in Section4_Requirements.v
Lemma 4: Integrator IntegratedIntegratorIntegrated in Section4_Proofs.v
Requirement 12: Literal PromotionLiteralPromotion in Section4_Requirements.v
Lemma 5: PromotionPromotion in Section4_Proofs.v
Lemma 6: Integrated MonotonicityIntegratedMonotonicity in Section4_Proofs.vActually mostly proved together in integrated_assumptions' in Section4_Proofs.v
Lemma 7: Integrated AssumptionsIntegratedAssumptions in Section4_Proofs.v
Lemma 8: Integrated PromotionIntegratedPromotion in Section4_Proofs.v
Lemma 9: Integrated ReflexivityIntegratedReflexivity in Section4_Proofs.v
Lemma 10: D-to-I Literal ConversionDeclarativeToIntegratedLiteralConversion in Section4_Proofs.v
Lemma 11: Integrated TransitivityIntegratedTransitivity in Section4_Proofs.v
Lemma 12: Integrated CompletenessIntegratedCompleteness in Section4_Proofs.v
Decidability of Extended Subtyping TheoremDecidabilityOfExtendedSubtyping and OptimizedDecidabilityOfExtendedSubtyping in Section4_Proofs.v
Requirement 13: Intersected PreservationIntersectedPreservation in Section5.v
Intersector Composability TheoremModule Composition in Section5.vDefines 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.
We start by formalizing types. Our framework is parameterized by user-defined literals Lit, so most things defined here either have this as a (usually implicit) parameter or are in a module that takes a definition of literals as parameter. Literals are mutually recursively defined with the rest of our types, i.e. unions, intersections, top, and bottom. However, as they are defined separately, we cannot use Coq's built-in mechanisms for mutual recursion. Instead UIType is parameterized by literals Lit; a user's definition of Lits can then recursively use UIType Lit, and the user can prove mutual recursion and induction principles using nested recursion. In the following, whenever we have context where Lits are defined, we define the notation T to mean UIType Lit. T is then equivalent to the types τ in the paper.



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.

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
.

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.
A last definition before the module type is the relation subui, which is the relation << used in Requirement 2.

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.
NOTE: for m_ui_l and m_ui_r, the paper technically only allows the reflexive closure of mlt, not the reflexive transitive closure. Again, this means that the requirement here is weaker than specified in the paper.

  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.
NOTE: this is a weaker requirement than in the paper as we allow monotonicity.

  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).
The proof of this theorem proceeds as follows:

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.

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).

  Lemma rsub_dsub : forall tl tr : T, rsub tl tr <-> dsub tl tr.

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.

Module Type Intersector (M_traditional : Traditional).

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.

  Parameter extension : T -> T -> Prop.
  Notation esub := (dsubda (@DPremise) extension).

The Intersector

intersect is the intersector ⊓, as in the paper (Section 4.2).

  Parameter intersect : list Lit -> T.

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.

  Parameter IntersectorSoundness : forall ls : list Lit, esub (Intersect ls) (intersect ls).

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.

  Parameter LiteralDereliction : forall ls : list Lit, rsub (intersect ls) (Intersect ls).

The Intersected Predicate

intersected is the intersected predicate φ, as in the paper (Section 4.5.2).

  Parameter intersected : list Lit -> Prop.

Requirement 11: Intersector Integrated

The result of applying the intersector to a list of literals counts as Integrated using the provided intersected predicate.

  Parameter IntersectorIntegrated : forall ls : list Lit, Integrated intersected (intersect ls).

Requirement 12: Literal Promotion

For every two lists of literals ls and ls', and list of reductive literal subtyping rules rsRRule such that
Forall (fun l' : Lit => Exists (fun r : (sig2T RRule) => proj2T2 r = l') rs) ls' /\ incl (map proj2T1 rs)
if intersected ls holds then there exists a list of reductive literal subtyping rules rs' such that intersect ls' is of the form ... ∪ ⋂ (map proj2T2 rs') ∪ ... and for all reductive literal subtyping rules r' in rs':
In (proj2T1 r') ls /\ 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')

  Parameter 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. [[]].
SopIntegrate is similar to Integrate, except that the intersect function it accepts turns lists of literals into sops instead of Ts, and SopIntegrate uses that to stitch them together into an sop. Note, however, that SopIntegrate still takes a T as its original input; the full analogue to Integrate just on sops instead of Ts turns out to be just flat_map. SopIntegrated, however, is the full sop-analogue to Integrated.

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.
In a second step, as mentioned in the paper, we define an optimized integrated subtyping relation and decider that first resolves all unions on the LHS, then everything down to literals on the RHS, then intersections on the LHS, finding the right matches for whatever the RHS requires. We prove that this subtyping relation is equivalent to integrated and therefore extended subtyping and hence again a decider for extended subtyping.

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.

Requirement 7: Intersector Completeness (SOP Version)

Requirement 8: Intersector Soundness (SOP Version)


  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 SopLiteralDereliction : forall ls : list Lit, rsub (sop2ui (sopintersect ls)) (Intersect ls).

Requirement 11: Intersector Integrated (SOP Version)

Requirement 12: Literal Promotion (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.

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 IntegratedDecidability : forall tl tr : T, {isub tl tr} + {~ isub tl tr}.

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 5: Promotion

If the LHS of a reductive subtyping proof is Integrated, then the reductive subtyping also holds after Integrating the RHS.
We first re-formulate the LiteralPromotion requirement a little bit into LiteralPromotion'. ssub_isects_litrules lets us extract the list of literal subtyping rules that are used in proving subtyping between to lists of literals. sui_promotion is the formulation of Lemma 5 for sops, Promotion is proved based on it.

  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.
A version based on sopintersect is proven in several steps via several subtyping representations, the main work is in issub_promotion. In order to translate the final version integrated_promotion (which is the one used in the later stages of the proof) to the version in the paper (IntegratedPromotion), we prove an intermediate lemma that essentially says that on the RHS, the DNF of a type is the form of it that allows the fewest subtypings. This is stronger than what we actually need since all we need is to talk about different balancings of a type that is already in DNF, but it does the trick without having to build up a lot of infrastructure.

Lemma 9: Integrated Reflexivity

Straightforward proof based on IntegratedAssumptions.

  Lemma IntegratedReflexivity : forall t : T, isub t t.

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 IntegratedTransitivity (t1 t2 t3 : T) : isub t1 t2 -> isub t2 t3 -> isub t1 t3.

Lemma 12: Integrated Completeness

Mostly applying the previous lemmas, some extra work to cover distributivity.

  Lemma IntegratedCompleteness : forall tl tr : T, esub tl tr -> isub tl tr.

Equivalence of Integrated and Extended Subtyping

Simply combines IntegratedSoundness and IntegratedCompleteness.

  Lemma isub_esub : forall tl tr : T, isub tl tr <-> esub tl tr.

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.
The nested inductives ouisub, ouisub_r, and ousub_l represent this priorization:
  • 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
In this section, we prove that this subtyping relation is equivalent to uisub if the LHS is a SumOfProducts (i.e. in DNF), and it is decidable under similar conditions as rsubf. All of this means that, properly instantiated, we can use ouisub to build a decision procedure for esub.

  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
  .

orsubf is the ouisub-equivalent to uisub's rsubf

  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.
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))
Similar to the definition of isub based on rsubf, we define oisub based on orsubf, and prove it's decidability (oisub_dec).

  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

  Lemma oisub_esub : forall tl tr : T, oisub tl tr <-> esub tl tr.

Actual MAIN THEOREM, Part 2: Optimized Decidability of Extended Subtyping

As oisub is decidable and equivalent to esub, esub is decidable.

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.

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.

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.

Requirement 7: Intersector Completeness

Requirement 8: Intersector Soundness


  Lemma rsubfi_refl : forall t : T, rsubf (@IPremise) t t.

  Lemma IntersectorSoundness : forall ls : list Lit, dsubda (@DPremise) extension (Intersect ls) (intersect ls).


Requirement 9: Measure Preservation


  Lemma MeasurePreservation : forall tl tr : T, clos_refl_trans M mlt (m (Integrate intersect tl) tr) (m tl tr).

Requirement 10: Literal Dereliction


  Lemma LiteralDereliction : forall ls : list Lit, rsub (intersect ls) (Intersect ls).

Requirement 11: Intersector Integrated

Requirement 12: Literal Promotion


  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

Introduction


S

Section3_Proofs
Section3_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