Module DerivedSubtyping

Set Implicit Arguments.
Require Import MyTactics.
Require Import DeBruijn.
Require Import Layers.
Require Import Types.
Require Import TypeEquality.
Require Import MoreTypeEquality.
Require Import TypeContexts.
Require Import FocusPaths.
Require Import Coercions.
Require Import Subtyping.
Require Import Environments.
Require Import PreliminaryLemmas.

Derived subtyping rules.

-------------------------------------------------------------------------

A slightly simpler typing rule for the identity coercion.

Lemma JCoIdentity:
  forall C T,
  wf T ->
  jco C CoId (T --> T).
Proof.
  econstructor. eapply tyeq_reflexive. eassumption. eassumption. eassumption.
Qed.

-------------------------------------------------------------------------

Inverting subtyping judgements.

Ltac jco_inversion :=
  match goal with
  | h: jco _ _ _ |- _ =>
      depelim h
  end.

-------------------------------------------------------------------------

Puns.

Lemma JCoForallElimTrivial:
  forall C T,
  wf T ->
  jco C CoForallElim (TyForall (lift_ty 0 T) --> T).
Proof.
  intros.
  pattern T at -1.
  replace T with (subst_ty TyPhyUnit 0 (lift_ty 0 T)).
  econstructor; eauto.
  eapply subst_lift_ty.
Qed.

Lemma JCoForallElimPun:
  forall C T,
  wf T ->
  jco C CoForallElim (TyForall (lift_ty 1 T) --> T).
Proof.
  intros. rewrite <- (pun_2_ty T 0) at 2. eauto.
Qed.

Lemma JCoExistsIntroPun:
  forall C T,
  wf T ->
  jco C CoExistsIntro (T --> TyExists (lift_ty 1 T)).
Proof.
  intros. rewrite <- (pun_2_ty T 0) at 1. eauto.
Qed.

-------------------------------------------------------------------------

Two universal quantifiers commute.

Definition CoForallForall :=
  CoForallExtrusion CoForall.

Lemma JCoForallForall:
  forall C T,
  wf T ->
  jco C CoForallForall
       (TyForall (TyForall T) -->
        TyForall (TyForall (rotate_ty 1 T))).
Proof.
  intros. econstructor. econstructor; wf. econstructor. simpl; econstructor.
  unfold rotate_ty, rotate. eauto.
Qed.

Lemma wf_rotate_ty:
  forall k T,
  wf T ->
  wf (rotate_ty k T).
Proof.
  unfold rotate_ty, rotate. eauto.
Qed.

Lemma JCoForallForall_alternate_formulation:
  forall C T,
  wf T ->
  jco C CoForallForall
       (TyForall (TyForall (rotate_ty 1 T)) -->
        TyForall (TyForall T)).
Proof.
  intros.
  rewrite <- (rotate_ty_1_self_inverse T) at -1.
  eapply JCoForallForall.
  eauto using wf_rotate_ty.
Qed.

Two existential quantifiers commute.

Definition CoExistsExists :=
  CoExistsIntrusion CoExists.

Lemma JCoExistsExists:
  forall C T,
  wf T ->
  jco C CoExistsExists
       (TyExists (TyExists (rotate_ty 1 T)) -->
        TyExists (TyExists T)).
Proof.
  intros. econstructor. econstructor. econstructor. unfold rotate_ty, rotate. econstructor; wf.
  eapply JCoExistsElim with (T := TyExists (TyExists T)); wf.
Qed.

Lemma JCoExistsExists_alternate_formulation:
  forall C T,
  wf T ->
  jco C CoExistsExists
       (TyExists (TyExists T) -->
        TyExists (TyExists (rotate_ty 1 T))).
Proof.
  intros.
  rewrite <- (rotate_ty_1_self_inverse T) at 1.
  eapply JCoExistsExists.
  eauto using wf_rotate_ty.
Qed.

A universal quantifier extrudes out of a universal quantifier.

Definition CoExistsForall :=
  CoForallExtrusion CoExists.

Lemma JCoExistsForall:
  forall C T,
  wf T ->
  jco C CoExistsForall
       (TyExists (TyForall T) -->
        TyForall (TyExists (rotate_ty 1 T))).
