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

Require Import List.
Require Import Nat.
Require Import Util.
Require Import Wf.
Require Import Wellfounded.Inverse_Image.
Require Import Section3_Requirements.
Require Import Section3_Infrastructure.
Require Import Section3_Proofs.

Import Relation_Operators.
Import List.
Import ListNotations.

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).
  Arguments sig2T { 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).
    destruct v. apply c.
  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))
  .
  Arguments dsubda : clear implicits.

End Integrator.
Arguments Intersect {Lit}.
Arguments Integrate {Lit}.
Arguments Integrated_int {Lit}.
Arguments Integrated {Lit}.
Arguments Exists_Intersection {Lit}.
Arguments sig2T {A B}.
Arguments dsubda {Lit DRule}.
Arguments dsubda_refl {Lit DRule DPremise}.
Arguments dsubda_trans {Lit DRule DPremise}.
Arguments dsubda_assume {Lit DRule DPremise}.
Arguments dsubda_lit {Lit DRule DPremise}.
Arguments dsubda_top {Lit DRule DPremise}.
Arguments dsubda_bot {Lit DRule DPremise}.
Arguments dsubda_uni_l {Lit DRule DPremise}.
Arguments dsubda_uni_rl {Lit DRule DPremise}.
Arguments dsubda_uni_rr {Lit DRule DPremise}.
Arguments dsubda_int_r {Lit DRule DPremise}.
Arguments dsubda_int_ll {Lit DRule DPremise}.
Arguments dsubda_int_lr {Lit DRule DPremise}.
Arguments dsubda_dist {Lit DRule DPremise}.

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).
  Import M_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).
  Arguments ruisub : clear implicits.

  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.

Arguments SopIntegrate {Lit}.
Arguments SopIntegrated {Lit}.
Arguments ui2sop {Lit}.
Arguments sop2ui {Lit}.
Arguments polof {Lit}.
Arguments polof_lit {Lit}.
Arguments polof_top {Lit}.
Arguments polof_int {Lit}.
Arguments sopof {Lit}.
Arguments sopof_pol {Lit}.
Arguments sopof_bot {Lit}.
Arguments sopof_uni {Lit}.
Arguments ProductOfLiterals {Lit}.
Arguments POL_top {Lit}.
Arguments POL_lit {Lit}.
Arguments POL_int {Lit}.
Arguments SumOfProducts {Lit}.
Arguments SOP_bot {Lit}.
Arguments SOP_uni {Lit}.
Arguments SOP_prod {Lit}.
Arguments ssub {Lit}.
Arguments ruisub {Lit}.
Arguments suisub {Lit}.
Arguments ruirec {Lit}.
Arguments suirec {Lit}.

This page has been generated by coqdoc