Library SS4

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 S4 which are described in Section 3 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
      • 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
    • Other lemmas
  • Admissibility of the cut rules
  • Equivalence between the two subtyping systems
    • Completeness
    • Soundness



Definition


This section contains definitions of the subtyping systems based on modal logic S4 which are described in Section 3 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 subtyping context as a list of typ.

Notation env := (list typ).
Notation empty := (@nil 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.

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

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"
  ].

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 the judgmental subtyping system, we use the following two judgments: the ordinary subtyping judgments Gamma; Sigma ~< B and the possibility subtyping judgments Gamma; Sigma %< B. Gamma is the global subtyping context, and Sigma is the ordinary subtyping context. Inference rules are from Figure 4 in the paper. Note that two judgments are mutually defined.

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 " G ; S ~< B " (at level 80).
Reserved Notation " G ; S %< B " (at level 80).

Inductive j_sub : env -> env -> typ -> Prop :=
  | j_refl : forall (Gamma Sigma1 Sigma2:env) (b:base),
    Gamma; Sigma1 ++ (typ_base b) :: Sigma2 ~< typ_base b

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

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

  | j_fun : forall (Gamma Sigma:env) (t1' t2':typ) (Sigma':list (typ*typ)),
    subseq Sigma' (pickFun Gamma ++ pickFun Sigma) ->
    (forall t, In t (fsttypList Sigma') -> empty; [t1'] ~< t) ->
    empty; (sndtypList Sigma') ~< t2' ->
    Gamma; Sigma ~< t1' --> t2'
    
  | j_refl_v : forall (Gamma1 Gamma2 Sigma:env) (b:base),
    Gamma1 ++ (typ_base b) :: Gamma2; Sigma ~< typ_base b

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

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

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

  | j_box_r : forall (Gamma Sigma: env) (t:typ),
    Gamma; empty ~< t ->
    Gamma; Sigma ~< [] t

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

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

with j_sub_p : env -> env -> typ -> Prop :=
  | j_and_lp : forall (Gamma Sigma1 Sigma2:env) (t1 t2 t3:typ),
    Gamma; (Sigma1 ++ t1 :: t2 :: Sigma2) %< t3 ->
    Gamma; (Sigma1 ++ (t1 & t2) :: Sigma2) %< t3

  | j_and_vp : forall (Gamma1 Gamma2 Sigma:env) (t1 t2 t3:typ),
    (Gamma1 ++ t1 :: t2 :: Gamma2); Sigma %< t3 ->
    (Gamma1 ++ (t1 & t2) :: Gamma2); Sigma %< t3

  | j_dia_lp : forall (Gamma Sigma1 Sigma2:env) (t1 t2:typ),
    Gamma; [t1] %< t2 ->
    Gamma; (Sigma1 ++ (<> t1) :: Sigma2) %< t2

  | j_dia_vp : forall (Gamma1 Gamma2 Sigma:env) (t1 t2:typ),
    Gamma1 ++ (<>t1)::Gamma2; [t1] %< t2 ->
    Gamma1 ++ (<>t1)::Gamma2 ; Sigma %< t2

  | j_box_lp : forall (Gamma Gamma1 Gamma2 Sigma1 Sigma2: env) (t1 t2:typ),
    Gamma1 ++ t1 :: Gamma2; Sigma1 ++ Sigma2 %< t2 ->
    Gamma = Gamma1 ++ Gamma2 ->
    Gamma; Sigma1 ++ ([]t1) :: Sigma2 %< t2
  
  | j_box_vp : forall (Gamma1 Gamma2 Sigma: env) (t1 t2:typ),
    Gamma1 ++ t1 :: Gamma2; Sigma %< t2 ->
    Gamma1 ++ ([]t1) :: Gamma2; Sigma %< t2

  | j_poss_p : forall (Gamma Sigma:env) (t:typ),
    Gamma; Sigma ~< t ->
    Gamma; Sigma %< t
    
where " Gamma ; Sigma %< B " := (j_sub_p Gamma Sigma B).

We use the minimality mutual induction scheme for two subtyping judgments.

Scheme j_sub_ind2 := Minimality for j_sub Sort Prop
  with j_sub_p_ind2 := Minimality for j_sub_p Sort Prop.



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

Tactic Notation "j_sub_p_cases" tactic(first) tactic(c) :=
  first;
  [ c "j_and_lp" | c "j_and_vp" | c "j_dia_lp"
  | c "j_dia_vp" | c "j_box_lp" | c "j_box_vp" | c "j_poss_p"
  ].

Tactic Notation "j_sub_j_sub_p_cases" tactic(first) tactic(c) :=
  first;
  [ c "j_refl" | c "j_and_l" | c "j_and_r" | c "j_fun"
  | c "j_refl_v" | c "j_and_v" | c "j_box_v" | c "j_box_l"
  | c "j_box_r" | c "j_dia_r"
  | c "j_and_lp" | c "j_and_vp" | c "j_dia_lp"
  | c "j_dia_vp" | c "j_box_lp" | c "j_box_vp" | c "j_poss_p"
  ].

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 global subtyping context is focused.


Gamma, |A|; Sigma ~< B and Gamma, |A|; Sigma %< B mean that A is the principal type of the last inference rule in their derivations.

Gamma, |A|; Sigma %< B does not include the rule j_dia_vp_mcf since we have to solve that case not in the first step (Lemma 1) but in the second step (Lemma 2). The principal type of that rule (<>A) still appears in the premise so that we have to solve that case by induction on the derivation which is done in the second step.

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

Inductive j_sub_mcf : env -> env -> typ -> typ -> Prop :=
  | j_fun_mcf : forall (Gamma Gamma1 Gamma2 Sigma :env) (t1 t2 t1' t2':typ) (Gamma'1 Gamma'2 Sigma':list (typ*typ)),
    subseq Gamma'1 (pickFun Gamma1) ->
    subseq Gamma'2 (pickFun Gamma2) ->
    subseq Sigma' (pickFun Sigma) ->
    Gamma = Gamma1 ++ Gamma2 ->
    (forall t, In t (fsttypList ((Gamma'1 ++ (t1,t2) :: Gamma'2) ++ Sigma')) -> empty; [t1'] ~< t) ->
    empty; (sndtypList ((Gamma'1 ++ (t1,t2) :: Gamma'2) ++ Sigma')) ~< t2' ->
    Gamma,|(t1 --> t2)|; Sigma ~< t1' --> t2'

  | j_refl_v_mcf : forall (Gamma Sigma:env) (b:base),
    Gamma,| (typ_base b) | ; Sigma ~< typ_base b
    
  | j_and_v_mcf : forall (Gamma Gamma1 Gamma2 Sigma:env) (t1 t2 t3:typ),
    (Gamma1 ++ t1 :: t2 :: Gamma2); Sigma ~< t3 ->
    Gamma = Gamma1 ++ Gamma2 ->
    Gamma,|(t1 & t2)|; Sigma ~< t3

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

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

Inductive j_sub_p_mcf : env -> env -> typ -> typ -> Prop :=
  | j_and_vp_mcf : forall (Gamma Gamma1 Gamma2 Sigma:env) (t1 t2 t3:typ),
    (Gamma1 ++ t1 :: t2 :: Gamma2); Sigma %< t3 ->
    Gamma = Gamma1 ++ Gamma2 ->
    Gamma,|(t1 & t2)|; Sigma %< t3

  | j_box_vp_mcf : forall (Gamma Gamma1 Gamma2 Sigma: env) (t1 t2:typ),
    Gamma1 ++ t1 :: Gamma2; Sigma %< t2 ->
    Gamma = Gamma1 ++ Gamma2 ->
    Gamma,|([]t1)|; Sigma %< t2

where "Gamma ,| A | ; Sigma %< B " := (j_sub_p_mcf Gamma Sigma A B).


A type in the ordinary subtyping context is focused.


Gamma; Sigma, |A| ~< B and Gamma; Sigma, |A| %< B mean that A is the principal type of the last inference rule in their derivations.

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

Inductive j_sub_ocf : env -> env -> typ -> typ -> Prop :=
  | j_refl_ocf : forall (Gamma Sigma:env) (b:base),
    Gamma; Sigma, | (typ_base b) | ~< typ_base b
    
  | j_and_l_ocf : forall (Gamma Sigma Sigma1 Sigma2:env) (t1 t2 t3:typ),
    Gamma; (Sigma1 ++ t1 :: t2 :: Sigma2) ~< t3 ->
    Sigma = Sigma1 ++ Sigma2 ->
    Gamma; Sigma, |(t1 & t2)| ~< t3

  | j_fun_ocf : forall (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))) -> empty; [t1'] ~< t) ->
    empty; (sndtypList (Gamma' ++ (Sigma'1 ++ (t1,t2) :: Sigma'2))) ~< t2' ->
    Gamma; Sigma, |(t1 --> t2)| ~< t1' --> t2'

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

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

Inductive j_sub_p_ocf : env -> env -> typ -> typ -> Prop :=
  | j_and_lp_ocf : forall (Gamma Sigma Sigma1 Sigma2:env) (t1 t2 t3:typ),
    Gamma; (Sigma1 ++ t1 :: t2 :: Sigma2) %< t3 ->
    Sigma = Sigma1 ++ Sigma2 ->
    Gamma; Sigma, |(t1 & t2)| %< t3

  | j_dia_lp_ocf : forall (Gamma Sigma:env) (t1 t2:typ),
    Gamma; [t1] %< t2 ->
    Gamma; Sigma, |<>t1| %< t2

  | j_box_lp_ocf : forall (Gamma Gamma1 Gamma2 Sigma: env) (t1 t2:typ),
    Gamma1 ++ t1 :: Gamma2; Sigma %< t2 ->
    Gamma = Gamma1 ++ Gamma2 ->
    Gamma; Sigma, |([]t1)| %< t2

where "Gamma ; Sigma , | A | %< B " := (j_sub_p_ocf Gamma Sigma A B).


The right-side is focused.


Gamma; Sigma ~< |B| means that B is the principal type of Gamma; Sigma ~< B; B is involved at the last inference rule. We do not need Gamma; Sigma %< |B| since there is no right rule for the possibility subtyping judgment.

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

Inductive j_sub_rf : env -> env -> typ -> Prop :=
  | j_refl_rf : forall (Gamma Sigma1 Sigma2:env) (b:base),
    Gamma; Sigma1 ++ (typ_base b) :: Sigma2 ~< | typ_base b |
    
  | j_and_r_rf : forall (Gamma Sigma:env) (t1 t2:typ),
    Gamma; Sigma ~< t1 ->
    Gamma; Sigma ~< t2 ->
    Gamma; Sigma ~< | t1 & t2 |

  | j_fun_rf : forall (Gamma Sigma:env) (t1' t2':typ) (Sigma':list (typ*typ)),
    subseq Sigma' (pickFun Gamma ++ pickFun Sigma) ->
    (forall t, In t (fsttypList Sigma') -> empty; [t1'] ~< t) ->
    empty; (sndtypList Sigma') ~< t2' ->
    Gamma; Sigma ~< | t1' --> t2' |

  | j_refl_v_rf : forall (Gamma1 Gamma2 Sigma:env) (b:base),
    Gamma1 ++ (typ_base b) :: Gamma2; Sigma ~< | typ_base b |

  | j_box_r_rf : forall (Gamma Sigma: env) (t:typ),
    Gamma; empty ~< t ->
    Gamma; Sigma ~< | [] t |

  | j_dia_r_rf : forall (Gamma Sigma:env) (t:typ),
    Gamma; Sigma %< t ->
    Gamma; Sigma ~< | <> t |

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


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

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.

Infrastructure lemmas


This section contains infrastructure lemmas of the subtyping systems based on modal logic S4 which are described in Section 3 of the paper.

Lemmas for the relational subtyping system


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.


We can generalize the lemma sub_weakening_left using Conj_right.

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


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


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.

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 |]
    | _ => 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]
    | _ => 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)


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


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


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 Conj_split: forall G1 G2 A B,
  Conj G1 A & Conj G2 B =< Conj (G1++A::G2) B.

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 lemma exploits the rule r_box_T.

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


Lemmas for the judgmental subtyping system


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.

Not all contexts are empty


Lemma context_is_not_nil: forall A,
  ~ (empty ; empty ~< A) /\ ~ (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 (Gamma Sigma Sigma':env), Gamma; Sigma ++ A :: Sigma' ~< A) /\
  (forall (Gamma Gamma' Sigma:env), Gamma ++ A :: Gamma'; Sigma ~< A).




Judgmental Subtyping is preserved under 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'.

This is the main lemma.
Lemma permute_j_sub_j_sub_p :
  (forall (Gamma Sigma:env) (A:typ), Gamma ; Sigma ~< A ->
    forall (Gamma' Sigma':env),
      Permutation Gamma Gamma' ->
      Permutation Sigma Sigma' ->
      Gamma'; Sigma' ~< A) /\
  (forall (Gamma Sigma:env) (A:typ), Gamma ; Sigma %< A ->
    forall (Gamma' Sigma':env),
      Permutation Gamma Gamma' ->
      Permutation Sigma Sigma' ->
      Gamma'; Sigma' %< A).

Definition permute_j_sub := proj1 permute_j_sub_j_sub_p.
Definition permute_j_sub_p := proj2 permute_j_sub_j_sub_p.

Weakening

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

Lemma weakening_cons_j_sub_j_sub_p:
  (forall (Gamma Sigma:env) (A:typ), Gamma; Sigma ~< A ->
    forall (C:typ),
      Gamma; C :: Sigma ~< A /\ C::Gamma; Sigma ~< A) /\
  (forall (Gamma Sigma:env) (A:typ), Gamma; Sigma %< A ->
    forall (C:typ),
      Gamma; C:: Sigma %< A /\ C::Gamma; Sigma %< A).

We may add an arbitrary type to the middle of the context.
Lemma weakening_gen_j_sub_j_sub_p: forall Gamma Gamma' Sigma Sigma' A C,
  (Gamma ++ Gamma'; Sigma ++ Sigma' ~< A ->
  Gamma ++ Gamma'; Sigma ++ C :: Sigma' ~< A /\ Gamma ++ C :: Gamma'; Sigma ++ Sigma' ~< A) /\
  (Gamma ++ Gamma'; Sigma ++ Sigma' %< A ->
  Gamma ++ Gamma'; Sigma ++ C :: Sigma' %< A /\ Gamma ++ C :: Gamma'; Sigma ++ Sigma' %< A).

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

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

Lemma weakening_gen_j_sub_p: forall (Gamma Sigma Sigma' : env) (A C : typ),
  Gamma; Sigma ++ Sigma' %< A ->
  Gamma; Sigma ++ C :: Sigma' %< A.

Lemma weakening_gen_j_sub_vp: forall (Gamma Gamma' Sigma : env) (A C : typ),
  Gamma ++ Gamma'; Sigma %< A ->
  Gamma ++ C :: Gamma'; Sigma %< A.


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

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

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


Lemma weakening_bunch_psub: forall (Gamma Sigma Sigma':env) (A:typ),
  Gamma; Sigma %< A ->
  Gamma; Sigma' ++ Sigma %< A.

Lemma weakening_bunch_psub': forall (Gamma Sigma Sigma':env) (A:typ),
  Gamma; Sigma %< A ->
  Gamma; Sigma ++ Sigma' %< A.


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

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


Lemma weakening_bunch_psub_v: forall (Gamma Gamma' Sigma:env) (A:typ),
  Gamma; Sigma %< A ->
  Gamma' ++ Gamma; Sigma %< A.

Lemma weakening_bunch_psub_v': forall (Gamma Gamma' Sigma:env) (A:typ),
  Gamma; Sigma %< A ->
  Gamma ++ 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:
Gamma; C::Sigma ~< A -> C::Gamma; Sigma ~< A.
Gamma; C::Sigma %< A -> C::Gamma; Sigma %< A.

The proof is done by nested induction on type C and the derivation of Gamma; C::Sigma ~< A or Gamma; C::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 Gamma Sigma C, Gamma; Sigma ~< C ->
    forall Sigma',
      Sigma = A :: Sigma' ->
      A :: Gamma; Sigma' ~< C) /\
  (forall Gamma Sigma C, Gamma; Sigma %< C ->
    forall Sigma',
      Sigma = A :: Sigma' ->
      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 Gamma Sigma C, Gamma; Sigma ~< C ->
    forall Sigma',
      Sigma = A :: Sigma' ->
      A :: Gamma; Sigma' ~< C) /\
  (forall Gamma Sigma C, Gamma; Sigma %< C ->
    forall Sigma',
      Sigma = A :: Sigma' ->
      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 Gamma Sigma C, Gamma; Sigma ~< C ->
    forall Sigma',
      Sigma = A :: Sigma' ->
      A :: Gamma; Sigma' ~< C) /\
  (forall Gamma Sigma C, Gamma; Sigma %< C ->
    forall Sigma',
      Sigma = A :: Sigma' ->
      A :: Gamma; Sigma' %< C).

This is the main lemma.

Lemma move_from_sig_to_gam_cons: forall A,
  (forall Gamma Sigma C, Gamma; Sigma ~< C ->
    forall Sigma',
      Sigma = A :: Sigma' ->
      A :: Gamma; Sigma' ~< C) /\
  (forall Gamma Sigma C, Gamma; Sigma %< C ->
    forall Sigma',
      Sigma = A :: Sigma' ->
      A :: Gamma; Sigma' %< C).


Invertible rules

The rules j_and_l and j_and_lp are invertible.


Lemma j_and_l_p_inv_cons:
  (forall Gamma Sigma C, Gamma; Sigma ~< C ->
    forall Sigma0 A B,
      Sigma = (A & B) :: Sigma0 ->
      Gamma; A :: B :: Sigma0 ~< C) /\
  (forall Gamma Sigma C, Gamma; Sigma %< C ->
    forall Sigma0 A B,
      Sigma = (A & B) :: Sigma0 ->
      Gamma; A :: B :: Sigma0 %< C).

Lemma j_and_l_p_inv: forall Gamma Sigma Sigma' A B C,
  (Gamma; Sigma ++ (A & B) :: Sigma' ~< C ->
  Gamma; Sigma ++ A :: B :: Sigma' ~< C) /\
  (Gamma; Sigma ++ (A & B) :: Sigma' %< C ->
  Gamma; Sigma ++ A :: B :: Sigma' %< C).

Definition j_and_l_inv Gamma Sigma Sigma' A B C := proj1 (j_and_l_p_inv Gamma Sigma Sigma' A B C).
Definition j_and_lp_inv Gamma Sigma Sigma' A B C := proj2 (j_and_l_p_inv Gamma Sigma Sigma' A B C).


The rules j_and_v and j_and_vp are invertible.


Lemma j_and_v_vp_inv_cons:
  (forall Gamma Sigma C, Gamma; Sigma ~< C ->
    forall Gamma0 A B,
      Permutation Gamma ((A&B) :: Gamma0) ->
      A :: B :: Gamma0; Sigma ~< C) /\
  (forall Gamma Sigma C, Gamma; Sigma %< C ->
    forall Gamma0 A B,
      Permutation Gamma ((A&B) :: Gamma0) ->
      A :: B :: Gamma0; Sigma %< C).

The rules j_box_v and j_box_vp are invertible.


Lemma j_sub_v_vp_inv_cons:
  (forall Gamma Sigma C, Gamma; Sigma ~< C ->
    forall Gamma0 A,
      Permutation Gamma (([]A) :: Gamma0) ->
      A :: Gamma0; Sigma ~< C) /\
  (forall Gamma Sigma C, Gamma; Sigma %< C ->
    forall Gamma0 A,
      Permutation Gamma (([]A) :: Gamma0) ->
      A :: Gamma0; Sigma %< C).

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

The rule j_dia_r is invertible.


Lemma j_dia_r_inv: forall Gamma Sigma C,
  Gamma; Sigma ~< <>C ->
  Gamma; Sigma %< C.

Contraction


Following is the contraction lemma to prove:
Gamma; C::C::Sigma ~< A -> Gamma; C::Sigma ~< A.
C::C::Gamma; Sigma ~< A -> C::Gamma; Sigma ~< A.
Gamma; C::C::Sigma %< A -> Gamma; C::Sigma %< A.
C::C::Gamma; Sigma %< A -> C::Gamma; Sigma %< A.

The proof is done by nested structural induction on type C and the derivation of the premise such as Gamma; C::C::Sigma ~< A. The simple nested induction, however, generates a lot of cases and many of them are solved by the same proof script. To reduce the proof script size, we change the induction scheme for the first induction, which is on type, from structural induction to size induction.

Definition contraction_IH_on_typ n :=
  forall A,
  size_typ A < n ->
    (forall Gamma Sigma C, Gamma; Sigma ~< C ->
      (forall Gamma0, Permutation Gamma (A :: A :: Gamma0) -> A::Gamma0; Sigma ~< C) /\
      (forall Sigma0, Permutation Sigma (A :: A :: Sigma0) -> Gamma; A::Sigma0 ~< C)) /\
    (forall Gamma Sigma C, Gamma; Sigma %< C ->
      (forall Gamma0, Permutation Gamma (A :: A :: Gamma0) -> A::Gamma0; Sigma %< C) /\
      (forall Sigma0, Permutation Sigma (A :: A :: Sigma0) -> Gamma; A::Sigma0 %< C)).

To manage the proof, we factor out the second induction part as an independent lemma. 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 contraction_cons_aux: forall A,
  contraction_IH_on_typ (size_typ A) ->
  (forall Gamma Sigma C, Gamma; Sigma ~< C ->
    (forall Gamma0, Permutation Gamma (A :: A :: Gamma0) -> A::Gamma0; Sigma ~< C) /\
    (forall Sigma0, Permutation Sigma (A :: A :: Sigma0) -> Gamma; A::Sigma0 ~< C)) /\
  (forall Gamma Sigma C, Gamma; Sigma %< C ->
    (forall Gamma0, Permutation Gamma (A :: A :: Gamma0) -> A::Gamma0; Sigma %< C) /\
    (forall Sigma0, Permutation Sigma (A :: A :: Sigma0) -> Gamma; A::Sigma0 %< C)).

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

Lemma contraction_cons_aux_typ: forall n A,
  size_typ A < n ->
  (forall Gamma Sigma C, Gamma; Sigma ~< C ->
    (forall Gamma0, Permutation Gamma (A :: A :: Gamma0) -> A::Gamma0; Sigma ~< C) /\
    (forall Sigma0, Permutation Sigma (A :: A :: Sigma0) -> Gamma; A::Sigma0 ~< C)) /\
  (forall Gamma Sigma C, Gamma; Sigma %< C ->
    (forall Gamma0, Permutation Gamma (A :: A :: Gamma0) -> A::Gamma0; Sigma %< C) /\
    (forall Sigma0, Permutation Sigma (A :: A :: Sigma0) -> Gamma; A::Sigma0 %< C)).

This is the main lemma.

Lemma contraction_cons: forall A,
  (forall Gamma Sigma C, Gamma; Sigma ~< C ->
    (forall Gamma0, Permutation Gamma (A :: A :: Gamma0) -> A::Gamma0; Sigma ~< C) /\
    (forall Sigma0, Permutation Sigma (A :: A :: Sigma0) -> Gamma; A::Sigma0 ~< C)) /\
  (forall Gamma Sigma C, Gamma; Sigma %< C ->
    (forall Gamma0, Permutation Gamma (A :: A :: Gamma0) -> A::Gamma0; Sigma %< C) /\
    (forall Sigma0, Permutation Sigma (A :: A :: Sigma0) -> Gamma; A::Sigma0 %< C)).

Followings are the generalized version of contraction lemmas.

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

Lemma contraction_bunch: forall Gamma Sigma A,
  (Gamma; Sigma ++ Sigma ~< A -> Gamma; Sigma ~< A) /\
  (Gamma; Sigma ++ Sigma %< A -> Gamma; Sigma %< A) /\
  (Gamma ++ Gamma; Sigma ~< A -> Gamma; Sigma ~< A) /\
  (Gamma ++ Gamma; Sigma %< A -> Gamma; Sigma %< A).

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:
  Gamma; Sigma %< A -> Gamma'; [A] ~< C -> Gamma ++ Gamma'; Sigma %< C
  Gamma; Sigma %< A -> Gamma'; [A] %< C -> Gamma ++ Gamma'; Sigma %< C
  Gamma; empty ~< A -> A::Gamma'; Sigma' ~< C -> Gamma ++ Gamma'; Sigma' ~< C
  Gamma; empty ~< A -> A::Gamma'; Sigma' %< C -> Gamma ++ Gamma'; Sigma' %< C
  Gamma; Sigma ~< A -> Gamma'; A::Sigma' ~< C -> Gamma ++ Gamma'; Sigma ++ Sigma' ~< C
  Gamma; Sigma ~< A -> Gamma'; A::Sigma' %< C -> Gamma ++ Gamma'; Sigma ++ 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 (Gamma Gamma' Sigma : env) (C : typ),
      Gamma; Sigma %< A -> Gamma'; [A] ~< C -> Gamma ++ Gamma'; Sigma %< C) /\
    (forall (Gamma Gamma' Sigma : env) (C : typ),
      Gamma; Sigma %< A -> Gamma'; [A] %< C -> Gamma ++ Gamma'; Sigma %< C) /\
    (forall (Gamma Gamma' Sigma' : env) (C : typ),
      Gamma; empty ~< A -> A :: Gamma'; Sigma' ~< C -> Gamma ++ Gamma'; Sigma' ~< C) /\
    (forall (Gamma Gamma' Sigma' : env) (C : typ),
      Gamma; empty ~< A -> A :: Gamma'; Sigma' %< C -> Gamma ++ Gamma'; Sigma' %< C) /\
    (forall (Gamma Gamma' Sigma Sigma' : env) (C : typ),
      Gamma; Sigma ~< A -> Gamma'; A :: Sigma' ~< C -> Gamma ++ Gamma'; Sigma ++ Sigma' ~< C) /\
    (forall (Gamma Gamma' Sigma Sigma' : env) (C : typ),
      Gamma; Sigma ~< A -> Gamma'; A :: Sigma' %< C -> Gamma ++ Gamma'; Sigma ++ 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 Gamma Sigma A,
  j_cut_ind_on_typ A ->
  Gamma; Sigma ~< |A| ->
  (Sigma = empty -> forall Gamma' Sigma' C, Gamma',|A|; Sigma' ~< C -> Gamma ++ Gamma'; Sigma' ~< C) /\
  (Sigma = empty -> forall Gamma' Sigma' C, Gamma',|A|; Sigma' %< C -> Gamma ++ Gamma'; Sigma' %< C) /\
  (forall Gamma' Sigma' C, Gamma'; Sigma', |A| ~< C -> Gamma ++ Gamma'; Sigma ++ Sigma' ~< C) /\
  (forall Gamma' Sigma' C, Gamma'; Sigma', |A| %< C -> Gamma ++ Gamma'; Sigma ++ Sigma' %< C).

Lemma2: A is the principal type of the first derivation such as Gamma; empty ~< A. We prove it by induction on the second derivations such as 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 Gamma' Sigma' C, Gamma'; Sigma' ~< C ->
    (forall Gamma Sigma Gamma'',
      Gamma; Sigma ~< |A| -> Sigma = empty -> Permutation Gamma' (A::Gamma'') -> Gamma ++ Gamma''; Sigma' ~< C) /\
    (forall Gamma Sigma Sigma'',
      Gamma; Sigma ~< |A| -> Sigma' = A::Sigma'' -> Gamma ++ Gamma'; Sigma ++ Sigma'' ~< C)
  ) /\
  (forall Gamma' Sigma' C, Gamma'; Sigma' %< C ->
    (forall Gamma Sigma Gamma'',
      Gamma; Sigma ~< |A| -> Sigma = empty -> Permutation Gamma' (A::Gamma'') -> Gamma ++ Gamma''; Sigma' %< C) /\
    (forall Gamma Sigma Sigma'',
      Gamma; Sigma ~< |A| -> Sigma' = A::Sigma'' -> Gamma ++ Gamma'; Sigma ++ Sigma'' %< C)).

Lemma2: the original form.

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

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

Lemma j_cut_cons_lemma3: forall A_dummy,
  j_cut_ind_on_typ A_dummy ->
  (forall Gamma Sigma A,
    Gamma; Sigma ~< A ->
    A_dummy = A ->
    (forall Gamma' Sigma' C, Sigma = empty -> A::Gamma'; Sigma' ~< C -> Gamma ++ Gamma'; Sigma' ~< C) /\
    (forall Gamma' Sigma' C, Sigma = empty -> A::Gamma'; Sigma' %< C -> Gamma ++ Gamma'; Sigma' %< C) /\
    (forall Gamma' Sigma' C, Gamma'; A::Sigma' ~< C -> Gamma ++ Gamma'; Sigma ++ Sigma' ~< C) /\
    (forall Gamma' Sigma' C, Gamma'; A::Sigma' %< C -> Gamma ++ Gamma'; Sigma ++ Sigma' %< C)) /\
  (forall Gamma Sigma A,
    Gamma; Sigma %< A ->
    A_dummy = A ->
    (forall Gamma' C, Gamma'; [A] ~< C -> Gamma ++ Gamma'; Sigma %< C) /\
    (forall Gamma' C, Gamma'; [A] %< C -> 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 Gamma Gamma' Sigma C, Gamma; Sigma %< A -> Gamma'; [A] ~< C -> Gamma ++ Gamma'; Sigma %< C) /\
  (forall Gamma Gamma' Sigma C, Gamma; Sigma %< A -> Gamma'; [A] %< C -> Gamma ++ Gamma'; Sigma %< C) /\
  (forall Gamma Gamma' Sigma' C, Gamma; empty ~< A -> A::Gamma'; Sigma' ~< C -> Gamma ++ Gamma'; Sigma' ~< C) /\
  (forall Gamma Gamma' Sigma' C, Gamma; empty ~< A -> A::Gamma'; Sigma' %< C -> Gamma ++ Gamma'; Sigma' %< C) /\
  (forall Gamma Gamma' Sigma Sigma' C, Gamma; Sigma ~< A -> Gamma'; A::Sigma' ~< C -> Gamma ++ Gamma'; Sigma ++ Sigma' ~< C) /\
  (forall Gamma Gamma' Sigma Sigma' C, Gamma; Sigma ~< A -> Gamma'; A::Sigma' %< C -> Gamma ++ Gamma'; Sigma ++ Sigma' %< C).

This is the main theorem.
Theorem j_cut_cons: forall A,
  (forall Gamma Gamma' Sigma C, Gamma; Sigma %< A -> Gamma'; [A] ~< C -> Gamma ++ Gamma'; Sigma %< C) /\
  (forall Gamma Gamma' Sigma C, Gamma; Sigma %< A -> Gamma'; [A] %< C -> Gamma ++ Gamma'; Sigma %< C) /\
  (forall Gamma Gamma' Sigma' C, Gamma; empty ~< A -> A::Gamma'; Sigma' ~< C -> Gamma ++ Gamma'; Sigma' ~< C) /\
  (forall Gamma Gamma' Sigma' C, Gamma; empty ~< A -> A::Gamma'; Sigma' %< C -> Gamma ++ Gamma'; Sigma' %< C) /\
  (forall Gamma Gamma' Sigma Sigma' C, Gamma; Sigma ~< A -> Gamma'; A::Sigma' ~< C -> Gamma ++ Gamma'; Sigma ++ Sigma' ~< C) /\
  (forall Gamma Gamma' Sigma Sigma' C, Gamma; Sigma ~< A -> Gamma'; A::Sigma' %< C -> Gamma ++ Gamma'; Sigma ++ Sigma' %< C).

Equivalence between the two subtyping systems


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

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 ->
  empty; A :: empty ~< 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.

Theorem soundness:
  (forall Gamma Sigma C, Gamma; Sigma ~< C ->
    (forall Gamma' A, Gamma = A::Gamma' -> Sigma = empty -> box_Conj_right ([]A) Gamma' =< C) /\
    (forall Sigma' A, Gamma = empty -> Sigma = A::Sigma' -> Conj_right A Sigma' =< C) /\
    (forall Gamma' A Sigma' B, Gamma = A::Gamma' -> Sigma = B::Sigma' -> typ_conj (box_Conj_right ([]A) Gamma') (Conj_right B Sigma') =< C)) /\
  (forall Gamma Sigma C, Gamma; Sigma %< C ->
    (forall Gamma' A, Gamma = A::Gamma' -> Sigma = empty -> box_Conj_right ([]A) Gamma' =< <> C) /\
    (forall Sigma' A, Gamma = empty -> Sigma = A::Sigma' -> Conj_right A Sigma' =< <> C) /\
    (forall Gamma' A Sigma' B, Gamma = A::Gamma' -> Sigma = B::Sigma' -> typ_conj (box_Conj_right ([]A) Gamma') (Conj_right B Sigma') =< <> C)).

This page has been generated by coqdoc