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

Set Implicit Arguments.

Require Export Coq.Lists.List.
Require Export Arith.
Require Export SfLib.
Require Export Subseq.
Require Export Permutation.
Require Export Perm_tactic.
Ltac inv H := inversion H; clear H; subst.

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 (* primitive type *)
  | typ_arrow : typ -> typ -> typ (* function type *)
  | typ_conj : typ -> typ -> typ. (* intersection type *)

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

(* Tactic for labeling cases. *)
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}.
Proof.
  decide equality. apply eq_nat_dec.
Qed.

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

We represent the 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).

Hint Constructors r_sub.

Tactic Notation "r_sub_cases" tactic(first) tactic(c) :=
  first;
  [ c "r_refl" | c "r_trans" | c "r_and_l1" | c "r_and_l2"
  | c "r_and_r" | c "r_fun" | c "r_fun_dist"
  ].

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

Hint Constructors j_sub.

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

Hint Constructors j_sub_ocf.

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

Hint Constructors j_sub_rf.

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.
Proof. reflexivity. Qed.

Example conj_A_B_C_D : forall A B C D,
  Conj [A, B, C] D = A & B & C & D.
Proof. reflexivity. Qed.

(* To rewrite an expression. *)
Proposition Conj_one_step: forall A Gamma At,
  Conj (A::Gamma) At = A & Conj Gamma At.
Proof. reflexivity. Qed.

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

Example conj_right_A : forall A,
  Conj_right A empty = A.
Proof. reflexivity. Qed.

Example conj_right_A_B_C_D : forall A B C D,
  Conj_right A [B, C, D] = ((A & B) & C) & D.
Proof. reflexivity. Qed.

(* To rewrite an expression. *)
Proposition Conj_right_one_step: forall A Gamma Ah,
  Conj_right Ah (A::Gamma) = Conj_right (Ah & A) Gamma.
Proof. reflexivity. Qed.

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.
Proof. reflexivity. Qed.

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

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

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.
Proof.
  intros.
  constructor; eauto.
Qed.

Lemma sub_weakening_right: forall A B C,
  A =< B ->
  C & A =< C & B.
Proof.
  intros.
  constructor; eauto.
Qed.

Hint Resolve sub_weakening_left sub_weakening_right.

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.
Proof.
  induction Sigma as [| b Sigma']; intros; simpl; auto.
Qed.

Lemma sub_conj: forall A A' B B',
  A =< A' ->
  B =< B' ->
  A & B =< A' & B'.
Proof.
  intros. eauto.
Qed.

Hint Resolve sub_conj.

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).
Proof.
  intros.
  constructor; auto.
    constructor 2 with (A & B); constructor.
Qed.

Lemma r_sub_assoc_right: forall A B C,
  A & (B & C) =< (A & B) & C.
Proof.
  intros.
  constructor; auto.
    constructor 2 with (B & C); constructor.
Qed.

Ltac switch_assoc :=
  match goal with
  | |- (?A & ?B) & ?C =< _ => constructor 2 with (A & (B & C)); [apply r_sub_assoc_left | ]
  | |- ?A & (?B & ?C) =< _ => constructor 2 with ((A & B) & C); [apply r_sub_assoc_right | ]
  | _ => fail "No match goal"
  end.

Ltac switch_assoc_right :=
  match goal with
  | |- _ =< (?A & ?B) & ?C => constructor 2 with (A & (B & C)); [| apply r_sub_assoc_right]
  | |- _ =< ?A & (?B & ?C) => constructor 2 with ((A & B) & C); [| apply r_sub_assoc_left]
  | _ => fail "No match goal"
  end.

Lemma Conj_right_assoc: forall Sigma1 Sigma2 A B1 B2,
  Conj_right A (Sigma1 ++ (B1 & B2) :: Sigma2) =< Conj_right A (Sigma1 ++ B1 :: B2 :: Sigma2).
Proof.
  induction Sigma1; simpl; intros; auto.
  Case "Sigma1 = nil".
  apply Conj_right_sub.
  switch_assoc. auto.