Proof.
  intros. econstructor. econstructor; wf. econstructor. simpl; econstructor.
  unfold rotate_ty, rotate. eauto.
Qed.

Lemma JCoExistsForall_alternate_formulation:
  forall C T,
  wf T ->
  jco C CoExistsForall
       (TyExists (TyForall (rotate_ty 1 T)) -->
        TyForall (TyExists T)).
Proof.
  intros.
  rewrite <- (rotate_ty_1_self_inverse T) at -1.
  eapply JCoExistsForall.
  eauto using wf_rotate_ty.
Qed.

-------------------------------------------------------------------------

A coercion is reversible when there exists an inverse coercion.

Definition inverse c1 c2 :=
  forall C T1 T2,
  jco C c1 (T1 --> T2) ->
  jco C c2 (T2 --> T1).

-------------------------------------------------------------------------

A coercion combinator that allows type equality on either side.

Lemma JCoTyEq:
  forall C c T1 T2 U1 U2,
  jco C c (T1 --> U1) ->
  tyeq T1 T2 ->
  tyeq U1 U2 ->
  wf T2 ->
  wf U2 ->
  jco C (CoTyEq c) (T2 --> U2).
Proof.
  unfold CoTyEq. intros. econstructor; eauto using tyeq_symmetric.
Qed.

-------------------------------------------------------------------------

An existential quantifier distributes into both sides of a pair.

Lemma JCoExistsPairDistrib:
  forall C layer1 layer2 T1 T2,
  wf T1 ->
  wf T2 ->
  jco C
    (CoExistsPairDistrib layer1 layer2)
    (TyExists (TyPair layer1 layer2 T1 T2) -->
     TyPair layer1 layer2 (TyExists T1) (TyExists T2)).
Proof.
  intros.
  econstructor.
  constructor.
  constructor; auto using JCoExistsIntroPun.
  replace (TyPair layer1 layer2 (TyExists (lift_ty 1 T1)) (TyExists (lift_ty 1 T2)))
     with (lift_ty 0 (TyPair layer1 layer2 (TyExists T1) (TyExists T2))); try reflexivity.
  constructor; auto.
Qed.

-------------------------------------------------------------------------

Scope restriction: an existential quantifier enters one side of a pair.

Lemma JCoExistsScopeRestrictionLeft:
  forall C layer1 layer2 T1 T2,
  wf T1 ->
  wf T2 ->
  jco C
    (CoExistsScopeRestrictionLeft layer1 layer2)
    (TyExists (TyPair layer1 layer2 T1 (lift_ty 0 T2)) -->
     TyPair layer1 layer2 (TyExists T1) T2).
Proof.
  econstructor; eauto 10 using JCoExistsPairDistrib.
Qed.

Lemma JCoExistsScopeRestrictionRight:
  forall C layer1 layer2 T1 T2,
  wf T1 ->
  wf T2 ->
  jco C
    (CoExistsScopeRestrictionRight layer1 layer2)
    (TyExists (TyPair layer1 layer2 (lift_ty 0 T1) T2) -->
     TyPair layer1 layer2 T1 (TyExists T2)).
Proof.
  econstructor; eauto 8 using JCoExistsPairDistrib.
Qed.

-------------------------------------------------------------------------

A universal quantifier enters one side of a pair, if the bound variable does not appear on the other side.

Lemma JCoForallPairLeft:
  forall C layer1 layer2 T1 T2,
  wf T1 ->
  wf T2 ->
  jco C (CoForallPairLeft layer1 layer2)
    (TyForall (TyPair layer1 layer2 T1 (lift_ty 0 T2)) -->
     TyPair layer1 layer2 (TyForall T1) T2).
Proof.
  intros. econstructor.
  eapply JCoForallPair; eauto.
  econstructor.
  econstructor; eauto.
  eapply JCoForallElimTrivial; eauto.
Qed.

-------------------------------------------------------------------------

A pair of universal quantifiers extrude out of a pair.

