Library SS5

Judgmental subtyping system with intersection types and modal types.
  • Author : Jeongbong Seo and Sungwoo Park
This file contains definitions, lemmas, and theorems of the subtyping systems based on modal logic S5 which are described in Section 4 of the paper.

Contents:
  • Definition
    • Pre-terms
    • Relational subtyping system
    • Judgmental subtyping system
      • Auxiliary functions
      • Subtyping judgments
      • The subsets of subtyping inference rules
    • Other auxiliary functions
  • Infrastructure lemmas
    • Lemmas for the relational subtyping system
      • Weakening and associativity
      • Conversion between Conj and Conj_right
      • The distributivity of function types over intersection types
      • Permutation (Commutativity)
      • More properties of the auxiliary functions
    • Lemmas for the judgmental subtyping system
      • Lemmas for case analysis on the remote node context
      • All all contexts are empty
      • General ver. of the rules j_refl and j_refl_v
      • Context permutation
      • Weakening
      • A type in the ordinary subtyping context can be moved to the global subtyping context
      • Invertible rules
      • Contraction
      • Contraction of empty local subtyping contexts
    • Other lemmas
  • Admissibility of the cut rules
  • Equivalence between the two subtyping systems
    • Completeness
    • Soundness

Set Implicit Arguments.

Require Export Coq.Lists.List.
Require Export Arith.
Require Export SfLib.
Require Export Subseq.
Require Import Permutation.
Require Export Perm_tactic.
Require Export wpermute.

Ltac inv H := inversion H; clear H; subst.
Ltac destruct_in H := destruct (in_split _ _ H) as [?l1 [?l2 ?Hl1l2]]; clear H; subst.

Definition


This file contains definitions of the subtyping systems based on modal logic S5 which are described in Section 4 of the paper.

Pre-terms


There are four type constructors:
  • A --> B denotes function types.
  • A & B denotes intersection types.
  • A denotes necessity modal types.
  • <> A denotes possibility modal types.

Notation base := nat.

Inductive typ : Set :=
  | typ_base : base -> typ (* 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 ordinary and global subtyping contexts as a list of typ.

Notation env := (list typ).
Notation empty := (@nil typ).

We represent the remote node context as a list of lists of typ. We will call each element as a local subtyping context.

Notation worlds := (list (list typ)).
Notation noworld := (@nil (list typ)).

We define the size of a type as the number of type constructors appearing in the type.

Fixpoint size_typ (t:typ) :=
  match t with
  | typ_base _ => 0
  | typ_arrow t1 t2 => S (size_typ t1 + size_typ t2)
  | typ_conj t1 t2 => S (size_typ t1 + size_typ t2)
  | typ_box t => S (size_typ t)
  | typ_dia t => S (size_typ t)
  end.

We define the size of a local subtyping context as the sum of the size of every type in the context.

Fixpoint size_env (ctx:env) :=
  match ctx with
  | nil => 0
  | A::ctx' => size_typ A + size_env ctx'
  end.

Relational subtyping system


For the relational subtyping system, we use the following notation 'A =< B' and it means that if an expression has type A then it also has type B. Inference rules are direct translations from the rules in Figure 1 in the paper.

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

Inductive r_sub : typ -> typ -> Prop :=
  | r_refl : forall (t : typ),
    t =< t

  | r_trans : forall (t1 t2 t3 : typ),
    t1 =< t2 ->
    t2 =< t3 ->
    t1 =< t3

  | r_and_l1 : forall (t1 t2 : typ),
    t1 & t2 =< t1

  | r_and_l2 : forall (t1 t2 : typ),
    t1 & t2 =< t2

  | r_and_r : forall (t1 t2 t3 : typ),
    t1 =< t2 ->
    t1 =< t3 ->
    t1 =< t2 & t3

  | r_fun : forall (t1 t2 t1' t2' : typ),
    t1' =< t1 ->
    t2 =< t2' ->
    t1 --> t2 =< t1'--> t2'

  | r_fun_dist : forall (t1 t2 t3 : typ),
    (t1 --> t2) & (t1 --> t3) =< t1 --> (t2 & t3)

  | r_box_T : forall (t : typ),
    [] t =< t

  | r_box_4 : forall (t : typ),
    [] t =< [] ( [] t )

  | r_box_K : forall (t1 t2 : typ),
    t1 =< t2 ->
    [] t1 =< [] t2

  | r_box_dist : forall (t1 t2 : typ),
    ([] t1) & ([] t2) =< [] (t1 & t2)

  | r_dia_T : forall (t : typ),
    t =< <> t

  | r_dia_4 : forall (t : typ),
    <> ( <>t ) =< <>t

  | r_dia_K : forall (t1 t2 :typ),
    t1 =< t2 ->
    <> t1 =< <> t2

  | r_box_dia_K : forall (t1 t2 t3 : typ),
    ([] t1) & t2 =< t3 ->
    ([] t1) & (<> t2) =< <> t3

  | r_dia_5 : forall (t: typ),
    <> t =< [] (<> t)

  | r_box_5 : forall (t: typ),
    <> ([] t) =< [] t

where "A =< B" := (r_sub A B).

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"
  | c "r_dia_5" | c "r_box_5"
  ].

Judgmental subtyping system


Auxiliary functions


These auxiliary functions are used to encode the rule j_fun of the judgmental subtyping system.

pickFun collects all function types from a typing context and converts each of them into type pairs (argument type and result type).
e.g. pickFun [P, A1-->B1, A2-->B2, A3 & A4] returns [(A1,B1), (A2,B2)].

fsttypList gets a list of type pairs and filters out the second element of each pair.
e.g. fstypList [(A1,B1), (A2,B2)] returns [A1, A2].

sndtypList gets a list of type pairs and filters out the first element of each pair.
e.g. fstypList [(A1,B1), (A2,B2)] returns [B1, B2].

makeFunList produces a list of function types from a list of type pairs.
e.g. makeFunList [(A1,B1), (A2,B2)] returns [A1-->B1, A2-->B2].

Fixpoint pickFun (l : env) : list (typ*typ) :=
  match l with
  | nil => nil
  | (X --> Y) :: l' => (X,Y) :: pickFun l'
  | _ :: l' => pickFun l'
  end.

Definition fsttypList l := map (@fst typ typ) l.
Definition sndtypList l := map (@snd typ typ) l.

Definition makeFunList l := map (prod_curry typ_arrow) l.

Subtyping judgments


For judgmental subtyping system, we use the following judgment Delta;; Gamma; Sigma ~< B. Delta is the remote node context, Gamma is the global subtyping context, and Sigma is the ordinary subtyping context. Inference rules are from Figure 6 in the paper.

