# Library Base

Judgmental subtyping system with intersection types and modal types.
• Author : Jeongbong Seo and Sungwoo Park
This file contains definitions, lemmas, and theorems of the base subtyping systems which are described in Section 2 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
• The context must not be empty
• General ver. of the rule j_refl
• Context permutation
• Weakening
• The rule j_and_l is invertible
• Contraction
• Other lemmas
• Admissibility of the cut rule
• Equivalence between the two subtyping systems
• Completeness
• Soundness

# Definition

This section contains definitions of the base subtyping systems which are described in Section 2 of the paper.

## Pre-terms

There are two type constructors:
• A --> B denotes function types.
• A & B denotes intersection types.

Notation base := nat.

Inductive typ : Set :=
| typ_base : base -> typ
| typ_arrow : typ -> typ -> typ
| typ_conj : typ -> 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).

Tactic Notation "typ_cases" tactic(first) tactic(c) :=
first;
[ c "typ_base" | c "typ_arrow" | c "typ_conj"
].

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 in terms of 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)
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)

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

## 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 notation Sigma ~< B. Inference rules are from Figure 3 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 a typing context 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 " A ~< B " (at level 80).

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

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

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

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

where " A ~< B " := (j_sub A B).

Tactic Notation "j_sub_cases" tactic(first) tactic(c) :=
first;
[ c "j_refl" | c "j_and_l" | c "j_and_r" | c "j_fun"
].

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

#### The left-side is focused.

Sigma, |A| ~< B means that A is the principal type of Sigma, A ~< B; A is involved at the last inference rule.

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

Inductive j_sub_ocf : env -> typ -> typ -> Prop :=
| j_refl_ocf : forall (Sigma:env) (b:base),
Sigma, | (typ_base b) | ~< typ_base b

| j_and_l_ocf : forall (Sigma Sigma1 Sigma2:env) (t1 t2 t3:typ),
(Sigma1 ++ t1 :: t2 :: Sigma2) ~< t3 ->
Sigma = Sigma1 ++ Sigma2 ->
Sigma, |(t1 & t2)| ~< t3

