Module Subtyping

Set Implicit Arguments.
Require Import Layers.
Require Import Types.
Require Import TypeEquality.
Require Import MoreTypeEquality.
Require Import Environments.
Require Import Coercions.
Require Import AntiFrameSwitch.
Require Import TypeContexts.
Require Import FocusPaths.

Notation "T --> U" := (TyArrow T U) (at level 58, right associativity).

The subtyping judgement, or coercion typing judgement.

Inductive jco: env -> coercion -> ty -> Prop :=
| JCoId:
    forall C T1 T2,
    tyeq T1 T2 ->
    wf T1 ->
    wf T2 ->
    jco C CoId (T1 --> T2)
| JCoSeq:
    forall C c1 c2 T1 T2 T3,
    jco C c1 (T1 --> T2) ->
    jco C c2 (T2 --> T3) ->
    jco C (CoSeq c1 c2) (T1 --> T3)
| JCoForallIntro:
    forall C T,
    wf T ->
    jco C CoForallIntro (T --> TyForall (lift_ty 0 T))
| JCoForallElim:
    forall C T U,
    wf T ->
    wf U ->
    jco C CoForallElim (TyForall T --> subst_ty U 0 T)
| JCoExistsIntro:
    forall C T U,
    wf T ->
    wf U ->
    jco C CoExistsIntro (subst_ty U 0 T --> TyExists T)
| JCoExistsLeftIntro:
    forall C T1 T2,
    wf T1 ->
    wf T2 ->
    jco C CoExistsLeftIntro (TyForall (TyArrow T1 (lift_ty 0 T2)) --> TyArrow (TyExists T1) T2)
| JCoExistsElim:
    forall C T,
    wf T ->
    jco C CoExistsElim (TyExists (lift_ty 0 T) --> T)
| JCoArrow:
    forall C c1 c2 T1 T2 U1 U2,
    jco C c1 (U1 --> T1) ->
    jco C c2 (T2 --> U2) ->
    jco C (CoArrow c1 c2) (TyArrow T1 T2 --> TyArrow U1 U2)
| JCoPair:
    forall C c1 c2 layer1 layer2 T1 T2 U1 U2,
    jco C c1 (T1 --> U1) ->
    jco C c2 (T2 --> U2) ->
    jco C (CoPair layer1 layer2 c1 c2) (TyPair layer1 layer2 T1 T2 --> TyPair layer1 layer2 U1 U2)
| JCoForall:
    forall C c T1 T2,
    jco (C!) c (T1 --> T2) ->
    jco C (CoForall c) (TyForall T1 --> TyForall T2)
| JCoExists:
    forall C c T1 T2,
    jco (C!) c (T1 --> T2) ->
    jco C (CoExists c) (TyExists T1 --> TyExists T2)
| JCoBang:
    forall C c T1 T2,
    jco C c (T1 --> T2) ->
    jco C (CoBang c) (TyBang T1 --> TyBang T2)
| JCoRegionCap:
    forall C c rk sigma T1 T2,
    wf sigma ->
    jco C c (T1 --> T2) ->
    jco C (CoRegionCap c) (TyRegionCap rk sigma T1 --> TyRegionCap rk sigma T2)
| JCoRegionCapPunched:
    forall C c rho sigma T1 T2,
    wf rho ->
    wf sigma ->
    jco C c (T1 --> T2) ->
    jco C (CoRegionCapPunched c) (TyRegionCapPunched rho T1 sigma --> TyRegionCapPunched rho T2 sigma)
| JCoRef:
    forall C c T1 T2,
    jco C c (T1 --> T2) ->
    jco C (CoRef c) (TyRef T1 --> TyRef T2)
| JCoDereliction:
    forall C T,
    wf T ->
    jco C CoDereliction (TyBang T --> T)
| JCoBangIdempotent:
    forall C T,
    wf T ->
    jco C CoBangIdempotent (TyBang T --> TyBang (TyBang T))
| JCoPairBang:
    forall C layer1 layer2 T1 T2,
    wf T1 ->
    wf T2 ->
    jco C CoPairBang (TyPair layer1 layer2 (TyBang T1) (TyBang T2) --> TyBang (TyPair layer1 layer2 T1 T2))
