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

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

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

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

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

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

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

Hint Constructors r_sub.

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

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.

Combined Scheme j_sub_j_sub_p_mutind from j_sub_ind2, j_sub_p_ind2.

Hint Constructors j_sub j_sub_p.

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

Hint Constructors j_sub_mcf j_sub_p_mcf.

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

Hint Constructors j_sub_ocf j_sub_p_ocf.

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

Hint Constructors j_sub_rf.

Other auxiliary functions


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

Conj family

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

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



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

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


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

Example conj_id_A : forall A,
  Conj empty A = A.
Proof. reflexivity. Qed.

Example conj_id_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_id_A : forall A,
  Conj_right A empty = A.
Proof. reflexivity. Qed.

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

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

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

(* To rewrite an expression. *)
Proposition box_Conj_one_step: forall A Gamma At,
  box_Conj (A::Gamma) At = ([] A) & box_Conj Gamma At.
Proof. reflexivity. Qed.

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

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

(* To rewrite an expression. *)
Proposition box_Conj_right_one_step: forall A Gamma Ah,
  box_Conj_right Ah (A::Gamma) = box_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 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.
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.

Hint Resolve Conj_right_sub.

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.

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).
Proof.
  unfold box_Conj_right;
  induction Sigma1; simpl; intros; auto.
  Case "Sigma1 = nil".
  apply Conj_right_sub.
  constructor 2 with (A & ([]B1) & ([] B2)); auto.
  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.

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.

Hint Immediate Conj_Conj_right Conj_right_Conj.

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_right_swap: forall t1 t2 A B,
  Conj_right A (t1 ++ B :: t2) =< Conj_right B (t1 ++ A ::t2).
Proof.
  intros.
  switch_left; switch_right; apply Conj_swap.
Qed.

Hint Immediate Conj_right_swap.

Hint Extern 1 (r_sub (Conj_right ?B (?A::?C)) (Conj_right ?A (?B::_))) =>
  rewrite <- app_nil_l with _ (A::C); apply Conj_right_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.

Hint Immediate Conj_swap_in.

Lemma Conj_right_swap_in: forall l1 l2 A B,
  Conj_right B (A :: l1 ++ l2) =< Conj_right B (l1 ++ A :: l2).
Proof.
  intros.
  switch_left; switch_right; apply Conj_swap_in.
Qed.

Hint Immediate Conj_right_swap_in.

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

Hint Immediate Conj_swap_in_conv.

Lemma Conj_right_swap_in_conv: forall l1 l2 A B,
  Conj_right B (l1 ++ A :: l2) =< Conj_right B (A :: l1 ++ l2).
Proof.
  intros.
  switch_left; switch_right; apply Conj_swap_in_conv.
Qed.

Hint Immediate Conj_right_swap_in_conv.

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

Lemma Conj_and : forall l A B,
  A =< B ->
  Conj l A =< B.
Proof.
  intros.
  induction l; simpl; auto.
  constructor 2 with (Conj l A); auto.
Qed.

Hint Resolve Conj_and.

Lemma Conj_right_and: forall l A B,
  A =< B ->
  Conj_right A l =< B.
Proof.
  intros; switch_left; auto.
Qed.

Hint Resolve Conj_right_and.

Lemma Conj_sub_middle: forall t1 t2 A B C,
  B =< C ->
  Conj (t1 ++ B :: t2) A =< C.
Proof.
  intros.
  constructor 2 with (Conj (t1++A::t2) B); [ apply Conj_swap | auto].
Qed.

Hint Resolve Conj_sub_middle.

Lemma Conj_right_sub_middle: forall t1 t2 A B C,
  B =< C ->
  Conj_right A (t1 ++ B :: t2) =< C.
Proof.
  intros; switch_left; auto.
Qed.

Hint Resolve Conj_right_sub_middle.

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).
Proof.
  intros.
  constructor 2 with (Conj_right B (G1++A::G2)); [apply Conj_right_swap |].
  constructor 2 with (Conj_right C (G1++A::G2)); [| apply Conj_right_swap]; auto.
Qed.

Hint Resolve Conj_right_middle_subst.

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.
Proof.
  intros.
  switch_left. simpl; auto.
Qed.

Lemma Conj_right_push_in: forall l A B,
  B & Conj_right A l =< Conj_right A (B :: l).
Proof.
  intros.
  switch_right; simpl; auto.
Qed.

Hint Immediate Conj_right_pop_out Conj_right_push_in.

Lemma Conj_split: forall G1 G2 A B,
  Conj G1 A & Conj G2 B =< Conj (G1++A::G2) B.
Proof.
  induction G1; intros; auto.
  simpl. switch_assoc. apply sub_weakening_right; auto.
Qed.

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).
Proof.
  induction l; intros; simpl; auto.
  constructor 2 with (Conj_right ([](A & a)) (map typ_box l)); auto.
  constructor 2 with ([] Conj_right ([](A & a)) (map typ_box l)); auto.
Qed.

Hint Immediate Conj_right_box_k.

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.
Proof.
  induction l; intros; auto.
  simpl. constructor 2 with (a & Conj (map typ_box l) A); auto.
Qed.

Hint Immediate Conj_sub_box_T.

Lemmas for the judgmental subtyping system


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.

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.

Not all contexts are empty


Lemma context_is_not_nil: forall A,
  ~ (empty ; empty ~< A) /\ ~ (empty ; empty %< A).
Proof.
  (typ_cases (induction A) Case); split; intro; inversion H; inversion H0; repeat
  match goal with
  | H: _ ++ _ :: _ = empty |- _ => symmetry in H; contradict H; apply app_cons_not_nil
  | H: subseq _ nil |- _ => inv H
  | _ => simpl in *; try intuition; auto
  end.
Qed.

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

Hint Extern 1 (j_sub _ (_ ++ ?A :: _) ?A) => apply j_refl_gen.
Hint Extern 1 (j_sub (_ ++ ?A :: _) _ ?A) => apply 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.

Hint Extern 1 (j_sub (?A::nil) _ ?A) =>
  rewrite <- app_nil_l with _ [A]; apply j_refl_gen.

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

Hint Resolve (@permute_app_middle typ).

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 nil; auto.
  Case "perm_skip".
  inversion Hsubseq; subst.
    exists nil; 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 nil; auto.
    inversion H1; subst.
      exists nil; 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_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).
Proof.
  (j_sub_j_sub_p_cases (apply j_sub_j_sub_p_mutind) Case); intros;
    match goal with
    | H: Permutation (_ ++ _ :: _) _ |- _ => destruct_permute H
    | _ => idtac
    end; auto.
  Case "j_fun".
  apply permute_pickFun in H4.
  apply permute_pickFun in H5.
  destruct (permute_pickFun_exists H (Permutation_app H4 H5)) as [Sigma'' [HPerm Hsubseq]].
  constructor 4 with Sigma''; auto.
    SCase "arg types".
    intros. apply H1; auto. revert H6. apply Permutation_in. apply Permutation_map. apply Permutation_sym. assumption.
    SCase "result types".
    apply H3; auto. apply Permutation_map; assumption.
  Case "j_box_l".
  constructor 8 with nil Gamma'; auto.
  Case "j_box_lp".
  constructor 5 with nil Gamma'; auto.
Qed.

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).
Proof.
  (j_sub_j_sub_p_cases (apply j_sub_j_sub_p_mutind) Case); intros; (split; [SCase "Sigma" | SCase "Gamma"]);
    try rewrite app_comm_cons; try solve [(try constructor; firstorder)].
  Case "j_fun".
    SCase "Sigma".
    constructor 4 with Sigma'; auto.
      apply (subseq_tran H); destruct C; simpl; auto with v62.
    SCase "Gamma".
    constructor 4 with Sigma'; auto.
      apply (subseq_tran H); destruct C; simpl; auto with v62.
  Case "j_box_l".
    SCase "Sigma".
    constructor 8 with Gamma1 Gamma2; subst; firstorder.
    SCase "Gamma".
    constructor 8 with (C::Gamma1) Gamma2; subst; firstorder.
  Case "j_box_lp".
    SCase "Sigma".
    constructor 5 with Gamma1 Gamma2; subst; firstorder.
    SCase "Gamma".
    constructor 5 with (C::Gamma1) Gamma2; subst; firstorder.
Qed.

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).
Proof.
  intros; split; intro;
  [ destruct ((proj1 weakening_cons_j_sub_j_sub_p) _ _ _ H C)
  | destruct ((proj2 weakening_cons_j_sub_j_sub_p) _ _ _ H C)];
  split;
  [ apply permute_j_sub with (Gamma ++ Gamma') (C::Sigma++Sigma')
  | apply permute_j_sub with (C::Gamma ++ Gamma') (Sigma ++ Sigma')
  | apply permute_j_sub_p with (Gamma ++ Gamma') (C::Sigma ++ Sigma')
  | apply permute_j_sub_p with (C::Gamma ++ Gamma') (Sigma ++ Sigma')
  ]; auto; perm_refl.