Lemma JCoForallPairExtrusion:
  forall C layer1 layer2 T1 T2,
  wf T1 ->
  wf T2 ->
  jco C
    (CoForallPairExtrusion layer1 layer2)
    (TyPair layer1 layer2 (TyForall T1) (TyForall T2) -->
     TyForall (TyPair layer1 layer2 T1 T2)).
Proof.
  intros.
  econstructor.
  econstructor. auto.
  constructor. simpl.
  auto using JCoForallElimPun.
Qed.

-------------------------------------------------------------------------

Covariance and contravariance.

An assertion variance true cc tc x k holds when the type tc is covariant in the type variable x. The coercion context cc is a witness of this covariance assertion. The integer k is the number of binders under which x appears within tc; that is, it is the number of variables that are captured by tc, viewed as a type context. An assertion variance false cc tc x k is a contravariance assertion.

Inductive variance : bool -> (coercion -> coercion) -> ty -> nat -> nat -> Prop :=
| VarianceHole:
    forall x,
    variance true (fun c => c) (TyVar x) x 0
| VarianceConstant:
    forall b x k T,
    wf T ->
    variance b (fun c => CoId) (lift_ty x T) x k
| VarianceArrow:
    forall b cc1 cc2 tc1 tc2 x k,
    variance (negb b) cc1 tc1 x k ->
    variance b cc2 tc2 x k ->
    variance b (fun c => CoArrow (cc1 c) (cc2 c)) (TyArrow tc1 tc2) x k
| VariancePair:
    forall b cc1 cc2 layer1 layer2 tc1 tc2 x k,
    variance b cc1 tc1 x k ->
    variance b cc2 tc2 x k ->
    variance b (fun c => CoPair layer1 layer2 (cc1 c) (cc2 c)) (TyPair layer1 layer2 tc1 tc2) x k
| VarianceForall:
    forall b cc tc x k,
    variance b cc tc (S x) k ->
    variance b (fun c => CoForall (cc c)) (TyForall tc) x (S k)
| VarianceExists:
    forall b cc tc x k,
    variance b cc tc (S x) k ->
    variance b (fun c => CoExists (cc c)) (TyExists tc) x (S k)
| VarianceBang:
    forall b cc tc x k,
    variance b cc tc x k ->
    variance b (fun c => CoBang (cc c)) (TyBang tc) x k
| VarianceRegionCap:
    forall rk sigma b cc tc x k,
    wf sigma ->
    variance b cc tc x k ->
    variance b (fun c => CoRegionCap (cc c)) (TyRegionCap rk (lift_ty x sigma) tc) x k
| VarianceRegionCapPunched:
    forall rho sigma b cc tc x k,
    wf rho ->
    wf sigma ->
    variance b cc tc x k ->
    variance b (fun c => CoRegionCapPunched (cc c)) (TyRegionCapPunched (lift_ty x rho) tc (lift_ty x sigma)) x k
| VarianceRef:
    forall b cc tc x k,
    variance b cc tc x k ->
    variance b (fun c => CoRef (cc c)) (TyRef tc) x k
.
TEMPORARY fill is non-capturing; redo everything with a capturing fill
TEMPORARY other cases? what about TyMu?

Hint Constructors variance.

-------------------------------------------------------------------------

A coercion arrow whose direction depends on a Boolean flag b.

Definition coerce (b : bool) T1 T2 :=
  if b then T1 --> T2 else T2 --> T1.

A few trivial lemmas about this notion.

Lemma coerce_negb:
  forall b T1 T2,
  coerce (negb b) T2 T1 = coerce b T1 T2.
Proof.
  intros [|]; simpl; auto.
Qed.

Lemma jco_coerce_negb:
  forall C c b T1 T2,
  jco C c (coerce b T1 T2) ->
  jco C c (coerce (negb b) T2 T1).
Proof.
  intros. rewrite coerce_negb. assumption.
Qed.

Lemma jco_coerce_lift:
  forall C c b T1 T2,
  jco C c (coerce b T1 T2) ->
  forall k,
  jco (lift_ty_env k C) c (coerce b (lift_ty k T1) (lift_ty k T2)).
Proof.
  intros; destruct b; simpl in *; auto using jco_ty_weakening_arrow.
Qed.