To encode the rule j_fun, we use three auxiliary functions and one inductive definition: pickFun, fsttypList, sndtypList, and subseq. We first collect all function types from Gamma and Sigma using pickFun, then pick some of them using subseq. We decompose gathered function types into argument types and result types using fsttypList and sndtypList, and use them to state premises.

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

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

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

  | j_fun : forall (Delta:worlds) (Gamma Sigma:env) (t1' t2':typ) (Sigma':list (typ*typ)),
    subseq Sigma' (pickFun Gamma ++ pickFun Sigma) ->
    (forall t, In t (fsttypList Sigma') -> noworld ;; empty; [t1'] ~< t) ->
    noworld ;; empty; (sndtypList Sigma') ~< t2' ->
    Delta ;; Gamma; Sigma ~< t1' --> t2'
    
  | j_and_lc : forall (Delta1 Delta2 : worlds) (Gamma Sigma Sigma1 Sigma2 : env) (t1 t2 t3 : typ),
    Delta1 ++ (Sigma1 ++ t1 :: t2 :: Sigma2) :: Delta2 ;; Gamma; Sigma ~< t3 ->
    Delta1 ++ (Sigma1 ++ (t1 & t2) :: Sigma2) :: Delta2 ;; Gamma; Sigma ~< t3

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

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

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

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

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

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

  | j_box_r : forall (Delta Delta1 Delta2:worlds) (Gamma Sigma: env) (t:typ),
    Delta1 ++ Sigma :: Delta2 ;; Gamma; empty ~< t ->
    Delta = Delta1 ++ Delta2 ->
    Delta ;; Gamma; Sigma ~< [] t

  | j_dia_lc : forall (Delta1 Delta2 : worlds) (Gamma Sigma Sigma1 Sigma2 : env) (t1 t2 : typ),
    Delta1 ++ (Sigma1 ++ Sigma2) :: [t1] :: Delta2 ;; Gamma; Sigma ~< t2 ->
    Delta1 ++ (Sigma1 ++ (<>t1) :: Sigma2) :: Delta2 ;; Gamma; Sigma ~< t2

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

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

  | j_dia_r : forall (Delta1 Delta2:worlds) (Gamma Sigma' Sigma:env) (t:typ),
    Delta1 ++ Sigma :: Delta2 ;; Gamma; Sigma' ~< t ->
    Delta1 ++ Sigma' :: Delta2 ;; Gamma; Sigma ~< <> t

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

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

Hint Constructors j_sub.

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

The subsets of subtyping inference rules.


To use the proof strategy explained in Section 2.2 of the paper, we need additional judgments that are capable of specifying the principal type of the derivation.

A type in the remote node context is focused.

Delta,, (PSigma, |A|) ;; Gamma; Sigma ~< B means that A is the principal type of the last inference rule in its derivation.

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

Inductive j_sub_lcf : worlds -> env -> typ -> env -> env -> typ -> Prop :=
  | j_and_lcf : forall (Delta Delta1 Delta2 : worlds)
    (Gamma PSigma Sigma Sigma1 Sigma2 : env) (t1 t2 t3 : typ),
    Delta1 ++ (Sigma1 ++ t1 :: t2 :: Sigma2) :: Delta2 ;; Gamma; Sigma ~< t3 ->
    Delta = Delta1 ++ Delta2 ->
    PSigma = Sigma1 ++ Sigma2 ->
    Delta,, PSigma, | t1 & t2 |;; Gamma; Sigma ~< t3

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

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

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

Hint Constructors j_sub_lcf.

Tactic Notation "j_sub_lcf_cases" tactic(first) tactic(c) :=
  first;
  [ c "j_and_lcf" | c "j_box_lcf" | c "j_dia_lcf" ].

A type in the global subtyping context is focused.

Delta;; Gamma, |A|; Sigma ~< B means that A is the principal type of the last inference rule in its derivation.

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

Inductive j_sub_vf : worlds -> env -> typ -> env -> typ -> Prop :=
  | j_refl_vf : forall (Delta:worlds) (Gamma Sigma:env) (b:base),
    Delta ;; Gamma, | typ_base b |; Sigma ~< typ_base b

  | j_fun_vf : forall (Delta:worlds) (Gamma Gamma1 Gamma2 Sigma:env)
    (t1 t2 t1' t2':typ) (Gamma1' Gamma2' Sigma':list (typ*typ)),
    subseq Gamma1' (pickFun Gamma1) ->
    subseq Gamma2' (pickFun Gamma2) ->
    subseq Sigma' (pickFun Sigma) ->
    Gamma = Gamma1 ++ Gamma2 ->
    (forall t, In t (fsttypList ((Gamma1' ++ (t1,t2) :: Gamma2') ++ Sigma')) -> noworld;; empty; [t1'] ~< t) ->
    noworld;; empty; (sndtypList ((Gamma1' ++ (t1,t2) :: Gamma2') ++ Sigma')) ~< t2' ->
    Delta;; Gamma, |(t1 --> t2)|; Sigma ~< t1' --> t2'
    
  | j_and_vf : forall (Delta:worlds) (Gamma Gamma1 Gamma2 Sigma:env) (t1 t2 t3:typ),
    Delta ;; (Gamma1 ++ t1 :: t2 :: Gamma2); Sigma ~< t3 ->
    Gamma = Gamma1 ++ Gamma2 ->
    Delta ;; Gamma, | t1 & t2 |; Sigma ~< t3

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

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

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

Hint Constructors j_sub_vf.

Tactic Notation "j_sub_vf_cases" tactic(first) tactic(c) :=
  first;
  [ c "j_refl_vf" | c "j_fun_vf"
  | c "j_and_vf" | c "j_box_vf" | c "j_dia_vf"
  ].

A type in the ordinary subtyping context is focused.

Delta;; Gamma; Sigma, |A| ~< |B| means that A is the principal type of the last inference rule in its derivation.

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

Inductive j_sub_lf : worlds -> env -> env -> typ -> typ -> Prop :=
  | j_refl_lf : forall (Delta:worlds) (Gamma Sigma:env) (b:base),
    Delta ;; Gamma ; Sigma, | typ_base b | ~< typ_base b

  | j_fun_lf : forall (Delta:worlds) (Gamma Sigma Sigma1 Sigma2:env)
    (t1 t2 t1' t2':typ) (Gamma' Sigma'1 Sigma'2:list (typ*typ)),
    subseq Gamma' (pickFun Gamma) ->
    subseq Sigma'1 (pickFun Sigma1) ->
    subseq Sigma'2 (pickFun Sigma2) ->
    Sigma = Sigma1 ++ Sigma2 ->
    (forall t, In t (fsttypList (Gamma' ++ (Sigma'1 ++ (t1,t2) :: Sigma'2))) -> noworld;; empty; [t1'] ~< t) ->
    noworld;; empty; (sndtypList (Gamma' ++ (Sigma'1 ++ (t1,t2) :: Sigma'2))) ~< t2' ->
    Delta ;; Gamma; Sigma, | t1 --> t2 | ~< t1' --> t2'

  | j_and_lf : forall (Delta:worlds) (Gamma Sigma Sigma1 Sigma2:env) (t1 t2 t3:typ),
    Delta ;; Gamma ; (Sigma1 ++ t1 :: t2 :: Sigma2) ~< t3 ->
    Sigma = Sigma1 ++ Sigma2 ->
    Delta ;; Gamma ; Sigma, | t1 & t2 | ~< t3

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

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

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

Hint Constructors j_sub_lf.

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

The right-side is focused.

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

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

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

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

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

  | j_box_rf : forall (Delta Delta1 Delta2:worlds) (Gamma Sigma: env) (t:typ),(*5*)
    Delta1 ++ Sigma :: Delta2 ;; Gamma; empty ~< t ->
    Delta = Delta1 ++ Delta2 ->
    Delta ;; Gamma; Sigma ~< | [] t |

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

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

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

Hint Constructors j_sub_rf.

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

Other auxiliary functions


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

Conj family

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

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



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

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


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

Example conj_id_A : forall A,
  Conj empty A = A.
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 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.

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


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

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

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

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

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

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

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

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

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

fun_dist


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

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

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

Example fun_dist_B : forall A B,
  fun_dist A empty B = A --> B.
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.

n_list


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

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


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

Infrastructure lemmas


Lemmas for the relational subtyping system


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

Weakening and associativity

Following two lemmas are weakening lemmas.

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

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

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

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


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

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

Hint Resolve sub_weakening_left sub_weakening_right.

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

Hint Resolve sub_conj.

We can generalize the lemma sub_weakening_left using Conj_right and del_to_typ_right_sub.

Lemma Conj_right_sub: forall Sigma A B,
  A =< B ->
  Conj_right A Sigma =< Conj_right B Sigma.
Proof.
  induction Sigma as [| b Sigma']; intros; simpl; auto.
Qed.

Hint Resolve Conj_right_sub.

Lemma del_to_typ_right_sub: forall Delta A B,
  A =< B ->
  del_to_typ_right A Delta =< del_to_typ_right B Delta.
Proof.
  induction Delta as [| PSigma Delta']; intros; simpl; auto.
  apply IHDelta'.
  clear IHDelta'.
  generalize dependent B.
  generalize dependent A.
  induction PSigma as [| C PSigma']; intros; simpl; auto.
Qed.

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.

Hint Immediate Conj_Conj_right Conj_right_Conj.

Lemma del_to_typ_del_to_typ_right: forall Delta A,
  del_to_typ Delta A =< del_to_typ_right A Delta.
Proof.
  induction Delta as [|Sigma Delta']; auto.
  intros.
  destruct Sigma as [|C Sigma'].
    simpl; auto.
    constructor 2 with (del_to_typ Delta' (A & (<> Conj_right C Sigma'))); [| apply IHDelta'].
    clear IHDelta'.
    simpl.
    remember (<> Conj_right C Sigma') as C'.
    clear HeqC'.
    generalize dependent C'.
    generalize dependent A.
    induction Delta' as [|Sigma2 Delta'']; intros.
    simpl; auto.
    simpl.
    destruct Sigma2 as [|C2 Sigma2']; simpl; auto.
    constructor 2 with ((<> Conj_right C2 Sigma2') & C' & del_to_typ Delta'' (A));
      [| apply sub_weakening_right; auto].
    switch_assoc.
    switch_assoc_right.
    apply sub_weakening_left.
    auto.
Qed.

Lemma del_to_typ_right_del_to_typ: forall Delta A,
  del_to_typ_right A Delta =< del_to_typ Delta A.
Proof.
  induction Delta as [|Sigma Delta']; auto.
  intros.
  destruct Sigma as [|C Sigma'].
    simpl; auto.
    constructor 2 with (del_to_typ Delta' (A & (<> Conj_right C Sigma'))); [apply IHDelta'|].
    clear IHDelta'.
    simpl.
    remember (<> Conj_right C Sigma') as C'.
    clear HeqC'.
    generalize dependent C'.
    generalize dependent A.
    induction Delta' as [|Sigma2 Delta'']; intros.
    simpl; auto.
    simpl.
    destruct Sigma2 as [|C2 Sigma2']; simpl; auto.
    constructor 2 with ((<> Conj_right C2 Sigma2') & C' & del_to_typ Delta'' (A));
      [apply sub_weakening_right; auto |].
    switch_assoc.
    switch_assoc_right.
    apply sub_weakening_left.
    auto.
Qed.

Exchange Conj_right and Conj or del_to_typ and del_to_typ_right.

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

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

The distributivity of function types over intersection types.


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



fun_dist and Conj help to encode this relation.

Lemma fun_dist_extend: forall A B Bs,
  fun_dist A Bs B =< A --> (Conj Bs B).
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)


Following lemmas say that intersection types are commutative.

Lemma Conj_swap: forall t1 t2 A B,
  Conj (t1 ++ B :: t2) A =< Conj (t1 ++ A ::t2) B.
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.

Lemma del_to_typ_swap_in_conv: forall D1 D2 S A,
  del_to_typ (D1++S::D2) A =< del_to_typ (S::D1++D2) A.
Proof.
  induction D1 as [|S2 D1']; intros; auto.
  repeat rewrite <- app_comm_cons.
  destruct S2 as [|C S2'].
  simpl.
  change (del_to_typ_aux S (del_to_typ (D1' ++ D2) A)) with (del_to_typ (S::D1' ++ D2) A).
  auto.
  constructor 2 with (del_to_typ ((C::S2')::S::D1'++D2) A).
  simpl.
  change (del_to_typ_aux S (del_to_typ (D1' ++ D2) A)) with (del_to_typ (S::D1' ++ D2) A).
  apply sub_weakening_right. auto.
  destruct S as [|C' S']; simpl; auto.
  switch_assoc.
  switch_assoc_right.
  auto.
Qed.

Lemma del_to_typ_swap_in_in_conv: forall D S1 S2 C A,
  del_to_typ ((S1++C::S2)::D) A =< del_to_typ ((C::S1++S2)::D) A.
Proof.
  induction S1 as [|S' S1']; intros; auto.
  repeat rewrite <- app_comm_cons.
  simpl.
  apply sub_weakening_left.
  constructor.
  change (Conj_right (C&S') (S1'++S2)) with (Conj_right C (S'::S1'++S2)).
  constructor 2 with (Conj_right C (S1'++S' ::S2)); auto.
Qed.

Lemma del_to_typ_swap_in: forall D1 D2 S A,
  del_to_typ (S::D1++D2) A =< del_to_typ (D1++S::D2) A.
Proof.
  induction D1 as [|S2 D1']; intros; auto.
  repeat rewrite <- app_comm_cons.
  destruct S2 as [|C S2'].
  simpl.
  change (del_to_typ_aux S (del_to_typ (D1' ++ D2) A)) with (del_to_typ (S::D1' ++ D2) A).
  auto.
  constructor 2 with (del_to_typ ((C::S2')::S::D1'++D2) A).
  destruct S as [|C' S']; simpl; auto.
  switch_assoc.
  switch_assoc_right.
  auto.
  simpl.
  change (del_to_typ_aux S (del_to_typ (D1' ++ D2) A)) with (del_to_typ (S::D1' ++ D2) A).
  apply sub_weakening_right. auto.
Qed.

Lemma del_to_typ_swap_in_in: forall D S1 S2 C A,
  del_to_typ ((C::S1++S2)::D) A =< del_to_typ ((S1++C::S2)::D) A.
Proof.
  induction S1 as [|S' S1']; intros; auto.
  repeat rewrite <- app_comm_cons.
  simpl.
  apply sub_weakening_left.
  constructor.
  change (Conj_right (C&S') (S1'++S2)) with (Conj_right C (S'::S1'++S2)).
  constructor 2 with (Conj_right C (S1'++S' ::S2)); auto.
Qed.

Lemma del_to_typ_right_swap_in_conv: forall D1 D2 S A,
  del_to_typ_right A (D1++S::D2) =< del_to_typ_right A (S::D1++D2).
Proof.
  intros.
  switch_left.
  switch_right.
  apply del_to_typ_swap_in_conv.
Qed.

Lemma del_to_typ_right_swap_in_in_conv: forall D S1 S2 C A,
  del_to_typ_right A ((S1++C::S2)::D) =< del_to_typ_right A ((C::S1++S2)::D).
Proof.
  intros.
  switch_left.
  switch_right.
  apply del_to_typ_swap_in_in_conv.
Qed.

Lemma del_to_typ_right_swap_in: forall D1 D2 S A,
  del_to_typ_right A (S::D1++D2) =< del_to_typ_right A (D1++S::D2).
Proof.
  intros.
  switch_left.
  switch_right.
  apply del_to_typ_swap_in.
Qed.

Lemma del_to_typ_right_swap_in_in: forall D S1 S2 C A,
  del_to_typ_right A ((C::S1++S2)::D) =< del_to_typ_right A ((S1++C::S2)::D).
Proof.
  intros.
  switch_left.
  switch_right.
  apply del_to_typ_swap_in_in.
Qed.

Lemma del_to_typ_swap: forall D1 D2 S A B,
  del_to_typ (D1++(B::S)::D2) (<> A) =< del_to_typ (D1++[A]::D2) (<> (Conj_right B S)).
Proof.
  induction D1 as [|P1 D1'].
  Case "D1 = noworld".
  induction D2 as [|P2 D2'].
    SCase "D2 = noworld".
    intros. simpl; auto.
    destruct P2 as [|C P2'].
      SSCase "P2 = empty".
      simpl; auto.
      SSCase "P2 = C::P2'".
      intros; simpl.
      constructor 2 with ((<> Conj_right C P2') & (<> Conj_right B S) & del_to_typ D2' (<> A)).
      switch_assoc.
      switch_assoc_right.
      apply sub_weakening_left; auto.
      constructor 2 with ((<> Conj_right C P2') & (<> A) & del_to_typ D2' (<> Conj_right B S));
        [| switch_assoc; switch_assoc_right; auto].
      apply sub_weakening_right.
      simpl in IHD2'. auto.
  Case "D1 = P1::D1'".
  destruct P1 as [|C P1']; simpl; auto.
Qed.

Lemma del_to_typ_right_swap: forall D1 D2 S A B,
  del_to_typ_right (<> A) (D1++(B::S)::D2) =< del_to_typ_right (<> (Conj_right B S)) (D1++[A]::D2).
Proof.
  intros.
  switch_left; switch_right; apply del_to_typ_swap.
Qed.

Lemma del_to_typ_right_permute: forall D D' A,
  Permutation D D' ->
  del_to_typ_right A D =< del_to_typ_right A D'.
Proof.
  intros D D' A H.
  generalize dependent A.
  induction H; intros; simpl; auto.
  Case "perm_swap".
  apply del_to_typ_right_sub; auto.
  destruct x, y; simpl; auto.
  constructor; auto.
  left_weak; auto.
  Case "perm_trans".
  constructor 2 with (del_to_typ_right A l'); auto.
Qed.

Following tactics facilitate applying the above lemmas.

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

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

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

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

    | _ => idtac
  end.

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

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

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

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

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

More properties of the auxiliary functions


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

Lemma Conj_subseq_weakening: forall l l' A C,
  subseq l l' ->
  Conj l A =< C ->
  Conj l' A =< C.
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 del_to_typ_right_and: forall Delta A B,
  A =< B ->
  del_to_typ_right A Delta =< B.
Proof.
  induction Delta as [| PSigma Delta']; intros; simpl; auto.
  apply IHDelta'.
  clear IHDelta'.
  generalize dependent B.
  generalize dependent A.
  induction PSigma as [| C PSigma']; intros; simpl; auto.
  apply r_trans with A; auto.
Qed.

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.

Lemma del_to_typ_right_middle_subst: forall D1 D2 B1 B2 C1 C2 A B C,
  <> (Conj_right B (B1++B2)) =< <> (Conj_right C (C1++C2)) ->
  del_to_typ_right A (D1++(B1++B::B2)::D2) =< del_to_typ_right A (D1++(C1++C::C2)::D2).
Proof.
  induction D1 as [|PSigma D1'].
  Case "D1 = noworld".
  destruct B1 as [|B' B1']; destruct C1 as [|C' C1']; intros; switch_left; switch_right.
    SCase "B1 = C2 = nil".
    simpl; auto.
    SCase "B1 = nil".
    simpl. apply sub_weakening_left.
    apply (r_trans H).
    constructor. rewrite <- app_comm_cons.
    swap_init_front. auto.
    SCase "B2 = nil".
    simpl. apply sub_weakening_left.
    apply r_trans with ( <> Conj_right B ((B' :: B1') ++ B2)); auto.
    constructor. rewrite <- app_comm_cons.
    swap_init_mid. auto.
    SCase "B1 <> nil & B2 <> nil".
    simpl. apply sub_weakening_left.
    apply r_trans with ( <> Conj_right B ((B' :: B1') ++ B2)).
    constructor. rewrite <- app_comm_cons.
    swap_init_mid. auto.
    apply (r_trans H); auto.
    constructor. rewrite <- app_comm_cons.
    swap_init_front. auto.
  Case "D1 = PSigma :: D1'".
  destruct PSigma as [|P' PSigma'].
    SCase "PSigma = empty".
    simpl. auto.
    SCase "PSigma = P'::PSigma'".
    intros.
    switch_left; switch_right.
    simpl; apply sub_weakening_right.
    switch_left; switch_right.
    auto.
Qed.

Following tactics facilitate applying the above lemmas.

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

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

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

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

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

Lemma Conj_right_pop_out: forall l A B,
  Conj_right A (B :: l) =< B & Conj_right A l.
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 del_to_typ_right_push_in_init: forall D A B,
  A & del_to_typ_right B D =< del_to_typ_right (A&B) D.
Proof.
  induction D as [|PSigma D']; simpl; auto.
  intros.
  destruct PSigma as [|C PSigma']; simpl; auto.
  constructor 2 with (del_to_typ_right (A & B & <> Conj_right C PSigma') D'); auto.
  apply del_to_typ_right_sub.
  switch_assoc. auto.
Qed.

Lemma del_to_typ_right_push_in_init_conv: forall D A B,
  del_to_typ_right (A&B) D =< A & del_to_typ_right B D.
Proof.
  induction D as [|PSigma D']; simpl; auto.
  intros.
  destruct PSigma as [|C PSigma']; simpl; auto.
  constructor 2 with (del_to_typ_right (A & B & <> Conj_right C PSigma') D'); auto.
  apply del_to_typ_right_sub.
  switch_assoc. auto.
Qed.

Lemma Conj_right_push_in_init: forall D A B,
  A & Conj_right B D =< Conj_right (A&B) D.
Proof.
  induction D as [|C D']; simpl; auto.
  intros.
  constructor 2 with (Conj_right (A&(B&C)) D');
    [| apply Conj_right_sub; switch_assoc; auto].
  auto.
Qed.

Lemma Conj_right_push_in_init_conv: forall D A B,
  Conj_right (A&B) D =< A & Conj_right B D.
Proof.
  induction D as [|C D']; simpl; auto.
  intros.
  focus_subst (A & (B&C)); auto.
  switch_assoc; auto.
Qed.

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

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

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

Lemma Conj_right_split_conv: forall G1 G2 A B,
  Conj_right B (G1++A::G2) =< Conj_right B G1 & Conj_right A G2.
Proof.
  intros.
  swap_init_mid.
  switch_left.
  constructor 2 with (Conj G1 B & Conj G2 A); [apply Conj_split_conv|].
  apply sub_conj; auto.
Qed.

Lemma Conj_right_split: forall G1 G2 A B,
  Conj_right A G1 & Conj_right B G2 =< Conj_right A (G1++B::G2).
Proof.
  intros.
  left_subst (Conj G1 A); auto.
  right_subst (Conj G2 B); auto.
  constructor 2 with (Conj (G1 ++ A :: G2) B).
  apply Conj_split.
  switch_left.
  swap_init_mid. auto.
Qed.

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

Lemma conj_right_fold : forall L1 L2 A,
  Conj_right (Conj_right A L1) L2 =< Conj_right A (L2 ++ L1).
Proof.
  induction L1 as [|C L1'].
  intros; simpl_list; auto.
  intros.
  move_mid_to_front_right.
  simpl; auto.
Qed.

del_to_typ_right skips an empty local subtyping context.

Lemma delta_simpl: forall n D A,
  del_to_typ_right A (n_list n empty ++ D) =< del_to_typ_right A D.
Proof.
  induction n as [| n']; simpl; auto.
Qed.

Lemma delta_unsimpl: forall n A,
  A =< del_to_typ_right A (n_list n empty).
Proof.
  induction n as [| n']; simpl; auto.
Qed.

Lemma delta_unsimpl2: forall n D A,
  del_to_typ_right A D =< del_to_typ_right A (n_list n empty ++ D).
Proof.
  induction n as [| n']; simpl; 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 two lemmas exploit the rule r_box_T.

Lemma Conj_sub_box_T: forall l A,
  Conj (map typ_box l) A =< Conj l A.
Proof.
  induction l; intros; auto.
  simpl. constructor 2 with (a & Conj (map typ_box l) A); auto.
Qed.

Hint Immediate Conj_sub_box_T.

Lemma Conj_right_box_T2 : forall A L1 L2,
  Conj_right A (map typ_box L1 ++ L2) =< Conj_right A (L1 ++ L2).
Proof.
  intros.
  switch_right.
  switch_left.
  generalize dependent L2.
  generalize dependent A.
  induction L1 as [| B L1']; intros; auto.
  simpl; apply sub_conj; auto.
Qed.

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

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


Lemma del_to_typ_right_box_split : forall Delta1 Delta2 Sigma1 Sigma2 A C,
  del_to_typ_right A (Delta1 ++ (Sigma1 ++ ([]C) :: Sigma2) :: Delta2) =<
  del_to_typ_right A (Delta1 ++ [[]C] :: (Sigma1 ++ Sigma2) :: Delta2).
Proof.
  intros.
  move_mid_to_front.
  move_mid_to_front.
  move_mid_to_front_right.
  remember (Sigma1 ++ Sigma2) as PSigma; clear HeqPSigma.
  simpl.
  move_mid_to_front_right.
  destruct PSigma as [|D PSigma']; auto.
  simpl. apply del_to_typ_right_sub.
  constructor; auto.
  constructor 2 with (<> Conj_right (([]C) & D) PSigma'); auto.
Qed.

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

A & B =< A & <>B
Lemma del_to_typ_right_sig_to_del: forall D G S A,
  del_to_typ_right (Conj_right A (G++S)) D =< del_to_typ_right (Conj_right A G) (S::D).
Proof.
  intros.
  destruct S as [| C S'].
  rewrite app_nil_r. simpl; auto.
  focus_subst (Conj_right A G & <> Conj_right C S').
  constructor 2 with (Conj_right A G & Conj_right C S'); auto; apply Conj_right_split_conv.
  push_del_to_typ_right. auto.
Qed.

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

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

Lemma del_to_typ_right_box_k: forall D G A,
  del_to_typ_right (Conj_right ([]A) (map typ_box G)) D =< [] del_to_typ_right (Conj_right ([]A) (map typ_box G)) D.
Proof.
  intros.
  focus_subst ([] (Conj_right ([]A) (map typ_box G))).
  apply Conj_right_box_k.
  constructor 2 with ([]del_to_typ_right ([] (Conj_right ([]A) (map typ_box G))) D);
    [| constructor; apply del_to_typ_right_sub; auto].
  remember (Conj_right ([]A) (map typ_box G)) as C.
  clear HeqC.
  generalize dependent C.
  induction D as [| PSigma D'].
  simpl; auto.
  intros; simpl.
  focus_subst ([] (del_to_typ_right_aux ([]C) PSigma)).
  destruct PSigma as [|D PSigma']; simpl; auto.
  right_subst ([] <> Conj_right D PSigma'); auto.
  left_subst ([] [] C); auto.
  (* *)
  constructor 2 with ([] del_to_typ_right ([]del_to_typ_right_aux ([]C) PSigma) D'); auto.
  constructor.
  apply del_to_typ_right_sub; auto.
Qed.

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

Lemma del_to_typ_right_box_k2: forall D A,
  del_to_typ_right (<>A) D =< [] del_to_typ_right (<> A) D.
Proof.
  induction D as [| PSigma D'].
  simpl; auto.
  intros; simpl.
  focus_subst (<> (del_to_typ_right_aux (<>A) PSigma)).
  destruct PSigma as [|D PSigma']; simpl; auto.
  constructor 2 with ([] del_to_typ_right (<>del_to_typ_right_aux (<>A) PSigma) D'); auto.
  constructor.
  apply del_to_typ_right_sub; auto.
  destruct PSigma as [|D PSigma']; simpl; auto.
  constructor.
  constructor 2 with (<><>A); auto.
  constructor 2 with (<> <> Conj_right D PSigma'); auto.
Qed.

Following lemma relates to the rule r_box_dia_K.

Abstract derivation:
  A & <>B =< C

      ...

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

      ...

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


Lemma del_to_typ_right_dia_tran : forall D A C,
  del_to_typ_right A D =< C ->
  del_to_typ_right (<> A) D =< <> C.
Proof.
  induction D as [|PSigma D']; intros.
  simpl; auto.
  destruct PSigma as [|P PSigma'].
  simpl; auto.
  simpl.
  constructor 2 with (<>A & del_to_typ_right (<> Conj_right P PSigma') D');
    [ apply del_to_typ_right_push_in_init_conv| ].
  right_subst ([] del_to_typ_right (<> Conj_right P PSigma') D');
  [apply del_to_typ_right_box_k2 |].
  swap_and.
  apply r_box_dia_K.
  swap_and.
  right_subst (del_to_typ_right (<> Conj_right P PSigma') D'); auto.
  constructor 2 with (del_to_typ_right (A & <> Conj_right P PSigma') D');
    [ apply del_to_typ_right_push_in_init| ].
  push_del_to_typ_right.
  assumption.
Qed.

Following lemma relates to the rule r_box_dia_K.

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


Lemma del_to_typ_right_dia_tran2 : forall G A,
  Conj_right (<>A) (map typ_box G) =< <> Conj_right A (map typ_box G).
Proof.
  induction G; intros; simpl; auto.
  constructor 2 with (<> A & (Conj_right ([] a) (map typ_box G)));
    [apply Conj_right_push_in_init_conv |].
  right_subst ([] Conj_right ([] a) (map typ_box G));
  [apply Conj_right_box_k |].
  swap_and.
  apply r_box_dia_K.
  swap_and.
  right_subst (Conj_right ([] a) (map typ_box G)); auto.
  apply Conj_right_push_in_init.
Qed.

We can rearrange the order of function applications.

Lemma del_to_typ_right_Conj_right : forall G D A,
  del_to_typ_right (Conj_right A G) D =< Conj_right (del_to_typ_right A D) G.
Proof.
  induction G as [|C G']; auto.
  intros.
  simpl.
  constructor 2 with (Conj_right (del_to_typ_right (A&C) D) G'); auto.
  apply Conj_right_sub; auto.
  constructor; auto using del_to_typ_right_sub, del_to_typ_right_and.
Qed.

Lemma Conj_right_del_to_typ_right : forall G D A,
  Conj_right (del_to_typ_right A D) G =< del_to_typ_right (Conj_right A G) D.
Proof.
  induction G as [|C G']; auto.
  intros.
  simpl.
  constructor 2 with (Conj_right (del_to_typ_right (A&C) D) G'); auto.
  apply Conj_right_sub; auto.
  clear IHG'.
  generalize dependent C.
  generalize dependent A.
  induction D as [|PSigma D'].
  intros; simpl; auto.
  intros; simpl.
  constructor 2 with (del_to_typ_right (del_to_typ_right_aux A PSigma & C) D'); auto.
  apply del_to_typ_right_sub.
  clear IHD'.
  destruct PSigma as [|D PSigma']; auto.
  simpl.
  constructor 2 with (C & (A & <> Conj_right D PSigma')); auto.
  switch_assoc.
  constructor; auto.
  left_weak; auto.
Qed.

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

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

Lemmas for the judgmental subtyping system


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

Lemma size_env_split: forall L1 L2,
  size_env (L1 ++ L2) = size_env L1 + size_env L2.
Proof.
  induction L1; intros; simpl; auto.
  rewrite IHL1.
  omega.
Qed.

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.

Lemma n_list_split: forall n1 n2,
  n_list n1 empty ++ n_list n2 empty = n_list (n1+n2) empty.
Proof.
  induction n1 as [| n1']; simpl; auto.
  intros. f_equal. auto.
Qed.

Lemmas for case analysis on the remote node context

For any remote node context, a) it may consist of empty local typing contexts, or b) it may contain at least one non-empty local typing context.
Lemma delta_dec : forall Delta,
  (exists n, Delta = n_list n empty) \/
  (exists n, exists A, exists PSigma, exists Delta',
    Delta = n_list n empty ++ (A::PSigma)::Delta').
Proof.
  induction Delta as [|PSigma Delta'].
  Case "Delta = noworld".
  left; exists 0. reflexivity.
  Case "Delta = PSigma :: Delta'".
  destruct PSigma as [|C PSigma'].
    SCase "PSigma = nil".
    destruct IHDelta'.
      destruct H as [n H].
      left; exists (S n); subst; auto.
      destruct H as [n [A [PSigma [Delta_tail H]]]].
      right; exists (S n), A, PSigma, Delta_tail; subst; auto.
    SCase "PSigma = C::PSigma'".
    destruct IHDelta'.
      destruct H as [n H].
      right; exists 0, C, PSigma', Delta'; subst; auto.
      destruct H as [n [A [PSigma [Delta_tail H]]]].
      right; exists 0, C, PSigma', Delta'; subst; auto.
Qed.

If l1++l2 is a list of empty lists, both l1 and l2 are also lists of empty lists.
Lemma n_list_empty_eq_split: forall n l1 l2,
  l1 ++ l2 = n_list n empty ->
  exists n1, exists n2, n = n1 + n2 /\ l1 = n_list n1 empty /\ l2 = n_list n2 empty.
Proof.
  induction n as [| n']; simpl; intros.
  destruct (app_eq_nil _ _ H); subst.
  exists 0, 0; auto.
  destruct l1 as [| a l1'].
  Case "l1 = noworld".
  destruct l2 as [| b l2'].
    SCase "l2 = noworld".
    inversion H.
    SCase "l2 = b::l2'".
    inversion H.
    rewrite <- app_nil_l in H2 at 1.
    destruct (IHn' _ _ H2) as [n1 [n2 [Hn' [Hl1 Hl2]]]].
    subst.
    exists 0, (S (n1 + n2)); intuition.
  Case "l1 = a :: l1'".
  inversion H.
  destruct (IHn' _ _ H2) as [n1 [n2 [Hn' [Hl1 Hl2]]]].
  subst.
  exists (S n1), n2; intuition.
Qed.

We can write the similar lemma using Permutation.
Lemma n_list_empty_permute_split: forall n D1 D2,
  Permutation (D1++D2) (n_list n empty) ->
  exists n1, exists n2, n = n1 + n2 /\ D1 = n_list n1 empty /\ D2 = n_list n2 empty.
Proof.
  induction n as [| n']; simpl; intros.
  apply Permutation_sym in H.
  apply Permutation_nil in H.
  destruct (app_eq_nil _ _ H); subst.
  exists 0, 0; auto.
  assert (In empty (D1 ++ D2)).
  apply Permutation_in with (empty ::n_list n' empty); auto with v62.
  apply Permutation_sym; assumption.
  destruct (in_app_or _ _ _ H0).
  Case "In empty D1".
  destruct_in H1.
  rewrite <- app_assoc in H.
  rewrite <- app_comm_cons in H.
  apply Permutation_sym in H; apply Permutation_cons_app_inv in H; apply Permutation_sym in H.
  rewrite app_assoc in H.
  destruct (IHn' _ _ H) as [n1 [n2 [Hn' [HD1 HD2]]]]. subst.
  exists (S n1), n2; intuition; auto.
  destruct (n_list_empty_eq_split _ _ _ HD1) as [nl1 [nl2 [Hneq [Hl1 Hl2]]]].
  subst.
  change (empty::n_list nl2 empty) with (n_list (S nl2) empty).
  rewrite n_list_split.
  f_equal; auto with v62.
  Case "In empty D2".
  destruct_in H1.
  rewrite app_assoc in H.
  apply Permutation_sym in H; apply Permutation_cons_app_inv in H; apply Permutation_sym in H.
  rewrite <- app_assoc in H.
  destruct (IHn' _ _ H) as [n1 [n2 [Hn' [HD1 HD2]]]]. subst.
  exists n1, (S n2); intuition; auto.
  destruct (n_list_empty_eq_split _ _ _ HD2) as [nl1 [nl2 [Hneq [Hl1 Hl2]]]].
  subst.
  change (empty::n_list nl2 empty) with (n_list (S nl2) empty).
  rewrite n_list_split.
  f_equal; auto with v62.
Qed.

Not all of subtyping contexts are empty.


At least one of the subtyping contexts must contain a type.
Lemma context_is_not_nil_gen: forall A_dummy Delta Gamma Sigma A,
  Delta;; Gamma; Sigma ~< A ->
  forall n,
    A = A_dummy ->
    Delta = n_list n empty ->
    Gamma = empty ->
    Sigma = empty ->
    False.
Proof.
  (typ_cases (induction A_dummy) Case);
  (j_sub_cases (induction 1) SCase); intros; repeat
  match goal with
  | H: _ ++ _ :: _ = empty |- _ => symmetry in H; contradict H; apply app_cons_not_nil
  | H: _ ++ _ :: _ = n_list _ empty |- _ => destruct (n_list_empty_eq_split _ _ _ H) as [n1 [n2 [Hn1n2 [Hsplit1 Hsplit2]]]];
    destruct n2; simpl in Hsplit2; inversion Hsplit2
  | H: subseq _ nil |- _ => inv H
  | _ => simpl in *; try intuition; try discriminate; subst; try rewrite n_list_split in H0; eauto 2
  end.
  SCase "j_fun".
  inv H3. apply IHA_dummy2 with noworld empty empty A_dummy2 O; auto.
  SCase "j_and_r".
  inv H1. eauto.
  SCase "j_box_r".
  inv H1. clear IHj_sub.
  simple eapply IHA_dummy; eauto.
  instantiate (1:=n+1).
  destruct (n_list_empty_eq_split _ _ _ H2) as [n1 [n2 [? [? ?]]]]; subst.
  change (empty :: n_list n2 empty) with (n_list (S n2) empty); rewrite n_list_split.
  f_equal; ring_simplify; reflexivity.
  SCase "j_dia_r".
  inv H0. eauto.
  SCase "j_dia_r'".
  inv H0. eauto.
Qed.

Lemma context_is_not_nil: forall A,
  ~ (noworld;; empty ; empty ~< A).
Proof.
  intros. change noworld with (n_list O empty); intro.
  eapply context_is_not_nil_gen; eauto.
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 (Delta:worlds) (Gamma Sigma Sigma':env), Delta;; Gamma; Sigma ++ A :: Sigma' ~< A) /\
  (forall (Delta:worlds) (Gamma Gamma' Sigma:env), Delta;; Gamma ++ A :: Gamma'; Sigma ~< A).
Proof.
  (typ_cases (induction A) Case); (split; [SCase "lsub" | SCase "vsub"]); intros; auto.
  Case "typ_arrow".
  SCase "lsub".
  constructor 3 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 3 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 10 with Gamma nil; auto with v62.
  constructor 11 with Delta nil; auto with v62; intuition.
  SCase "vsub".
  constructor.
  constructor 11 with Delta nil; auto with v62; intuition.
  Case "typ_dia".
  SCase "lsub".
  constructor 14 with Delta nil; auto with v62.
  constructor.
  change [A] with (empty ++ [A]). intuition.
  SCase "vsub".
  constructor 13 with Delta nil; auto with v62.
  constructor.
  change [A] with (empty ++ [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.

Context permutation


Hint Resolve (@permute_app_middle typ) (@permute_app_middle env).

We assume that the contexts are unordered.

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

Lemma permute_pickFun : forall Sigma Sigma',
  Permutation Sigma Sigma' ->
  Permutation (pickFun Sigma) (pickFun Sigma').
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. 
As the global context is a list of lists, each element of it itself can be permuted.
Hence, we introduce a new predicate WPermutation to catch this nature.
We refer readers to wpermute.v for the definition of it.
*)


Lemma permute_j_sub : forall (Delta:worlds) (Gamma Sigma:env) (A:typ),
  Delta;; Gamma ; Sigma ~< A ->
  forall (Delta':worlds) (Gamma' Sigma':env),
    WPermutation Delta Delta' ->
    Permutation Gamma Gamma' ->
    Permutation Sigma Sigma' ->
    Delta';; Gamma'; Sigma' ~< A.
Proof.
  (j_sub_cases (induction 1) Case); intros; subst; repeat
    match goal with
    | H: Permutation (_ ++ _ :: _) _ |- _ => destruct_permute H
    | H: Permutation (?r :: ?rs) _ |- _ => rewrite <- app_nil_l with _ (r::rs) in H; destruct_permute H; simpl in *
    | H: WPermutation (_ ++ _ :: _) _ |- _ => destruct_wpermute H
    end; auto; try solve
    [ econstructor; eauto; apply IHj_sub; eauto with v62
    | try rewrite <- app_nil_l with _ Delta';
      try rewrite <- app_nil_l with _ Gamma';
      econstructor; eauto; apply IHj_sub; eauto with v62
    ].
  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 3 with Sigma''; auto.
    SCase "arg types".
    intros. apply H0; auto. revert H6. apply Permutation_in. apply Permutation_map. apply Permutation_sym. assumption.
    SCase "result types".
    apply IHj_sub; auto. apply Permutation_map; assumption.
  Case "j_box_l".
  apply j_box_l with nil Gamma'; auto.
Qed.

Weakening

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

Lemma weakening_cons: forall (Delta:worlds) (Gamma Sigma:env) (A:typ),
  Delta;; Gamma; Sigma ~< A ->
  forall (C:typ),
    Delta;; Gamma; C :: Sigma ~< A /\
    Delta;; C::Gamma; Sigma ~< A /\
    forall (Delta':worlds) (Sigma':env),
      Permutation Delta (Sigma' :: Delta') ->
      (C::Sigma')::Delta';; Gamma; Sigma ~< A.
Proof.
  (j_sub_cases (induction 1) Case); intros; (split; [SCase "Sigma" | split; [SCase "Gamma" | SCase "Delta"]]); intros;
  match goal with
  | H: Permutation (?G1 ++ ?S1 :: ?G2) (?S2 :: ?G) |- _ =>
    destruct (list_eq_dec typ_dec S1 S2);
      [ SSCase "S1 = S2"; subst; apply Permutation_sym in H; apply Permutation_cons_app_inv in H; apply Permutation_sym in H
      | SSCase "S1 <> S2"; assert (In S1 G) as Hin;
        [ apply Permutation_in with (x := S1) 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 := S1) in H ]
      ]
  | _ => idtac
  end;
  match goal with
  | |- j_sub (?A::?G) _ _ _ => rewrite <- app_nil_l with _ (A::G)
  | _ => idtac
  end;
  try rewrite app_comm_cons; subst; try solve
    [ (try constructor; firstorder)
    | econstructor; eauto; simpl; apply IHj_sub; firstorder
      try repeat apply Permutation_app_cons; try (rewrite app_comm_cons; repeat apply permute_app_middle); assumption
    | simpl; change ((C :: Sigma') :: Delta') with ([C :: Sigma'] ++ Delta');
      clear H; econstructor; eauto; apply IHj_sub; auto with v62
    ].
  Case "j_fun".
    SCase "Sigma".
    constructor 3 with Sigma'; auto.
      apply (subseq_tran H); destruct C; simpl; auto with v62.
    SCase "Gamma".
    constructor 3 with Sigma'; auto.
      apply (subseq_tran H); destruct C; simpl; auto with v62.
  Case "j_box_lc".
    SCase "Gamma".
    apply j_box_lc with (C::Gamma1) Gamma2; [| rewrite <- app_comm_cons; subst; auto]. apply IHj_sub.
  Case "j_box_l".
    SCase "Gamma".
    apply j_box_l with (C::Gamma1) Gamma2; subst; firstorder.
  Case "j_box_r".
    SCase "Sigma".
    apply j_box_r with Delta1 Delta2; auto with v62.
    apply permute_j_sub with ((C::Sigma)::Delta1++Delta2) Gamma empty; auto with v62.
    apply IHj_sub; perm_refl.
  Case "j_dia_r".
    SCase "Sigma".
    apply j_dia_r.
    apply permute_j_sub with ((C::Sigma)::Delta1++Delta2) Gamma Sigma'; auto with v62.
    apply IHj_sub; perm_refl.
    SCase "Delta".
    apply j_dia_r.
    apply permute_j_sub with (Delta1++Sigma::Delta2) Gamma (C::Sigma'0); auto with v62.
    apply IHj_sub.
Qed.

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

Lemma weakening_cons_lcc: forall (Delta:worlds) (Gamma Sigma:env) (A:typ),
  Delta;; Gamma; Sigma ~< A ->
  forall (Sigma':env),
    Sigma'::Delta;; Gamma; Sigma ~< A.
Proof.
  (j_sub_cases (induction 1) Case); intros; subst; try solve
    [ econstructor; eauto; firstorder
    | rewrite app_comm_cons; clear H; econstructor; eauto; apply IHj_sub
    ].
Qed.

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

Lemma weakening_gen_l: forall (Delta:worlds) (Gamma Sigma Sigma' : env) (A C : typ),
  Delta;; Gamma; Sigma ++ Sigma' ~< A ->
  Delta;; Gamma; Sigma ++ C :: Sigma' ~< A.
Proof.
  intros.
  apply permute_j_sub with Delta Gamma (C::Sigma++Sigma'); perm_refl; [| apply WPermutation_refl].
  apply weakening_cons; assumption.
Qed.

Lemma weakening_gen_v: forall (Delta:worlds) (Gamma Gamma' Sigma : env) (A C : typ),
  Delta;; Gamma ++ Gamma'; Sigma ~< A ->
  Delta;; Gamma ++ C :: Gamma'; Sigma ~< A.
Proof.
  intros.
  apply permute_j_sub with Delta (C::Gamma++Gamma') Sigma; perm_refl; [| apply WPermutation_refl].
  apply weakening_cons; assumption.
Qed.

Lemma weakening_gen_lc: forall (Delta Delta':worlds) (PSigma PSigma':env) (Gamma Sigma : env) (A C : typ),
  Delta ++ (PSigma ++ PSigma') :: Delta';; Gamma; Sigma ~< A ->
  Delta ++ (PSigma ++ C :: PSigma') :: Delta';; Gamma; Sigma ~< A.
Proof.
  intros.
  apply permute_j_sub with ((C::PSigma++PSigma')::Delta ++ Delta') Gamma Sigma; auto with v62.
  eapply weakening_cons; eauto with v62.
Qed.

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

Lemma weakening_gen_lcc: forall (Delta1 Delta2:worlds) (Gamma Sigma' Sigma:env) (A:typ),
  Delta1 ++ Delta2;; Gamma; Sigma ~< A ->
  Delta1 ++ Sigma' :: Delta2;; Gamma; Sigma ~< A.
Proof.
  intros.
  apply permute_j_sub with (Sigma'::Delta1++Delta2) Gamma Sigma; auto with v62.
  apply weakening_cons_lcc; auto.
Qed.

Hint Immediate weakening_gen_lcc weakening_gen_l weakening_gen_v weakening_gen_lc.

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

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

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

Hint Immediate weakening_bunch_l weakening_bunch_l'.

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

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

Hint Immediate weakening_bunch_v weakening_bunch_v' .

Lemma weakening_bunch_lc: forall (PSigma:env) (Delta Delta':worlds) (PSigma' Gamma Sigma : env) (A : typ),
  Delta ++ PSigma' :: Delta';; Gamma; Sigma ~< A ->
  Delta ++ (PSigma ++ PSigma') :: Delta';; Gamma; Sigma ~< A.
Proof.
  induction PSigma as [|C PSigma'']; intros; auto.
  simpl.
  rewrite <- app_nil_l with _ (C::PSigma''++PSigma').
  apply weakening_gen_lc.
  simpl; auto.
Qed.

Lemma weakening_bunch_lc': forall (PSigma:env) (Delta Delta':worlds) (PSigma' Gamma Sigma : env) (A : typ),
  Delta ++ PSigma' :: Delta';; Gamma; Sigma ~< A ->
  Delta ++ (PSigma' ++ PSigma) :: Delta';; Gamma; Sigma ~< A.
Proof.
  intros.
  apply permute_j_sub with (Delta ++ (PSigma++PSigma')::Delta') Gamma Sigma; auto with v62.
  apply weakening_bunch_lc; assumption.
  apply WPermutation_app_mid; auto with v62; perm_refl.
Qed.

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


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

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

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

(* 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 Delta Gamma Sigma C, Delta;; Gamma; Sigma ~< C ->
      (forall Sigma',
        Sigma = A :: Sigma' ->
        Delta;; A :: Gamma; Sigma' ~< C) /\
      (forall (Delta':worlds) (PSigma:env),
        Permutation Delta ((A::PSigma)::Delta') ->
        PSigma::Delta';; A::Gamma; Sigma ~< C).

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

Lemma move_from_sig_to_gam_cons_on_typ_aux: forall A,
  move_from_sig_to_gam_IH_on_typ (size_typ A) ->
  forall Delta Gamma Sigma C, Delta;; Gamma; Sigma ~< C ->
    (forall Sigma',
      Sigma = A :: Sigma' ->
      Delta;; A :: Gamma; Sigma' ~< C) /\
    (forall (Delta':worlds) (PSigma:env),
      Permutation Delta ((A::PSigma)::Delta') ->
      PSigma::Delta';; A::Gamma; Sigma ~< C).
Proof.
  intros A IHA.
  (j_sub_cases (induction 1) Case); intros; (split; [SCase "Sigma" | SCase "Delta"]); intros; subst; simpl in *; auto;
  repeat match goal with
  | H: ?G ++ _ = _ :: _ |- _ => destruct G; inv H
  | H: Permutation (?G1 ++ ?S1 :: ?G2) (?S2 :: ?G) |- _ =>
    destruct (list_eq_dec typ_dec S1 S2) as [Heq | Heq];
      [ SSCase "S1 = S2"; rewrite Heq in H; apply Permutation_sym in H; apply Permutation_cons_app_inv in H; apply Permutation_sym in H
      | SSCase "S1 <> S2"; assert (In S1 G) as Hin;
        [ apply Permutation_in with (x := S1) in H; auto with v62; simpl in H; destruct H as [Ha|?]; [inversion Ha; congruence | assumption]
        | destruct_in Hin; rewrite app_comm_cons in *; apply Permutation_app_inv with (a := S1) in H ]
      ]
  end;
  match goal with
  | |- j_sub (?A::?D) (?B::?G) _ _ => rewrite <- app_nil_l with _ (A::D)
  | _ => idtac
  end;
  try repeat rewrite app_comm_cons; try solve
    [ constructor; firstorder
    | firstorder
    | econstructor; eauto; simpl; apply IHj_sub; auto with v62; firstorder
      try repeat apply Permutation_app_cons; try (rewrite app_comm_cons; repeat apply permute_app_middle); assumption
    | change ((A :: B :: Sigma') :: Delta') with ([A :: B :: Sigma'] ++ Delta');
      clear H; econstructor; eauto;
      simpl; apply IHj_sub;
        match goal with
        | |- Permutation _ (?A::?B::?C) => apply Permutation_trans with (B::A::C); perm_refl; simpl; apply Permutation_app_cons; assumption
        end
    | change (noworld++PSigma::Delta') with ([PSigma]++Delta');
      econstructor; eauto; simpl; apply IHj_sub; apply Permutation_app_cons_cons; assumption
    ];
  (* Half of remaining cases *)
  match goal with
  | |- j_sub _ (?B::?G) _ _ => rewrite <- app_nil_l with _ (B::G)
  | |- j_sub _ ((?B::?G1)++?G2) _ _ => rewrite <- app_comm_cons; rewrite <- app_nil_l with _ (B::G1++G2)
  | _ => idtac
  end;
  try solve
    [ econstructor; eauto; try apply (permute_j_sub H); simpl; perm_refl; auto with v62 ].
  Case "j_fun".
    SCase "Sigma".
    (* A is not function type *)
    destruct A; try solve [(constructor 3 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 3 with Sigma''; auto.
      SSCase "arg types".
      intros. apply H0. revert H5. apply Permutation_in. apply Permutation_sym. apply Permutation_map. assumption.
      SSCase "result types".
      apply (permute_j_sub H2); try apply Permutation_map; auto.
    SCase "Delta".
    constructor 3 with Sigma'; auto.
      SSCase "subseq".
      apply (subseq_tran H); destruct A; simpl; auto with v62.
  Case "j_and_lc".
    SCase "Delta".
    constructor. simpl.
    apply permute_j_sub with (PSigma::Delta') (t2::t1::Gamma) Sigma; auto using WPermutation_refl; perm_refl.
    eapply (IHA t2); simpl; auto with arith.
    eapply (IHA t1); simpl; auto with arith.
    apply (permute_j_sub H); auto with v62.
  Case "j_and_l".
  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 Delta Gamma (t1::t2::Sigma'); auto with v62; perm_refl.
  Case "j_box_r".
    SCase "Sigma".
    apply j_box_r with Delta1 Delta2; auto.
    apply permute_j_sub with (Sigma'::Delta1++Delta2) (A::Gamma) empty; auto;
      [ apply IHj_sub; auto; perm_refl
        | apply WPermutation_cons_app; auto using WPermutation_refl
      ].
  Case "j_dia_lc".
    apply j_dia_v with noworld (PSigma::Delta'); auto.
    apply (permute_j_sub H); simpl; perm_refl; auto with v62.
  Case "j_dia_r".
    SCase "Sigma".
    constructor.
    apply permute_j_sub with (Sigma'0::Delta1++Delta2) (A::Gamma) Sigma'; auto with v62.
    apply IHj_sub; auto with v62.
    SCase "Delta".
    constructor.
    apply permute_j_sub with (Delta1++Sigma::Delta2) (A::Gamma) PSigma; auto with v62.
    apply IHj_sub; auto with v62.
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 Delta Gamma Sigma C, Delta;; Gamma; Sigma ~< C ->
    (forall Sigma',
      Sigma = A :: Sigma' ->
      Delta;; A :: Gamma; Sigma' ~< C) /\
    (forall (Delta':worlds) (PSigma:env),
      Permutation Delta ((A::PSigma)::Delta') ->
      PSigma::Delta';; A::Gamma; Sigma ~< C).
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 Delta Gamma Sigma C, Delta;; Gamma; Sigma ~< C ->
    (forall Sigma',
      Sigma = A :: Sigma' ->
      Delta;; A :: Gamma; Sigma' ~< C) /\
    (forall (Delta':worlds) (PSigma:env),
      Permutation Delta ((A::PSigma)::Delta') ->
      PSigma::Delta';; A::Gamma; Sigma ~< C).
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, j_and_lc, and j_and_v are invertible.


Lemma j_and_l_lc_inv_cons: forall Delta Gamma Sigma C,
  Delta;; Gamma; Sigma ~< C ->
  (forall Sigma0 A B,
    Sigma = (A & B) :: Sigma0 ->
    Delta;; Gamma; A :: B :: Sigma0 ~< C) /\
  (forall Delta' Sigma' A B,
    Permutation Delta (((A & B)::Sigma') :: Delta') ->
    (A::B::Sigma')::Delta';; Gamma; Sigma ~< C).
Proof.
  (j_sub_cases (induction 1) Case); intros; (split; [SCase "Sigma" | SCase "Delta"]); intros; subst; simpl in *; auto;
  repeat match goal with
  | H: ?G ++ _ = _ :: _ |- _ => destruct G; inv H
  | H: Permutation (?G1 ++ ?S1 :: ?G2) (?S2 :: ?G) |- _ =>
    destruct (list_eq_dec typ_dec S1 S2) as [Heq | Heq];
      [ SSCase "S1 = S2"; rewrite Heq in H; apply Permutation_sym in H; apply Permutation_cons_app_inv in H; apply Permutation_sym in H
      | SSCase "S1 <> S2"; assert (In S1 G) as Hin;
        [ apply Permutation_in with (x := S1) in H; auto with v62; simpl in H; destruct H as [Ha|?]; [inversion Ha; congruence | assumption]
        | destruct_in Hin; rewrite app_comm_cons in *; apply Permutation_app_inv with (a := S1) in H ]
      ]
  end;
  match goal with
  | |- j_sub (?A::?G) _ _ _ => rewrite <- app_nil_l with _ (A::G)
  | _ => idtac
  end;
  try repeat rewrite app_comm_cons; try solve
    [ simpl; constructor; firstorder
    | firstorder
    | econstructor; eauto; simpl; apply IHj_sub; firstorder
      try repeat apply Permutation_app_cons; try (rewrite app_comm_cons; repeat apply permute_app_middle); assumption
    | simpl; change ((A :: B :: Sigma') :: Delta') with ([A :: B :: Sigma'] ++ Delta');
      clear H; econstructor; eauto;
      simpl; apply IHj_sub;
        match goal with
        | |- Permutation _ (?A::?B::?C) => apply Permutation_trans with (B::A::C); perm_refl; simpl; apply Permutation_app_cons; assumption
        end
    ].
  Case "j_fun".
  apply j_fun with Sigma'; auto.
  apply (subseq_tran H); destruct A, B; simpl; auto with v62.
  Case "j_and_lc".
    SCase "Delta".
    simpl in *.
    apply (permute_j_sub H); auto with v62.
  Case "j_box_r".
    SCase "Sigma".
    clear H; econstructor; eauto.
    apply permute_j_sub with ((A::B::Sigma0)::Delta1++Delta2) Gamma empty; auto with v62.
    apply IHj_sub; perm_refl.
  Case "j_dia_r".
    SCase "Sigma".
    econstructor; eauto.
    apply permute_j_sub with ((A::B::Sigma0)::Delta1++Delta2) Gamma Sigma'; auto with v62.
    apply IHj_sub; perm_refl.
    SCase "Delta".
    constructor.
    apply permute_j_sub with (Delta1 ++ Sigma :: Delta2) Gamma (A::B::Sigma'0); auto with v62.
    apply IHj_sub; assumption.
Qed.

Lemma j_and_l_inv: forall Delta Gamma Sigma Sigma' A B C,
  Delta;; Gamma; Sigma ++ (A & B) :: Sigma' ~< C ->
  Delta;; Gamma; Sigma ++ A :: B :: Sigma' ~< C.
Proof.
  intros.
  apply permute_j_sub with Delta Gamma (A::B::Sigma ++ Sigma'); try perm_refl; [| apply WPermutation_refl].
  apply permute_j_sub with (Delta:=Delta) (Gamma:=Gamma) (Sigma:=Sigma ++(A&B):: Sigma') (Delta':=Delta) (Gamma':=Gamma) (Sigma':=(A&B)::Sigma ++ Sigma') in H; try perm_refl; [|apply WPermutation_refl].
  eapply j_and_l_lc_inv_cons; eauto.
Qed.

Lemma j_and_lc_inv: forall Delta Delta' PSigma PSigma' Gamma Sigma A B C,
  Delta ++ (PSigma ++ (A & B) :: PSigma') :: Delta';; Gamma; Sigma ~< C ->
  Delta ++ (PSigma ++ A :: B :: PSigma') :: Delta';; Gamma; Sigma ~< C.
Proof.
  intros.
  apply permute_j_sub with ((A::B::PSigma ++ PSigma')::Delta++Delta') Gamma Sigma; try perm_refl;
    [| apply WPermutation_cons_app; [apply WPermutation_refl | perm_refl]].
  apply permute_j_sub with (Delta:=Delta++(PSigma++(A & B)::PSigma')::Delta') (Gamma:=Gamma) (Sigma:=Sigma)
    (Delta':=((A&B)::PSigma++PSigma')::Delta++Delta') (Gamma':=Gamma) (Sigma':=Sigma) in H; try perm_refl;
      [| apply WPermutation_app_cons; [apply WPermutation_refl | perm_refl]].
  eapply (j_and_l_lc_inv_cons); eauto.
Qed.

Hint Resolve j_and_l_inv j_and_lc_inv.

Lemma j_and_v_inv_cons: forall Delta Gamma Sigma C,
  Delta;; Gamma; Sigma ~< C ->
  forall Gamma0 A B,
    Permutation Gamma ((A&B) :: Gamma0) ->
    Delta;; A :: B :: Gamma0; Sigma ~< C.
Proof.
  (j_sub_cases (induction 1) 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 IHj_sub; rewrite app_comm_cons; auto
    | try apply (permute_j_sub H);
      auto using WPermutation_refl; apply Permutation_sym; repeat apply Permutation_cons_app;
      apply Permutation_cons_app_inv with (A&B); apply Permutation_sym; assumption
    | subst; change (A::B::Gamma0) with ([A, B]++Gamma0); clear H; econstructor; eauto;
      simpl; apply IHj_sub; auto with v62
    ].
  Case "j_fun".
  apply permute_pickFun in H3; simpl in H3.
  pose proof (Permutation_refl (pickFun Sigma)).
  destruct (permute_pickFun_exists H (Permutation_app H3 H4)) as [Sigma'' [HPerm Hsubseq]].
  constructor 3 with Sigma''; auto.
    SCase "subseq".
    apply (subseq_tran Hsubseq). destruct A, B; simpl; auto with v62.
    SCase "arg types".
    intros. apply H0; auto. revert H5. apply Permutation_in. apply Permutation_map. apply Permutation_sym. assumption.
    SCase "result types".
    apply (permute_j_sub H2); auto. apply Permutation_map. assumption.
Qed.

Lemma j_and_v_inv: forall Delta Gamma0 Gamma1 Sigma A B C,
    Delta;; Gamma0 ++ (A & B) :: Gamma1; Sigma ~< C ->
    Delta;; Gamma0 ++ A :: B :: Gamma1; Sigma ~< C.
Proof.
  intros. apply permute_j_sub with (Delta:=Delta) (Gamma:=A::B::Gamma0++Gamma1) (Sigma:=Sigma); try perm_refl; auto using WPermutation_refl.
  apply (j_and_v_inv_cons H); try perm_refl.
Qed.

The rules j_box_l, j_box_lc, and j_box_v are invertible.


Lemma j_box_v_inv_cons: forall Delta Gamma Sigma C,
  Delta;; Gamma; Sigma ~< C ->
  forall Gamma0 A,
    Permutation Gamma (([]A) :: Gamma0) ->
    Delta;; A :: Gamma0; Sigma ~< C.
Proof.
  (j_sub_cases (induction 1) 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;
  subst; try rewrite app_comm_cons; try solve
    [ constructor; simpl; apply IHj_sub; rewrite app_comm_cons; auto
    | try change (A::Gamma0) with ([A]++Gamma0);
      clear H; econstructor; eauto; simpl; apply IHj_sub; auto with v62
    | try apply (permute_j_sub H); auto using WPermutation_refl;
      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 H3; simpl in H3.
  pose proof (Permutation_refl (pickFun Sigma)).
  destruct (permute_pickFun_exists H (Permutation_app H3 H4)) as [Sigma'' [HPerm Hsubseq]].
  constructor 3 with Sigma''; auto.
    SCase "subseq".
    apply (subseq_tran Hsubseq). destruct A; simpl; auto with v62.
    SCase "arg types".
    intros. apply H0; auto. revert H5. apply Permutation_in. apply Permutation_map. apply Permutation_sym. assumption.
    SCase "result types".
    apply (permute_j_sub H2); auto. apply Permutation_map. assumption.
Qed.

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

Hint Resolve j_box_v_inv.

Lemma j_box_l_inv: forall Delta Gamma1 Gamma2 Sigma1 Sigma2 A C,
  Delta;; Gamma1 ++ Gamma2; Sigma1 ++ ([]A) :: Sigma2 ~< C ->
  Delta;; Gamma1 ++ A :: Gamma2; Sigma1 ++ Sigma2 ~< C.
Proof.
  intros.
  apply j_box_v_inv.
  apply permute_j_sub with (Delta':=Delta) (Gamma':=Gamma1++Gamma2) (Sigma':=([]A)::Sigma1++Sigma2) in H; auto with v62.
  apply permute_j_sub with (Delta:=Delta) (Gamma:=([]A)::Gamma1++Gamma2) (Sigma:=Sigma1++Sigma2); auto with v62.
  eapply (move_from_sig_to_gam_cons ([]A)); eauto.
Qed.

Lemma j_box_lc_inv: forall Delta1 Delta2 Gamma1 Gamma2 Sigma Sigma1 Sigma2 A C,
  Delta1 ++ (Sigma1 ++ ([]A) :: Sigma2) ::Delta2;; Gamma1 ++ Gamma2; Sigma ~< C ->
  Delta1 ++ (Sigma1 ++ Sigma2) ::Delta2;; Gamma1 ++ A :: Gamma2; Sigma ~< C.
Proof.
  intros.
  apply j_box_v_inv.
  apply permute_j_sub with (Delta':=Delta1++(([]A)::Sigma1++Sigma2)::Delta2) (Gamma':=Gamma1++Gamma2) (Sigma':=Sigma) in H; auto with v62.
  apply permute_j_sub with (Delta:=(Sigma1++Sigma2)::Delta1++Delta2) (Gamma:=([]A)::Gamma1++Gamma2) (Sigma:=Sigma); auto with v62.
  eapply (move_from_sig_to_gam_cons ([]A)); eauto with v62.
Qed.

Hint Resolve j_box_l_inv j_box_lc_inv.

The rules j_dia_l, j_dia_lc, and j_dia_v are invertible.


Lemma j_dia_l_lc_inv_cons: forall Delta Gamma Sigma C,
  Delta;; Gamma; Sigma ~< C ->
  (forall Sigma0 A,
    Sigma = (<>A) :: Sigma0 ->
    [A]::Delta;; Gamma; Sigma0 ~< C) /\
  (forall Delta' Sigma' A,
    Permutation Delta (((<>A)::Sigma') :: Delta') ->
    Sigma'::[A]::Delta';; Gamma; Sigma ~< C).
Proof.
  (j_sub_cases (induction 1) Case); intros; (split; [SCase "Sigma" | SCase "Delta"]); intros; subst; simpl in *; auto;
  repeat match goal with
  | H: ?G ++ _ = _ :: _ |- _ => destruct G; inv H
  | H: Permutation (?G1 ++ ?S1 :: ?G2) (?S2 :: ?G) |- _ =>
    destruct (list_eq_dec typ_dec S1 S2) as [Heq | Heq];
      [ SSCase "S1 = S2"; rewrite Heq in H; apply Permutation_sym in H; apply Permutation_cons_app_inv in H; apply Permutation_sym in H
      | SSCase "S1 <> S2"; assert (In S1 G) as Hin;
        [ apply Permutation_in with (x := S1) in H; auto with v62; simpl in H; destruct H as [Ha|?]; [inversion Ha; congruence | assumption]
        | destruct_in Hin; rewrite app_comm_cons in *; apply Permutation_app_inv with (a := S1) in H ]
      ]
  end;
  try repeat rewrite app_comm_cons; try solve
    [ simpl; constructor; auto with v62; firstorder
    | econstructor; eauto; simpl; apply IHj_sub; auto with v62; firstorder
      try repeat apply Permutation_app_cons;
      try (rewrite app_comm_cons; repeat apply permute_app_middle);
      assumption
    | apply (permute_j_sub H); simpl; auto with v62;
      apply Permutation_WPermutation; perm_refl
    | match goal with
      | |- j_sub ?G _ _ _ => rewrite <- app_nil_l with _ G
      end;
      clear H; econstructor; eauto; apply IHj_sub; auto with v62
    | change (Sigma'::[A]::Delta') with (([Sigma',[A]]) ++ Delta');
      clear H; econstructor; eauto; simpl; apply IHj_sub; auto with v62
    ].
  Case "j_dia_lc".
    SSCase "S1 = S2".
    match goal with
    |- j_sub ?G _ _ _ => rewrite <- app_nil_l with _ G
    end.
    constructor.
    apply permute_j_sub with ((Sigma1++Sigma2)::[A]::[t1]::Delta1++Delta2) Gamma Sigma; intuition; auto with v62.
    simpl; apply Permutation_WPermutation; perm_refl; assumption.
  Case "j_dia_r".
    SCase "Sigma".
    constructor.
    apply permute_j_sub with (Sigma0::[A]::Delta1++Delta2) Gamma Sigma'; auto with v62.
    apply IHj_sub; auto with v62.
    SCase "Delta".
    subst.
    match goal with
      | |- j_sub ?G _ _ _ => rewrite <- app_nil_l with _ G
    end;
    econstructor; eauto.
    simpl; apply permute_j_sub with ([A]::Delta1++Sigma::Delta2) Gamma Sigma'0; auto with v62.
    apply IHj_sub; auto.
    apply Permutation_WPermutation.
    perm_refl. simpl; auto with v62.
Qed.

Lemma j_dia_l_inv: forall Delta1 Delta2 Gamma Sigma1 Sigma2 A C,
  Delta1 ++ Delta2;; Gamma; Sigma1 ++ (<>A) :: Sigma2 ~< C ->
  Delta1 ++ [A] :: Delta2;; Gamma; Sigma1 ++ Sigma2 ~< C.
Proof.
  intros. apply permute_j_sub with (Delta:=[A]::Delta1++Delta2) (Gamma:=Gamma) (Sigma:=Sigma1++Sigma2); auto with v62.
  apply permute_j_sub with (Delta':=Delta1++Delta2) (Gamma':=Gamma) (Sigma':=(<>A)::Sigma1++Sigma2) in H; auto with v62.
  apply (j_dia_l_lc_inv_cons H); auto.
Qed.

Lemma j_dia_lc_inv: forall Delta1 Delta2 Gamma Sigma Sigma1 Sigma2 A C,
  Delta1 ++ (Sigma1 ++ (<>A) :: Sigma2) ::Delta2;; Gamma; Sigma ~< C ->
  Delta1 ++ (Sigma1 ++ Sigma2) :: [A] ::Delta2;; Gamma; Sigma ~< C.
Proof.
  intros. apply permute_j_sub with (Delta:=(Sigma1++Sigma2)::[A]::Delta1++Delta2) (Gamma:=Gamma) (Sigma:=Sigma); auto with v62.
  apply permute_j_sub with (Delta':=((<>A)::Sigma1++Sigma2)::Delta1++Delta2) (Gamma':=Gamma) (Sigma':=Sigma) in H; auto with v62.
  apply (j_dia_l_lc_inv_cons H); auto.
Qed.

Hint Resolve j_dia_l_inv j_dia_lc_inv.

Lemma j_dia_v_inv_cons: forall Delta Gamma Sigma C,
  Delta;; Gamma; Sigma ~< C ->
  forall Gamma0 A,
    Permutation Gamma ((<>A) :: Gamma0) ->
    [A]::Delta;; Gamma0; Sigma ~< C.
Proof.
  (j_sub_cases (induction 1) Case); intros; auto;
  repeat match goal with
  | H: Permutation (_ ++ (typ_dia ?A) :: _) ((typ_dia ?A) :: ?G) |- _ => idtac
  | H: Permutation (_ ++ (typ_dia ?A) :: _) ((typ_dia ?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;
  subst; try rewrite app_comm_cons; try solve
    [ try rewrite <- app_nil_l with _ Gamma0; clear H; econstructor; eauto; simpl; apply IHj_sub; auto with v62
    | constructor; simpl; apply IHj_sub; rewrite app_comm_cons; auto
    | try apply (permute_j_sub H); auto with v62;
      try apply Permutation_WPermutation; perm_refl; apply Permutation_app_cons_inv with (<>A); assumption
    ].
  Case "j_fun".
  apply permute_pickFun in H3; simpl in H3.
  pose proof (Permutation_refl (pickFun Sigma)).
  destruct (permute_pickFun_exists H (Permutation_app H3 H4)) as [Sigma'' [HPerm Hsubseq]].
  constructor 3 with Sigma''; auto.
    SCase "arg types".
    intros. apply H0; auto. revert H5. apply Permutation_in. apply Permutation_map. apply Permutation_sym. assumption.
    SCase "result types".
    apply (permute_j_sub H2); auto. apply Permutation_map. assumption.
Qed.

Lemma j_dia_v_inv: forall Delta1 Delta2 Gamma1 Gamma2 Sigma A C,
  Delta1 ++ Delta2;; Gamma1 ++ (<>A) :: Gamma2; Sigma ~< C ->
  Delta1 ++ [A] :: Delta2;; Gamma1 ++ Gamma2; Sigma ~< C.
Proof.
  intros. apply permute_j_sub with (Delta:=[A]::Delta1++Delta2) (Gamma:=Gamma1++Gamma2) (Sigma:=Sigma); auto with v62.
  apply permute_j_sub with (Delta':=Delta1++Delta2) (Gamma':=(<>A)::Gamma1++Gamma2) (Sigma':=Sigma) in H; auto with v62.
  apply (j_dia_v_inv_cons H); auto.
Qed.

Hint Resolve j_dia_v_inv.

Contraction


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

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

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

(* Induction hypothesis on the total size of type C and context PSigma. *)

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

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

Lemma contraction_cons_aux_aux: forall A PCSigma,
  contraction_IH (size_typ A + size_env PCSigma) ->
  (forall Delta Gamma Sigma C, Delta;; Gamma; Sigma ~< C ->
    (forall Delta', PCSigma = Sigma -> Permutation Delta (Sigma::Delta') -> Delta';; Gamma; Sigma ~< C) /\
    (forall Gamma0, Permutation Gamma (A :: A :: Gamma0) -> Delta;; A::Gamma0; Sigma ~< C) /\
    (forall Sigma0, Sigma = (A :: A :: Sigma0) -> Delta;; Gamma; A::Sigma0 ~< C) /\
    (forall Delta', Permutation Delta (PCSigma::PCSigma::Delta') -> PCSigma::Delta';; Gamma; Sigma ~< C) /\
    (forall Delta' PSigma, Permutation Delta ((A::A::PSigma)::Delta') -> (A::PSigma)::Delta';; Gamma; Sigma ~< C)
  ).
Proof.
  intros A PCSigma IH.
  (j_sub_cases (induction 1) Case); intros;
    (split; [SCase "DeltaSigma"
      | split; [SCase "vsub"
        | split; [SCase "lsub"
          | split; [SCase "Delta_w" | SCase "Delta"]]]]);
  intros; auto;
  repeat match goal with
  | H: ?G ++ _ = _ :: _ :: _ |- _ =>
    let G' := fresh G "'" in
    destruct G as [| ?C1 ?G']; [SSSCase "Sigma1 = nil" | ]; inv H
  | H: ?G ++ _ = _ :: _ |- _ =>
    let G' := fresh G "'" in
    destruct G as [| ?C2 ?G']; [SSSCase "Sigma1' = nil" | SSSCase "Sigma1' = C2::Sigma1''"]; inv H
  | 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]
      ]
   | H: Permutation (?G1 ++ ?S1 :: ?G2) (?S2 :: ?G) |- _ =>
     destruct (list_eq_dec typ_dec S1 S2) as [Heq | Heq];
       [ SSCase "S1 = S2"; subst; try (apply Permutation_sym in H; apply Permutation_cons_app_inv in H; apply Permutation_sym in H)
         | SSCase "S1 <> S2";
           match G with
             | S2::?G' =>
               assert (In S1 G') as Hin;
                 [ apply Permutation_in with (x := S1) in H; auto with v62; simpl in H; repeat destruct H; try congruence; auto with v62
                   | destruct_in Hin; repeat rewrite app_comm_cons in H; apply Permutation_app_inv with (a := S1) in H ]
             | _ =>
               assert (In S1 G) as Hin;
                 [ apply Permutation_in with (x := S1) in H; auto with v62; simpl in H; repeat destruct H; try congruence; auto with v62
                   | destruct_in Hin; repeat rewrite app_comm_cons in H; apply Permutation_app_inv with (a := S1) in H ]
           end
       ]
  | H: Permutation ?G (?A::_) |- _ =>
    match type of A with
    | env =>
      assert (In A G) as Hin;
        [ apply Permutation_sym in H; apply (Permutation_in _ H); auto with v62
          | destruct_in Hin; repeat rewrite app_comm_cons in *; apply Permutation_app_cons_inv in H
        ]
    end
  end;
  subst; 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::?G;; _; _ ~< _ => rewrite <- app_nil_l with _ (A::G)
  | _ => idtac
  end;
  try solve
    [ constructor; simpl; intuition; auto with v62
    | constructor; simpl; apply IHj_sub; repeat rewrite app_comm_cons; auto with v62
    | econstructor; simpl; eauto 1; apply IHj_sub; repeat rewrite app_comm_cons; auto with v62
    | (* Delta_w *)
      simpl; change (PCSigma :: Delta') with ([PCSigma] ++ Delta');
      clear H; econstructor; eauto 1;
      simpl; apply IHj_sub;
      try change (PCSigma :: PCSigma :: [t1] :: Delta') with ([PCSigma, PCSigma] ++ [t1] :: Delta'); auto with v62
    | (* Delta *)
      clear H; simpl; change ((A::PSigma)::Delta') with ([A::PSigma]++Delta');
      econstructor; eauto 1;
      simpl; apply IHj_sub; auto with v62
    | clear H; simpl; change (A::Gamma0) with ([A]++Gamma0);
      econstructor; eauto 1;
      simpl; apply IHj_sub; auto with v62
    ].
  Case "j_fun".
    SCase "vsub".
    apply permute_pickFun in H3.
    pose proof (Permutation_refl (pickFun Sigma)).
    destruct (permute_pickFun_exists H (Permutation_app H3 H4)) as [Sigma'' [HPerm Hsubseq]].
    (* A is not function type *)
    destruct A; try solve [
      constructor 3 with Sigma''; auto;
      [ intros; apply H0; auto; revert H5; 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 H4.
    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 H5.
        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 3 with Sigma''; auto;
          [ apply (subseq_tran H6); 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 3 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 H5.
        SSSCase "No more type is selected.".
        constructor 3 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 3 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 3 with ((A1,A2)::l0); auto;
     &