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




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
  | typ_arrow : typ -> typ -> typ
  | typ_conj : typ -> typ -> typ
  | typ_box : typ -> typ
  | typ_dia : typ -> typ.
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 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}.

Proposition typ_pair_dec: forall (a b: typ*typ), {a = b} + {a <> b}.

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


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


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


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


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 | ~< t3

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

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

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


Tactic Notation "j_sub_lf_cases" tactic(first) tactic(c) :=
  first;
  [ c "j_refl_lf" | c "j_fun_lf"
  | c "j_and_lf" | c "j_box_lf" | c "j_dia_lf"
  ].

The right-side is focused.

Delta;; Gamma; Sigma ~< |B| means B is the principal type of Delta;; Gamma; Sigma ~< B; B is involved at the last inference rule.

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

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

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

  | j_fun_rf : 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_rf : forall (Delta:worlds) (Gamma Sigma:env) (t1 t2:typ),
    Delta ;; Gamma; Sigma ~< t1 ->
    Delta ;; Gamma; Sigma ~< t2 ->
    Delta ;; Gamma; Sigma ~< | t1 & t2 |

  | j_box_rf : 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_rf : forall (Delta Delta1 Delta2:worlds) (Gamma Sigma' Sigma:env) (t:typ),
    Delta1 ++ Sigma :: Delta2 ;; Gamma; Sigma' ~< t ->
    Delta1 ++ Sigma' :: Delta2 ;; Gamma; Sigma ~< | <> t |

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

where " Delta ;; Gamma ; Sigma ~< | A |" := (j_sub_rf Delta Gamma Sigma A).


Tactic Notation "j_sub_rf_cases" tactic(first) tactic(c) :=
  first;
  [ c "j_refl_v_rf" | c "j_refl_rf" | c "j_fun_rf"
  | c "j_and_rf" | c "j_box_rf" | c "j_dia_rf" | c "j_dia_rf'"
  ].

Other auxiliary functions


Following functions are used to convert a subtyping judgment to a corresponding subtyping relation. They are used to prove the equivalence between the two subtyping systems.

Conj family

Conj and Conj_right convert a typing context to a single type by recursively building an intersection type using types in the context.

They requires an initial type in case an empty context is given because there is no corresponding type for an empty context, e.g.,
Conj [] A returns A



Conj combines elements right associatively while Conj_right combines elements right associatively; e.g.,
Conj [A1, A2, A3] A returns A1 & (A2 & (A3 & A))

whereas
Conj_right A [A1, A2, A3] returns ((A & A1) & A2) & A3.


Definition Conj (hd:env) (tl:typ) := fold_right typ_conj tl hd.

Example conj_id_A : forall A,
  Conj empty A = A.

Example conj_id_A_B_C_D : forall A B C D,
  Conj [A, B, C] D = A & B & C & D.

Proposition Conj_one_step: forall A Gamma At,
  Conj (A::Gamma) At = A & Conj Gamma At.

Definition Conj_right (hd:typ) (tl:env) := fold_left typ_conj tl hd.

Example conj_right_id_A : forall A,
  Conj_right A empty = A.

Example conj_right_id_A_B_C_D : forall A B C D,
  Conj_right A [B, C, D] = ((A & B) & C) & D.

Proposition Conj_right_one_step: forall A Gamma Ah,
  Conj_right Ah (A::Gamma) = Conj_right (Ah & A) Gamma.

box_Conj and box_Conj_right work in the similar way except that they apply necessity modal type constructor to each type. Note that they do not change the initial type. For example,
box_Conj [A1, A2, A3] A returns []A1 & []A2 & [] A3 & A.


Definition box_Conj (hd:env) (tl:typ) := Conj (map typ_box hd) tl.
Definition box_Conj_right (hd:typ) (tl:env) := Conj_right hd (map typ_box tl).

Example conj_box_A: forall A,
  box_Conj empty ([]A) = [] A.

Example conj_box_A_B_C_D : forall A B C D,
  box_Conj [A, B, C] ([]D) =([] A) & ([] B) & ([] C) & ([] D).

Proposition box_Conj_one_step: forall A Gamma At,
  box_Conj (A::Gamma) At = ([] A) & box_Conj Gamma At.

Example conj_right_box_A : forall A,
  box_Conj_right ([]A) empty = [] A.

Example conj_right_box_A_B_C_D : forall A B C D,
  box_Conj_right ([]A) [B, C, D] = ((([]A) & ([]B)) & ([]C)) & ([]D).

Proposition box_Conj_right_one_step: forall A Gamma Ah,
  box_Conj_right Ah (A::Gamma) = box_Conj_right (Ah & [] A) Gamma.

del_to_tup and del_to_typ_right convert the remote node context into a single type. Note that they do not change the initial type, either. For example,
del_to_typ [[A11, A12], [A21, A22]] A returns <>(A11 & A12) & <>(A21 & A22) & A.


Definition del_to_typ_aux (PSigma:env) (A:typ) :=
  match PSigma with
  | nil => A
  | B::PSigma' => <> (Conj_right B PSigma') & A
  end.

Definition del_to_typ (Delta:worlds) (A:typ) : typ :=
  fold_right (del_to_typ_aux ) A Delta.

Definition del_to_typ_right_aux (A:typ) (PSigma:env) :=
  match PSigma with
  | nil => A
  | B::PSigma' => A & <> (Conj_right B PSigma')
  end.

Definition del_to_typ_right (A:typ) (Delta:worlds) : typ :=
  fold_left (del_to_typ_right_aux ) Delta A.

Following tactics rewrite a sub-expression in the goal by unfolding functions including map or Conj_right. For instance, push_box changes any occurrence of the form ([] A)::(map typ_box L) in the goal to map typ_box (A::L).

Tactic Notation "push_box" :=
  match goal with
  | |- context[(typ_box ?x)::map typ_box ?L] =>
    change ((typ_box x)::map typ_box L) with (map typ_box (x::L))
  | _ => idtac
  end.

Tactic Notation "push_dia" :=
  match goal with
  | |- context[(typ_dia (Conj_right ?x ?xs)) & del_to_typ ?D ?A] =>
    change ((typ_dia (Conj_right x xs)) & del_to_typ D A) with (del_to_typ ((x::xs)::D) A)
  | |- context[(typ_dia ?x) & del_to_typ ?D ?A] =>
    change ((typ_dia x) & del_to_typ D A) with (del_to_typ ([x]::D) A)
  | _ => idtac
  end.

Tactic Notation "push_conj_right" :=
  match goal with
  | |- context[Conj_right (?A & ?B) ?L] =>
    change (Conj_right (A&B) L) with (Conj_right A (B::L))
  | _ => idtac
  end.

Tactic Notation "push_del_to_typ_right" :=
  match goal with
  | |- context[del_to_typ_right (?A & (typ_dia (Conj_right ?B ?C))) ?L] =>
    change (del_to_typ_right (A&<>(Conj_right B C)) L) with (del_to_typ_right A ((B::C)::L))
  | |- context[del_to_typ_right (?A & (typ_dia ?B)) ?L] =>
    change (del_to_typ_right (A&<>B) L) with (del_to_typ_right A ([B]::L))
  | _ => idtac
  end.

fun_dist


fun_dist A hd tl is to express the distributivity of function types over intersection types; A is an argument type, tl is one result type, and hd is a set of remaining result types.

For example, fun_dist A [B1, B2] B3 returns (A-->B1) & (A-->B2) & (A-->B3).

Definition fun_dist (A:typ) (hd:env) (tl:typ) := Conj (map (typ_arrow A) hd) (A --> tl).

Example fun_dist_B : forall A B,
  fun_dist A empty B = A --> B.

Example fun_dist_B1_B2_B3 : forall A B1 B2 B3,
  fun_dist A [B1, B2] B3 = (A-->B1) & (A-->B2) & (A-->B3).

Proposition fun_dist_one_step: forall B1 Y1 Y2 Ys,
  fun_dist B1 (Y2 :: Ys) Y1 = B1 --> Y2 & fun_dist B1 Ys Y1.

n_list


n_list n x returns a list consisting of n xs, e.g., n_list 3 "a" returns ["a", "a", "a"].

It is used to encode global contexts consisting of empty local contexts such that
[], [[]], [[], []], [[], [], []], ...


Fixpoint n_list {X:Type} (n:nat) (x:X) : list X :=
  match n with
    | O => nil
    | S n' => x :: (n_list n' x)
  end.

Infrastructure lemmas


Lemmas for the relational subtyping system


This section contains infrastructure lemmas of the relational subtyping system based on modal logic S5 which is described in Section 4 of the paper.

Weakening and associativity

Following two lemmas are weakening lemmas.

Lemma sub_weakening_left: forall A B C,
  A =< B ->
  A & C =< B & C.

Lemma sub_weakening_right: forall A B C,
  A =< B ->
  C & A =< C & B.