| JCoBangPair:
    forall C layer1 layer2 T1 T2,
    wf T1 ->
    wf T2 ->
    jco C CoBangPair (TyBang (TyPair layer1 layer2 T1 T2) --> TyBang (TyPair layer1 layer2 (TyBang T1) (TyBang T2)))
| JCoBangRef:
    forall C T1 T2,
    wf T1 ->
    wf T2 ->
    jco C CoBangRef (TyBang (TyRef T1) --> T2)
| JCoBangRegionCap:
    forall C T1 rk sigma T2,
    wf T1 ->
    wf sigma ->
    wf T2 ->
    jco C CoBangRegionCap (TyBang (TyRegionCap rk sigma T1) --> T2)
| JCoBangRegionCapPunched:
    forall C T1 rho sigma T2,
    wf T1 ->
    wf rho ->
    wf sigma ->
    wf T2 ->
    jco C CoBangRegionCapPunched (TyBang (TyRegionCapPunched rho T1 sigma) --> T2)
| JCoUnitBang:
    forall C layer,
    jco C CoUnitBang (TyUnit layer --> TyBang (TyUnit layer))
| JCoAtBang:
    forall C sigma,
    wf sigma ->
    jco C CoAtBang (TyAt sigma --> TyBang (TyAt sigma))
| JCoDistrib:
    forall C T1 T2,
    wf T1 ->
    wf T2 ->
    anti_frame_disabled ->
    jco C CoDistrib (TyForall (TyArrow T1 T2) --> TyArrow (TyForall T1) (TyForall T2))
| JCoSingletonToGroup:
    forall C sigma T,
    wf sigma ->
    wf T ->
    jco C CoSingletonToGroup (TyRegionCap Singleton sigma T --> TyRegionCap Group sigma T)
| JCoForallPair:
    forall C layer1 layer2 T1 T2,
    wf T1 ->
    wf T2 ->
    jco C CoForallPair
      (TyForall (TyPair layer1 layer2 T1 T2) -->
       TyPair layer1 layer2 (TyForall T1) (TyForall T2))
| JCoForallBang:
    forall C T,
    wf T ->
    jco C CoForallBang (TyForall (TyBang T) --> TyBang (TyForall T))
| JCoForallRef:
    forall C T,
    wf T ->
    jco C CoForallRef (TyForall (TyRef T) --> TyRef (TyForall T))
| JCoForallRegionCap:
    forall C rk sigma T,
    wf sigma ->
    wf T ->
    jco C CoForallRegionCap (TyForall (TyRegionCap rk (lift_ty 0 sigma) T) -->
                             TyRegionCap rk sigma (TyForall T))
| JCoForallRegionCapPunched:
    forall C rho sigma T,
    wf rho ->
    wf sigma ->
    wf T ->
    jco C CoForallRegionCapPunched (TyForall (TyRegionCapPunched (lift_ty 0 rho) T (lift_ty 0 sigma)) -->
                                    TyRegionCapPunched rho (TyForall T) sigma)
| JCoSingletonRegionCapExists:
    forall C sigma T,
    wf sigma ->
    wf T ->
    jco C CoSingletonRegionCapExists (TyRegionCap Singleton sigma (TyExists T) -->
                       TyExists (TyRegionCap Singleton (lift_ty 0 sigma) T))
| JCoPairExistsLeft:
    forall C layer1 layer2 T1 T2,
    wf T1 ->
    wf T2 ->
    jco C CoPairExistsLeft
      (TyPair layer1 layer2 (TyExists T1) T2 -->
       TyExists (TyPair layer1 layer2 T1 (lift_ty 0 T2)))
| JCoPairExistsRight:
    forall C layer1 layer2 T1 T2,
    wf T1 ->
    wf T2 ->
    jco C CoPairExistsRight
      (TyPair layer1 layer2 T1 (TyExists T2) -->
       TyExists (TyPair layer1 layer2 (lift_ty 0 T1) T2))
| JCoBangExists:
    forall C T,
    wf T ->
    jco C CoBangExists (TyBang (TyExists T) --> TyExists (TyBang T))