Qed.

Lemma weakening_gen_j_sub: forall (Gamma Sigma Sigma' : env) (A C : typ),
  Gamma; Sigma ++ Sigma' ~< A ->
  Gamma; Sigma ++ C :: Sigma' ~< A.
Proof.
  intros.
  rewrite <- app_nil_l with _ Gamma.
  apply weakening_gen_j_sub_j_sub_p; auto.
Qed.

Lemma weakening_gen_j_sub_v: forall (Gamma Gamma' Sigma : env) (A C : typ),
  Gamma ++ Gamma'; Sigma ~< A ->
  Gamma ++ C :: Gamma'; Sigma ~< A.
Proof.
  intros.
  rewrite <- app_nil_l with _ Sigma.
  apply weakening_gen_j_sub_j_sub_p; auto.
Qed.

Lemma weakening_gen_j_sub_p: forall (Gamma Sigma Sigma' : env) (A C : typ),
  Gamma; Sigma ++ Sigma' %< A ->
  Gamma; Sigma ++ C :: Sigma' %< A.
Proof.
  intros.
  rewrite <- app_nil_l with _ Gamma.
  apply weakening_gen_j_sub_j_sub_p; auto.
Qed.

Lemma weakening_gen_j_sub_vp: forall (Gamma Gamma' Sigma : env) (A C : typ),
  Gamma ++ Gamma'; Sigma %< A ->
  Gamma ++ C :: Gamma'; Sigma %< A.
Proof.
  intros.
  rewrite <- app_nil_l with _ Sigma.
  apply weakening_gen_j_sub_j_sub_p; auto.
Qed.

Hint Immediate weakening_gen_j_sub weakening_gen_j_sub_v weakening_gen_j_sub_p weakening_gen_j_sub_vp.

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

Lemma weakening_bunch_j_sub': forall (Gamma Sigma Sigma':env) (A:typ),
  Gamma; Sigma ~< A ->
  Gamma; Sigma ++ Sigma' ~< A.
Proof.
  intros. apply permute_j_sub with Gamma (Sigma' ++ Sigma); perm_refl; auto using weakening_bunch_j_sub.
Qed.

Hint Immediate weakening_bunch_j_sub weakening_bunch_j_sub'.

Lemma weakening_bunch_psub: forall (Gamma Sigma Sigma':env) (A:typ),
  Gamma; Sigma %< A ->
  Gamma; Sigma' ++ Sigma %< A.
Proof.
  induction Sigma' as [|b Sigma'']; intros; simpl; auto.
  apply weakening_cons_j_sub_j_sub_p; auto.
Qed.

Lemma weakening_bunch_psub': forall (Gamma Sigma Sigma':env) (A:typ),
  Gamma; Sigma %< A ->
  Gamma; Sigma ++ Sigma' %< A.
Proof.
  intros. apply permute_j_sub_p with Gamma (Sigma' ++ Sigma); perm_refl; auto using weakening_bunch_psub.
Qed.

Hint Immediate weakening_bunch_psub weakening_bunch_psub'.

Lemma weakening_bunch_j_v: forall (Gamma Gamma' Sigma:env) (A:typ),
  Gamma; Sigma ~< A ->
  Gamma' ++ Gamma; Sigma ~< A.
Proof.
  induction Gamma' as [|b Gamma'']; intros; simpl; auto.
  apply weakening_cons_j_sub_j_sub_p; auto.
Qed.

Lemma weakening_bunch_j_v': forall (Gamma Gamma' Sigma:env) (A:typ),
  Gamma; Sigma ~< A ->
  Gamma ++ Gamma'; Sigma ~< A.
Proof.
  intros. apply permute_j_sub with (Gamma' ++ Gamma) Sigma; perm_refl; auto using weakening_bunch_j_v.
Qed.

Hint Immediate weakening_bunch_j_v weakening_bunch_j_v'.

Lemma weakening_bunch_psub_v: forall (Gamma Gamma' Sigma:env) (A:typ),
  Gamma; Sigma %< A ->
  Gamma' ++ Gamma; Sigma %< A.
Proof.
  induction Gamma' as [|b Gamma'']; intros; simpl; auto.
  apply weakening_cons_j_sub_j_sub_p; auto.
Qed.

Lemma weakening_bunch_psub_v': forall (Gamma Gamma' Sigma:env) (A:typ),
  Gamma; Sigma %< A ->
  Gamma ++ Gamma'; Sigma %< A.
Proof.
  intros. apply permute_j_sub_p with (Gamma' ++ Gamma) Sigma; perm_refl; auto using weakening_bunch_psub_v.
Qed.

Hint Immediate weakening_bunch_psub_v weakening_bunch_psub_v'.

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.

(* Induction hypothesis on the size of type C. *)
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).
Proof.
  intros A IHA.
  (j_sub_j_sub_p_cases (apply j_sub_j_sub_p_mutind) Case); intros; subst; simpl; auto;
  match goal with
  | H: ?G ++ _ :: _ = _ :: _ |- _ => destruct G; inv H
  | _ => idtac
  end;
  try rewrite app_comm_cons; try solve [econstructor; simpl; eauto | auto].
  Case "j_refl".
  rewrite <- app_nil_l with _ (typ_base b :: Gamma); auto.
  Case "j_and_l".
  rewrite <- app_nil_l with _ ((t1 & t2)::Gamma).
  constructor. simpl.
  apply (IHA t1) with (t1::Sigma'); simpl; auto with arith.
  apply (IHA t2) with (t2::t1::Sigma'); simpl; auto with arith.
  apply permute_j_sub with Gamma (t1::t2::Sigma'); auto; perm_refl.
  Case "j_fun".
  (* A is not function type *)
  destruct A; try solve [(constructor 4 with Sigma'; auto)].
  (* A is function type *)
  simpl in H.
  destruct (permute_pickFun_exists) with
    (Funs:=Sigma')
    (Sigma:=pickFun Gamma ++ (A1,A2)::pickFun Sigma'0)
    (Sigma':= (A1,A2)::pickFun Gamma ++ pickFun Sigma'0) as [Sigma'' [? ?]]; auto; perm_refl.
  constructor 4 with Sigma''; auto.
    SCase "arg types".
    intros. apply H0. revert H6. apply Permutation_in. apply Permutation_sym. apply Permutation_map. assumption.
    SCase "result types".
    apply (permute_j_sub H2); try apply Permutation_map; auto.
  Case "j_box_l".
    SCase "nil".
    rewrite <- app_comm_cons. rewrite <- app_nil_l with _ (([]t1) :: Gamma1 ++ Gamma2). constructor. simpl.
    apply (permute_j_sub H); auto; perm_refl.
    SCase "cons".
    constructor 8 with (A::Gamma1) Gamma2; auto.
  Case "j_box_r".
  constructor; apply weakening_cons_j_sub_j_sub_p; auto.
  Case "j_and_lp".
  rewrite <- app_nil_l with _ ((t1&t2)::Gamma).
  constructor. simpl.
  apply (IHA t1) with (t1::Sigma'); simpl; auto with arith.
  apply (IHA t2) with (t2::t1::Sigma'); simpl; auto with arith.
  apply permute_j_sub_p with Gamma (t1::t2::Sigma'); auto; perm_refl.
  Case "j_dia_lp".
    SCase "nil".
    rewrite <- app_nil_l with _ ((<>t1)::Gamma); auto.
    SCase "cons".
    constructor. apply weakening_cons_j_sub_j_sub_p; assumption.
  Case "j_dia_vp".
  constructor.
  rewrite <- app_comm_cons.
  apply weakening_cons_j_sub_j_sub_p; assumption.
  Case "j_box_lp".
    SCase "nil".
    rewrite <- app_comm_cons.
    rewrite <- app_nil_l with _ (([]t1) :: Gamma1 ++ Gamma2).
    constructor. simpl in *.
    apply (permute_j_sub_p H); perm_refl.
    SCase "cons".
    constructor 5 with (A::Gamma1) Gamma2; auto.
Qed.

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

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).
Proof.
  intros. apply move_from_sig_to_gam_cons_on_typ with (S (size_typ A)); auto.
Qed.

Hint Resolve move_from_sig_to_gam_cons.

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).
Proof.
  (j_sub_j_sub_p_cases (apply j_sub_j_sub_p_mutind) Case); intros; subst; simpl in *; auto;
  match goal with
  | H: ?G ++ _ = _ :: _ |- _ => destruct G; inv H
  | _ => idtac
  end;
  try do 2 rewrite app_comm_cons; try solve [econstructor; simpl; eauto | auto].
  Case "j_fun".
  constructor 4 with Sigma'; auto.
    apply (subseq_tran H); destruct A, B; simpl; auto with v62.
Qed.

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).
Proof.
  intros; split; intro.
  Case "lsub".
  apply permute_j_sub with Gamma (A::B::Sigma ++ Sigma'); try perm_refl.
  apply permute_j_sub with (Gamma:=Gamma) (Sigma:=Sigma ++(A&B):: Sigma') (Gamma':=Gamma) (Sigma':=(A&B)::Sigma ++ Sigma') in H; try perm_refl.
  eapply (proj1 j_and_l_p_inv_cons); eauto.
  Case "psub".
  apply permute_j_sub_p with Gamma (A::B::Sigma ++ Sigma'); try perm_refl.
  apply permute_j_sub_p with (Gamma:=Gamma) (Sigma:=Sigma ++(A&B):: Sigma') (Gamma':=Gamma) (Sigma':=(A&B)::Sigma ++ Sigma') in H; try perm_refl.
  eapply (proj2 j_and_l_p_inv_cons); eauto.
Qed.

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

Hint Resolve j_and_l_inv j_and_lp_inv.

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).
Proof.
  (j_sub_j_sub_p_cases (apply j_sub_j_sub_p_mutind) Case); intros; auto;
  repeat match goal with
  | H: Permutation (_ ++ (typ_conj ?A ?B) :: _) ((typ_conj ?A ?B) :: ?G) |- _ => idtac
  | H: Permutation (_ ++ (typ_conj ?A1 ?B1) :: _) ((typ_conj ?A2 ?B2) :: ?G) |- _ =>
    lazymatch goal with
    | H: typ_conj ?A1 ?B1 <> typ_conj ?A2 ?B2 |- _ => fail
    | _ => destruct (typ_dec (typ_conj A1 B1) (typ_conj A2 B2)) as [Htyp|Htyp]; [inversion Htyp; subst | ]
    end
  | H: Permutation (_ ++ ?A :: _) (_ :: ?G) |- _ =>
      assert (In A G) as Hin;
        [ apply Permutation_in with (x := A) in H; auto with v62; simpl in H; destruct H; [inversion H; congruence | assumption]
        | destruct_in Hin; rewrite app_comm_cons in *; apply Permutation_app_inv with (a := A) in H ]
  end;
  try rewrite app_comm_cons; try solve
    [ econstructor; simpl; eauto
    | auto
    | constructor; simpl; apply H0; rewrite app_comm_cons; auto
    | try apply (permute_j_sub_p H); try apply (permute_j_sub H); auto; apply Permutation_sym; repeat apply Permutation_cons_app; apply Permutation_cons_app_inv with (A&B); apply Permutation_sym; assumption
    ].
  Case "j_fun".
  apply permute_pickFun in H4; simpl in H4.
  pose proof (Permutation_refl (pickFun Sigma)).
  destruct (permute_pickFun_exists H (Permutation_app H4 H5)) as [Sigma'' [HPerm Hsubseq]].
  constructor 4 with Sigma''; auto.
    SCase "subseq".
    apply (subseq_tran Hsubseq). destruct A, B; simpl; auto with v62.
    SCase "arg types".
    intros. apply H0; auto. revert H6. apply Permutation_in. apply Permutation_map. apply Permutation_sym. assumption.
    SCase "result types".
    apply (permute_j_sub H2); auto. apply Permutation_map. assumption.
  Case "j_box_l".
  replace (A::B::Gamma0) with ([A, B]++Gamma0) by reflexivity.
  constructor 8 with [A, B] Gamma0; auto; simpl; apply H0.
  subst; apply Permutation_trans with (t1::(A & B)::Gamma0); [apply Permutation_sym; apply Permutation_cons_app; apply Permutation_sym; assumption | apply perm_swap].
  Case "j_box_lp".
  replace (A::B::Gamma0) with ([A,B]++Gamma0) by reflexivity.
  constructor 5 with [A, B] Gamma0; auto; simpl; apply H0.
  subst; apply Permutation_trans with (t1::(A&B)::Gamma0); [apply Permutation_sym; apply Permutation_cons_app; apply Permutation_sym; assumption | apply perm_swap].
Qed.

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).
Proof.
  (j_sub_j_sub_p_cases (apply j_sub_j_sub_p_mutind) Case); intros; auto;
  repeat match goal with
  | H: Permutation (_ ++ (typ_box ?A) :: _) ((typ_box ?A) :: ?G) |- _ => idtac
  | H: Permutation (_ ++ (typ_box ?A) :: _) ((typ_box ?B) :: ?G) |- _ =>
    lazymatch goal with
    | H: A <> B |- _ => fail
    | _ => destruct (typ_dec A B); [subst | ]
    end
  | H: Permutation (_ ++ ?A :: _) (_ :: ?G) |- _ =>
      assert (In A G) as Hin;
        [ apply Permutation_in with (x := A) in H; auto with v62; simpl in H; destruct H; [inversion H; congruence | assumption]
        | destruct_in Hin; rewrite app_comm_cons in *; apply Permutation_app_inv with (a := A) in H ]
  end;
  try rewrite app_comm_cons; try solve
    [ econstructor; simpl; eauto
    | auto
    | constructor; simpl; apply H0; rewrite app_comm_cons; auto
    | try apply (permute_j_sub_p H); try apply (permute_j_sub H); auto; apply Permutation_sym; apply Permutation_cons_app; apply Permutation_cons_app_inv with ([]A); apply Permutation_sym; assumption
    ].
  Case "j_fun".
  apply permute_pickFun in H4; simpl in H4.
  pose proof (Permutation_refl (pickFun Sigma)).
  destruct (permute_pickFun_exists H (Permutation_app H4 H5)) as [Sigma'' [HPerm Hsubseq]].
  constructor 4 with Sigma''; auto.
    SCase "subseq".
    apply (subseq_tran Hsubseq). destruct A; simpl; auto with v62.
    SCase "arg types".
    intros. apply H0; auto. revert H6. apply Permutation_in. apply Permutation_map. apply Permutation_sym. assumption.
    SCase "result types".
    apply (permute_j_sub H2); auto. apply Permutation_map. assumption.
  Case "j_box_l".
  replace (A::Gamma0) with ([A]++Gamma0) by reflexivity.
  constructor 8 with [A] Gamma0; auto; simpl; apply H0.
  subst; apply Permutation_trans with (t1::([]A)::Gamma0); [apply Permutation_sym; apply Permutation_cons_app; apply Permutation_sym; assumption | apply perm_swap].
  Case "j_box_lp".
  replace (A::Gamma0) with ([A]++Gamma0) by reflexivity.
  constructor 5 with [A] Gamma0; auto; simpl; apply H0.
  subst; apply Permutation_trans with (t1::([]A)::Gamma0); [apply Permutation_sym; apply Permutation_cons_app; apply Permutation_sym; assumption | apply perm_swap].
Qed.

Lemma j_box_v_inv: forall Gamma0 Gamma1 Sigma A C,
    Gamma0 ++ ([]A) :: Gamma1; Sigma ~< C ->
    Gamma0 ++ A :: Gamma1; Sigma ~< C.
Proof.
  intros. apply permute_j_sub with (Gamma:=A::Gamma0++Gamma1) (Sigma:=Sigma); try perm_refl.
  apply ((proj1 j_sub_v_vp_inv_cons) _ _ _ H); try perm_refl.
Qed.

The rule j_dia_r is invertible.


Lemma j_dia_r_inv: forall Gamma Sigma C,
  Gamma; Sigma ~< <>C ->
  Gamma; Sigma %< C.
Proof.
  intros.
  remember (<>C) as diaC.
  generalize dependent C.
  (j_sub_cases (induction H) Case); intros; auto; try discriminate HeqdiaC.
  Case "j_box_l".
  constructor 5 with Gamma1 Gamma2; auto.
  Case "j_dia_r".
  inversion HeqdiaC; subst; auto.
Qed.

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.

(* Induction hypothesis on the size of type C. *)
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)).
Proof.
  intros A IHA.
  (j_sub_j_sub_p_cases (apply j_sub_j_sub_p_mutind) Case); intros; (split; [SCase "vsub" | SCase "lsub"]); intros; auto;
  try match goal with
  | H: Permutation (_ ++ ?A :: _) (?B::?B::?G) |- _ =>
    destruct (typ_dec A B);
      [ SSCase "A = B"; subst; apply Permutation_sym in H; apply Permutation_cons_app_inv in H; apply Permutation_sym in H
      | SSCase "A <> B"; assert (In A G) as Hin;
        [ apply Permutation_in with (x := A) in H; auto with v62; simpl in H; destruct H; [congruence | destruct H; [congruence | assumption]]
| destruct_in Hin; repeat rewrite app_comm_cons in *; apply Permutation_app_inv with (a := A) in H]
      ]
  end;
  try rewrite app_comm_cons;
  match goal with
  | |- _; ?A::?S ~< _ => rewrite <- app_nil_l with _ (A::S)
  | |- ?A::?G; _ ~< _ => rewrite <- app_nil_l with _ (A::G)
  | |- _; ?A::?S %< _ => rewrite <- app_nil_l with _ (A::S)
  | |- ?A::?G; _ %< _ => rewrite <- app_nil_l with _ (A::G)
  | _ => idtac
  end;
  try solve
    [ constructor; firstorder
    | constructor; simpl; apply H0; repeat rewrite app_comm_cons; auto
    ].
  Case "j_and_l".
  SSCase "A = B".
  constructor. simpl.
  apply (IHA t1) with (t1::t1::t2::Sigma0); simpl; auto with arith.
  apply permute_j_sub with Gamma (t2::t1::t1::Sigma0); try perm_refl.
  apply (IHA t2) with (t2::t2::t1::t1::Sigma0); simpl; auto with arith.
  apply permute_j_sub with Gamma (t1::t2::t1::t2::Sigma0); try perm_refl.
  apply (proj1 j_and_l_p_inv_cons) with ((t1&t2)::t1::t2::Sigma0); auto.
  apply (permute_j_sub H); auto.
  replace ((t1&t2)::t1::t2::Sigma0) with ([t1&t2]++t1::t2::Sigma0) by reflexivity; auto.
  Case "j_fun".
  SCase "vsub".
  apply permute_pickFun in H4.
  pose proof (Permutation_refl (pickFun Sigma)).
  destruct (permute_pickFun_exists H (Permutation_app H4 H5)) as [Sigma'' [HPerm Hsubseq]].
  (* A is not function type *)
  destruct A; try solve [
    constructor 4 with Sigma''; auto;
      [ intros; apply H0; auto; revert H6; apply Permutation_in; apply Permutation_map; apply Permutation_sym; assumption
      | apply (permute_j_sub H2); auto; apply Permutation_map; assumption
      ]
    ].
  (* A is function type *)
  clear H1 H3.
  simpl in Hsubseq.
  inv Hsubseq.
    SSCase "No type is selected".
    apply Permutation_sym in HPerm; apply Permutation_nil in HPerm; subst.
    contradict H2; simpl; apply context_is_not_nil.
    SSCase "The first A is not selected".
    inv H6.
      SSSCase "No more type is selected".
      apply Permutation_sym in HPerm; apply Permutation_nil in HPerm; subst.
      contradict H2; simpl; apply context_is_not_nil.
      SSSCase "The second A is not selected".
      constructor 4 with Sigma''; auto;
      [ apply (subseq_tran H7); simpl pickFun; auto with v62
      | intros t Ht; apply H0; auto; revert Ht; apply Permutation_in; apply Permutation_map; apply Permutation_sym; assumption
      | apply (permute_j_sub H2); auto; apply Permutation_map; assumption
      ].
      SSSCase "The second A is selected (Sigma'' = (A1,A2)::l1)".
      constructor 4 with ((A1,A2)::l1); auto;
      [ simpl; auto
      | intros t Ht; apply H0; auto; revert Ht; apply Permutation_in; apply Permutation_map; apply Permutation_sym; assumption
      | apply (permute_j_sub H2); auto; apply Permutation_map; assumption
      ].
    SSCase "The first A is selected".
    inv H6.
      SSSCase "No more type is selected.".
      constructor 4 with [(A1,A2)]; auto;
      [ simpl; auto
      | intros t Ht; apply H0; auto; revert Ht; apply Permutation_in; apply Permutation_map; apply Permutation_sym; assumption
      | apply (permute_j_sub H2); auto; apply Permutation_map; assumption
      ].
      SSSCase "The second A is not selected".
      constructor 4 with ((A1,A2)::l1); auto;
      [ simpl; auto
      | intros t Ht; apply H0; auto; revert Ht; apply Permutation_in; apply Permutation_map; apply Permutation_sym; assumption
      | apply (permute_j_sub H2); auto; apply Permutation_map; assumption
      ].
      SSSCase "The second A is selected (Sigma'' = (A1,A2)::(A1,A2)::l0".
      constructor 4 with ((A1,A2)::l0); auto;
      [ simpl; auto
      | intros t Ht; apply H0; apply Permutation_sym in HPerm;
        apply Permutation_map with (B:=typ) (f:=@fst typ typ) in HPerm; simpl map in HPerm; simpl fsttypList in Ht;
        apply Permutation_in with (x:=t) in HPerm; auto with v62
      | simpl; apply (IHA A2) with (A2::A2::sndtypList l0); simpl; auto with arith;
        change (A2::A2::sndtypList l0) with (sndtypList ((A1,A2)::(A1,A2)::l0));
        apply (permute_j_sub H2); try apply Permutation_map; auto
      ].
  SCase "lsub".
  apply permute_pickFun in H4.
  pose proof (Permutation_refl (pickFun Gamma)).
  destruct (permute_pickFun_exists H (Permutation_app H5 H4)) as [Sigma'' [HPerm Hsubseq]].
  (* A is not function type *)
  destruct A; try solve [
    constructor 4 with Sigma''; auto;
      [ intros; apply H0; auto; revert H6; apply Permutation_in; apply Permutation_map; apply Permutation_sym; assumption
      | apply (permute_j_sub H2); auto; apply Permutation_map; assumption
      ]
    ].
  (* A is function type *)
  clear H1 H3.
  simpl in Hsubseq.
  destruct (subseq_split _ _ Hsubseq) as [Gam' [Sig' [Heq [? ?]]]]; subst.
  inv H3.
    SSCase "No type is selected from Sigma".
    rewrite app_nil_r in *.
    constructor 4 with Gam'; auto;
      [ apply (subseq_tran H1); auto with v62
      | intros t Ht; apply H0; auto; revert Ht; apply Permutation_in; apply Permutation_map; apply Permutation_sym; assumption
      | apply (permute_j_sub H2); auto; apply Permutation_map; assumption
      ].
    SSCase "The first A is not selected".
    inv H8.
      SSSCase "No more type is selected from Sigma".
      rewrite app_nil_r in *.
      constructor 4 with Gam'; auto;
        [ apply (subseq_tran H1); auto with v62
        | intros t Ht; apply H0; auto; revert Ht; apply Permutation_in; apply Permutation_map; apply Permutation_sym; assumption
        | apply (permute_j_sub H2); auto; apply Permutation_map; assumption
        ].
      SSSCase "The second A is not selected".
      constructor 4 with (Gam'++Sig'); auto;
        [ apply (subseq_tran (subseq_app H1 H7)); simpl; auto with v62
        | intros t Ht; apply H0; auto; revert Ht; apply Permutation_in; apply Permutation_map; apply Permutation_sym; assumption
        | apply (permute_j_sub H2); auto; apply Permutation_map; assumption
        ].
      SSSCase "The second A is selected (Sig' = (A1,A2)::l1)".
      constructor 4 with (Gam' ++ (A1,A2)::l1); auto;
      [ apply (subseq_tran (subseq_app H1 (extendSubseq (A1,A2) H7))); auto with v62
      | intros t Ht; apply H0; auto; revert Ht; apply Permutation_in; apply Permutation_map; apply Permutation_sym; assumption
      | apply (permute_j_sub H2); auto; apply Permutation_map; assumption
      ].
    SSCase "The first A is selected".
    inv H8.
      SSSCase "No more type is selected.".
      constructor 4 with (Gam' ++ [(A1,A2)]); auto;
      [ simpl; auto with v62
      | intros t Ht; apply H0; auto; revert Ht; apply Permutation_in; apply Permutation_map; apply Permutation_sym; assumption
      | apply (permute_j_sub H2); auto; apply Permutation_map; assumption
      ].
      SSSCase "The second A is not selected".
      constructor 4 with (Gam' ++ (A1,A2)::l1); auto;
      [ simpl; auto with v62
      | intros t Ht; apply H0; auto; revert Ht; apply Permutation_in; apply Permutation_map; apply Permutation_sym; assumption
      | apply (permute_j_sub H2); auto; apply Permutation_map; assumption
      ].
      SSSCase "The second A is selected (Sigma'' = (A1,A2)::(A1,A2)::l0".
      constructor 4 with (Gam' ++ (A1,A2)::l0); auto;
      [ simpl; auto with v62
      | intros t Ht; apply H0; apply Permutation_sym in HPerm;
        apply Permutation_map with (B:=typ) (f:=@fst typ typ) in HPerm; simpl map in HPerm; rewrite fsttypList_app in Ht; simpl fsttypList in Ht;
        apply Permutation_in with (x:=t) in HPerm; try rewrite map_app; try apply in_app_or in Ht; simpl; intuition
      | rewrite sndtypList_app; simpl; apply permute_j_sub with empty (A2::sndtypList Gam' ++ sndtypList l0); perm_refl;
        apply (IHA A2) with (A2::A2::sndtypList Gam' ++ sndtypList l0); simpl; auto with arith;
        apply permute_j_sub with empty (sndtypList Gam' ++ A2::A2::sndtypList l0); perm_refl;
        change (A2::A2::sndtypList l0) with (sndtypList ((A1,A2)::(A1,A2)::l0)); rewrite <- sndtypList_app;
        apply (permute_j_sub H2); try apply Permutation_map; auto
      ].
  Case "j_and_v".
  SSCase "A = B".
    constructor. simpl.
    apply (IHA t1) with (t1::t1::t2::Gamma0); simpl; auto with arith.
    apply permute_j_sub with (t2::t1::t1::Gamma0) Sigma; try perm_refl.
    apply (IHA t2) with (t2::t2::t1::t1::Gamma0); simpl; auto with arith.
    apply permute_j_sub with (t1::t2::t1::t2::Gamma0) Sigma; try perm_refl.
    apply (proj1 j_and_v_vp_inv_cons) with ((t1&t2)::t1::t2::Gamma0); auto.
    apply (permute_j_sub H); auto.
    replace ((t1&t2)::t1::t2::Gamma0) with ([t1&t2]++t1::t2::Gamma0) by reflexivity; auto.
  Case "j_box_v".
  SSCase "A = B".
    constructor. simpl.
    apply (IHA t1) with (t1::t1::Gamma0); simpl; auto with arith.
    apply (proj1 j_sub_v_vp_inv_cons) with (([]t1)::t1::Gamma0); auto.
    replace (([]t1)::t1::Gamma0) with ([[]t1]++t1::Gamma0) by reflexivity.
    apply (permute_j_sub H); auto.
  Case "j_box_l".
  SCase "vsub".
    simpl. replace (A::Gamma0) with ([A] ++ Gamma0) by reflexivity.
    constructor 8 with [A] Gamma0; auto.
    simpl; apply H0.
    subst; replace (A::A::t1::Gamma0) with ([A,A] ++ t1::Gamma0); auto.
  SCase "lsub".
    SSCase "A = B".
      constructor 8 with nil (Gamma1 ++ Gamma2); try reflexivity.
      simpl; apply (IHA t1) with (t1::t1::Gamma1 ++ Gamma2); auto.
      apply (proj1 j_sub_v_vp_inv_cons) with (([]t1)::t1::Gamma1 ++ Gamma2); auto.
      apply (proj1 (move_from_sig_to_gam_cons ([]t1))) with (([]t1)::Sigma0); auto.
      apply (permute_j_sub H); perm_refl; auto.
    SSCase "A <> B".
      constructor 8 with Gamma1 Gamma2; auto.
      firstorder.
  Case "j_and_lp".
  SSCase "A = B".
    constructor. simpl.
    apply (IHA t1) with (t1::t1::t2::Sigma0); simpl; auto with arith.
    apply permute_j_sub_p with Gamma (t2::t1::t1::Sigma0); try perm_refl.
    apply (IHA t2) with (t2::t2::t1::t1::Sigma0); simpl; auto with arith.
    apply permute_j_sub_p with Gamma (t1::t2::t1::t2::Sigma0); try perm_refl.
    apply (proj2 j_and_l_p_inv_cons) with ((t1&t2)::t1::t2::Sigma0); auto.
    apply (permute_j_sub_p H); auto.
    replace ((t1&t2)::t1::t2::Sigma0) with ([t1&t2]++t1::t2::Sigma0) by reflexivity; auto.
  Case "j_and_vp".
  SSCase "A = B".
    constructor. simpl.
    apply (IHA t1) with (t1::t1::t2::Gamma0); simpl; auto with arith.
    apply permute_j_sub_p with (t2::t1::t1::Gamma0) Sigma; try perm_refl.
    apply (IHA t2) with (t2::t2::t1::t1::Gamma0); simpl; auto with arith.
    apply permute_j_sub_p with (t1::t2::t1::t2::Gamma0) Sigma; try perm_refl.
    apply (proj2 j_and_v_vp_inv_cons) with ((t1&t2)::t1::t2::Gamma0); auto.
    apply (permute_j_sub_p H); auto.
    replace ((t1&t2)::t1::t2::Gamma0) with ([t1&t2]++t1::t2::Gamma0) by reflexivity; auto.
  Case "j_dia_vp".
  constructor.
  apply H0. apply Permutation_sym; apply Permutation_cons_app; apply Permutation_sym; assumption.
  Case "j_box_lp".
  SCase "vsub".
    simpl. replace (A::Gamma0) with ([A] ++ Gamma0) by reflexivity.
    constructor 5 with [A] Gamma0; auto.
    simpl; apply H0.
    subst; replace (A::A::t1::Gamma0) with ([A,A] ++ t1::Gamma0); auto.
  SCase "lsub".
    SSCase "A = B".
      constructor 5 with nil (Gamma1 ++ Gamma2); try reflexivity.
      simpl; apply (IHA t1) with (t1::t1::Gamma1 ++ Gamma2); auto.
      apply (proj2 j_sub_v_vp_inv_cons) with (([]t1)::t1::Gamma1 ++ Gamma2); auto.
      apply (proj2 (move_from_sig_to_gam_cons ([]t1))) with (([]t1)::Sigma0); auto.
      apply (permute_j_sub_p H); perm_refl; auto.
    SSCase "A <> B".
      constructor 5 with Gamma1 Gamma2; auto.
      firstorder.
  Case "j_box_vp".
  SSCase "A = B".
    constructor. simpl.
    apply (IHA t1) with (t1::t1::Gamma0); simpl; auto with arith.
    apply (proj2 j_sub_v_vp_inv_cons) with (([]t1)::t1::Gamma0); auto.
    replace (([]t1)::t1::Gamma0) with ([[]t1]++t1::Gamma0) by reflexivity.
    apply (permute_j_sub_p H); auto.
Qed.

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)).
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 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)).
Proof.
  intros. apply contraction_cons_aux_typ with (S (size_typ A)); auto.
Qed.

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)).
Proof.
  split; [induction Sigma' as [| b Sigma''] | induction Gamma' as [| b Gamma'']]; intros; split; auto; intro; simpl;
    [ apply (proj1 (contraction_cons b) Gamma (Sigma'' ++ b :: b:: Sigma))
    | apply (proj2 (contraction_cons b) Gamma (Sigma'' ++ b :: b:: Sigma))
    | apply (proj1 (contraction_cons b) (Gamma'' ++ b :: b:: Gamma) Sigma)
    | apply (proj2 (contraction_cons b) (Gamma'' ++ b :: b:: Gamma) Sigma)
    ]; perm_refl; try apply IHSigma''; try apply IHGamma''; try apply (permute_j_sub H); try apply (permute_j_sub_p H); perm_refl.
Qed.

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).
Proof.
  intros. repeat split; intros;
  [ rewrite <- app_nil_r with _ Sigma
  | rewrite <- app_nil_r with _ Sigma
  | rewrite <- app_nil_r with _ Gamma
  | rewrite <- app_nil_r with _ Gamma
  ];
  apply contraction_bunch_cons;
  rewrite app_nil_r; assumption.
Qed.

Other 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 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 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).
Proof.
  intros; (typ_cases (destruct A) Case); inv H0; repeat (split; intros; subst); try inv H1; try inv H0; auto;
    try solve
      [ (* typ_conj *)
        apply contraction_bunch_cons;
        apply (H A2); simpl; auto with arith;
        match goal with
        | |- ?A :: ?G1 ++ ?G2; ?S ~< _ => apply permute_j_sub with (G1 ++ A :: G2) S; perm_refl
        | |- ?A :: ?G1 ++ ?G2; ?S %< _ => apply permute_j_sub_p with (G1 ++ A :: G2) S; perm_refl
        end;
        apply (H A1); simpl; auto with arith;
        try apply (permute_j_sub H7); try apply (permute_j_sub_p H7); perm_refl
      | (* typ_conj 2 *)
        apply contraction_bunch_cons;
        apply (proj1 contraction_bunch_cons);
        apply (H A2); simpl; auto with arith;
        match goal with
        | |- ?G; ?A :: ?S1 ++ ?S2 ~< _ => apply permute_j_sub with G (S1 ++ A :: S2); perm_refl
        | |- ?G; ?A :: ?S1 ++ ?S2 %< _ => apply permute_j_sub_p with G (S1 ++ A :: S2); perm_refl
        end;
        apply (H A1); simpl; auto with arith;
        try apply (permute_j_sub H7); try apply (permute_j_sub_p H7); perm_refl
      | (* typ_box *)
        apply (H A); simpl; auto with arith;
        try apply (permute_j_sub H2); try apply (permute_j_sub_p H2); perm_refl
    ].
  Case "typ_base".
  symmetry in H2; contradict H2; auto with v62.
  Case "typ_arrow".
    SCase "Gam".
    constructor 4 with (Sigma' ++ Gamma'1 ++ Gamma'2 ++ Sigma'1).
      SSCase "subseq".
      repeat rewrite pickFun_app in *.
      repeat rewrite <- app_assoc.
      apply subseq_app.
        simpl in H3. rewrite app_nil_r in H3. assumption.
        repeat apply subseq_app; assumption.
      SSCase "arg types".
      repeat rewrite fsttypList_app in *; simpl in H12.
      rewrite <- app_assoc in H12; rewrite <- app_comm_cons in H12.
      intros.
      apply in_app_or in H0. intuition.
      apply H6 in H1.
      rewrite <- app_nil_r with _ empty.
      rewrite app_comm_cons.
      apply (H A1); simpl; auto with v62.
      SSCase "result types".
      repeat rewrite sndtypList_app in *; simpl in H14.
      rewrite <- app_nil_r with _ empty.
      apply (H A2); simpl; auto with v62.
      apply (permute_j_sub H14); perm_refl.
    SCase "Sig".
    destruct (subseq_split _ _ H3) as [Gamma0 [Sigma0 [? [? ?]]]]. subst.
    constructor 4 with (Gamma0 ++ Gamma'0 ++ Sigma0 ++ Sigma'1 ++ Sigma'2).
      SSCase "subseq".
      repeat rewrite pickFun_app in *.
      repeat rewrite <- app_assoc.
      auto using subseq_app.
      SSCase "arg types".
      repeat rewrite fsttypList_app in *; simpl in H12.
      intros.
      assert (In t ((fsttypList Gamma0 ++ fsttypList Sigma0) ++
                    (fsttypList Gamma'0 ++ fsttypList Sigma'1 ++ fsttypList Sigma'2))).
        revert H0. apply Permutation_in; perm_refl.
      clear H0.
      apply in_app_or in H9. intuition.
        (* *)
        apply H6 in H0.
        rewrite <- app_nil_r with _ empty.
        rewrite app_comm_cons.
        apply (H A1); simpl; auto with v62. apply H12; auto with v62.
        (* *)
        apply H12. apply in_app_or in H0; intuition.
      SSCase "result types".
      repeat rewrite sndtypList_app in *; simpl in H14.
      apply permute_j_sub with empty ((sndtypList Gamma0 ++ sndtypList Sigma0) ++
        sndtypList Gamma'0 ++ sndtypList Sigma'1 ++ sndtypList Sigma'2); perm_refl.
      rewrite <- app_nil_r with _ empty.
      apply (H A2); simpl; auto with v62.
      apply (permute_j_sub H14); perm_refl.
  Case "typ_box".
    SCase "Gam".
    apply weakening_bunch_j_sub.
    apply (H A); auto with arith.
    apply (permute_j_sub H2); perm_refl.
    (* *)
    apply weakening_bunch_psub.
    apply (H A); simpl; auto with arith.
    apply (permute_j_sub_p H2); perm_refl.
  Case "typ_dia".
  apply weakening_bunch_psub'.
  rewrite <- app_nil_r with _ Sigma.
  edestruct (H A) as [_ [? [_ [_ [_ _]]]]]; simpl; auto with arith.
Qed.

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)).
Proof.
  intros.
  (j_sub_j_sub_p_cases (apply j_sub_j_sub_p_mutind) Case); intros; (split; [SCase "vsub" | SCase "lsub"]); intros; subst; intuition;
    (* the derivation was a right rule, solved by IH *)
    eauto;
    (* When A is a principal fomula, solved by lemma 1 *)
    match goal with
      | H: ?G ++ _ = _ :: _ |- _ => destruct G; inv H
      | H: Permutation (_ ++ ?A :: _) (?B::?G) |- _ =>
        destruct (typ_dec A B);
          [ SSCase "A = B"; subst; apply Permutation_sym in H; apply Permutation_cons_app_inv in H; apply Permutation_sym in H
          | SSCase "A <> B"; assert (In A G) as Hin;
            [ apply Permutation_in with (x := A) in H; auto with v62; simpl in H; destruct H; [congruence | assumption]
            | destruct_in Hin; repeat rewrite app_comm_cons in *; apply Permutation_app_inv with (a := A) in H]
          ]
      | _ => idtac
    end;
    auto; try rewrite app_assoc; try solve [
      auto
      | constructor; rewrite <- app_assoc; eauto; apply H3 with empty; auto; rewrite app_comm_cons; repeat apply permute_app_middle; assumption
      | apply (j_cut_cons_lemma1 H H0); auto
      | apply (j_cut_cons_lemma1 H H2); eauto
      | rewrite <- app_assoc; apply (j_cut_cons_lemma1 H H3); eauto
    ].
  Case "j_fun".
    SCase "vsub".
    apply permute_pickFun in H7.
    pose proof (Permutation_refl (pickFun Sigma)).
    destruct (permute_pickFun_exists H0 (Permutation_app H7 H4)) as [Sigma'' [HPerm Hsubseq]].
    (* A is not function type *)
    destruct A; try solve [ constructor 4 with Sigma''; auto;
        [ simpl in Hsubseq; apply (subseq_tran Hsubseq); rewrite pickFun_app; auto with v62
        | intros; apply H1; auto; revert H9; apply Permutation_in; apply Permutation_map; apply Permutation_sym; assumption
        | apply (permute_j_sub H3); auto; apply Permutation_map; assumption
        ] ].
    (* A is function type *)
    simpl in Hsubseq.
    inv Hsubseq.
      SSCase "No type is selected".
      apply Permutation_sym in HPerm; apply Permutation_nil in HPerm; subst.
      contradict H3; simpl; apply context_is_not_nil.
      SSCase "A was not selected".
      constructor 4 with Sigma'';
        [ rewrite pickFun_app; apply (subseq_tran H11); auto with v62
        | intros ? Hin; apply H1; revert Hin; apply Permutation_in; apply Permutation_map; apply Permutation_sym; assumption
        | apply (permute_j_sub H3); auto; apply Permutation_map; assumption].
      SSCase "A was selected".
      apply (proj1 (j_cut_cons_lemma1 H H5)); auto.
      destruct (subseq_split _ _ H11) as [Gam' [Sig' [Heq [? ?]]]]; subst.
      constructor 1 with nil Gamma'' nil Gam' Sig'; auto; rewrite app_nil_l; rewrite <- app_comm_cons;
        [ intros ? Hin; apply H1; revert Hin; apply Permutation_in; apply Permutation_map; apply Permutation_sym; assumption
        | apply (permute_j_sub H3); auto; apply Permutation_map; assumption].
    SCase "lsub".
    clear H6 H7 H2.
    (* A is not function type *)
    destruct A; try solve [
      constructor 4 with Sigma'; auto;
        simpl in H0; apply (subseq_tran H0); repeat rewrite pickFun_app; auto with v62].
    (* A is function type *)
    simpl in H0.
    destruct (subseq_split _ _ H0) as [Gam' [Sig' [Heq [? ?]]]]; subst.
    clear H0. inv H4.
      SSCase "No type from sigma".
      constructor 4 with Gam'; rewrite app_nil_r in *; auto.
      apply (subseq_tran H2). repeat rewrite pickFun_app; auto with v62.
      SSCase "A was not selected".
      constructor 4 with (Gam' ++ Sig'); auto.
      apply (subseq_tran (subseq_app H2 H7)). repeat rewrite pickFun_app; auto with v62.
      SSCase "A was selected".
      apply (j_cut_cons_lemma1 H H5); auto.
      constructor 3 with nil Sigma'' Gam' nil l1; auto.
  Case "j_and_v".
    SSCase "A = B".
    apply (proj1 (j_cut_cons_lemma1 H H2)); auto.
    constructor 3 with empty Gamma''; auto.
    simpl; apply (permute_j_sub H0); auto.
      apply Permutation_sym; do 2 apply Permutation_cons_app; apply Permutation_sym; assumption.
  Case "j_box_v".
    SSCase "A = B".
    apply ( (j_cut_cons_lemma1 H H2)); auto.
    constructor 4 with empty Gamma''; auto.
    simpl; apply (permute_j_sub H0); auto.
      apply Permutation_sym; apply Permutation_cons_app; apply Permutation_sym; assumption.
  Case "j_box_l".
    SCase "vsub".
    constructor 8 with Gamma0 Gamma''; auto.
      apply H2 with empty; auto.
        replace (A::t1::Gamma'') with ([A]++t1::Gamma'') by auto; apply permute_app_middle; auto.
    SCase "lsub".
      SSCase "Sigma = nil".
      rewrite app_assoc.
      constructor 8 with (Gamma0 ++ Gamma1) Gamma2; auto.
      repeat rewrite <- app_assoc; auto.
  Case "j_and_vp".
    SSCase "A = B".
    apply (proj1 (proj2 (j_cut_cons_lemma1 H H2))); auto.
    constructor 1 with empty Gamma''; simpl; auto.
    apply (permute_j_sub_p H0); auto; apply Permutation_sym; repeat apply Permutation_cons_app; apply Permutation_sym; assumption.
  Case "j_dia_vp".
    SSCase "A = B".
    apply permute_j_sub_p with (Gamma++Gamma1++Gamma2) Sigma; perm_refl; auto.
    rewrite <- app_nil_l with _ Sigma.
    apply weakening_bunch_psub'.
    apply (contraction_bunch_cons).
    edestruct (H t1) as [_ [? [_ [_ [_ _]]]]]; simpl; auto with arith.
    apply H1; [inversion H2; subst; assumption|].
    apply H3 with empty; auto with v62.
  Case "j_box_lp".
    SCase "vsub".
    constructor 5 with Gamma0 Gamma''; auto.
      apply H2 with empty; auto.
        replace (A::t1::Gamma'') with ([A]++t1::Gamma'') by auto. apply permute_app_middle; auto.
    SCase "lsub".
      SSCase "Sigma = nil".
      rewrite app_assoc.
      constructor 5 with (Gamma0 ++ Gamma1) Gamma2; auto.
      repeat rewrite <- app_assoc; auto.
  Case "j_box_vp".
    SSCase "A = B".
    apply ( (j_cut_cons_lemma1 H H2)); auto.
    constructor 3 with empty Gamma''; simpl; auto.
    apply (permute_j_sub_p H0); auto; apply Permutation_sym; apply Permutation_cons_app; apply Permutation_sym; assumption.
Qed.

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).
Proof.
  intros.
  destruct (j_cut_cons_lemma2_ori H).
  repeat split; intros; subst;
    try apply H1 in H4; try apply H1 in H3;
    try apply H2 in H4; try apply H2 in H3;
    try destruct H3; try destruct H4; eauto.
Qed.

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)).
Proof.
  intros.
  (j_sub_j_sub_p_cases (apply j_sub_j_sub_p_mutind) Case); intros; subst; try (apply IHj_sub in H; clear IHj_sub);
    try solve [ (* right rules are solved by lemma2 *)
      apply (j_cut_cons_lemma2a H); eauto
    ];
    (* remaining cases are solved by IH *)
    repeat split; intros;
    match goal with
    | H: _ ++ _ :: _ = _ |- _ => symmetry in H; contradict H; auto with v62
    | _ => idtac
    end;
    try solve [
      subst; repeat rewrite <- app_assoc; repeat rewrite <- app_comm_cons; econstructor; eauto;
      repeat rewrite app_comm_cons; repeat rewrite app_assoc; intuition
      | rewrite <- app_nil_r with _ Sigma; apply H1; 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 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).
Proof.
  induction k; intros; [inversion H|].
  assert (j_cut_ind_on_typ A) by (unfold j_cut_ind_on_typ; intros; apply IHk; eauto with arith); clear IHk.
  pose proof (j_cut_cons_lemma3 H0).
  firstorder.
Qed.

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).
Proof.
  intro A; apply j_cut_cons_aux with (S (size_typ A)); auto.
Qed.

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.
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 (proj1 (proj2 (proj2 (proj2 (proj2 (j_cut_cons 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.
  Case "r_box_T".
  constructor 8 with empty empty; auto.
  Case "r_box_4".
  constructor 8 with empty empty; auto.
  Case "r_box_K".
  constructor 8 with empty empty; auto.
  constructor; simpl; apply (proj1 (move_from_sig_to_gam_cons t1)) with [t1]; auto.
  Case "r_box_dist".
  constructor.
  constructor 8 with empty empty; auto.
  constructor 8 with (empty ++ [t1]) empty; auto.
  repeat constructor; auto.
  simpl; rewrite <- app_nil_l with _ [t1,t2]; auto.
  Case "r_dia_4".
  constructor. constructor.
  rewrite <- app_nil_l with _ [<>t]; constructor.
  rewrite <- app_nil_l with _ [t]; auto.
  Case "r_box_dia_K".
  constructor.
  constructor.
  constructor 5 with empty empty; auto.
  constructor.
  apply j_dia_r_inv.
  apply j_box_v_inv.
  simpl.
  apply (proj1 (move_from_sig_to_gam_cons ([]t1))) with [[]t1, t2]; auto.
  change ([[]t1,t2]) with (empty ++ ([[]t1,t2])).
  apply j_and_l_inv.
  apply j_dia_r.
  apply j_poss_p.
  assumption.
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 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)).
Proof.
  unfold box_Conj_right;
  (j_sub_j_sub_p_cases (apply j_sub_j_sub_p_mutind) Case); intros;
    (split; [SCase "Sig=nil" | split; [SCase "Gam=nil" | SCase "Both are not nil"]]); intros;
  repeat match goal with
  | H: _ ++ _ :: _ = empty |- _ => symmetry in H; contradict H; auto with v62
  | H: _ ++ _ = empty |- _ => destruct (app_eq_nil _ _ H); clear H
  | H: ?G ++ _ = _ :: _ |- _ => destruct G; inv H; simpl in *
  end;
  subst; try rewrite map_app in *; simpl; auto; intuition;
  try solve [
      rewrite <- Conj_right_one_step; auto
    | match goal with
        | |- _ & ?A =< typ_base _ => solve [constructor 2 with A; auto]
        | |- ?A & _ =< typ_base _ => solve [constructor 2 with A; auto]
        | |- Conj_right ?A (?l1 ++ (?t1 & ?t2) :: ?l2) =< _ =>
          constructor 2 with (Conj_right A (l1++t1::t2::l2));
            [apply Conj_right_assoc| ]; auto
        | |- ?Head & Conj_right ?A (?l1 ++ (?t1 & ?t2) :: ?l2) =< _ =>
          constructor 2 with (Head & Conj_right A (l1++t1::t2::l2));
            [apply sub_weakening_right; apply Conj_right_assoc| ]; auto
        | |- Conj_right ([](?A&?B)) (map typ_box ?l) =< _ =>
          constructor 2 with (Conj_right ([]A) (map typ_box (B::l)));
            [simpl| ]; auto
        | |- Conj_right ([](?A&?B)) (map typ_box ?l) & ?Tail=< _ =>
          constructor 2 with (Conj_right ([]A) (map typ_box (B::l)) & Tail);
            [simpl| ]; auto
        | |- Conj_right ?C (map typ_box ?G1 ++ ([](?A&?B)) :: map typ_box ?G2) =< _ =>
          constructor 2 with (Conj_right C (map typ_box G1 ++ map typ_box (A::B::G2)));
            [ simpl; constructor 2 with (Conj_right C (map typ_box G1 ++ (([]A)&([]B))::map typ_box G2)); [| apply Conj_right_assoc]
            | rewrite <- map_app ]; auto
        | |- Conj_right ?C (map typ_box ?G1 ++ ([](?A&?B)) :: map typ_box ?G2) & ?Tail=< _ =>
          constructor 2 with (Conj_right C (map typ_box G1 ++ map typ_box (A::B::G2)) & Tail);
            [simpl; apply sub_weakening_left; constructor 2 with (Conj_right C (map typ_box G1 ++ (([]A)&([]B))::map typ_box G2)); [| apply Conj_right_assoc]
            | rewrite <- map_app ]; auto
        | |- Conj_right ([]([]?A)) ?l =< _ =>
          constructor 2 with (Conj_right ([]A) l);
            [simpl| ]; auto
        | |- Conj_right ([]([]?A)) ?l & ?Tail=< _ =>
          constructor 2 with (Conj_right ([]A) l & Tail);
            [simpl| ]; auto
        | |- Conj_right ?C (map typ_box ?G1 ++ ([]([]?A)) :: map typ_box ?G2) =< _ =>
          constructor 2 with (Conj_right C (map typ_box G1 ++ map typ_box (A::G2)));
            [simpl; constructor 2 with (Conj_right C (map typ_box G1 ++ ([]A)::map typ_box G2))
            | rewrite <- map_app ]; auto
        | |- Conj_right ?C (map typ_box ?G1 ++ ([]([]?A)) :: map typ_box ?G2) & ?Tail=< _ =>
          constructor 2 with (Conj_right C (map typ_box G1 ++ map typ_box (A::G2)) & Tail);
            [simpl; apply sub_weakening_left; constructor 2 with (Conj_right C (map typ_box G1 ++ ([]A)::map typ_box G2))
            | rewrite <- map_app ]; auto
        | |- _ =< <> ?t =>
          solve [
             constructor 2 with t; auto
           | constructor 2 with (<>t1); auto; constructor 2 with (<><>t2); auto; constructor; change t1 with (Conj_right t1 empty); auto
        ]
      end
  ].
  Case "j_fun".
    SCase "Sig=nil".
    destruct Sigma' as [|(b1,b2) Funs]; [contradict H2; apply context_is_not_nil|].
    clear H0 H2.
    assert (Conj (makeFunList Funs) (b1 --> b2) =< t1' --> t2').
      SSCase "Proof of assertion".
      apply fun_dist_gen; auto.
        constructor 2 with (Conj_right b2 (sndtypList Funs)); [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_right A (map typ_box Gamma')); auto.
    switch_left.
    destruct (typ_dec A (b1 --> b2)).
      SSCase "A = b1 --> b2".
      subst A.
      simpl in H. rewrite app_nil_r in H.
      apply extendSubseq_inv in H.
      constructor 2 with (Conj Gamma' (b1-->b2)); auto.
      apply Conj_subseq_weakening with (makeFunList Funs); auto.
      apply subseq_tran with (makeFunList (pickFun Gamma')).
        unfold makeFunList; auto with v62.
        apply subseq_makeFunList_pickFun.
      SSCase "A <> b1 --> b2".
      assert (subseq ((b1, b2) :: Funs) (pickFun Gamma')).
        SSSCase "Proof of assertion".
        destruct A; simpl in H; rewrite app_nil_r in H; try assumption.
        apply extraSubseq_inv with (A1,A2); auto.
        intuition. inversion H2. apply n; f_equal; auto.
      assert (Conj (makeFunList ((b1, b2)::Funs)) (A) =< t1' --> t2').
        SSSCase "Proof of assertion".
        constructor 2 with (Conj (A :: makeFunList Funs) (b1-->b2)).
          simpl makeFunList; auto.
          simpl. constructor 2 with (Conj (makeFunList Funs) (b1-->b2)); auto.
      constructor 2 with (Conj Gamma' A); auto.
      apply Conj_subseq_weakening with (makeFunList ((b1,b2)::Funs)); auto.
      apply subseq_tran with (makeFunList (pickFun Gamma')).
        unfold makeFunList; auto with v62.
        apply subseq_makeFunList_pickFun.
    SCase "Gam=nil".
    destruct Sigma' as [|(b1,b2) Funs]; [contradict H2; apply context_is_not_nil|].
    clear H0 H2.
    assert (Conj (makeFunList Funs) (b1 --> b2) =< t1' --> t2').
      SSCase "Proof of assertion".
      apply fun_dist_gen; auto.
        switch_left; 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.
    switch_left.
    destruct (typ_dec A (b1 --> b2)).
      SSCase "A = b1 --> b2".
      subst A.
      simpl in H.
      apply extendSubseq_inv in H.
      apply Conj_subseq_weakening with (makeFunList Funs); auto.
      apply subseq_tran with (makeFunList (pickFun Sigma'0)).
        unfold makeFunList; auto with v62.
        apply subseq_makeFunList_pickFun.
      SSCase "A <> b1 --> b2".
      assert (subseq ((b1, b2) :: Funs) (pickFun Sigma'0)).
        SSSCase "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)::Funs)) (A) =< t1' --> t2').
        SSSCase "Proof of assertion".
        constructor 2 with (Conj (A :: makeFunList Funs) (b1-->b2)).
          simpl makeFunList; auto.
          simpl. constructor 2 with (Conj (makeFunList Funs) (b1-->b2)); auto.
      apply Conj_subseq_weakening with (makeFunList ((b1,b2)::Funs)); auto.
      apply subseq_tran with (makeFunList (pickFun Sigma'0)).
        unfold makeFunList; auto with v62.
        apply subseq_makeFunList_pickFun.
    SCase "Both are not nil".
    destruct Sigma' as [|(b1,b2) Funs]; [contradict H2; apply context_is_not_nil|].
    clear H0 H2.
    assert (Conj (makeFunList Funs) (b1 --> b2) =< t1' --> t2').
      SSCase "Proof of assertion".
      apply fun_dist_gen; auto.
        switch_left; 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_right A (map typ_box Gamma') & Conj_right B Sigma'0); auto.
    constructor 2 with (Conj (map typ_box Gamma') A & Conj_right B Sigma'0); auto.
    constructor 2 with (Conj (map typ_box Gamma') A & Conj Sigma'0 B); auto.
    constructor 2 with (Conj Gamma' A & Conj Sigma'0 B); auto.
    constructor 2 with (Conj (Gamma'++B::Sigma'0) A).
      constructor 2 with (Conj (Gamma' ++ A::Sigma'0) B); auto using Conj_swap. apply Conj_split.
    destruct (typ_dec A (b1 --> b2)).
      SSCase "A = b1 --> b2".
      subst A.
      rewrite <- pickFun_app in H. simpl in H.
      apply extendSubseq_inv in H.
      apply Conj_subseq_weakening with (makeFunList Funs); auto.
      apply subseq_tran with (makeFunList (pickFun (Gamma'++B::Sigma'0))).
        unfold makeFunList; auto with v62.
        apply subseq_makeFunList_pickFun.
      SSCase "A <> b1 --> b2".
      assert (subseq ((b1, b2) :: Funs) (pickFun (Gamma'++B::Sigma'0))).
        SSSCase "Proof of assertion".
        destruct A; rewrite <- pickFun_app in H; 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)::Funs)) (A) =< t1' --> t2').
        SSSCase "Proof of assertion".
        constructor 2 with (Conj (A :: makeFunList Funs) (b1-->b2)).
          simpl makeFunList; auto.
          simpl. constructor 2 with (Conj (makeFunList Funs) (b1-->b2)); auto.
      apply Conj_subseq_weakening with (makeFunList ((b1,b2)::Funs)); auto.
      apply subseq_tran with (makeFunList (pickFun (Gamma'++B::Sigma'0))).
        unfold makeFunList; auto with v62.
        apply subseq_makeFunList_pickFun.
  Case "j_box_l".
    SCase "Gam=nil".
      SSCase "Sigma1=nil".
      destruct Sigma'; [change empty with (map typ_box empty); auto|].
      constructor 2 with (Conj_right ([]t1) (map typ_box empty) & Conj_right t Sigma'); auto.
      switch_left.
      constructor 2 with (Conj (([]t1)::Sigma') t); [|simpl]; auto.
      SSCase "Sigma1=A::Sigma1".
      constructor 2 with (Conj_right ([]t1) (map typ_box empty) & Conj_right A (Sigma1 ++ Sigma2)); auto.
      simpl.
      constructor 2 with (Conj_right A (([]t1)::Sigma1++Sigma2)); [apply Conj_right_swap_in_conv|].
      switch_left.
      simpl. apply sub_weakening_right; auto.
    SCase "Both are not nil".
      SSCase "Sigma1=nil".
        SSSCase "Gamma1=nil".
        destruct Sigma'.
          SSSSCase "Sigma2=nil".
          constructor 2 with (Conj_right ([]t1) (map typ_box (A::Gamma'))); auto.
          constructor 2 with (([]t1) & Conj_right ([]A) (map typ_box Gamma')); auto.
          constructor 2 with (Conj_right ([]A) (([]t1)::map typ_box Gamma')); [|simpl]; auto.
          SSSSCase "Sigma2=t::Sigma'".
          constructor 2 with (Conj_right ([]t1) (map typ_box (A::Gamma')) & Conj_right t Sigma'); auto.
          constructor 2 with (Conj_right ([]A) (map typ_box Gamma') & Conj_right t (([]t1)::Sigma')); auto.
          constructor 2 with (Conj_right ([]A) (map typ_box Gamma') & ([]t1) & Conj_right t Sigma'); auto.
          switch_assoc.
          apply sub_weakening_left.
          constructor 2 with (([]t1) & Conj_right ([]A) (map typ_box Gamma')); auto.
          constructor 2 with (Conj_right ([]A) (([]t1)::map typ_box Gamma')); [|simpl]; auto.
        SSSCase "Gamma1=A::Gamma1".
        destruct Sigma'.
          SSSSCase "Sigma2=nil". (**)
          constructor 2 with (Conj_right ([]A) (map typ_box (Gamma1 ++ t1 :: Gamma2))); auto.
          rewrite map_app. simpl.
          constructor 2 with (Conj (map typ_box Gamma1 ++ map typ_box Gamma2) ([]A) & []t1); auto.
          constructor 2 with (Conj (([]t1) :: map typ_box Gamma1 ++ map typ_box Gamma2) ([]A)); [simpl|]; auto.
          constructor 2 with (Conj (map typ_box Gamma1 ++ ([]t1) :: map typ_box Gamma2) ([]A)); auto.
          SSSSCase "Sigma2=t::Sigma'".
          constructor 2 with (Conj_right ([]A) (map typ_box (Gamma1++t1::Gamma2)) & Conj_right t Sigma'); auto.
          constructor 2 with ((Conj_right ([]A) (map typ_box Gamma1 ++ map typ_box Gamma2)) & Conj (t::Sigma') ([]t1)); auto.
          constructor 2 with ((Conj_right ([]A) (map typ_box Gamma1 ++ map typ_box Gamma2)) & Conj (([]t1)::Sigma') t); auto.
          simpl.
          constructor 2 with (Conj_right ([]A) (map typ_box Gamma1 ++ map typ_box Gamma2) & ([]t1) & Conj_right t Sigma'); auto.
          switch_assoc.
          apply sub_weakening_left.
          constructor 2 with (([]t1) & Conj_right ([]A) (map typ_box Gamma1 ++ map typ_box Gamma2)); auto.
          constructor 2 with (([]t1) & Conj (map typ_box Gamma1 ++ map typ_box Gamma2) ([]A)); auto.
          change (([]t1)