left_weak works like a rule
 A =< C
----------
A & B =< C

and right_weak works like a rule
 B =< C
----------
A & B =< C


Tactic Notation "left_weak" :=
  match goal with
    | |- ?A & ?B =< _ =>
      constructor 2 with A; [auto|]
    | _ => idtac
  end.

Tactic Notation "right_weak" :=
  match goal with
    | |- ?A & ?B =< _ =>
      constructor 2 with B; [auto|]
    | _ => idtac
  end.


Lemma sub_conj: forall A A' B B',
  A =< A' ->
  B =< B' ->
  A & B =< A' & B'.


We can generalize the lemma sub_weakening_left using Conj_right and del_to_typ_right_sub.

Lemma Conj_right_sub: forall Sigma A B,
  A =< B ->
  Conj_right A Sigma =< Conj_right B Sigma.


Lemma del_to_typ_right_sub: forall Delta A B,
  A =< B ->
  del_to_typ_right A Delta =< del_to_typ_right B Delta.

Following lemmas are related to the associativity of the intersection types.

Lemma r_sub_assoc_left: forall A B C,
  (A & B) & C =< A & (B & C).

Lemma r_sub_assoc_right: forall A B C,
  A & (B & C) =< (A & B) & C.



Lemma Conj_right_assoc: forall Sigma1 Sigma2 A B1 B2,
  Conj_right A (Sigma1 ++ (B1 & B2) :: Sigma2) =< Conj_right A (Sigma1 ++ B1 :: B2 :: Sigma2).

Lemma box_Conj_right_assoc: forall Sigma1 Sigma2 A B1 B2,
  box_Conj_right A (Sigma1 ++ (B1 & B2) :: Sigma2) =< box_Conj_right A (Sigma1 ++ B1 :: B2 :: Sigma2).

Conversion between Conj and Conj_right


The differences between Conj and Conj_right are the position of the initial type and the way the initial type combines with other types. But they are equivalent to each other (=they are subtype of each other) and we may use them interchangeably.

Lemma Conj_right_Conj: forall Gamma A,
  Conj_right A Gamma =< Conj Gamma A.

Lemma Conj_Conj_right: forall Gamma A,
  Conj Gamma A =< Conj_right A Gamma.


Lemma del_to_typ_del_to_typ_right: forall Delta A,
  del_to_typ Delta A =< del_to_typ_right A Delta.

Lemma del_to_typ_right_del_to_typ: forall Delta A,
  del_to_typ_right A Delta =< del_to_typ Delta A.

Exchange Conj_right and Conj or del_to_typ and del_to_typ_right.

Tactic Notation "switch_left" :=
  match goal with
    | |- Conj_right ?A ?C =< _ => constructor 2 with (Conj C A); [apply Conj_right_Conj |]
    | |- Conj ?C ?A =< _ => constructor 2 with (Conj_right A C); [apply Conj_Conj_right |]
    | |- del_to_typ_right ?A ?C =< _ => constructor 2 with (del_to_typ C A); [apply del_to_typ_right_del_to_typ |]
    | |- del_to_typ ?C ?A =< _ => constructor 2 with (del_to_typ_right A C); [apply del_to_typ_del_to_typ_right |]
    | _ => idtac
  end.

Tactic Notation "switch_right" :=
  match goal with
    | |- _ =< Conj_right ?A ?C => constructor 2 with (Conj C A); [| apply Conj_Conj_right]
    | |- _ =< Conj ?C ?A => constructor 2 with (Conj_right A C); [| apply Conj_right_Conj]
    | |- _ =< del_to_typ_right ?A ?C => constructor 2 with (del_to_typ C A); [| apply del_to_typ_del_to_typ_right]
    | |- _ =< del_to_typ ?C ?A => constructor 2 with (del_to_typ_right A C); [| apply del_to_typ_right_del_to_typ]
    | _ => idtac
  end.

The distributivity of function types over intersection types.


We can extend the rule r_fun_dist to involve more then two argument types s.t.
(A --> B_1) & ... & (A --> B_n) =< A --> (B_1 & ... & B_n).



fun_dist and Conj help to encode this relation.

Lemma fun_dist_extend: forall A B Bs,
  fun_dist A Bs B =< A --> (Conj Bs B).


Following lemma corresponds to the rule j_fun in the judgmental subtyping system.
B1 =< X B1 =< X_i (for 1 <= i <= n) Y & Y1 & ... & Yn =< B2
---------------------------------------------------------------------
(X-->Y) & (X_1-->Y_1) & ... & (X_n-->Y_n) =< B1 --> B2


Lemma fun_dist_gen: forall (X Y B1 B2 : typ) (XYs : list (typ * typ)),
  (Conj (sndtypList XYs) Y) =< B2 ->
  B1 =< X ->
  (forall x, In x (fsttypList XYs) -> B1 =< x) ->
  Conj (makeFunList XYs) (X --> Y) =< B1 --> B2.

Permutation (Commutativity)


Following lemmas say that intersection types are commutative.

Lemma Conj_swap: forall t1 t2 A B,
  Conj (t1 ++ B :: t2) A =< Conj (t1 ++ A ::t2) B.


Lemma Conj_right_swap: forall t1 t2 A B,
  Conj_right A (t1 ++ B :: t2) =< Conj_right B (t1 ++ A ::t2).



Lemma Conj_swap_in: forall l1 l2 A B,
  Conj (A :: l1 ++ l2) B =< Conj (l1 ++ A :: l2) B.


Lemma Conj_right_swap_in: forall l1 l2 A B,
  Conj_right B (A :: l1 ++ l2) =< Conj_right B (l1 ++ A :: l2).


Lemma Conj_swap_in_conv: forall l1 l2 A B,
  Conj (l1 ++ A :: l2) B =< Conj (A :: l1 ++ l2) B.


Lemma Conj_right_swap_in_conv: forall l1 l2 A B,
  Conj_right B (l1 ++ A :: l2) =< Conj_right B (A :: l1 ++ l2).


Lemma del_to_typ_swap_in_conv: forall D1 D2 S A,
  del_to_typ (D1++S::D2) A =< del_to_typ (S::D1++D2) A.

Lemma del_to_typ_swap_in_in_conv: forall D S1 S2 C A,
  del_to_typ ((S1++C::S2)::D) A =< del_to_typ ((C::S1++S2)::D) A.

Lemma del_to_typ_swap_in: forall D1 D2 S A,
  del_to_typ (S::D1++D2) A =< del_to_typ (D1++S::D2) A.

Lemma del_to_typ_swap_in_in: forall D S1 S2 C A,
  del_to_typ ((C::S1++S2)::D) A =< del_to_typ ((S1++C::S2)::D) A.

Lemma del_to_typ_right_swap_in_conv: forall D1 D2 S A,
  del_to_typ_right A (D1++S::D2) =< del_to_typ_right A (S::D1++D2).

Lemma del_to_typ_right_swap_in_in_conv: forall D S1 S2 C A,
  del_to_typ_right A ((S1++C::S2)::D) =< del_to_typ_right A ((C::S1++S2)::D).

Lemma del_to_typ_right_swap_in: forall D1 D2 S A,
  del_to_typ_right A (S::D1++D2) =< del_to_typ_right A (D1++S::D2).

Lemma del_to_typ_right_swap_in_in: forall D S1 S2 C A,
  del_to_typ_right A ((C::S1++S2)::D) =< del_to_typ_right A ((S1++C::S2)::D).

Lemma del_to_typ_swap: forall D1 D2 S A B,
  del_to_typ (D1++(B::S)::D2) (<> A) =< del_to_typ (D1++[A]::D2) (<> (Conj_right B S)).

Lemma del_to_typ_right_swap: forall D1 D2 S A B,
  del_to_typ_right (<> A) (D1++(B::S)::D2) =< del_to_typ_right (<> (Conj_right B S)) (D1++[A]::D2).

Lemma del_to_typ_right_permute: forall D D' A,
  Permutation D D' ->
  del_to_typ_right A D =< del_to_typ_right A D'.

Following tactics facilitate applying the above lemmas.

Tactic Notation "move_mid_to_front" :=
  match goal with
    | |- Conj_right ?A (?C1++?B::?C2) =< _ =>
      constructor 2 with (Conj_right A (B::C1++C2)); [apply Conj_right_swap_in_conv |]
    | |- del_to_typ_right ?A ((?B1++?B::?B2)::?C) =< _ =>
      constructor 2 with (del_to_typ_right A ((B::B1++B2)::C));
        [ apply del_to_typ_right_swap_in_in_conv |]
    | |- del_to_typ_right ?A (?C1++?B::?C2) =< _ =>
      constructor 2 with (del_to_typ_right A (B::C1++C2)); [apply del_to_typ_right_swap_in_conv |]
    | |- del_to_typ_right (Conj_right ?A (?C1++?B::?C2)) ?D =< _ =>
      constructor 2 with (del_to_typ_right (Conj_right A (B::C1++C2)) D); [
        apply del_to_typ_right_sub; apply Conj_right_swap_in_conv |]
    | _ => idtac
  end.