| JCoRefExists:
    forall C T,
    wf T ->
    jco C CoRefExists (TyRef (TyExists T) --> TyExists (TyRef T))
| JCoDefocus:
    forall C sigma T TC pi,
    jpath pi TC ->
    wf sigma ->
    wf T ->
    jco C (CoDefocus pi) (TyMixPair (fill TC (TyAt sigma)) (TyRegionCap Singleton sigma T) --> fill TC T)
| JCoDefocusGroup:
    forall C rho sigma T,
    wf rho ->
    wf sigma ->
    wf T ->
    jco C CoDefocusGroup (TyLogPair (TyRegionCap Singleton sigma T) (TyRegionCapPunched rho T sigma) -->
                          TyRegionCap Group rho T)
| JCoStarCommutative:
    forall C layer1 layer2 T1 T2,
    wf T1 ->
    wf T2 ->
    (layer1 = Logical \/ layer2 = Logical) ->
    jco C CoStarCommutative (TyPair layer1 layer2 T1 T2 --> TyPair layer2 layer1 T2 T1)
| JCoStarAssociative:
    forall C layer1 layer2 layer3 T1 T2 T3,
    wf T1 ->
    wf T2 ->
    wf T3 ->
    layer1 = Logical \/ layer2 = Logical \/ layer3 = Logical ->
    jco C CoStarAssociative
      (TyPair (layer_conj layer1 layer2) layer3 (TyPair layer1 layer2 T1 T2) T3 -->
       TyPair layer1 (layer_conj layer2 layer3) T1 (TyPair layer2 layer3 T2 T3))
| JCoStarRef:
    forall C T1 T2,
    wf T1 ->
    wf T2 ->
    jco C CoStarRef (TyMixPair (TyRef T1) T2 --> TyRef (TyMixPair T1 T2))
| JCoRefStar:
    forall C T1 T2,
    wf T1 ->
    wf T2 ->
    jco C CoRefStar (TyRef (TyMixPair T1 T2) --> TyMixPair (TyRef T1) T2)
| JCoStarSingleton:
    forall C sigma T1 T2,
    wf sigma ->
    wf T1 ->
    wf T2 ->
    jco C CoStarSingleton (TyLogPair (TyRegionCap Singleton sigma T1) T2 -->
                           TyRegionCap Singleton sigma (TyMixPair T1 T2))
| JCoSingletonStar:
    forall C sigma T1 T2,
    wf sigma ->
    wf T1 ->
    wf T2 ->
    jco C CoSingletonStar (TyRegionCap Singleton sigma (TyMixPair T1 T2) -->
                           TyLogPair (TyRegionCap Singleton sigma T1) T2)
| JCoTensorExchange:
    forall C T A B A' B' n Us,
    commutative_pair A B A' B' ->
    length Us = n ->
    wf A ->
    wf B ->
    wf T ->
    wfs Us ->
    jco C (CoTensorExchange n) (tensors (TyTensor (TyTensor T A) B') Us --> tensors (TyTensor (TyTensor T B) A') Us)
| JCoVar:

Here, T stands for a coercion type; it will always be of the form T1 --> T2, but the proofs are simpler if we don't impose that (we are then able to re-use a number of general lemmas, including jenv_substitution). In the paper, we lie a little bit and show a version of the rule that has T1 --> T2, because this looks less confusing.

    forall C x T,
    jenv C x T ->
    wf T ->
    jco C (CoVar x) T
| JCoMu:
    forall C c T U,
    jco (C;; T --> U) c (T --> U) ->
    wf T ->
    wf U ->
    jco C (CoMu c) (T --> U)
.

Hint Constructors jco.

Lemma JCoTensorExchangeZero:
  forall C T A B A' B',
  commutative_pair A B A' B' ->
  wf A ->
  wf B ->
  wf T ->
  jco C (CoTensorExchange 0) (TyTensor (TyTensor T A) B' --> TyTensor (TyTensor T B) A').

Proof.

intros. eapply JCoTensorExchange with (Us := nil); eauto.
Qed.

Hint Resolve JCoTensorExchangeZero.