-------------------------------------------------------------------------

Properties of variance.

The filling of a covariant (resp. contravariant) context is compatible with subtyping.

Lemma variance_fill:
  forall b cc tc x k,
  variance b cc tc x k ->
  forall C c T1 T2,
  jco C c (coerce b T1 T2) ->
  jco C (cc c) (subst_ty T1 x tc --> subst_ty T2 x tc).
Proof.
  induction 1; simpl; intros; repeat rewrite subst_lift_ty; eauto using jco_coerce_negb, jco_coerce_lift.
VarianceHole
  repeat rewrite subst_var_identity. assumption.
Qed.

A covariant (resp. contravariant) context is well-formed.

Lemma variance_wf:
  forall b cc tc x k,
  variance b cc tc x k ->
  wf tc.
Proof.
  induction 1; eauto.
Qed.

Covariance (resp. contravariance) is preserved by lifting.

Lemma variance_lift:
  forall b cc tc x k,
  variance b cc tc x k ->
  forall j, j <= x ->
  variance b cc (lift_ty j tc) (S x) k.
Proof.
  induction 1; simpl; intros; repeat rewrite (@lift_lift_ty _ j); eauto.
VarianceHole
  unfold lift_var. by_cases; auto.
Qed.

-------------------------------------------------------------------------

A universal quantifier extrudes out of any covariant context.

The witness that appears in the statement explains why this is safe: it is a simple matter of (i) introducing a universal quantifier at the root of the context; (ii) instantiating the universal quantifier found in the hole of the context; this is permitted because the context is covariant.

Lemma JCoForallExtrusion:
  forall cc tc x k,
  variance true cc tc x k ->
  forall C T,
  wf T ->
  jco C (CoForallExtrusion cc)
        (subst_ty (TyForall T) x tc --> TyForall (subst_ty T (S x) (lift_ty 0 tc))).
Proof.
  intros. econstructor.
  eauto using wf_subst, variance_wf.
  constructor. rewrite lift_subst_1_ty; eauto. simpl.
  eapply variance_fill. eapply variance_lift; eauto. simpl.
  auto using JCoForallElimPun.
Qed.

-------------------------------------------------------------------------

A universal quantifier extrudes out of a pair. We prove this using the above general result. It turns out to be more work than proving it directly.

Lemma JCoForallPairExtrusionLeft:
  forall C layer1 layer2 T1 T2,
  wf T1 ->
  wf T2 ->
  jco C (CoForallPairExtrusionLeft layer1 layer2)
        (TyPair layer1 layer2 (TyForall T1) T2 --> TyForall (TyPair layer1 layer2 T1 (lift_ty 0 T2))).
Proof.
  introv wf1 wf2.
  assert (v1: variance true
           (fun c => CoPair layer1 layer2 c CoId)
           (TyPair layer1 layer2 (TyVar 0) (lift_ty 0 T2)) 0 0). eauto.
  generalize (JCoForallExtrusion v1 C wf1); simpl.
  rewrite subst_lift_ty.
  unfold lift_var. simpl.
  repeat rewrite subst_var_identity.
  rewrite lift_lift_ty; eauto.
  rewrite subst_lift_ty.
  tauto.
Qed.

-------------------------------------------------------------------------

The existential left introduction axiom is reversible.

Lemma JCoExistsLeftIntroReversed:
  forall C T1 T2,
  wf T1 ->
  wf T2 ->
  jco C CoExistsLeftIntroReversed (TyArrow (TyExists T1) T2 --> TyForall (TyArrow T1 (lift_ty 0 T2))).
Proof.
  intros.
  econstructor.
  econstructor; auto.
  econstructor.
  simpl. econstructor.
  auto using JCoExistsIntroPun.
  econstructor; eauto.
Qed.

Goal inverse CoExistsLeftIntro CoExistsLeftIntroReversed.
Proof.
  repeat intro. jco_inversion. eauto using JCoExistsLeftIntroReversed.
Qed.

One might wish to also prove inverse CoExistsLeftIntroReversed c, for some appropriately chosen coercion c. However, CoExistsLeftIntroReversed allows proving more subtyping assertions than stated by JCoExistsLeftIntroReversed, and some of these subtyping assertions may not be reversible. We do not investigate this issue in depth for the time being.