Tactic Notation "move_mid_to_front_right" :=
  match goal with
    | |- _ =< Conj_right ?A (?C1++?B::?C2) =>
      constructor 2 with (Conj_right A (B::C1++C2)); [| apply Conj_right_swap_in]
    | |- _ =< del_to_typ_right ?A (?C1++?B::?C2) =>
      constructor 2 with (del_to_typ_right A (B::C1++C2)); [| apply del_to_typ_right_swap_in]
    | |- _ =< del_to_typ_right (Conj_right ?A (?C1++?B::?C2)) ?D =>
      constructor 2 with (del_to_typ_right (Conj_right A (B::C1++C2)) D);
        [| apply del_to_typ_right_sub; apply Conj_right_swap_in]
    | _ => idtac
  end.

Tactic Notation "move_front_to_mid" :=
  match goal with
    | |- Conj_right ?A (?B :: ?C1++?C2) =< _ =>
      constructor 2 with (Conj_right A (C1++B::C2)); [apply Conj_right_swap_in |]
    | |- del_to_typ_right ?A (?B :: ?C1++?C2) =< _ =>
      constructor 2 with (del_to_typ_right A (C1++B::C2)); [apply del_to_typ_right_swap_in |]
    | |- del_to_typ_right (Conj_right ?A (?B :: ?C1++?C2)) ?D =< _ =>
      constructor 2 with (del_to_typ_right (Conj_right A (C1++B::C2)) D);
        [apply del_to_typ_right_sub; apply Conj_right_swap_in |]
    | _ => idtac
  end.

Tactic Notation "move_front_to_mid_right" :=
  match goal with
    | |- _ =< Conj_right ?A (?B :: ?C1++?C2) =>
      constructor 2 with (Conj_right A (C1++B::C2)); [| apply Conj_right_swap_in_conv]
    | |- _ =< del_to_typ_right ?A (?B :: ?C1++?C2) =>
      constructor 2 with (del_to_typ_right A (C1++B::C2)); [| apply del_to_typ_right_swap_in_conv]
    | |- _ =< del_to_typ_right (Conj_right ?A (?B :: ?C1++?C2)) ?D =>
      constructor 2 with (del_to_typ_right (Conj_right A (C1++B::C2)) D);
        [| apply del_to_typ_right_sub; apply Conj_right_swap_in_conv]

    | _ => idtac
  end.

