Library SS5

Judgmental subtyping system with intersection types and modal types.
  • Author : Jeongbong Seo and Sungwoo Park
This file contains definitions, lemmas, and theorems of the subtyping systems based on modal logic S5 which are described in Section 4 of the paper.

Contents:
  • Definition
    • Pre-terms
    • Relational subtyping system
    • Judgmental subtyping system
      • Auxiliary functions
      • Subtyping judgments
      • The subsets of subtyping inference rules
    • Other auxiliary functions
  • Infrastructure lemmas
    • Lemmas for the relational subtyping system
      • Weakening and associativity
      • Conversion between Conj and Conj_right
      • The distributivity of function types over intersection types
      • Permutation (Commutativity)
      • More properties of the auxiliary functions
    • Lemmas for the judgmental subtyping system
      • Lemmas for case analysis on the remote node context
      • All all contexts are empty
      • General ver. of the rules j_refl and j_refl_v
      • Context permutation
      • Weakening
      • A type in the ordinary subtyping context can be moved to the global subtyping context
      • Invertible rules
      • Contraction
      • Contraction of empty local subtyping contexts
    • Other lemmas
  • Admissibility of the cut rules
  • Equivalence between the two subtyping systems
    • Completeness
    • Soundness

Set Implicit Arguments.

Require Export Coq.Lists.List.
Require Export Arith.
Require Export SfLib.
Require Export Subseq.
Require Import Permutation.
Require Export Perm_tactic.
Require Export wpermute.

Ltac inv H := inversion H; clear H; subst.
Ltac destruct_in H := destruct (in_split _ _ H) as [?l1 [?l2 ?Hl1l2]]; clear H; subst.

Definition


This file contains definitions of the subtyping systems based on modal logic S5 which are described in Section 4 of the paper.

Pre-terms


There are four type constructors:
  • A --> B denotes function types.
  • A & B denotes intersection types.
  • A denotes necessity modal types.
  • <> A denotes possibility modal types.

Notation base := nat.

Inductive typ : Set :=
  | typ_base : base -> typ (* primitive type *)
  | typ_arrow : typ -> typ -> typ (* function type *)
  | typ_conj : typ -> typ -> typ (* intersection type *)
  | typ_box : typ -> typ (* necessity modal type *)
  | typ_dia : typ -> typ. (* possibility modal type *)

Notation " A --> B " := (typ_arrow A B) (at level 64, right associativity).
Notation " A & B " := (typ_conj A B) (at level 65, right associativity).
Notation " [] A " := (typ_box A) (at level 65).
Notation " <> A " := (typ_dia A) (at level 65).

(* Tactic for labeling cases. *)
Tactic Notation "typ_cases" tactic(first) tactic(c) :=
  first;
  [ c "typ_base" | c "typ_arrow" | c "typ_conj"
  | c "typ_box" | c "typ_dia"
  ].

Proposition typ_dec: forall (a b: typ), {a = b} + {a <> b}.
Proof.
  decide equality. apply eq_nat_dec.
Qed.

Proposition typ_pair_dec: forall (a b: typ*typ), {a = b} + {a <> b}.
Proof.
  decide equality; apply typ_dec.
Qed.

We represent the ordinary and global subtyping contexts as a list of typ.

Notation env := (list typ).
Notation empty := (@nil typ).

We represent the remote node context as a list of lists of typ. We will call each element as a local subtyping context.

Notation worlds := (list (list typ)).
Notation noworld := (@nil (list typ)).

We define the size of a type as the number of type constructors appearing in the type.

Fixpoint size_typ (t:typ) :=
  match t with
  | typ_base _ => 0
  | typ_arrow t1 t2 => S (size_typ t1 + size_typ t2)
  | typ_conj t1 t2 => S (size_typ t1 + size_typ t2)
  | typ_box t => S (size_typ t)
  | typ_dia t => S (size_typ t)
  end.

We define the size of a local subtyping context as the sum of the size of every type in the context.

Fixpoint size_env (ctx:env) :=
  match ctx with
  | nil => 0
  | A::ctx' => size_typ A + size_env ctx'
  end.

Relational subtyping system


For the relational subtyping system, we use the following notation 'A =< B' and it means that if an expression has type A then it also has type B. Inference rules are direct translations from the rules in Figure 1 in the paper.

Reserved Notation " A =< B " (at level 80).