-------------------------------------------------------------------------

An existential quantifier enters a pair.

Lemma JCoExistsPairIntrusion:
  forall C layer1 layer2 T1 T2,
  wf T1 ->
  wf T2 ->
  jco C
    (CoExistsPairIntrusion layer1 layer2)
    (TyExists (TyPair layer1 layer2 T1 T2) --> TyPair layer1 layer2 (TyExists T1) (TyExists T2)).
Proof.
  intros.
  econstructor.
  econstructor.
  auto using JCoExistsIntroPun.
  apply JCoExistsElim with (T := TyPair layer1 layer2 (TyExists T1) (TyExists T2)). auto.
Qed.

-------------------------------------------------------------------------

The above result, JCoExistsPairIntrusion, is only a special case of a much more general property: an existential quantifier distributes into any covariant multi-hole context, provided the context itself has no occurrence of the existentially bound variable. The statement and proof are dual to those of JCoForallExtrusion.

Lemma JCoExistsIntrusion:
  forall cc tc x k,
  variance true cc tc x k ->
  forall C T,
  wf T ->
  jco C (CoExistsIntrusion cc)
        (TyExists (subst_ty T (S x) (lift_ty 0 tc)) --> subst_ty (TyExists T) x tc).
Proof.
  intros.
  econstructor; [ idtac | eauto using wf_subst, variance_wf ].
  constructor. rewrite lift_subst_1_ty; eauto. simpl.
  eapply variance_fill. eapply variance_lift; eauto. simpl.
  auto using JCoExistsIntroPun.
Qed.

-------------------------------------------------------------------------

As an application of JCoExistsIntrusion, we show that CoSingletonRegionCapExists is reversible. In fact, while CoSingletonRegionCapExists is valid only for singleton regions, its inverse is valid for both singleton and group regions.

Lemma JCoExistsCap:
  forall C rk sigma T,
  wf sigma ->
  wf T ->
  jco C CoExistsCap (TyExists (TyRegionCap rk (lift_ty 0 sigma) T) -->
                     TyRegionCap rk sigma (TyExists T)).
Proof.
  introv wfsigma wfT.
  assert (v1: variance true (fun c => CoRegionCap c) (TyRegionCap rk (lift_ty 0 sigma) (TyVar 0)) 0 0). eauto.
  generalize (JCoExistsIntrusion v1 C wfT); simpl.
  rewrite subst_lift_ty.
  unfold lift_var. simpl.
  repeat rewrite subst_var_identity.
  rewrite lift_lift_ty; eauto.
  rewrite subst_lift_ty.
  tauto.
Qed.

Goal inverse CoSingletonRegionCapExists CoExistsCap.
Proof.
  repeat intro. jco_inversion. eauto using JCoExistsCap.
Qed.

-------------------------------------------------------------------------

CoPairBang and CoBangPair are reversible.

Lemma JCoPairBangReversed:
  forall C layer1 layer2 T1 T2,
  wf T1 ->
  wf T2 ->
  jco C CoPairBangReversed (TyBang (TyPair layer1 layer2 T1 T2) --> TyPair layer1 layer2 (TyBang T1) (TyBang T2)).
Proof.
  intros. econstructor; eauto.
Qed.

Goal inverse CoPairBang CoPairBangReversed.
Proof.
  repeat intro. jco_inversion. eauto using JCoPairBangReversed.
Qed.

Lemma JCoBangPairReversed:
  forall C layer1 layer2 T1 T2,
  wf T1 ->
  wf T2 ->
  jco C
    (CoBangPairReversed layer1 layer2)
    (TyBang (TyPair layer1 layer2 (TyBang T1) (TyBang T2)) -->
     TyBang (TyPair layer1 layer2 T1 T2)).
Proof.
  intros.
  econstructor.
  econstructor; econstructor; eauto.
Qed.

-------------------------------------------------------------------------

The primitive coercion CoStarAssociative moves from left to right. Here is its inverse.