Tactic Notation "swap_init_mid" :=
  match goal with
    | |- Conj_right ?A (?C1++?B::?C2) =< _ =>
      constructor 2 with (Conj_right B (C1++A::C2)); [apply Conj_right_swap |]
    | |- del_to_typ_right (typ_dia ?A) (?C1++(?B::?B')::?C2) =< _ =>
      constructor 2 with (del_to_typ_right (typ_dia (Conj_right B B')) (C1++[A]::C2));
        [apply del_to_typ_right_swap |]
    | |- del_to_typ_right (Conj_right ?A (?C1++?B::?C2)) ?D =< _ =>
      constructor 2 with (del_to_typ_right (Conj_right B (C1++A::C2)) D);
        [apply del_to_typ_right_sub; apply Conj_right_swap |]
    | _ => idtac
  end.

Tactic Notation "swap_init_front" :=
  match goal with
    | |- Conj_right ?A (?B::?C) =< _ =>
        
      rewrite <- app_nil_l with _ (B::C); swap_init_mid; rewrite app_nil_l
    | |- del_to_typ_right (typ_dia ?A) ((?B::?B')::?C) =< _ =>
      rewrite <- app_nil_l with _ ((B::B')::C); swap_init_mid; rewrite app_nil_l
    | |- del_to_typ_right (Conj_right ?A (?B::?C)) ?D =< _ =>
        
      rewrite <- app_nil_l with _ (B::C); swap_init_mid; rewrite app_nil_l
    | _ => idtac
  end.

Tactic Notation "push_box_mid" :=
  match goal with
  | |- Conj_right _ ((typ_box _) :: map typ_box (_ ++ _) ++ _) =< _ =>
      rewrite map_app;
      rewrite <- app_assoc;
      move_front_to_mid;
      rewrite app_comm_cons;
      push_box;
      rewrite app_assoc;
      rewrite <- map_app
  end.

Tactic Notation "pop_box_mid" :=
  match goal with
  | |- Conj_right _ (map typ_box (_ ++ _ :: _) ++ _) =< _ =>
      rewrite map_app;
      simpl;
      rewrite <- app_assoc;
      rewrite <- app_comm_cons;
      move_mid_to_front;
      rewrite app_assoc;
      rewrite <- map_app
  end.

Tactic Notation "swap_and" :=
  match goal with
    | |- ?A & ?B =< _ =>
      constructor 2 with (B & A); [auto |]
    | _ => idtac
  end.

More properties of the auxiliary functions


Followings are other form of weakening lemmas using subseq and Conj.

Lemma Conj_subseq_weakening: forall l l' A C,
  subseq l l' ->
  Conj l A =< C ->
  Conj l' A =< C.

Lemma Conj_and : forall l A B,
  A =< B ->
  Conj l A =< B.


Lemma Conj_right_and: forall l A B,
  A =< B ->
  Conj_right A l =< B.


Lemma del_to_typ_right_and: forall Delta A B,
  A =< B ->
  del_to_typ_right A Delta =< B.

Lemma Conj_sub_middle: forall t1 t2 A B C,
  B =< C ->
  Conj (t1 ++ B :: t2) A =< C.


Lemma Conj_right_sub_middle: forall t1 t2 A B C,
  B =< C ->
  Conj_right A (t1 ++ B :: t2) =< C.


Lemma Conj_right_middle_subst: forall G1 G2 A B C,
  B =< C ->
  Conj_right A (G1++B::G2) =< Conj_right A (G1++C::G2).


Lemma del_to_typ_right_middle_subst: forall D1 D2 B1 B2 C1 C2 A B C,
  <> (Conj_right B (B1++B2)) =< <> (Conj_right C (C1++C2)) ->
  del_to_typ_right A (D1++(B1++B::B2)::D2) =< del_to_typ_right A (D1++(C1++C::C2)::D2).

Following tactics facilitate applying the above lemmas.

Tactic Notation "mid_subst" constr(E) :=
  match goal with
    | |- Conj_right ?A (?C1++?B::?C2) =< _ =>
      constructor 2 with (Conj_right A (C1++E::C2)); [apply Conj_right_middle_subst |]
    | |- del_to_typ_right ?A (?C1++?B::?C2) =< _ =>
      constructor 2 with (del_to_typ_right A (C1++E::C2)); [apply del_to_typ_right_middle_subst |]
    | |- del_to_typ_right (Conj_right ?A (?C1++?B::?C2)) ?D =< _ =>
      constructor 2 with (del_to_typ_right (Conj_right A (C1++E::C2)) D);
        [apply del_to_typ_right_sub; apply Conj_right_middle_subst |]
    | _ => idtac
  end.

Tactic Notation "left_subst" constr(E) :=
  match goal with
    | |- ?A & ?B =< _ =>
      constructor 2 with (E & B); [apply sub_weakening_left |]
    | _ => idtac
  end.

Tactic Notation "right_subst" constr(E) :=
  match goal with
    | |- ?A & ?B =< _ =>
      constructor 2 with (A & E); [apply sub_weakening_right |]
    | _ => idtac
  end.

Tactic Notation "focus_subst" constr(E) :=
  match goal with
    | |- Conj_right ?A ?C =< _ =>
      constructor 2 with (Conj_right E C); [apply Conj_right_sub |]
    | |- del_to_typ_right ?A ?C =< _ =>
      constructor 2 with (del_to_typ_right E C); [apply del_to_typ_right_sub |]
    | _ => idtac
  end.

We can rewrite Conj_right by picking one type out of the list, or the other way around.

Lemma Conj_right_pop_out: forall l A B,
  Conj_right A (B :: l) =< B & Conj_right A l.

Lemma Conj_right_push_in: forall l A B,
  B & Conj_right A l =< Conj_right A (B :: l).


Lemma del_to_typ_right_push_in_init: forall D A B,
  A & del_to_typ_right B D =< del_to_typ_right (A&B) D.

Lemma del_to_typ_right_push_in_init_conv: forall D A B,
  del_to_typ_right (A&B) D =< A & del_to_typ_right B D.

Lemma Conj_right_push_in_init: forall D A B,
  A & Conj_right B D =< Conj_right (A&B) D.

Lemma Conj_right_push_in_init_conv: forall D A B,
  Conj_right (A&B) D =< A & Conj_right B D.

We can divide or merge an expression of the function Conj.

Lemma Conj_split: forall G1 G2 A B,
  Conj G1 A & Conj G2 B =< Conj (G1++A::G2) B.

Lemma Conj_split_conv: forall G1 G2 A B,
  Conj (G1++A::G2) B =< Conj G1 A & Conj G2 B.

Lemma Conj_right_split_conv: forall G1 G2 A B,
  Conj_right B (G1++A::G2) =< Conj_right B G1 & Conj_right A G2.

Lemma Conj_right_split: forall G1 G2 A B,
  Conj_right A G1 & Conj_right B G2 =< Conj_right A (G1++B::G2).

Tactic Notation "conj_right_merge" :=
  match goal with
    | |- Conj_right ?A ?AL & Conj_right ?B ?BL =< _ =>
      constructor 2 with (Conj_right A (AL++B::BL)); [apply Conj_right_split |]
    | _ => idtac
  end.

Lemma conj_right_fold : forall L1 L2 A,
  Conj_right (Conj_right A L1) L2 =< Conj_right A (L2 ++ L1).

del_to_typ_right skips an empty local subtyping context.

Lemma delta_simpl: forall n D A,
  del_to_typ_right A (n_list n empty ++ D) =< del_to_typ_right A D.

Lemma delta_unsimpl: forall n A,
  A =< del_to_typ_right A (n_list n empty).

Lemma delta_unsimpl2: forall n D A,
  del_to_typ_right A D =< del_to_typ_right A (n_list n empty ++ D).

Following lemma is combining the rules r_box_K and r_box_dist.

Lemma Conj_right_box_k: forall l A,
  Conj_right ([]A) (map typ_box l) =< [] Conj_right ([]A) (map typ_box l).


Following two lemmas exploit the rule r_box_T.

Lemma Conj_sub_box_T: forall l A,
  Conj (map typ_box l) A =< Conj l A.


Lemma Conj_right_box_T2 : forall A L1 L2,
  Conj_right A (map typ_box L1 ++ L2) =< Conj_right A (L1 ++ L2).

Following lemma says <>(A & []B) =< <>A & <>[]B.

Abstract derivation:
.................................A & []B =< A.......A & []B =< []B
.............................------------------....--------------------
.A & []B =< A & []B.........<>(A & []B) =< <>A....<>(A & []B) =< <>[]B
------------------------.....------------------------------------------
<>(A & []B) =< <>(A & []B)..........<>(A & []B) =< <>A & <>[]B
-------------------------------------------------------------------
...................<>(A & []B) =< <>A & <>[]B


Lemma del_to_typ_right_box_split : forall Delta1 Delta2 Sigma1 Sigma2 A C,
  del_to_typ_right A (Delta1 ++ (Sigma1 ++ ([]C) :: Sigma2) :: Delta2) =<
  del_to_typ_right A (Delta1 ++ [[]C] :: (Sigma1 ++ Sigma2) :: Delta2).

Tactic Notation "pop_delta" :=
  match goal with
  | |- del_to_typ_right ?A (?D1++(?S1++(typ_box ?C)::?S2)::?D2) =< _ =>
    constructor 2 with (del_to_typ_right A (D1++[typ_box C]::(S1++S2)::D2));
      [apply del_to_typ_right_box_split|]
  | |- Conj_right (del_to_typ_right ?A (?D1++(?S1++(typ_box ?C)::?S2)::?D2)) ?E =< _ =>
    focus_subst (del_to_typ_right A (D1++[typ_box C]::(S1++S2)::D2));
      [apply del_to_typ_right_box_split|]
  | _ => idtac
  end.

A & B =< A & <>B
Lemma del_to_typ_right_sig_to_del: forall D G S A,
  del_to_typ_right (Conj_right A (G++S)) D =< del_to_typ_right (Conj_right A G) (S::D).

Tactic Notation "move_sig_to_del" :=
  match goal with
  | |- del_to_typ_right (Conj_right ?A (?B ++ ?C)) ?D =< _ =>
    constructor 2 with (del_to_typ_right (Conj_right A B) (C::D));
      [apply del_to_typ_right_sig_to_del|]
  | _ => idtac
  end.

A & <>B1 & ... & <>Bn =< (A & <>B1 & ... & <>Bn)
<>A & <>B1 & ... & <>Bn =< (<>A & <>B1 & ... & <>Bn)

Lemma del_to_typ_right_box_k2: forall D A,
  del_to_typ_right (<>A) D =< [] del_to_typ_right (<> A) D.

Following lemma relates to the rule r_box_dia_K.

Abstract derivation:
  A & <>B =< C

      ...

  A & []<>B =< C
------------------- r_box_dia_K
<>A & []<>B =< <>C

      ...

<>A & <>B =< <>C


Lemma del_to_typ_right_dia_tran : forall D A C,
  del_to_typ_right A D =< C ->
  del_to_typ_right (<> A) D =< <> C.

Following lemma relates to the rule r_box_dia_K.

Abstract derivation:
   A & [] B =< A & [] B
-------------------------- r_box_dia_K
<>A & [] B =< <> (A & [] B)


Lemma del_to_typ_right_dia_tran2 : forall G A,
  Conj_right (<>A) (map typ_box G) =< <> Conj_right A (map typ_box G).

We can rearrange the order of function applications.

Lemma del_to_typ_right_Conj_right : forall G D A,
  del_to_typ_right (Conj_right A G) D =< Conj_right (del_to_typ_right A D) G.

Lemma Conj_right_del_to_typ_right : forall G D A,
  Conj_right (del_to_typ_right A D) G =< del_to_typ_right (Conj_right A G) D.

Tactic Notation "alter_left" :=
  match goal with
  | |- del_to_typ_right (Conj_right ?A ?G) ?D =< _ =>
    constructor 2 with (Conj_right (del_to_typ_right A D) G);
      [apply del_to_typ_right_Conj_right|]
  | |- Conj_right (del_to_typ_right ?A ?D) ?G =< _ =>
    constructor 2 with (del_to_typ_right (Conj_right A G) D);
      [apply Conj_right_del_to_typ_right|]
  end.

Tactic Notation "alter_right" :=
  match goal with
  | |- _ =< del_to_typ_right (Conj_right ?A ?G) ?D =>
    constructor 2 with (Conj_right (del_to_typ_right A D) G);
      [|apply Conj_right_del_to_typ_right]
  | |- _ =< Conj_right (del_to_typ_right ?A ?D) ?G =>
    constructor 2 with (del_to_typ_right (Conj_right A G) D);
      [|apply del_to_typ_right_Conj_right]
  end.

Lemmas for the judgmental subtyping system


This section contains infrastructure lemmas of the judgmental subtyping system based on modal logic S5 which is described in Section 4 of the paper.

Lemma size_env_split: forall L1 L2,
  size_env (L1 ++ L2) = size_env L1 + size_env L2.

Lemma pickFun_app: forall l1 l2,
  pickFun(l1 ++ l2) = pickFun l1 ++ pickFun l2.

Lemma fsttypList_app : forall l1 l2,
  fsttypList (l1 ++ l2) = fsttypList l1 ++ fsttypList l2.

Lemma sndtypList_app: forall l1 l2,
  sndtypList (l1 ++ l2) = sndtypList l1 ++ sndtypList l2.

Lemma n_list_split: forall n1 n2,
  n_list n1 empty ++ n_list n2 empty = n_list (n1+n2) empty.

Lemmas for case analysis on the remote node context

For any remote node context, a) it may consist of empty local typing contexts, or b) it may contain at least one non-empty local typing context.
Lemma delta_dec : forall Delta,
  (exists n, Delta = n_list n empty) \/
  (exists n, exists A, exists PSigma, exists Delta',
    Delta = n_list n empty ++ (A::PSigma)::Delta').

If l1++l2 is a list of empty lists, both l1 and l2 are also lists of empty lists.
Lemma n_list_empty_eq_split: forall n l1 l2,
  l1 ++ l2 = n_list n empty ->
  exists n1, exists n2, n = n1 + n2 /\ l1 = n_list n1 empty /\ l2 = n_list n2 empty.

We can write the similar lemma using Permutation.
Lemma n_list_empty_permute_split: forall n D1 D2,
  Permutation (D1++D2) (n_list n empty) ->
  exists n1, exists n2, n = n1 + n2 /\ D1 = n_list n1 empty /\ D2 = n_list n2 empty.

Not all of subtyping contexts are empty.


At least one of the subtyping contexts must contain a type.
Lemma context_is_not_nil_gen: forall A_dummy Delta Gamma Sigma A,
  Delta;; Gamma; Sigma ~< A ->
  forall n,
    A = A_dummy ->
    Delta = n_list n empty ->
    Gamma = empty ->
    Sigma = empty ->
    False.

Lemma context_is_not_nil: forall A,
  ~ (noworld;; empty ; empty ~< A).

General ver. of the rules j_refl and j_refl_v


The rules j_refl and j_refl_v involve a primitive type, but we can derive the reflexivity rules for an arbitrary type.

Lemma j_refl_gen: forall (A:typ),
  (forall (Delta:worlds) (Gamma Sigma Sigma':env), Delta;; Gamma; Sigma ++ A :: Sigma' ~< A) /\
  (forall (Delta:worlds) (Gamma Gamma' Sigma:env), Delta;; Gamma ++ A :: Gamma'; Sigma ~< A).




Context permutation



We assume that the contexts are unordered.

Since pickFun gathers all function types from a context without changing the order, if Sigma is a permutation of Sigma' then pickFun Sigma is also a permutation of pickFun Sigma'.

Lemma permute_pickFun : forall Sigma Sigma',
  Permutation Sigma Sigma' ->
  Permutation (pickFun Sigma) (pickFun Sigma').

Lemma permute_pickFun_exists: forall (Funs Sigma Sigma': list (typ * typ)),
  subseq Funs Sigma ->
  Permutation Sigma Sigma' ->
  exists Funs', Permutation Funs Funs' /\ subseq Funs' Sigma'.


Lemma permute_j_sub : forall (Delta:worlds) (Gamma Sigma:env) (A:typ),
  Delta;; Gamma ; Sigma ~< A ->
  forall (Delta':worlds) (Gamma' Sigma':env),
    WPermutation Delta Delta' ->
    Permutation Gamma Gamma' ->
    Permutation Sigma Sigma' ->
    Delta';; Gamma'; Sigma' ~< A.

Weakening

We may append an arbitrary type to the front of the context.

Lemma weakening_cons: forall (Delta:worlds) (Gamma Sigma:env) (A:typ),
  Delta;; Gamma; Sigma ~< A ->
  forall (C:typ),
    Delta;; Gamma; C :: Sigma ~< A /\
    Delta;; C::Gamma; Sigma ~< A /\
    forall (Delta':worlds) (Sigma':env),
      Permutation Delta (Sigma' :: Delta') ->
      (C::Sigma')::Delta';; Gamma; Sigma ~< A.

We may append an arbitrary local subtyping context to the front of the remote node context.

Lemma weakening_cons_lcc: forall (Delta:worlds) (Gamma Sigma:env) (A:typ),
  Delta;; Gamma; Sigma ~< A ->
  forall (Sigma':env),
    Sigma'::Delta;; Gamma; Sigma ~< A.

We may add an arbitrary type to the middle of the context.

Lemma weakening_gen_l: forall (Delta:worlds) (Gamma Sigma Sigma' : env) (A C : typ),
  Delta;; Gamma; Sigma ++ Sigma' ~< A ->
  Delta;; Gamma; Sigma ++ C :: Sigma' ~< A.

Lemma weakening_gen_v: forall (Delta:worlds) (Gamma Gamma' Sigma : env) (A C : typ),
  Delta;; Gamma ++ Gamma'; Sigma ~< A ->
  Delta;; Gamma ++ C :: Gamma'; Sigma ~< A.

Lemma weakening_gen_lc: forall (Delta Delta':worlds) (PSigma PSigma':env) (Gamma Sigma : env) (A C : typ),
  Delta ++ (PSigma ++ PSigma') :: Delta';; Gamma; Sigma ~< A ->
  Delta ++ (PSigma ++ C :: PSigma') :: Delta';; Gamma; Sigma ~< A.

We may append an arbitrary local subtyping context to the middle of the remote node context.

Lemma weakening_gen_lcc: forall (Delta1 Delta2:worlds) (Gamma Sigma' Sigma:env) (A:typ),
  Delta1 ++ Delta2;; Gamma; Sigma ~< A ->
  Delta1 ++ Sigma' :: Delta2;; Gamma; Sigma ~< A.


We may add an arbitrary set of types to the context.

Lemma weakening_bunch_l: forall (Delta:worlds) (Gamma Sigma Sigma':env) (A:typ),
  Delta;; Gamma; Sigma ~< A ->
  Delta;; Gamma; Sigma' ++ Sigma ~< A.

Lemma weakening_bunch_l': forall (Delta:worlds) (Gamma Sigma Sigma':env) (A:typ),
  Delta;; Gamma; Sigma ~< A ->
  Delta;; Gamma; Sigma ++ Sigma' ~< A.


Lemma weakening_bunch_v: forall (Delta:worlds) (Gamma Gamma' Sigma:env) (A:typ),
  Delta;; Gamma; Sigma ~< A ->
  Delta;; Gamma' ++ Gamma; Sigma ~< A.

Lemma weakening_bunch_v': forall (Delta:worlds) (Gamma Gamma' Sigma:env) (A:typ),
  Delta;; Gamma; Sigma ~< A ->
  Delta;; Gamma ++ Gamma'; Sigma ~< A.


Lemma weakening_bunch_lc: forall (PSigma:env) (Delta Delta':worlds) (PSigma' Gamma Sigma : env) (A : typ),
  Delta ++ PSigma' :: Delta';; Gamma; Sigma ~< A ->
  Delta ++ (PSigma ++ PSigma') :: Delta';; Gamma; Sigma ~< A.

Lemma weakening_bunch_lc': forall (PSigma:env) (Delta Delta':worlds) (PSigma' Gamma Sigma : env) (A : typ),
  Delta ++ PSigma' :: Delta';; Gamma; Sigma ~< A ->
  Delta ++ (PSigma' ++ PSigma) :: Delta';; Gamma; Sigma ~< A.

A type in the ordinary subtyping context can be moved to the global subtyping context.


Following is the contraction lemma to prove:
Delta;; Gamma; C::Sigma ~< A -> Delta;; C::Gamma; Sigma ~< A.
(C::PSigma)::Delta;; Gamma; Sigma ~< A -> PSigma::Delta;; C::Gamma; Sigma ~< A.

The proof is done by nested induction on type C and the derivation of Delta;; Gamma; C::Sigma ~< A or (C::PSigma)::Delta;; Gamma; Sigma ~< A.

To reduce the proof script size, we divide the proof into two steps.

Definition move_from_sig_to_gam_IH_on_typ n :=
  forall A,
    size_typ A < n ->
    forall Delta Gamma Sigma C, Delta;; Gamma; Sigma ~< C ->
      (forall Sigma',
        Sigma = A :: Sigma' ->
        Delta;; A :: Gamma; Sigma' ~< C) /\
      (forall (Delta':worlds) (PSigma:env),
        Permutation Delta ((A::PSigma)::Delta') ->
        PSigma::Delta';; A::Gamma; Sigma ~< C).

In the presence of the induction hypothesis on the size of type C, the following lemma proves the goal by induction on the derivation.

Lemma move_from_sig_to_gam_cons_on_typ_aux: forall A,
  move_from_sig_to_gam_IH_on_typ (size_typ A) ->
  forall Delta Gamma Sigma C, Delta;; Gamma; Sigma ~< C ->
    (forall Sigma',
      Sigma = A :: Sigma' ->
      Delta;; A :: Gamma; Sigma' ~< C) /\
    (forall (Delta':worlds) (PSigma:env),
      Permutation Delta ((A::PSigma)::Delta') ->
      PSigma::Delta';; A::Gamma; Sigma ~< C).

The main lemma is proven by induction on the size of type C.

Lemma move_from_sig_to_gam_cons_on_typ: forall n A,
  size_typ A < n ->
  forall Delta Gamma Sigma C, Delta;; Gamma; Sigma ~< C ->
    (forall Sigma',
      Sigma = A :: Sigma' ->
      Delta;; A :: Gamma; Sigma' ~< C) /\
    (forall (Delta':worlds) (PSigma:env),
      Permutation Delta ((A::PSigma)::Delta') ->
      PSigma::Delta';; A::Gamma; Sigma ~< C).

This is the main lemma.

Lemma move_from_sig_to_gam_cons: forall A,
  forall Delta Gamma Sigma C, Delta;; Gamma; Sigma ~< C ->
    (forall Sigma',
      Sigma = A :: Sigma' ->
      Delta;; A :: Gamma; Sigma' ~< C) /\
    (forall (Delta':worlds) (PSigma:env),
      Permutation Delta ((A::PSigma)::Delta') ->
      PSigma::Delta';; A::Gamma; Sigma ~< C).


Invertible rules

The rules j_and_l, j_and_lc, and j_and_v are invertible.


Lemma j_and_l_lc_inv_cons: forall Delta Gamma Sigma C,
  Delta;; Gamma; Sigma ~< C ->
  (forall Sigma0 A B,
    Sigma = (A & B) :: Sigma0 ->
    Delta;; Gamma; A :: B :: Sigma0 ~< C) /\
  (forall Delta' Sigma' A B,
    Permutation Delta (((A & B)::Sigma') :: Delta') ->
    (A::B::Sigma')::Delta';; Gamma; Sigma ~< C).

Lemma j_and_l_inv: forall Delta Gamma Sigma Sigma' A B C,
  Delta;; Gamma; Sigma ++ (A & B) :: Sigma' ~< C ->
  Delta;; Gamma; Sigma ++ A :: B :: Sigma' ~< C.

Lemma j_and_lc_inv: forall Delta Delta' PSigma PSigma' Gamma Sigma A B C,
  Delta ++ (PSigma ++ (A & B) :: PSigma') :: Delta';; Gamma; Sigma ~< C ->
  Delta ++ (PSigma ++ A :: B :: PSigma') :: Delta';; Gamma; Sigma ~< C.


Lemma j_and_v_inv_cons: forall Delta Gamma Sigma C,
  Delta;; Gamma; Sigma ~< C ->
  forall Gamma0 A B,
    Permutation Gamma ((A&B) :: Gamma0) ->
    Delta;; A :: B :: Gamma0; Sigma ~< C.

Lemma j_and_v_inv: forall Delta Gamma0 Gamma1 Sigma A B C,
    Delta;; Gamma0 ++ (A & B) :: Gamma1; Sigma ~< C ->
    Delta;; Gamma0 ++ A :: B :: Gamma1; Sigma ~< C.

The rules j_box_l, j_box_lc, and j_box_v are invertible.


Lemma j_box_v_inv_cons: forall Delta Gamma Sigma C,
  Delta;; Gamma; Sigma ~< C ->
  forall Gamma0 A,
    Permutation Gamma (([]A) :: Gamma0) ->
    Delta;; A :: Gamma0; Sigma ~< C.

Lemma j_box_v_inv: forall Delta Gamma0 Gamma1 Sigma A C,
    Delta;; Gamma0 ++ ([]A) :: Gamma1; Sigma ~< C ->
    Delta;; Gamma0 ++ A :: Gamma1; Sigma ~< C.


Lemma j_box_l_inv: forall Delta Gamma1 Gamma2 Sigma1 Sigma2 A C,
  Delta;; Gamma1 ++ Gamma2; Sigma1 ++ ([]A) :: Sigma2 ~< C ->
  Delta;; Gamma1 ++ A :: Gamma2; Sigma1 ++ Sigma2 ~< C.

Lemma j_box_lc_inv: forall Delta1 Delta2 Gamma1 Gamma2 Sigma Sigma1 Sigma2 A C,
  Delta1 ++ (Sigma1 ++ ([]A) :: Sigma2) ::Delta2;; Gamma1 ++ Gamma2; Sigma ~< C ->
  Delta1 ++ (Sigma1 ++ Sigma2) ::Delta2;; Gamma1 ++ A :: Gamma2; Sigma ~< C.


The rules j_dia_l, j_dia_lc, and j_dia_v are invertible.


Lemma j_dia_l_lc_inv_cons: forall Delta Gamma Sigma C,
  Delta;; Gamma; Sigma ~< C ->
  (forall Sigma0 A,
    Sigma = (<>A) :: Sigma0 ->
    [A]::Delta;; Gamma; Sigma0 ~< C) /\
  (forall Delta' Sigma' A,
    Permutation Delta (((<>A)::Sigma') :: Delta') ->
    Sigma'::[A]::Delta';; Gamma; Sigma ~< C).

Lemma j_dia_l_inv: forall Delta1 Delta2 Gamma Sigma1 Sigma2 A C,
  Delta1 ++ Delta2;; Gamma; Sigma1 ++ (<>A) :: Sigma2 ~< C ->
  Delta1 ++ [A] :: Delta2;; Gamma; Sigma1 ++ Sigma2 ~< C.

Lemma j_dia_lc_inv: forall Delta1 Delta2 Gamma Sigma Sigma1 Sigma2 A C,
  Delta1 ++ (Sigma1 ++ (<>A) :: Sigma2) ::Delta2;; Gamma; Sigma ~< C ->
  Delta1 ++ (Sigma1 ++ Sigma2) :: [A] ::Delta2;; Gamma; Sigma ~< C.


Lemma j_dia_v_inv_cons: forall Delta Gamma Sigma C,
  Delta;; Gamma; Sigma ~< C ->
  forall Gamma0 A,
    Permutation Gamma ((<>A) :: Gamma0) ->
    [A]::Delta;; Gamma0; Sigma ~< C.

Lemma j_dia_v_inv: forall Delta1 Delta2 Gamma1 Gamma2 Sigma A C,
  Delta1 ++ Delta2;; Gamma1 ++ (<>A) :: Gamma2; Sigma ~< C ->
  Delta1 ++ [A] :: Delta2;; Gamma1 ++ Gamma2; Sigma ~< C.


Contraction


Following is the contraction lemma to prove:
Delta;; Gamma; C::C::Sigma ~< A -> Delta;; Gamma; C::Sigma ~< A.
Delta;; C::C::Gamma; Sigma ~< A -> Delta;; C::Gamma; Sigma ~< A.
(C::C::PSigma)::Delta;; Gamma; Sigma ~< A -> (C::PSigma)::Delta;; Gamma; Sigma ~< A.

PSigma::PSigma::Delta;; Gamma; Sigma ~< A -> PSigma::Delta;; Gamma; Sigma ~< A.
PSigma::Delta;; Gamma; PSigma ~< A -> Delta;; Gamma; PSigma ~< A.

The proof is done by nested induction on (the size of type C + the size of context PSigma) and the derivation of premise such as Delta;; Gamma; C::C::Sigma ~< A.


Definition contraction_IH n :=
  forall A PCSigma,
    size_typ A + size_env PCSigma < n ->
    (forall Delta Gamma Sigma C, Delta;; Gamma; Sigma ~< C ->
      (forall Delta', PCSigma = Sigma -> Permutation Delta (Sigma::Delta') -> Delta';; Gamma; Sigma ~< C) /\
      (forall Gamma0, Permutation Gamma (A :: A :: Gamma0) -> Delta;; A::Gamma0; Sigma ~< C) /\
      (forall Sigma0, Sigma = (A :: A :: Sigma0) -> Delta;; Gamma; A::Sigma0 ~< C) /\
      (forall Delta', Permutation Delta (PCSigma::PCSigma::Delta') -> PCSigma::Delta';; Gamma; Sigma ~< C) /\
      (forall Delta' PSigma, Permutation Delta ((A::A::PSigma)::Delta') -> (A::PSigma)::Delta';; Gamma; Sigma ~< C)
    ).

In the presence of the induction hypothesis on the total size of type C and context PSigma, the following lemma proves the goal by induction on the derivation.

Lemma contraction_cons_aux_aux: forall A PCSigma,
  contraction_IH (size_typ A + size_env PCSigma) ->
  (forall Delta Gamma Sigma C, Delta;; Gamma; Sigma ~< C ->
    (forall Delta', PCSigma = Sigma -> Permutation Delta (Sigma::Delta') -> Delta';; Gamma; Sigma ~< C) /\
    (forall Gamma0, Permutation Gamma (A :: A :: Gamma0) -> Delta;; A::Gamma0; Sigma ~< C) /\
    (forall Sigma0, Sigma = (A :: A :: Sigma0) -> Delta;; Gamma; A::Sigma0 ~< C) /\
    (forall Delta', Permutation Delta (PCSigma::PCSigma::Delta') -> PCSigma::Delta';; Gamma; Sigma ~< C) /\
    (forall Delta' PSigma, Permutation Delta ((A::A::PSigma)::Delta') -> (A::PSigma)::Delta';; Gamma; Sigma ~< C)
  ).

The main lemma is proven by induction on the total size of type C and context PSigma.

Lemma contraction_cons_aux: forall n A PCSigma,
  size_typ A + size_env PCSigma < n ->
  (forall Delta Gamma Sigma C, Delta;; Gamma; Sigma ~< C ->
    (forall Delta', PCSigma = Sigma -> Permutation Delta (Sigma::Delta') -> Delta';; Gamma; Sigma ~< C) /\
    (forall Gamma0, Permutation Gamma (A :: A :: Gamma0) -> Delta;; A::Gamma0; Sigma ~< C) /\
    (forall Sigma0, Sigma = (A :: A :: Sigma0) -> Delta;; Gamma; A::Sigma0 ~< C) /\
    (forall Delta', Permutation Delta (PCSigma::PCSigma::Delta') -> PCSigma::Delta';; Gamma; Sigma ~< C) /\
    (forall Delta' PSigma, Permutation Delta ((A::A::PSigma)::Delta') -> (A::PSigma)::Delta';; Gamma; Sigma ~< C)
  ).

This is the main lemma.

Lemma contraction_cons: forall A PCSigma,
  (forall Delta Gamma Sigma C, Delta;; Gamma; Sigma ~< C ->
    (forall Delta', PCSigma = Sigma -> Permutation Delta (Sigma::Delta') -> Delta';; Gamma; Sigma ~< C) /\
    (forall Gamma0, Permutation Gamma (A :: A :: Gamma0) -> Delta;; A::Gamma0; Sigma ~< C) /\
    (forall Sigma0, Sigma = (A :: A :: Sigma0) -> Delta;; Gamma; A::Sigma0 ~< C) /\
    (forall Delta', Permutation Delta (PCSigma::PCSigma::Delta') -> PCSigma::Delta';; Gamma; Sigma ~< C) /\
    (forall Delta' PSigma, Permutation Delta ((A::A::PSigma)::Delta') -> (A::PSigma)::Delta';; Gamma; Sigma ~< C)
  ).

Followings are the generalized version of contraction lemmas.

Lemma contraction_gen_l: forall Delta Gamma Sigma Sigma' A C,
  Delta;; Gamma; Sigma ++ C :: C :: Sigma' ~< A ->
  Delta;; Gamma; Sigma ++ C :: Sigma' ~< A.

Lemma contraction_gen_v: forall Delta Gamma Gamma' Sigma A C,
  Delta;; Gamma ++ C :: C :: Gamma'; Sigma ~< A ->
  Delta;; Gamma ++ C :: Gamma'; Sigma ~< A.

Lemma contraction_gen_lc: forall Delta1 Delta2 PSigma1 PSigma2 Gamma Sigma A C,
  Delta1 ++ (PSigma1 ++ C :: C :: PSigma2) :: Delta2;; Gamma; Sigma ~< A ->
  Delta1 ++ (PSigma1 ++ C :: PSigma2) :: Delta2;; Gamma; Sigma ~< A.

Lemma contraction_gen_lcc: forall Delta1 Delta2 PSigma Gamma Sigma A,
  Delta1 ++ PSigma :: PSigma :: Delta2;; Gamma; Sigma ~< A ->
  Delta1 ++ PSigma :: Delta2;; Gamma; Sigma ~< A.

Lemma contraction_gen_l_lc: forall Delta1 Delta2 Gamma Sigma A,
  Delta1 ++ Sigma :: Delta2;; Gamma; Sigma ~< A ->
  Delta1 ++ Delta2;; Gamma; Sigma ~< A.

Lemma contraction_bunch_cons:
  (forall Sigma' Delta Gamma Sigma A,
    Delta;; Gamma; Sigma' ++ Sigma' ++ Sigma ~< A ->
    Delta;; Gamma; Sigma' ++ Sigma ~< A) /\
  (forall Gamma' Delta Gamma Sigma A,
    Delta;; Gamma' ++ Gamma' ++ Gamma; Sigma ~< A ->
    Delta;; Gamma' ++ Gamma; Sigma ~< A) /\
  (forall Delta' Delta Gamma Sigma A,
    Delta' ++ Delta' ++ Delta;; Gamma; Sigma ~< A ->
    Delta' ++ Delta;; Gamma; Sigma ~< A) /\
  (forall PSigma' Delta1 Delta2 PSigma Gamma Sigma A,
    Delta1++(PSigma'++PSigma'++PSigma)::Delta2;; Gamma; Sigma ~< A ->
    Delta1++(PSigma'++PSigma)::Delta2;; Gamma; Sigma ~< A).

Lemma contraction_bunch:
  (forall Delta Gamma Sigma A,
    Delta;; Gamma; Sigma ++ Sigma ~< A ->
    Delta;; Gamma; Sigma ~< A) /\
  (forall Delta Gamma Sigma A,
    Delta;; Gamma ++ Gamma; Sigma ~< A ->
    Delta;; Gamma; Sigma ~< A) /\
  (forall Delta1 Delta2 PSigma Gamma Sigma A,
    Delta1++(PSigma++PSigma)::Delta2;; Gamma; Sigma ~< A ->
    Delta1++(PSigma)::Delta2;; Gamma; Sigma ~< A) /\
  (forall Delta Gamma Sigma A,
    Delta ++ Delta;; Gamma; Sigma ~< A ->
    Delta;; Gamma; Sigma ~< A).


Contraction of empty local subtyping contexts


We can omit empty local subtyping contexts from the remote node context.

Lemma contraction_empty : forall Delta Gamma Sigma C,
  Delta;; Gamma; Sigma ~< C ->
  forall Delta',
    Permutation Delta (empty::Delta') ->
    Delta';; Gamma; Sigma ~< C.

Lemma contraction_gen_empty: forall Delta1 Delta2 Gamma Sigma A,
  Delta1 ++ empty :: Delta2;; Gamma; Sigma ~< A ->
  Delta1 ++ Delta2;; Gamma; Sigma ~< A.


Etc.


We can move a local subtyping context in the global subtyping context into the ordinary subtyping context.

Lemma move_from_del_to_sig : forall (Delta1 Delta2:worlds) (Gamma PSigma Sigma:env) (C:typ),
  Delta1 ++ PSigma :: Delta2;; Gamma; Sigma ~< C ->
  Delta1 ++ Delta2;; Gamma; PSigma ++ Sigma ~< C.

We can merge two local subtyping contexts in the global subtyping context.

Lemma merge_psig : forall Delta1 Delta2 PSigma1 PSigma2 Gamma Sigma C,
  Delta1 ++ PSigma1 ::PSigma2 :: Delta2;; Gamma; Sigma ~< C ->
  Delta1 ++ (PSigma1 ++ PSigma2) :: Delta2;; Gamma; Sigma ~< C.

Other lemmas


Lemma in_weakening : forall (A:Type) (l1 l2:list A) (x y:A),
  In x (l1 ++ l2) ->
  In x (l1 ++ y :: l2).


Lemma pickFun_in: forall (t1 t2:typ) L,
  In (t1,t2) (pickFun L) ->
  In (t1-->t2) L.

Lemma subseq_makeFunList_pickFun: forall l,
  subseq (makeFunList (pickFun l)) l.

Admissibility of the cut rules


This section contains the proof of admissibility of the cut rules of the judgmental subtyping system.

Following is the main theorem to prove:
  Delta;; Gamma; empty ~< A ->
  Delta';; A::Gamma'; Sigma' ~< C ->
  Delta ++ Delta';; Gamma ++ Gamma'; Sigma' ~< C

  Delta;; Gamma; Sigma ~< A ->
  Delta';; Gamma'; A::Sigma' ~< C ->
  Delta ++ Delta';; Gamma ++ Gamma'; Sigma ++ Sigma' ~< C

  Delta;; Gamma; Sigma ~< A ->
  (A::PSigma)::Delta';; Gamma'; Sigma' ~< C ->
  Delta ++ (Sigma ++PSigma) :: Delta';; Gamma ++ Gamma'; Sigma' ~< C



As we explained in the paper, we proceed in three steps, consisting of j_cut_cons_lemma1, 2, and 3, as in the proof of cut elimination in display logic.

Following definition, j_cut_ind_on_typ A, corresponds to /A/ which is in the paper, but j_cut_ind_on_typ A is stronger in a sense that it can be applied to any smaller-sized type that is not a proper constituent type of A.

Definition j_cut_ind_on_typ A' :=
  forall A : typ,
    size_typ A < size_typ A' ->
    (forall Delta Delta' Gamma Gamma' Sigma' C,
      Delta;; Gamma; empty ~< A ->
      Delta';; A::Gamma'; Sigma' ~< C ->
      Delta ++ Delta';; Gamma ++ Gamma'; Sigma' ~< C) /\
    (forall Delta Delta' Gamma Gamma' Sigma Sigma' C,
      Delta;; Gamma; Sigma ~< A ->
      Delta';; Gamma'; A::Sigma' ~< C ->
      Delta ++ Delta';; Gamma ++ Gamma'; Sigma ++ Sigma' ~< C) /\
    (forall Delta Delta' PSigma Gamma Gamma' Sigma Sigma' C,
      Delta;; Gamma; Sigma ~< A ->
      (A::PSigma)::Delta';; Gamma'; Sigma' ~< C ->
      Delta ++ (Sigma ++PSigma) :: Delta';; Gamma ++ Gamma'; Sigma' ~< C).

Lemma1: A is the principal type of both derivations. We prove it by case analysis of type A.

Lemma j_cut_cons_lemma1: forall Delta Gamma Sigma A,
  j_cut_ind_on_typ A ->
  Delta;; Gamma; Sigma ~< |A| ->
  (Sigma = empty ->
    forall Delta' Gamma' Sigma' C,
      Delta';; Gamma',|A|; Sigma' ~< C ->
      Delta ++ Delta';; Gamma ++ Gamma'; Sigma' ~< C) /\
  (forall Delta' Gamma' Sigma' C,
    Delta';; Gamma'; Sigma', |A| ~< C ->
    Delta ++ Delta';; Gamma ++ Gamma'; Sigma ++ Sigma' ~< C) /\
  (forall Delta' PSigma Gamma' Sigma' C,
    Delta',, PSigma, |A|;; Gamma'; Sigma' ~< C ->
    Delta ++ (Sigma++PSigma) :: Delta';; Gamma ++ Gamma'; Sigma' ~< C).

Lemma2: A is the principal type of the first derivation such as Delta;; Gamma; empty ~< A. We prove it by induction on the second derivations such as Delta;; Gamma; A::Sigma' ~< C. When type A is principal type of that derivation, we use Lemma 1. To apply induction on the second premises, we rewrite the lemma changing the order of premises.

Lemma j_cut_cons_lemma2_ori: forall A,
  j_cut_ind_on_typ A ->
  forall Delta' Gamma' Sigma' C, Delta';; Gamma'; Sigma' ~< C ->
    (forall Delta Gamma Sigma Gamma'',
      Delta;; Gamma; Sigma ~< |A| ->
      Sigma = empty ->
      Permutation Gamma' (A::Gamma'') ->
      Delta ++ Delta';; Gamma ++ Gamma''; Sigma' ~< C) /\
    (forall Delta Gamma Sigma Sigma'',
      Delta;; Gamma; Sigma ~< |A| ->
      Sigma' = A::Sigma'' ->
      Delta ++ Delta';; Gamma ++ Gamma'; Sigma ++ Sigma'' ~< C) /\
    (forall Delta Gamma Sigma Delta'' PSigma,
      Delta;; Gamma; Sigma ~< |A| ->
      Permutation Delta' ((A::PSigma)::Delta'') ->
      Delta ++ (Sigma++PSigma) :: Delta'';; Gamma ++ Gamma'; Sigma' ~< C).

Lemma2: the original form.

Lemma j_cut_cons_lemma2: forall A Delta Gamma Sigma,
  j_cut_ind_on_typ A ->
  Delta;; Gamma; Sigma ~< |A| ->
    (Sigma = empty ->
      forall Delta' Gamma' Sigma' C,
        Delta';; A::Gamma'; Sigma' ~< C ->
        Delta ++ Delta';; Gamma ++ Gamma'; Sigma' ~< C) /\
    (forall Delta' Gamma' Sigma' C,
      Delta';; Gamma'; A::Sigma' ~< C ->
      Delta ++ Delta';; Gamma ++ Gamma'; Sigma ++ Sigma' ~< C) /\
    (forall Delta' PSigma Gamma' Sigma' C,
      (A::PSigma)::Delta';; Gamma'; Sigma' ~< C ->
      Delta ++ (Sigma++PSigma) :: Delta';; Gamma ++ Gamma'; Sigma' ~< C).

Lemma3: General case. We prove it by induction on the first premises such as Delta;; Gamma; empty ~< A. When type A is principal type of that derivation, we use Lemma 2.

Lemma j_cut_cons_lemma3: forall A,
  j_cut_ind_on_typ A ->
  forall Delta Gamma Sigma,
    Delta;; Gamma; Sigma ~< A ->
    (Sigma = empty ->
      forall Delta' Gamma' Sigma' C,
        Delta';; A::Gamma'; Sigma' ~< C ->
        Delta ++ Delta';; Gamma ++ Gamma'; Sigma' ~< C) /\
    (forall Delta' Gamma' Sigma' C,
      Delta';; Gamma'; A::Sigma' ~< C ->
      Delta ++ Delta';; Gamma ++ Gamma'; Sigma ++ Sigma' ~< C) /\
    (forall Delta' PSigma Gamma' Sigma' C,
      (A::PSigma)::Delta';; Gamma'; Sigma' ~< C ->
      Delta ++ (Sigma++PSigma) :: Delta';; Gamma ++ Gamma'; Sigma' ~< C).

We prove the main theorem by induction on the size of type A. Lemma 3 directly completes the proof.

Lemma j_cut_cons_aux: forall k A,
  size_typ A < k ->
  (forall Delta Delta' Gamma Gamma' Sigma' C,
    Delta;; Gamma; empty ~< A ->
    Delta';; A::Gamma'; Sigma' ~< C ->
    Delta ++ Delta';; Gamma ++ Gamma'; Sigma' ~< C) /\
  (forall Delta Delta' Gamma Gamma' Sigma Sigma' C,
    Delta;; Gamma; Sigma ~< A ->
    Delta';; Gamma'; A::Sigma' ~< C ->
    Delta ++ Delta';; Gamma ++ Gamma'; Sigma ++ Sigma' ~< C) /\
  (forall Delta Delta' PSigma Gamma Gamma' Sigma Sigma' C,
    Delta;; Gamma; Sigma ~< A ->
    (A::PSigma)::Delta';; Gamma'; Sigma' ~< C ->
    Delta ++ (Sigma ++PSigma) :: Delta';; Gamma ++ Gamma'; Sigma' ~< C).

Theorem j_cut_cons: forall A,
  (forall Delta Delta' Gamma Gamma' Sigma' C,
    Delta;; Gamma; empty ~< A ->
    Delta';; A::Gamma'; Sigma' ~< C ->
    Delta ++ Delta';; Gamma ++ Gamma'; Sigma' ~< C) /\
  (forall Delta Delta' Gamma Gamma' Sigma Sigma' C,
    Delta;; Gamma; Sigma ~< A ->
    Delta';; Gamma'; A::Sigma' ~< C ->
    Delta ++ Delta';; Gamma ++ Gamma'; Sigma ++ Sigma' ~< C) /\
  (forall Delta Delta' PSigma Gamma Gamma' Sigma Sigma' C,
    Delta;; Gamma; Sigma ~< A ->
    (A::PSigma)::Delta';; Gamma'; Sigma' ~< C ->
    Delta ++ (Sigma ++PSigma) :: Delta';; Gamma ++ Gamma'; Sigma' ~< C).

Equivalence between the two subtyping systems


This section contains the equivalence proof between the two subtyping systems.

Tactic Notation "destruct_eq_list" :=
  repeat match goal with
  | H: _ ++ _ :: _ = empty |- _ => symmetry in H; contradict H; auto with v62
  | H: _ ++ _ = empty |- _ => destruct (app_eq_nil _ _ H); clear H
  | H: ?G ++ _ = _ :: _ |- _ => destruct G; inv H; simpl in *
  end.

Tactic Notation "destruct_permute_list" :=
  match goal with
   | H: Permutation (?G1 ++ ?S1 :: ?G2) (?S2 :: ?G) |- _ =>
     destruct (list_eq_dec typ_dec S1 S2) as [Heq | Heq];
       [ SSCase "S1 = S2"; rewrite Heq in H; apply Permutation_app_cons_inv in H
         | SSCase "S1 <> S2";
           match G with
             | S2::?G' =>
               assert (In S1 G') as Hin;
                 [ apply Permutation_in with (x := S1) in H; auto with v62; simpl in H; repeat destruct H; try congruence; auto with v62
                   | destruct_in Hin; repeat rewrite app_comm_cons in H; apply Permutation_app_inv with (a := S1) in H ]
             | _ =>
               assert (In S1 G) as Hin;
                 [ apply Permutation_in with (x := S1) in H; auto with v62; simpl in H; repeat destruct H; try congruence; auto with v62
                   | destruct_in Hin; repeat rewrite app_comm_cons in H; apply Permutation_app_inv with (a := S1) in H ]
           end
       ]
    | _ => idtac
  end.

Completeness


The judgmental subtyping system is complete with respect to the relational subtyping system. For the case of the rule r_trans, we use the cut lemma.

Theorem completeness: forall A B,
  A =< B ->
  noworld;; empty; [A] ~< B.

Soundness


The judgmental subtyping system is sound with respect to the relational subtyping system. Following theorem states precisely the intuition behind the subtyping judgment.

To convert contexts to a single type, we need to know at least one type in the contexts because our converting functions require one initial type. Therefore, we split the lemma into three cases in which one of three contexts is non-empty. Note that we use Permutation for the case of the remote node context because the first element of Delta can be an empty list.

Theorem soundness: forall Delta Gamma Sigma C,
  Delta;; Gamma; Sigma ~< C ->
  (forall Gamma' A,
    Gamma = (A::Gamma') ->
    del_to_typ_right (Conj_right ([]A) ((map typ_box Gamma') ++ Sigma)) Delta =< C) /\
  (forall Sigma' A,
    Sigma = (A::Sigma') ->
    del_to_typ_right (Conj_right A ((map typ_box Gamma) ++ Sigma')) Delta =< C) /\
  (forall Delta' PSigma B,
    Permutation Delta ((B::PSigma)::Delta') ->
    Conj_right (del_to_typ_right (<> (Conj_right B PSigma)) Delta') ((map typ_box Gamma) ++ Sigma) =< C).

This page has been generated by coqdoc