Inductive r_sub : typ -> typ -> Prop :=
  | r_refl : forall (t : typ),
    t =< t

  | r_trans : forall (t1 t2 t3 : typ),
    t1 =< t2 ->
    t2 =< t3 ->
    t1 =< t3

  | r_and_l1 : forall (t1 t2 : typ),
    t1 & t2 =< t1

  | r_and_l2 : forall (t1 t2 : typ),
    t1 & t2 =< t2

  | r_and_r : forall (t1 t2 t3 : typ),
    t1 =< t2 ->
    t1 =< t3 ->
    t1 =< t2 & t3

  | r_fun : forall (t1 t2 t1' t2' : typ),
    t1' =< t1 ->
    t2 =< t2' ->
    t1 --> t2 =< t1'--> t2'

  | r_fun_dist : forall (t1 t2 t3 : typ),
    (t1 --> t2) & (t1 --> t3) =< t1 --> (t2 & t3)

  | r_box_T : forall (t : typ),
    [] t =< t

  | r_box_4 : forall (t : typ),
    [] t =< [] ( [] t )

  | r_box_K : forall (t1 t2 : typ),
    t1 =< t2 ->
    [] t1 =< [] t2

  | r_box_dist : forall (t1 t2 : typ),
    ([] t1) & ([] t2) =< [] (t1 & t2)

  | r_dia_T : forall (t : typ),
    t =< <> t

  | r_dia_4 : forall (t : typ),
    <> ( <>t ) =< <>t

  | r_dia_K : forall (t1 t2 :typ),
    t1 =< t2 ->
    <> t1 =< <> t2

  | r_box_dia_K : forall (t1 t2 t3 : typ),
    ([] t1) & t2 =< t3 ->
    ([] t1) & (<> t2) =< <> t3

  | r_dia_5 : forall (t: typ),
    <> t =< [] (<> t)

  | r_box_5 : forall (t: typ),
    <> ([] t) =< [] t

where "A =< B" := (r_sub A B).

Hint Constructors r_sub.

Tactic Notation "r_sub_cases" tactic(first) tactic(c) :=
  first;
  [ c "r_refl" | c "r_trans" | c "r_and_l1" | c "r_and_l2"
  | c "r_and_r" | c "r_fun" | c "r_fun_dist"
  | c "r_box_T" | c "r_box_4" | c "r_box_K" | c "r_box_dist"
  | c "r_dia_T" | c "r_dia_4" | c "r_dia_K" | c "r_box_dia_K"
  | c "r_dia_5" | c "r_box_5"
  ].

Judgmental subtyping system


Auxiliary functions


These auxiliary functions are used to encode the rule j_fun of the judgmental subtyping system.

pickFun collects all function types from a typing context and converts each of them into type pairs (argument type and result type).
e.g. pickFun [P, A1-->B1, A2-->B2, A3 & A4] returns [(A1,B1), (A2,B2)].

fsttypList gets a list of type pairs and filters out the second element of each pair.
e.g. fstypList [(A1,B1), (A2,B2)] returns [A1, A2].

sndtypList gets a list of type pairs and filters out the first element of each pair.
e.g. fstypList [(A1,B1), (A2,B2)] returns [B1, B2].

makeFunList produces a list of function types from a list of type pairs.
e.g. makeFunList [(A1,B1), (A2,B2)] returns [A1-->B1, A2-->B2].

Fixpoint pickFun (l : env) : list (typ*typ) :=
  match l with
  | nil => nil
  | (X --> Y) :: l' => (X,Y) :: pickFun l'
  | _ :: l' => pickFun l'
  end.

Definition fsttypList l := map (@fst typ typ) l.
Definition sndtypList l := map (@snd typ typ) l.

Definition makeFunList l := map (prod_curry typ_arrow) l.

Subtyping judgments


For judgmental subtyping system, we use the following judgment Delta;; Gamma; Sigma ~< B. Delta is the remote node context, Gamma is the global subtyping context, and Sigma is the ordinary subtyping context. Inference rules are from Figure 6 in the paper.

To encode the rule j_fun, we use three auxiliary functions and one inductive definition: pickFun, fsttypList, sndtypList, and subseq. We first collect all function types from Gamma and Sigma using pickFun, then pick some of them using subseq. We decompose gathered function types into argument types and result types using fsttypList and sndtypList, and use them to state premises.

Reserved Notation "D ;; G ; S ~< B " (at level 80).