Lemma JCoStarAssociativeReversed:
  forall C layer1 layer2 layer3 T1 T2 T3,
  wf T1 ->
  wf T2 ->
  wf T3 ->
  (layer1 = Physical /\ layer2 = Logical /\ layer3 = Logical) \/
  (layer1 = Logical /\ layer2 = Physical /\ layer3 = Logical) \/
  (layer1 = Logical /\ layer2 = Logical /\ layer3 = Physical) ->
  jco C (CoStarAssociativeReversed layer1 layer2 layer3)
    (TyPair layer1 (layer_conj layer2 layer3) T1 (TyPair layer2 layer3 T2 T3) -->
     TyPair (layer_conj layer1 layer2) layer3 (TyPair layer1 layer2 T1 T2) T3).
Proof.
  intros.
  econstructor.
  econstructor; eauto. layers; tauto.
  econstructor.
  econstructor.
    econstructor; eauto. layers; tauto.
    econstructor; eauto.
  econstructor.
  rewrite layer_conj_commutative. econstructor; eauto. layers; tauto.
  econstructor.
  econstructor; eauto. layers; tauto.
  rewrite layer_conj_commutative. econstructor.
  econstructor; eauto. layers; tauto.
  eauto.
Qed.

-------------------------------------------------------------------------

This coercion exchanges two mixed pairs, hoisting one out of the other.

Lemma JCoMixPairExchange:
  forall C T1 T2 T3,
  wf T1 ->
  wf T2 ->
  wf T3 ->
  jco C CoMixPairExchange
    (TyMixPair (TyMixPair T1 T2) T3 -->
     TyMixPair (TyMixPair T1 T3) T2).
Proof.
  intros.
  econstructor.
  eapply JCoStarAssociative with (layer1 := Physical) (layer2 := Logical); eauto.
  econstructor.
  econstructor.
    eauto.
    econstructor; eauto.
  eapply JCoStarAssociativeReversed; eauto.
Qed.

-------------------------------------------------------------------------

A coercion that exchanges two type composition operators, in the special case where we have a commutative pair. Whereas the primitive coercion CoTensorExchange exchanges two tensors, the derived coercion CoComposExchange exchanges two type composition operators. In short, this requires applying CoTensorExchange under a context and composing it with a coercion that exchanges the two outer pairs.

Lemma JCoComposExchange:
  forall C T A B A' B',
  commutative_pair A B A' B' ->
  wf A ->
  wf B ->
  wf T ->
  jco C CoComposExchange (TyCompos (TyCompos T A) B' --> TyCompos (TyCompos T B) A').
Proof.
  intros.
First, on each side, use type equality and the lemma exploit_commutative_pair.
  eapply JCoTyEq; [
    idtac
  | eapply exploit_commutative_pair; [ eassumption | wf | wf | wf ]
  | eapply exploit_commutative_pair; [ eapply commutative_pair_symmetric; eassumption | wf | wf | wf ]
  | wf | wf ].
We now have a sequence of two coercion steps.
  econstructor.
The first step applies the coercion c under two levels of pairs in order to exchange two tensors. By hypothesis, c is able to achieve this.
  econstructor. econstructor.
    eapply JCoTensorExchangeZero; eauto.
    eapply JCoIdentity; eauto using commutative_pair_wf_first.
    eapply JCoIdentity; eauto using commutative_pair_wf_second.
The second step exchanges two mixed pairs.
  eapply JCoMixPairExchange; wf.
Qed.

Hint Resolve JCoComposExchange.

-------------------------------------------------------------------------

A coercion that lifts a composition operator out of a pair.

Lemma JCoMixPairComposExchange:
  forall C T1 T2 U,
  wf T1 ->
  wf T2 ->
  wf U ->
  jco C CoMixPairComposExchange (TyMixPair (TyCompos T1 U) (TyTensor T2 U) --> TyCompos (TyMixPair T1 T2) U).
Proof.
  unfold CoMixPairComposExchange. intros.
  econstructor.
    eauto using JCoMixPairExchange.
    econstructor; eauto.
      eapply tyeq_pair; eauto.
      eauto using tyeq_tensor_pair, tyeq_symmetric.
Qed.

Generated by coq2html