| j_fun_ocf : forall (Sigma Sigma1 Sigma2:env) (t1 t2 t1' t2':typ) (Sigma'1 Sigma'2:list (typ*typ)),
subseq Sigma'1 (pickFun Sigma1) ->
subseq Sigma'2 (pickFun Sigma2) ->
Sigma = Sigma1 ++ Sigma2 ->
(forall t, In t (fsttypList (Sigma'1 ++ (t1,t2) :: Sigma'2)) -> [t1'] ~< t) ->
(sndtypList (Sigma'1 ++ (t1,t2) :: Sigma'2)) ~< t2' ->
Sigma, |(t1 --> t2)| ~< t1' --> t2'
where "Sigma , | A | ~< B " := (j_sub_ocf Sigma A B).

Tactic Notation "j_sub_ocf_cases" tactic(first) tactic(c) :=
first;
[ c "j_refl_ocf" | c "j_and_l_ocf" | c "j_fun_ocf"
].

#### The right-side is focused.

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

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

Inductive j_sub_rf : env -> typ -> Prop :=
| j_refl_rf : forall (Sigma1 Sigma2:env) (b:base),
Sigma1 ++ (typ_base b) :: Sigma2 ~< | typ_base b |

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

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

where " A ~< | B |" := (j_sub_rf A B).

Tactic Notation "j_sub_rf_cases" tactic(first) tactic(c) :=
first;
[ c "j_refl_rf" | c "j_and_r_rf" | c "j_fun_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_A : forall A,
Conj empty A = A.

Example conj_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_A : forall A,
Conj_right A empty = A.

Example conj_right_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.

### 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 base subtyping systems which are described in Section 2 of the paper.

## Lemmas for the relational subtyping system

### Weakening and associativity

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

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

### 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_swap_in: forall l1 l2 A B,
Conj (A :: l1 ++ l2) B =< Conj (l1 ++ A :: l2) B.

### More properties of the auxiliary functions

Following is another form of weakening lemma using subseq.

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

## Lemmas for the judgmental subtyping system

### The context must not be empty.

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

### General ver. of the rule j_refl

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

The rule j_refl involves a primitive type, but we can derive the reflexivity rule for an arbitrary type.

Lemma j_refl_gen: forall (A:typ) (Sigma Sigma':env),
Sigma ++ A :: Sigma' ~< A.

### Context permutation

To prove the main lemma permute_lsub, we need some auxiliary lemmas. 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 : forall (Sigma Sigma':env) (A:typ),
Sigma ~< A ->
Permutation Sigma Sigma' ->
Sigma' ~< A.

### Weakening

We may append an arbitrary type to the front of the context.
Lemma weakening_cons: forall Sigma A C,
Sigma ~< A ->
C :: Sigma ~< A.

We may add an arbitrary type to the middle of the context.
Lemma weakening_gen: forall Sigma Sigma' A C,
Sigma ++ Sigma' ~< A ->
Sigma ++ C :: Sigma' ~< A.

### The rule j_and_l is invertible.

Lemma j_and_l_inv_cons: forall Sigma A B C,
(A & B):: Sigma ~< C ->
A :: B :: Sigma ~< C.

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

### Rewriting lemmas

Lemma in_weakening : forall (A:Type) (l1 l2:list A) (x y:A),
In x (l1 ++ l2) ->
In x (l1 ++ y :: 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.

### Contraction

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

The proof is done by nested structural induction on type C and the derivation of 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 C Sigma A,
size_typ C < n ->
C::C::Sigma ~< A ->
C::Sigma ~< A.

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, it proves the goal by induction on the derivation of C :: C :: Sigma ~< A.

Lemma contraction_cons_aux: forall C Sigma A,
contraction_IH_on_typ (size_typ C) ->
C::C::Sigma ~< A ->
C::Sigma ~< A.

The main lemma is proven by induction on the size of type C.
Lemma contraction_cons_aux_typ: forall n C Sigma A,
size_typ C < n ->
C::C::Sigma ~< A ->
C::Sigma ~< A.

This is the main lemma.
Lemma contraction_cons: forall C Sigma A,
C::C::Sigma ~< A ->
C::Sigma ~< A.

Followings are the generalized version of contraction lemmas.
Lemma contraction_gen: forall Sigma Sigma' A C,
Sigma ++ C :: C :: Sigma' ~< A ->
Sigma ++ C :: Sigma' ~< A.

Lemma contraction_bunch_cons: forall Sigma Sigma' A,
Sigma ++ Sigma ++ Sigma' ~< A ->
Sigma ++ Sigma' ~< A.

Lemma contraction_bunch: forall Sigma A,
Sigma ++ Sigma ~< A ->
Sigma ~< A.

## Other lemmas

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 rule

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

Following is the main theorem to prove:
Sigma ~< A ->
A :: Sigma' ~< C ->
Sigma ++ Sigma' ~< C.

As we explained in the paper, we proceeds 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 used 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 Sigma Sigma' A' C,
size_typ A' < size_typ A ->
Sigma ~< A' ->
A' :: Sigma' ~< C ->
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 Sigma Sigma' A C,
j_cut_ind_on_typ A ->
Sigma ~< | A | ->
Sigma', | A | ~< C ->
Sigma ++ Sigma' ~< C.

Lemma2: A is the principal type of the first derivation. We prove it by induction on A::Sigma' ~< C. When type A is the principal type of that derivation, we use Lemma 1.

Lemma j_cut_cons_lemma2: forall Sigma Sigma' A C,
j_cut_ind_on_typ A ->
Sigma ~< | A | ->
A :: Sigma' ~< C ->
Sigma ++ Sigma' ~< C.

Lemma3: General case. We prove it by induction on Sigma ~< A. When type A is the principal type of that derivation, we use Lemma 2.

Lemma j_cut_cons_lemma3: forall Sigma Sigma' A C,
j_cut_ind_on_typ A ->
Sigma ~< A ->
A :: Sigma' ~< C ->
Sigma ++ 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 Sigma Sigma' A C,
size_typ A < k ->
Sigma ~< A ->
A :: Sigma' ~< C ->
Sigma ++ Sigma' ~< C.

This is the main theorem.
Theorem j_cut_cons: forall Sigma Sigma' A C,
Sigma ~< A ->
A :: Sigma' ~< C ->
Sigma ++ Sigma' ~< C.

# Equivalence between the two subtyping systems

This section contains the equivalence proof between the two base 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 ->
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 Sigma A C,
A::Sigma ~< C ->
Conj_right A Sigma =< C.