Inductive j_sub : worlds -> env -> env -> typ -> Prop :=
  | j_refl_v : forall (Delta:worlds) (Gamma1 Gamma2 Sigma:env) (b:base),
    Delta ;; Gamma1 ++ (typ_base b) :: Gamma2; Sigma ~< typ_base b

  | j_refl : forall (Delta:worlds) (Gamma Sigma1 Sigma2:env) (b:base),
    Delta ;; Gamma ; Sigma1 ++ (typ_base b) :: Sigma2 ~< typ_base b

  | j_fun : forall (Delta:worlds) (Gamma Sigma:env) (t1' t2':typ) (Sigma':list (typ*typ)),
    subseq Sigma' (pickFun Gamma ++ pickFun Sigma) ->
    (forall t, In t (fsttypList Sigma') -> noworld ;; empty; [t1'] ~< t) ->
    noworld ;; empty; (sndtypList Sigma') ~< t2' ->
    Delta ;; Gamma; Sigma ~< t1' --> t2'
    
  | j_and_lc : forall (Delta1 Delta2 : worlds) (Gamma Sigma Sigma1 Sigma2 : env) (t1 t2 t3 : typ),
    Delta1 ++ (Sigma1 ++ t1 :: t2 :: Sigma2) :: Delta2 ;; Gamma; Sigma ~< t3 ->
    Delta1 ++ (Sigma1 ++ (t1 & t2) :: Sigma2) :: Delta2 ;; Gamma; Sigma ~< t3

  | j_and_v : forall (Delta:worlds) (Gamma1 Gamma2 Sigma:env) (t1 t2 t3:typ),
    Delta ;; (Gamma1 ++ t1 :: t2 :: Gamma2); Sigma ~< t3 ->
    Delta ;; (Gamma1 ++ (t1 & t2) :: Gamma2); Sigma ~< t3

  | j_and_l : forall (Delta:worlds) (Gamma Sigma1 Sigma2:env) (t1 t2 t3:typ),
    Delta ;; Gamma ; (Sigma1 ++ t1 :: t2 :: Sigma2) ~< t3 ->
    Delta ;; Gamma ; (Sigma1 ++ (t1 & t2) :: Sigma2) ~< t3

  | j_and_r : forall (Delta:worlds) (Gamma Sigma:env) (t1 t2:typ),
    Delta ;; Gamma; Sigma ~< t1 ->
    Delta ;; Gamma; Sigma ~< t2 ->
    Delta ;; Gamma; Sigma ~< (t1 & t2)

  | j_box_lc : forall (Delta1 Delta2 : worlds) (Gamma Gamma1 Gamma2 Sigma Sigma1 Sigma2 : env) (t1 t2 : typ),
    Delta1 ++ (Sigma1 ++ Sigma2) :: Delta2 ;; Gamma1 ++ t1 :: Gamma2; Sigma ~< t2 ->
    Gamma = Gamma1 ++ Gamma2 ->
    Delta1 ++ (Sigma1 ++ ([]t1) :: Sigma2) :: Delta2 ;; Gamma; Sigma ~< t2

  | j_box_v : forall (Delta:worlds) (Gamma1 Gamma2 Sigma: env) (t1 t2:typ),
    Delta ;; Gamma1 ++ t1 :: Gamma2; Sigma ~< t2 ->
    Delta ;; Gamma1 ++ ([]t1) :: Gamma2; Sigma ~< t2

  | j_box_l : forall (Delta:worlds) (Gamma Gamma1 Gamma2 Sigma1 Sigma2: env) (t1 t2:typ),
    Delta ;; Gamma1 ++ t1 :: Gamma2; Sigma1 ++ Sigma2 ~< t2 ->
    Gamma = Gamma1 ++ Gamma2 ->
    Delta ;; Gamma; Sigma1 ++ ([]t1) :: Sigma2 ~< t2

  | j_box_r : forall (Delta Delta1 Delta2:worlds) (Gamma Sigma: env) (t:typ),
    Delta1 ++ Sigma :: Delta2 ;; Gamma; empty ~< t ->
    Delta = Delta1 ++ Delta2 ->
    Delta ;; Gamma; Sigma ~< [] t

  | j_dia_lc : forall (Delta1 Delta2 : worlds) (Gamma Sigma Sigma1 Sigma2 : env) (t1 t2 : typ),
    Delta1 ++ (Sigma1 ++ Sigma2) :: [t1] :: Delta2 ;; Gamma; Sigma ~< t2 ->
    Delta1 ++ (Sigma1 ++ (<>t1) :: Sigma2) :: Delta2 ;; Gamma; Sigma ~< t2

  | j_dia_v : forall (Delta Delta1 Delta2 : worlds) (Gamma1 Gamma2 Sigma : env) (t1 t2 : typ),
    Delta1 ++ [t1] :: Delta2 ;; Gamma1 ++ Gamma2; Sigma ~< t2 ->
    Delta = Delta1 ++ Delta2 ->
    Delta ;; Gamma1 ++ (<>t1) :: Gamma2; Sigma ~< t2

  | j_dia_l : forall (Delta Delta1 Delta2 : worlds) (Gamma Sigma1 Sigma2 : env) (t1 t2 : typ),
    Delta1 ++ [t1] :: Delta2 ;; Gamma; Sigma1 ++ Sigma2 ~< t2 ->
    Delta = Delta1 ++ Delta2 ->
    Delta ;; Gamma; Sigma1 ++ (<>t1) :: Sigma2 ~< t2

  | j_dia_r : forall (Delta1 Delta2:worlds) (Gamma Sigma' Sigma:env) (t:typ),
    Delta1 ++ Sigma :: Delta2 ;; Gamma; Sigma' ~< t ->
    Delta1 ++ Sigma' :: Delta2 ;; Gamma; Sigma ~< <> t

  | j_dia_r' : forall (Delta:worlds) (Gamma Sigma:env) (t:typ),
    Delta ;; Gamma; Sigma ~< t ->
    Delta ;; Gamma; Sigma ~< <> t

where " Delta ;; Gamma ; Sigma ~< B " := (j_sub Delta Gamma Sigma B).

Hint Constructors j_sub.

Tactic Notation "j_sub_cases" tactic(first) tactic(c) :=
  first;
  [ c "j_refl_v" | c "j_refl" | c "j_fun"
  | c "j_and_lc" | c "j_and_v" | c "j_and_l" | c "j_and_r"
  | c "j_box_lc" | c "j_box_v" | c "j_box_l" | c "j_box_r"
  | c "j_dia_lc" | c "j_dia_v" | c "j_dia_l" | c "j_dia_r"
  | c "j_dia_r'"
  ].

The subsets of subtyping inference rules.


To use the proof strategy explained in Section 2.2 of the paper, we need additional judgments that are capable of specifying the principal type of the derivation.

A type in the remote node context is focused.

Delta,, (PSigma, |A|) ;; Gamma; Sigma ~< B means that A is the principal type of the last inference rule in its derivation.

Reserved Notation " Delta ,, PSigma , | A | ;; Gamma ; Sigma ~< B " (at level 80).

Inductive j_sub_lcf : worlds -> env -> typ -> env -> env -> typ -> Prop :=
  | j_and_lcf : forall (Delta Delta1 Delta2 : worlds)
    (Gamma PSigma Sigma Sigma1 Sigma2 : env) (t1 t2 t3 : typ),
    Delta1 ++ (Sigma1 ++ t1 :: t2 :: Sigma2) :: Delta2 ;; Gamma; Sigma ~< t3 ->
    Delta = Delta1 ++ Delta2 ->
    PSigma = Sigma1 ++ Sigma2 ->
    Delta,, PSigma, | t1 & t2 |;; Gamma; Sigma ~< t3

  | j_box_lcf : forall (Delta Delta1 Delta2 : worlds)
    (Gamma Gamma1 Gamma2 PSigma Sigma: env) (t1 t2 : typ),
    Delta1 ++ PSigma :: Delta2 ;; Gamma1 ++ t1 :: Gamma2; Sigma ~< t2 ->
    Gamma = Gamma1 ++ Gamma2 ->
    Delta = Delta1 ++ Delta2 ->
    Delta,, PSigma, | []t1 |;; Gamma; Sigma ~< t2

  | j_dia_lcf : forall (Delta Delta1 Delta2 : worlds) (Gamma PSigma Sigma: env) (t1 t2 : typ),
    Delta1 ++ PSigma :: [t1] :: Delta2 ;; Gamma; Sigma ~< t2 ->
    Delta = Delta1 ++ Delta2 ->
    Delta,, PSigma, | <>t1 |;; Gamma; Sigma ~< t2

where " Delta ,, PSigma , | A | ;; Gamma ; Sigma ~< B " := (j_sub_lcf Delta PSigma A Gamma Sigma B).

Hint Constructors j_sub_lcf.

Tactic Notation "j_sub_lcf_cases" tactic(first) tactic(c) :=
  first;
  [ c "j_and_lcf" | c "j_box_lcf" | c "j_dia_lcf" ].

A type in the global subtyping context is focused.

Delta;; Gamma, |A|; Sigma ~< B means that A is the principal type of the last inference rule in its derivation.

Reserved Notation "Delta ;; Gamma , | A | ; Sigma ~< B " (at level 80).

Inductive j_sub_vf : worlds -> env -> typ -> env -> typ -> Prop :=
  | j_refl_vf : forall (Delta:worlds) (Gamma Sigma:env) (b:base),
    Delta ;; Gamma, | typ_base b |; Sigma ~< typ_base b

  | j_fun_vf : forall (Delta:worlds) (Gamma Gamma1 Gamma2 Sigma:env)
    (t1 t2 t1' t2':typ) (Gamma1' Gamma2' Sigma':list (typ*typ)),
    subseq Gamma1' (pickFun Gamma1) ->
    subseq Gamma2' (pickFun Gamma2) ->
    subseq Sigma' (pickFun Sigma) ->
    Gamma = Gamma1 ++ Gamma2 ->
    (forall t, In t (fsttypList ((Gamma1' ++ (t1,t2) :: Gamma2') ++ Sigma')) -> noworld;; empty; [t1'] ~< t) ->
    noworld;; empty; (sndtypList ((Gamma1' ++ (t1,t2) :: Gamma2') ++ Sigma')) ~< t2' ->
    Delta;; Gamma, |(t1 --> t2)|; Sigma ~< t1' --> t2'
    
  | j_and_vf : forall (Delta:worlds) (Gamma Gamma1 Gamma2 Sigma:env) (t1 t2 t3:typ),
    Delta ;; (Gamma1 ++ t1 :: t2 :: Gamma2); Sigma ~< t3 ->
    Gamma = Gamma1 ++ Gamma2 ->
    Delta ;; Gamma, | t1 & t2 |; Sigma ~< t3

  | j_box_vf : forall (Delta:worlds) (Gamma Gamma1 Gamma2 Sigma: env) (t1 t2:typ),
    Delta ;; Gamma1 ++ t1 :: Gamma2; Sigma ~< t2 ->
    Gamma = Gamma1 ++ Gamma2 ->
    Delta ;; Gamma, | []t1 |; Sigma ~< t2

  | j_dia_vf : forall (Delta Delta1 Delta2 : worlds) (Gamma Sigma : env) (t1 t2 : typ),
    Delta1 ++ [t1] :: Delta2 ;; Gamma; Sigma ~< t2 ->
    Delta = Delta1 ++ Delta2 ->
    Delta ;; Gamma, | <>t1 |; Sigma ~< t2

where " Delta ;; Gamma , | A | ; Sigma ~< B " := (j_sub_vf Delta Gamma A Sigma B).

Hint Constructors j_sub_vf.

Tactic Notation "j_sub_vf_cases" tactic(first) tactic(c) :=
  first;
  [ c "j_refl_vf" | c "j_fun_vf"
  | c "j_and_vf" | c "j_box_vf" | c "j_dia_vf"
  ].

A type in the ordinary subtyping context is focused.

Delta;; Gamma; Sigma, |A| ~< |B| means that A is the principal type of the last inference rule in its derivation.

Reserved Notation "Delta ;; Gamma ; Sigma , | A | ~< B " (at level 80).

Inductive j_sub_lf : worlds -> env -> env -> typ -> typ -> Prop :=
  | j_refl_lf : forall (Delta:worlds) (Gamma Sigma:env) (b:base),
    Delta ;; Gamma ; Sigma, | typ_base b | ~< typ_base b

  | j_fun_lf : forall (Delta:worlds) (Gamma Sigma Sigma1 Sigma2:env)
    (t1 t2 t1' t2':typ) (Gamma' Sigma'1 Sigma'2:list (typ*typ)),
    subseq Gamma' (pickFun Gamma) ->
    subseq Sigma'1 (pickFun Sigma1) ->
    subseq Sigma'2 (pickFun Sigma2) ->
    Sigma = Sigma1 ++ Sigma2 ->
    (forall t, In t (fsttypList (Gamma' ++ (Sigma'1 ++ (t1,t2) :: Sigma'2))) -> noworld;; empty; [t1'] ~< t) ->
    noworld;; empty; (sndtypList (Gamma' ++ (Sigma'1 ++ (t1,t2) :: Sigma'2))) ~< t2' ->
    Delta ;; Gamma; Sigma, | t1 --> t2 | ~< t1' --> t2'

  | j_and_lf : forall (Delta:worlds) (Gamma Sigma Sigma1 Sigma2:env) (t1 t2 t3:typ),
    Delta ;; Gamma ; (Sigma1 ++ t1 :: t2 :: Sigma2) ~< t3 ->
    Sigma = Sigma1 ++ Sigma2 ->
    Delta ;; Gamma ; Sigma, | t1 & t2 | ~< t