Qed.

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.
Proof.
  induction Gamma as [| B Gamma']; intros; auto.
  Case "Gamma = B :: Gamma'".
  simpl.
  constructor 2 with (Conj Gamma' (A & B)); [apply IHGamma' | ].
    clear IHGamma'.
    generalize dependent A.
    generalize dependent B.
    induction Gamma' as [| C Gamma'']; intros; simpl; auto.
    constructor 2 with (C & (B & (Conj Gamma'' A))); auto.
      constructor 2 with ((C & B) & (Conj Gamma'' A)); [apply r_sub_assoc_right | ].
        constructor 2 with ((B & C) & (Conj Gamma'' A)); [auto | apply r_sub_assoc_left].
Qed.

Lemma Conj_Conj_right: forall Gamma A,
  Conj Gamma A =< Conj_right A Gamma.
Proof.
  induction Gamma as [| B Gamma']; intros; auto.
  Case "Gamma = B :: Gamma'".
  simpl.
  constructor 2 with (Conj Gamma' (A & B)); [| apply IHGamma'].
    clear IHGamma'.
    generalize dependent A.
    generalize dependent B.
    induction Gamma' as [| C Gamma'']; intros; simpl; auto.
    simpl.
    constructor 2 with (C & (B & (Conj Gamma'' A))); auto.
      constructor 2 with ((B & C) & (Conj Gamma'' A)); [apply r_sub_assoc_right | ].
        constructor 2 with ((C & B) & (Conj Gamma'' A)); [auto | apply r_sub_assoc_left].
Qed.

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).
Proof.
  induction Bs as [| B' Bs'].
  Case "Bs = nil".
  unfold fun_dist; simpl. constructor.
  Case "Bs = B'::Bs'".
  simpl. apply r_trans with ((A --> B') & (A --> Conj Bs' B)); auto.
    rewrite fun_dist_one_step. auto.
Qed.

Hint Resolve fun_dist_extend.

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.
Proof.
  intros.
  apply r_trans with (B1 --> Conj (sndtypList XYs) Y); auto.
  apply r_trans with (fun_dist B1 (sndtypList XYs) Y); auto.
  clear H.
  generalize dependent X.
  generalize dependent Y.
  induction XYs as [| (X', Y') XYs']; intros.
  Case "XYs = nil".
  unfold sndtypList, fsttypList, fun_dist in *.
  simpl in *; auto.
  Case "XYs = (X', Y') :: XYs'".
  simpl in H1.
  simpl. rewrite fun_dist_one_step; auto.
Qed.

Permutation (Commutativity)


Lemma Conj_swap: forall t1 t2 A B,
  Conj (t1 ++ B :: t2) A =< Conj (t1 ++ A ::t2) B.
Proof.
  induction t1; intros; simpl; auto.
  induction t2; simpl; auto.
  constructor 2 with (a & B & (Conj t2 A)).
    switch_assoc.
    switch_assoc_right.
    auto.
  constructor 2 with (a & A & (Conj t2 B)); [auto | ].
    switch_assoc.
    switch_assoc_right.
    auto.
Qed.

(* Special case : t1 is nil *)
Hint Extern 1 (r_sub (Conj (?A::?C) ?B) (Conj (?B::_) ?A)) =>
  rewrite <- app_nil_l with _ (A::C); apply Conj_swap.

Lemma Conj_swap_in: forall l1 l2 A B,
  Conj (A :: l1 ++ l2) B =< Conj (l1 ++ A :: l2) B.
Proof.
  induction l1 as [| C l1']; simpl; intros; auto.
  constructor 2 with (C & (Conj (A::l1' ++ l2) B)); auto.
  simpl.
  switch_assoc.
  switch_assoc_right.
  apply sub_weakening_left; auto.
Qed.

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.
Proof.
  intros.
  constructor 2 with (Conj l A); auto. clear H0.
  induction H; simpl; intros; auto.
  Case "nil".
  destruct l2; [simpl; auto |].
  constructor 2 with (Conj (A::l2) t); [|simpl]; auto.
  Case "extendSubseq".
  constructor 2 with (Conj l2 A); auto.
Qed.

Lemmas for the judgmental subtyping system


The context must not be empty.


Lemma context_is_not_nil: forall A,
  ~ (empty ~< A).
Proof.
  induction A; intro; inversion H;
  match goal with
  | H: _ ++ _ :: _ = empty |- _ => symmetry in H; contradict H; apply app_cons_not_nil
  | _ => auto
  end.
  inv H2; auto.
Qed.

General ver. of the rule j_refl


Lemma pickFun_app: forall l1 l2,
  pickFun(l1 ++ l2) = pickFun l1 ++ pickFun l2.
Proof.
  induction l1 as [| b l1']; intros; [ reflexivity | destruct b; simpl; f_equal; auto].
Qed.

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.
Proof.
  (typ_cases (induction A) Case); intros; auto.
  Case "typ_arrow".
  constructor 4 with [(A1,A2)]; simpl.
    SCase "subseq".
    rewrite pickFun_app; simpl; auto with v62.
    SCase "arg types".
    intros. destruct H; [subst t; rewrite <- app_nil_l with (l:=[A1]); apply IHA1 | inversion H].
    SCase "result types".
    rewrite <- app_nil_l with (l:=[A2]); apply IHA2.
  Case "typ_conj".
  repeat constructor.
  apply IHA1.
  replace (Sigma ++ A1 :: A2 :: Sigma') with ((Sigma ++ [A1]) ++ A2 :: Sigma').
  apply IHA2.
    rewrite <- app_assoc.
    reflexivity.
Qed.

Hint Resolve j_refl_gen.

(* Hint for a case when context is a singleton *)
Hint Extern 1 (j_sub (?A::nil) ?A) =>
  rewrite <- app_nil_l with _ [A]; apply j_refl_gen.

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').
Proof.
  induction 1.
  Case "empty".
  auto.
  Case "x::l".
  destruct x; simpl; auto using perm_skip.
  Case "y::x::l".
  destruct x, y; simpl; auto using perm_skip, perm_swap.
  Case "trans".
  eauto using perm_trans.
Qed.

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'.
Proof.
  intros Funs Sigma Sigma' Hsubseq Hperm.
  generalize dependent Funs.
  induction Hperm; intros.
  Case "Perm_nil". inversion Hsubseq; subst; exists []; auto.
  Case "perm_skip".
  inversion Hsubseq; subst.
    exists []; auto.
    destruct (IHHperm _ H1) as [Funs' [? ?]]. exists Funs'; auto.
    destruct (IHHperm _ H1) as [Funs' [? ?]]. exists (x::Funs'); auto.
  Case "perm_swap".
  inversion Hsubseq; subst.
    exists []; auto.
    inversion H1; subst.
      exists []; auto.
      exists Funs; auto.
      exists (x::l1); auto.
    inversion H1; subst.
      exists [y]; auto.
      exists (y::l1); auto.
      exists (x::y::l0); auto using perm_swap.
  Case "perm_trans".
  destruct (IHHperm1 _ Hsubseq) as [Funs' [? HFuns']].
  destruct (IHHperm2 _ HFuns') as [Funs'' [? ?]].
  exists Funs''; eauto using perm_trans.
Qed.

This is the main lemma.
Lemma permute_j_sub : forall (Sigma Sigma':env) (A:typ),
  Sigma ~< A ->
  Permutation Sigma Sigma' ->
  Sigma' ~< A.
Proof.
  intros Sigma Sigma' A H.
  generalize dependent Sigma'.
  (j_sub_cases (induction H) Case); intros.
  Case "j_refl".
  destruct_permute H. constructor.
  Case "j_and_l".
  destruct_permute H0.
  constructor.
    apply IHj_sub. do 2 apply permute_app_middle; assumption.
  Case "j_and_r".
  constructor; auto.
  Case "j_fun".
  apply permute_pickFun in H3.
  destruct (permute_pickFun_exists H H3) as [Sigma'' [HPerm Hsubseq]].
  constructor 4 with Sigma''; auto.
    SCase "arg types".
    intros. apply H1; auto. revert H4. apply Permutation_in. apply Permutation_map. apply Permutation_sym. assumption.
    SCase "result types".
    apply IHj_sub. apply Permutation_map. assumption.
Qed.

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.
Proof.
  (j_sub_cases (induction 1) Case); intros.
  Case "j_refl".
  rewrite app_comm_cons. constructor.
  Case "j_and_l".
  rewrite app_comm_cons. constructor; auto.
  Case "j_and_r".
  constructor; auto.
  Case "j_fun".
  constructor 4 with Sigma'; auto.
  destruct C; simpl; auto.
Qed.

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.
Proof.
  intros.
  apply permute_j_sub with (C::Sigma ++ Sigma').
    apply weakening_cons; assumption.
    apply Permutation_cons_app.
      apply Permutation_refl.
Qed.

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.
Proof.
  intros Sigma A B C H.
  remember ((A & B)::Sigma) as Sigma'.
  generalize dependent A.
  generalize dependent B.
  generalize dependent Sigma.
  (j_sub_cases (induction H) Case); intros; subst; auto.
  Case "j_refl".
  destruct Sigma1 as [| p Sigma1'].
    SCase "(A & B) was focused".
    inv HeqSigma'.
    SCase "(A & B) was not focused".
    inv HeqSigma'.
    do 2 rewrite app_comm_cons. constructor.
  Case "j_and_l".
  destruct Sigma1 as [| p Sigma1'].
    SCase "(A & B) was focused".
    simpl in *.
    inv HeqSigma'; assumption.
    SCase "(A & B) was not focused".
    simpl in HeqSigma'. inv HeqSigma'.
    do 2 rewrite app_comm_cons.
    constructor.
      simpl. apply IHj_sub. reflexivity.
  Case "j_fun".
  constructor 4 with Sigma'; auto.
  simpl in H.
  destruct A, B; simpl; auto.
Qed.

Lemma j_and_l_inv: forall Sigma Sigma' A B C,
  Sigma ++ (A & B) :: Sigma' ~< C ->
  Sigma ++ A :: B :: Sigma' ~< C.
Proof.
  intros.
  apply permute_j_sub with (A :: B :: Sigma ++ Sigma').
  apply j_and_l_inv_cons.
  apply permute_j_sub with (Sigma ++ (A & B) :: Sigma'); [assumption |].
    apply Permutation_sym.
    apply Permutation_cons_app.
    apply Permutation_refl.
    do 2 apply Permutation_cons_app.
    apply Permutation_refl.
Qed.

Rewriting lemmas


Lemma in_weakening : forall (A:Type) (l1 l2:list A) (x y:A),
  In x (l1 ++ l2) ->
  In x (l1 ++ y :: l2).
Proof.
  intros.
  apply in_app_iff.
  destruct (in_app_or _ _ _ H); auto with v62.
Qed.

Hint Resolve in_weakening : database v62.

Lemma fsttypList_app : forall l1 l2,
  fsttypList (l1 ++ l2) = fsttypList l1 ++ fsttypList l2.
Proof.
  apply map_app.
Qed.

Lemma sndtypList_app: forall l1 l2,
  sndtypList (l1 ++ l2) = sndtypList l1 ++ sndtypList l2.
Proof.
  apply map_app.
Qed.

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.

(* Induction hypothesis on the size of type C. *)
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.
Proof.
  intros C Sigma A IHtyp IHcc.
  remember (C::C::Sigma) as Sigma'.
  generalize dependent Sigma.
  (j_sub_cases (induction IHcc) Case); intros; auto.
  Case "j_refl".
  destruct Sigma1 as [| b' Sigma1''].
    SCase "The first C was focused".
    inv HeqSigma'.
    rewrite <- app_nil_l with _ (typ_base b::Sigma). constructor.
    SCase "C was not focused / Both C were not focused".
    inv HeqSigma'.
    constructor.
  Case "j_and_l".
  destruct Sigma1 as [| b Sigma1']; simpl in HeqSigma'.
    SCase "The first C was focused".
    inversion HeqSigma'. subst C.
    rewrite <- app_nil_l with typ ((t1 & t2)::Sigma). constructor. simpl.
      apply IHtyp; simpl; auto with arith.
      apply permute_j_sub with (t2::t1::t1::Sigma); perm_refl.
      apply IHtyp; simpl; auto with arith.
      apply permute_j_sub with (t1::t2::t1::t2::Sigma); perm_refl.
      simpl in IHcc. subst Sigma2.
      replace (t1::t2::t1::t2::Sigma) with ((t1::t2::nil)++(t1::t2::Sigma)) by auto with v62.
      replace (t1::t2::(t1&t2)::Sigma) with ((t1::t2::nil)++(t1&t2)::Sigma) in IHcc by auto with v62.
      apply j_and_l_inv; auto.
    inversion HeqSigma'. subst b.
    destruct Sigma1' as [| b' Sigma1''].
    SCase "The second C was focused".
    inversion H1; clear H1; subst.
    constructor.
      apply IHtyp; simpl; auto with arith.
      apply permute_j_sub with ((t2::t1::nil)++t1::Sigma); perm_refl.
      apply IHtyp; simpl; auto with arith.
      apply permute_j_sub with ((t1::t2::t1::empty)++t2::Sigma); perm_refl.
      simpl. apply j_and_l_inv_cons; assumption.
    SCase "Cs were not focused".
    inversion H1. subst b'.
    constructor. simpl. apply IHIHcc. reflexivity.
  Case "j_fun".
  clear H1 IHIHcc.
  subst Sigma.
  destruct C;
    (* C is not function type *)
    try solve [(simpl in H; constructor 4 with Sigma'; auto)].
  (* C is function type *)
  simpl in H.
  inv H.
    SCase "No type was selected.(contradict)".
    contradict IHcc; apply context_is_not_nil.
    SCase "The first C was not selected".
    inv H3.
      SSCase "No type was selected.(contradict)".
      contradict IHcc; apply context_is_not_nil.
      SSCase "The second C was not selected".
      constructor 4 with Sigma'; simpl; auto.
      SSCase "The second C was selected".
      constructor 4 with ((C1,C2)::l1); simpl; auto.
    SCase "The first C was selected".
    inv H3.
      SSCase "No more type was selected.".
      constructor 4 with ([(C1,C2)]); simpl; auto.
      SSCase "The second C was not selected".
      constructor 4 with ((C1,C2)::l1); simpl; auto.
      SSCase "The second C was selected.".
      constructor 4 with ((C1,C2)::l0); simpl in *; auto.
      apply IHtyp; auto with arith.
Qed.

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.
Proof.
  induction n as [| n'].
    intros. inversion H.
    intros. apply contraction_cons_aux; auto.
      unfold contraction_IH_on_typ. intros. apply IHn'; eauto with arith.
Qed.

This is the main lemma.
Lemma contraction_cons: forall C Sigma A,
  C::C::Sigma ~< A ->
  C::Sigma ~< A.
Proof.
  intros. apply contraction_cons_aux_typ with (S (size_typ C)); auto.
Qed.

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.
Proof.
  intros.
  apply permute_j_sub with (C::Sigma ++ Sigma'); perm_refl.
  apply contraction_cons.
  apply permute_j_sub with (Sigma ++ C :: C :: Sigma'); [assumption | perm_refl].
Qed.

Lemma contraction_bunch_cons: forall Sigma Sigma' A,
  Sigma ++ Sigma ++ Sigma' ~< A ->
  Sigma ++ Sigma' ~< A.
Proof.
  induction Sigma as [| b Sigma']; intros; auto.
  Case "Sigma = b :: Sigma'".
  simpl.
  apply contraction_cons.
  apply permute_j_sub with (Sigma' ++ b :: b :: Sigma'0); perm_refl.
  apply IHSigma'.
  apply (permute_j_sub H); perm_refl.
Qed.

Lemma contraction_bunch: forall Sigma A,
  Sigma ++ Sigma ~< A ->
  Sigma ~< A.
Proof.
  intros.
  rewrite <- app_nil_r with _ Sigma.
  apply contraction_bunch_cons with (Sigma' := nil).
  rewrite app_nil_r.
  assumption.
Qed.

Other lemmas


Lemma pickFun_in: forall (t1 t2:typ) L,
  In (t1,t2) (pickFun L) ->
  In (t1-->t2) L.
Proof.
  induction L as [| b L']; intros.
  simpl in H. inversion H.
  destruct b; simpl in *; intuition.
  inversion H0; left; f_equal; assumption.
Qed.

Lemma subseq_makeFunList_pickFun: forall l,
  subseq (makeFunList (pickFun l)) l.
Proof.
  induction l as [| b l'].
  simpl; auto.
  destruct b; simpl makeFunList; auto.
Qed.

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.
Proof.
  intros; (typ_cases (destruct A) Case); inv H0; inv H1.
  Case "typ_base".
  rewrite <- app_assoc.
  rewrite <- app_comm_cons.
  constructor.
  Case "typ_arrow".
  constructor 4 with (Sigma'0 ++ Sigma'1 ++ Sigma'2).
    SCase "subseq".
    repeat (rewrite pickFun_app; apply subseq_app; try assumption).
    SCase "arg types".
    repeat rewrite fsttypList_app in *; simpl in H10.
    intros.
    apply in_app_or in H0.
    destruct H0; auto with v62.
    rewrite <- app_nil_r with _ [t1'].
    apply H with A1; simpl; auto with arith v62.
    SCase "result types".
    repeat rewrite sndtypList_app in *; simpl in H12.
    apply H with A2; simpl; auto with arith.
    apply (permute_j_sub H12); perm_refl.
  Case "typ_conj".
  apply permute_j_sub with _ (A1::Sigma1 ++ A2 :: Sigma2) _ in H4; perm_refl.
  unfold j_cut_ind_on_typ in H.
  assert (size_typ A1 < size_typ (A1 & A2)) by (simpl; auto with arith).
  assert (size_typ A2 < size_typ (A1 & A2)) by (simpl; auto with arith).
  pose proof (H _ _ _ _ H0 H5 H4).
  apply permute_j_sub with _ (A2::Sigma ++ Sigma1 ++ Sigma2) _ in H2; perm_refl.
  pose proof (H _ _ _ _ H1 H6 H2).
  apply contraction_bunch_cons; assumption.
Qed.

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.
Proof.
  intros Sigma Sigma' A C Htyp Hd He.
  remember (A::Sigma') as ASigma'.
  generalize dependent A.
  generalize dependent Sigma'.
  generalize dependent Sigma.
  (j_sub_cases (induction He) Case); intros;
    (* the derivation was a right rule, solved by IH *)
    eauto;
    (* When A is a principal type, solved by lemma 1 *)
    try (destruct Sigma1 as [| B Sigma1']; inv HeqASigma';
      [ eauto using j_cut_cons_lemma1
      | rewrite app_assoc; auto]).
  Case "j_and_l".
  constructor; rewrite <- app_assoc; eauto.
  Case "j_fun".
  (* A is not function type. *)
  subst Sigma; destruct A; simpl in H;
    try solve [(constructor 4 with Sigma'; auto;
                rewrite pickFun_app; auto with v62)].
  inv H.
  SCase "No type is selected".
  contradict He; apply context_is_not_nil.
  SCase "A is not selected".
    constructor 4 with Sigma'; auto.
    rewrite pickFun_app; auto with v62.
  SCase "A is selected".
    apply j_cut_cons_lemma1 with (A1 --> A2); auto.
    constructor 3 with nil Sigma'0 nil l1; simpl; auto.
Qed.

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.
Proof.
  (j_sub_cases (induction 2) Case); intros; eauto using j_cut_cons_lemma2.
  Case "j_and_l".
  rewrite <- app_assoc.
  rewrite <- app_comm_cons.
  constructor.
  repeat rewrite app_comm_cons.
  rewrite app_assoc.
  auto.
Qed.

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.
Proof.
  induction k; intros; [inversion H|].
    apply j_cut_cons_lemma3 with A; auto.
      unfold j_cut_ind_on_typ. intros; apply IHk with A'; eauto with arith.
Qed.

This is the main theorem.
Theorem j_cut_cons: forall Sigma Sigma' A C,
  Sigma ~< A ->
  A :: Sigma' ~< C ->
  Sigma ++ Sigma' ~< C.
Proof.
  intros. apply j_cut_cons_aux with (S (size_typ A)) A; auto.
Qed.

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.
Proof.
  intros A B H.
  rewrite <- app_nil_l with _ [A].
  (r_sub_cases (induction H) Case); auto.
  Case "r_trans".
  simpl in *.
  rewrite <- app_nil_r with _ empty.
  rewrite app_comm_cons.
  apply j_cut_cons with t2; auto.
  Case "r_and_l2".
  constructor.
  replace (empty ++ [t1,t2]) with ([t1] ++ t2 :: empty) by reflexivity. auto.
  Case "r_fun".
  constructor 4 with ([(t1,t2)]); simpl; auto.
    intros; destruct H1; subst; intuition.
  Case "r_fun_dist".
  constructor.
  constructor 4 with ([(t1,t2), (t1,t3)]); simpl; intuition; subst; auto.
    SCase "result types".
    constructor.
      rewrite <- app_nil_l with (l := [t2,t3]); auto.
      replace [t2,t3] with ([t2] ++ t3::empty) by reflexivity; auto.
Qed.

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.
Proof.
  intros Sigma A C H.
  remember (A::Sigma) as Sigma'.
  generalize dependent A.
  generalize dependent Sigma.
  (j_sub_cases (induction H) Case); intros; auto.
  Case "j_refl".
  constructor 2 with (Conj Sigma A); [apply Conj_right_Conj |].
  destruct Sigma1 as [| t' Sigma1'].
    SCase "C was focused".
    inv HeqSigma'.
    induction Sigma as [|B Sigma']; simpl; auto.
    constructor 2 with (Conj Sigma' (typ_base b)); auto.
    SCase "C was not focused".
    inv HeqSigma'.
    induction Sigma1' as [|B Sigma1'']; simpl; auto.
    constructor 2 with (Conj (Sigma1'' ++ typ_base b :: Sigma2) A); auto.
  Case "j_and_l".
  destruct Sigma1 as [| b Sigma1'].
    SCase "A was focused".
    inv HeqSigma'.
    rewrite <- Conj_right_one_step; auto.
    SCase "A was not focused".
    inv HeqSigma'.
    constructor 2 with (Conj_right A (Sigma1' ++ t1::t2::Sigma2)); [apply Conj_right_assoc | auto].
  Case "j_fun".
  destruct Sigma' as [| (b1,b2) Sigma''];
    [ simpl in H2; contradict H2; apply context_is_not_nil | ].
  clear H0 H2.
  assert (Conj (makeFunList Sigma'') (b1 --> b2) =< t1' --> t2').
    SSCase "Proof of assertion".
    apply fun_dist_gen; auto.
      constructor 2 with (Conj_right b2 (sndtypList Sigma'')); [apply Conj_Conj_right | auto].
      replace t1' with (Conj_right t1' empty) by reflexivity. apply H1; simpl; auto.
      intros. replace t1' with (Conj_right t1' empty) by reflexivity. apply H1; simpl; auto.
  constructor 2 with (Conj Sigma0 A); [apply Conj_right_Conj |].
  subst Sigma.
  destruct (typ_dec A (b1 --> b2)).
    SCase "A = b1 --> b2".
    subst A.
    simpl in H.
    apply extendSubseq_inv in H.
    apply Conj_subseq_weakening with (makeFunList Sigma''); auto.
    apply subseq_tran with (makeFunList (pickFun Sigma0)).
      unfold makeFunList; auto with v62.
      apply subseq_makeFunList_pickFun.
    SCase "A <> b1 --> b2".
    assert (subseq ((b1, b2) :: Sigma'') (pickFun Sigma0)).
      SSCase "Proof of assertion".
      destruct A; simpl in H; try assumption.
      apply extraSubseq_inv with (A1,A2); auto.
        intuition. inversion H2. apply n; f_equal; auto.
    assert (Conj (makeFunList ((b1, b2)::Sigma'')) (A) =< t1' --> t2').
      SSCase "Proof of assertion".
      constructor 2 with (Conj (A :: makeFunList Sigma'') (b1-->b2)).
        simpl makeFunList; auto.
        simpl. constructor 2 with (Conj (makeFunList Sigma'') (b1-->b2)); auto.
    apply Conj_subseq_weakening with (makeFunList ((b1,b2)::Sigma'')); auto.
    apply subseq_tran with (makeFunList (pickFun Sigma0)).
      unfold makeFunList; auto with v62.
      apply subseq_makeFunList_pickFun.
Qed.

This page has been generated by coqdoc