Module Coercions

Set Implicit Arguments.
Require Import MyTactics.
Require Import DeBruijn.
Require Import Layers.
Require Import FocusPaths.

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

We are interested in a call-by-value semantics. We use administrative normal form, also known as fine-grain call-by-value: that is, we distinguish between values and terms, inject values into terms, and reduce the number of evaluation contexts to the bare minimum.

Coercions are explicit witnesses of the subtyping relationship.

Coercions do not contain any type variables or term variables. They contain coercion variables, which can be bound by CoMu to form recursive coercions, following the Amadio/Cardelli and Brandt/Henglein formulations of subtyping for recursive types.

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

The body of a CoMu coercion must be contractive in the bound variable; this is stated as part of the typing judgement.

A coercion is contractive with respect to variable k if k occurs only under contractive coercion constructors.

The following table tells which coercion constructors are contractive: CoSeq not contractive CoArrow contractive in both arguments CoPair contractive in both arguments, if both layers are physical CoForall not contractive CoExists not contractive CoBang not contractive CoRegionCap not contractive CoRegionCapPunched not contractive CoRef contractive CoMu not contractive

A coercion c is well-formed if, within c, the body of every recursive coercion is contractive with respect to the mu-bound variable.

Inductive cwf : coercion -> Prop :=
| WfCoId:
    cwf CoId
| WfCoSeq:
    forall c1 c2,
    cwf c1 ->
    cwf c2 ->
    cwf (CoSeq c1 c2)
| WfCoForallIntro:
    cwf CoForallIntro
| WfCoForallElim:
    cwf CoForallElim
| WfCoExistsIntro:
    cwf CoExistsIntro
| WfCoExistsLeftIntro:
    cwf CoExistsLeftIntro
| WfCoExistsElim:
    cwf CoExistsElim
| WfCoArrow:
    forall c1 c2,
    cwf c1 ->
    cwf c2 ->
    cwf (CoArrow c1 c2)
| WfCoPair:
    forall layer1 layer2 c1 c2,
    cwf c1 ->
    cwf c2 ->
    cwf (CoPair layer1 layer2 c1 c2)
| WfCoForall:
    forall c,
    cwf c ->
    cwf (CoForall c)
| WfCoExists:
    forall c,
    cwf c ->
    cwf (CoExists c)
| WfCoBang:
    forall c,
    cwf c ->
    cwf (CoBang c)
| WfCoRegionCap:
    forall c,
    cwf c ->
    cwf (CoRegionCap c)
| WfCoRegionCapPunched:
    forall c,
    cwf c ->
    cwf (CoRegionCapPunched c)
| WfCoRef:
    forall c,
    cwf c ->
    cwf (CoRef c)
| WfCoDereliction:
    cwf CoDereliction
| WfCoBangIdempotent:
    cwf CoBangIdempotent
| WfCoPairBang:
    cwf CoPairBang
| WfCoBangPair:
    cwf CoBangPair
| WfCoUnitBang:
    cwf CoUnitBang
| WfCoBangRef:
    cwf CoBangRef
| WfCoBangRegionCap:
    cwf CoBangRegionCap
| WfCoBangRegionCapPunched:
    cwf CoBangRegionCapPunched
| WfCoAtBang:
    cwf CoAtBang
| WfCoDistrib:
    cwf CoDistrib
| WfCoSingletonToGroup:
    cwf CoSingletonToGroup
| WfCoForallPair:
    cwf CoForallPair
| WfCoForallBang:
    cwf CoForallBang
| WfCoForallRef:
    cwf CoForallRef
| WfCoForallRegionCap:
    cwf CoForallRegionCap
| WfCoForallRegionCapPunched:
    cwf CoForallRegionCapPunched
| WfCoSingletonRegionCapExists:
    cwf CoSingletonRegionCapExists
| WfCoPairExistsLeft:
    cwf CoPairExistsLeft
| WfCoPairExistsRight:
    cwf CoPairExistsRight
| WfCoBangExists:
    cwf CoBangExists
| WfCoRefExists:
    cwf CoRefExists
| WfCoDefocus:
    forall pi,
    cwf (CoDefocus pi)
| WfCoDefocusGroup:
    cwf CoDefocusGroup
| WfCoStarCommutative:
    cwf CoStarCommutative
| WfCoStarAssociative:
    cwf CoStarAssociative
| WfCoStarRef:
    cwf CoStarRef
| WfCoRefStar:
    cwf CoRefStar
| WfCoStarSingleton:
    cwf CoStarSingleton
| WfCoSingletonStar:
    cwf CoSingletonStar
| WfCoTensorExchange:
    forall n,
    cwf (CoTensorExchange n)
| WfCoVar:
    forall x,
    cwf (CoVar x)
| WfCoMu:
    forall c,
    cwf c ->
    ccontractive 0 c ->
    cwf (CoMu c)
.

Hint Constructors cwf.

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

De Bruijn operations over coercions.

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

Unfolding the body of a recursive coercion.

Definition cunfold c :=
subst_co (CoMu c) 0 c.

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

De Bruijn lemmas.

Lemma subst_lift_co:
subst_lift lift_co subst_co.

Proof.

subst_lift_tac.
Qed.

Local Hint Resolve subst_lift_co.

Lemma lift_lift_co:
lift_lift lift_co.

Proof.

lift_lift_tac.
Qed.

Local Hint Resolve lift_lift_co.

Lemma lift_zero_lift_co:
lift_zero_lift lift_co.

Proof.

lift_zero_lift_tac.
Qed.

Ltac lzl_co :=
lzl lift_co lift_zero_lift_co.

Hint Extern 1 => lzl_co : lift_subst_1_db.
Hint Extern 1 => lzl_co : lift_subst_2_db.
Hint Extern 1 => lzl_co : subst_subst_db.

Lemma lift_subst_1_co:
lift_subst_1 lift_co lift_co subst_co.

Proof.

lift_subst_1_tac.
Qed.

Local Hint Resolve lift_subst_1_co.

Hint Extern 1 => rewrite lift_subst_1_co; [ idtac | omega ] : subst_subst_db.

Lemma lift_subst_2_co:
lift_subst_2 lift_co lift_co subst_co.

Proof.

lift_subst_2_tac.
Qed.

Local Hint Resolve lift_subst_2_co.

Lemma subst_subst_co:
subst_subst lift_co subst_co subst_co.

Proof.

subst_subst_tac.
Qed.

Local Hint Resolve subst_subst_co.

These hints are useful in certain lemmas.

Hint Extern 1 => rewrite lift_subst_2_co : weaken_co.

Hint Extern 1 => rewrite <- lift_lift_co : weaken_co.

More De Bruijn lemmas about cunfold.

Lemma cunfold_lift:
  forall k c,
  lift_co k (cunfold c) =
  cunfold (lift_co (S k) c).

Proof.

unfold cunfold. intuition eauto with weaken_co.
Qed.

Lemma cunfold_subst:
  forall k c d,
  subst_co d k (cunfold c) =
  cunfold (subst_co (lift_co 0 d) (S k) c).

Proof.

unfold cunfold. intros. rewrite subst_subst_co. auto. omega.
Qed.

Lemma cunfold_subst_mu:
  forall k c d,
  subst_co (CoMu d) k (cunfold c) =
  cunfold (subst_co (CoMu (lift_co 1 d)) (S k) c).

Proof.

intros. rewrite cunfold_subst. reflexivity.
Qed.

More De Bruijn lemmas about contractiveness.

Lemma ccontractive_lift_1:
  forall k1 c,
  ccontractive k1 c ->
  forall k2,
  k1 >= k2 ->
  ccontractive (S k1) (lift_co k2 c).

Proof.

induction 1; intros; simpl; eauto.
constructor. unfold lift_var; by_cases; easy.
Qed.

Lemma ccontractive_lift_2:
  forall k1 c,
  ccontractive k1 c ->
  forall k2,
  k1 < k2 ->
  ccontractive k1 (lift_co k2 c).

Proof.

induction 1; intros; simpl; eauto.
constructor. unfold lift_var; by_cases; easy.
Qed.

Lemma ccontractive_lift_3:
forall c k,
ccontractive k (lift_co k c).

Proof.

induction c; simpl; intros; eauto.
constructor. unfold lift_var; by_cases; easy.
Qed.

Lemma ccontractive_subst_1:
  forall c d k1,
  ccontractive k1 d ->
  ccontractive (S k1) c ->
  forall k2,
  k1 >= k2 ->
  ccontractive k1 (subst_co d k2 c).

Proof.

induction c; simpl; introv hd hc ?; dependent destruction hc; eauto using ccontractive_lift_1.
unfold subst_var. by_cases; eauto.
Qed.

Lemma ccontractive_subst_2:
  forall c d k1,
  ccontractive k1 d ->
  ccontractive k1 c ->
  forall k2,
  k1 < k2 ->
  ccontractive k1 (subst_co d k2 c).

Proof.

induction c; simpl; introv hd hc ?; dependent destruction hc; eauto using ccontractive_lift_1.
unfold subst_var. by_cases; eauto.
Qed.

Lemma ccontractive_cunfold:
  forall k c,
  ccontractive (S k) c ->
  ccontractive k (cunfold c).

Proof.

unfold cunfold. eauto using ccontractive_subst_1.
Qed.

Lemma cwf_lift:
  forall c,
  cwf c ->
  forall k,
  cwf (lift_co k c).

Proof.

induction 1; intros; simpl; eauto using ccontractive_lift_2.
Qed.

Lemma cwf_subst:
  forall c,
  cwf c ->
  forall d k,
  cwf d ->
  cwf (subst_co d k c).

Proof.

induction 1; intros; simpl; eauto.

CoVar

unfold subst_var. by_cases; easy.

CoMu

eauto using cwf_lift, ccontractive_subst_2, ccontractive_lift_3.
Qed.

Lemma cwf_cunfold:
  forall c,
  cwf c ->
  ccontractive 0 c ->
  cwf (cunfold c).

Proof.

intros. apply cwf_subst; eauto.
Qed.

Lemma cwf_mu:
  forall c,
  cwf (CoMu c) ->
  ccontractive 0 c.

Proof.

inversion 1. auto.
Qed.

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

Some derived coercions.

At this point, we give only the definitions of these derived coercions, not their typing rules -- see DerivedSubtyping.

Definition CoTyEq c :=
  CoSeq CoId (CoSeq c CoId).

Lemma ContractiveCoTyEq:
  forall k c,
  ccontractive k c ->
  ccontractive k (CoTyEq c).

Proof.

econstructor; eauto.
Qed.

Lemma WfCoTyEq:
  forall c,
  cwf c ->
  cwf (CoTyEq c).

Proof.

econstructor; eauto.
Qed.

Hint Resolve ContractiveCoTyEq WfCoTyEq.

Definition CoExistsPairDistrib layer1 layer2 :=
  CoSeq (CoExists (CoPair layer1 layer2 CoExistsIntro CoExistsIntro)) CoExistsElim.

Definition CoExistsScopeRestrictionLeft layer1 layer2 :=
  CoSeq (CoExistsPairDistrib layer1 layer2) (CoPair layer1 layer2 CoId CoExistsElim).

Definition CoExistsScopeRestrictionRight layer1 layer2 :=
  CoSeq (CoExistsPairDistrib layer1 layer2) (CoPair layer1 layer2 CoExistsElim CoId).

Definition CoForallPairLeft layer1 layer2 :=
  CoSeq CoForallPair (CoPair layer1 layer2 CoId CoForallElim).

Lemma ContractiveCoForallPairLeft:
  forall k layer1 layer2,
  ccontractive k (CoForallPairLeft layer1 layer2).

Proof.

econstructor; eauto.
Qed.

Lemma WfCoForallPairLeft:
forall layer1 layer2,
cwf (CoForallPairLeft layer1 layer2).

Proof.

econstructor; eauto.
Qed.

Hint Resolve ContractiveCoForallPairLeft WfCoForallPairLeft.

Definition CoForallPairExtrusion layer1 layer2 :=
  CoSeq CoForallIntro (CoForall (CoPair layer1 layer2 CoForallElim CoForallElim)).

Definition CoForallExtrusion cc :=
  CoSeq CoForallIntro (CoForall (cc CoForallElim)).

Definition CoForallPairExtrusionLeft layer1 layer2 :=
  CoSeq CoForallIntro (CoForall (CoPair layer1 layer2 CoForallElim CoId)).

Lemma ContractiveCoForallPairExtrusionLeft:
  forall k layer1 layer2,
  ccontractive k (CoForallPairExtrusionLeft layer1 layer2).

Proof.

econstructor; eauto.
Qed.

Lemma WfCoForallPairExtrusionLeft:
forall layer1 layer2,
cwf (CoForallPairExtrusionLeft layer1 layer2).

Proof.

econstructor; eauto.
Qed.

Hint Resolve ContractiveCoForallPairExtrusionLeft WfCoForallPairExtrusionLeft.

Definition CoExistsLeftIntroReversed :=
  CoSeq CoForallIntro (CoForall (CoArrow CoExistsIntro CoId)).

Definition CoExistsPairIntrusion layer1 layer2 :=
  CoSeq (CoExists (CoPair layer1 layer2 CoExistsIntro CoExistsIntro)) CoExistsElim.

Definition CoExistsIntrusion cc :=
  CoSeq (CoExists (cc CoExistsIntro)) CoExistsElim.

Definition CoExistsCap :=
  CoExistsIntrusion CoRegionCap.

Definition CoPairBangReversed :=
  CoSeq CoBangPair CoDereliction.

Definition CoBangPairReversed layer1 layer2 :=
  CoBang (CoPair layer1 layer2 CoDereliction CoDereliction).

Definition CoStarAssociativeReversed layer1 layer2 layer3 :=
  CoSeq(

1(23)

CoStarCommutative
)(CoSeq(

(23)1

CoPair (layer_conj layer2 layer3) layer1 CoStarCommutative CoId
)(CoSeq(

(32)1

CoStarAssociative
)(CoSeq(

3(21)

CoStarCommutative
)(

(21)3

CoPair (layer_conj layer2 layer1) layer3 CoStarCommutative CoId

(12)3

  )))).

Lemma cwf_CoStarAssociativeReversed:
  forall layer1 layer2 layer3,
  cwf (CoStarAssociativeReversed layer1 layer2 layer3).

Proof.

repeat econstructor.
Qed.

Hint Resolve cwf_CoStarAssociativeReversed.

Definition CoMixPairExchange :=
CoSeq(

(12)3

CoStarAssociative
)(CoSeq(

1(23)

CoPair Physical Logical CoId CoStarCommutative
)(

1(32)

CoStarAssociativeReversed Physical Logical Logical

(13)2

)).

Lemma cwf_CoMixPairExchange:
cwf CoMixPairExchange.

Proof.

repeat econstructor.
Qed.

Hint Resolve cwf_CoMixPairExchange.

Definition CoComposExchange :=
CoTyEq (CoSeq (CoMixPair (CoMixPair (CoTensorExchange 0) CoId) CoId) CoMixPairExchange).

Lemma cwf_CoComposExchange:
cwf CoComposExchange.

Proof.

repeat econstructor.
Qed.

Hint Resolve cwf_CoComposExchange.

Definition CoMixPairComposExchange :=
CoSeq CoMixPairExchange CoId.

Lemma cwf_CoMixPairComposExchange:
cwf CoMixPairComposExchange.

Proof.

repeat econstructor.
Qed.

Hint Resolve cwf_CoMixPairComposExchange.

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

The revelation lemma for subtyping can be viewed as the statement that the covariance of tensor in its first argument is admissible: if T1 <= T2 holds, then TyTensor T1 U <= TyTensor T2 U holds as well.

In fact, the coercion that proves the latter assertion is almost identical to the coercion that proves the former. The only difference lies in the insertion of some extra CoId steps, which are required in order to allow us to take advantage of the equational theory of tensor. One could eliminate this noise, at the cost of adding more tyeq premises in the definition of the subtyping judgement.

co_tensor witnesses the covariance of tensor in its left-hand argument. It is not a new coercion constructor, but a function: that is, the covariance of tensor is an admissible rule.

The parameter n carried by CoTensorExchange can be viewed as an indication of the presence of n suspended applications of co_tensor. So, applying co_tensor once more just increments n.

      CoTensorExchange (S n)
  end.

Lemma contractive_co_tensor:
  forall k c,
  ccontractive k c ->
  ccontractive k (co_tensor c).

Proof.

induction 1; simpl; eauto.
Qed.

Lemma cwf_co_tensor:
  forall c,
  cwf c ->
  cwf (co_tensor c).

Proof.

induction 1; simpl; eauto using contractive_co_tensor.
Qed.

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

Is TyCompos covariant in its left-hand argument? Yes, in the same way as tensor is covariant in its left-hand argument: that is, this is an admissible rule.

Definition co_compos c :=
  CoMixPair (co_tensor c) CoId.

Lemma cwf_co_compos:
  forall c,
  cwf c ->
  cwf (co_compos c).

Proof.

unfold co_compos. eauto using cwf_co_tensor.
Qed.

The same holds of iterated applications of TyCompos.

Fixpoint co_composs n c :=
  match n with
  | 0 =>
      c
  | S n =>
      co_composs n (co_compos c)
  end.

Lemma cwf_co_composs:
  forall n c,
  cwf c ->
  cwf (co_composs n c).

Proof.

induction n; simpl; eauto using cwf_co_compos.
Qed.

The following coercion exchanges two compositions under a context of n compositions. It plays a role in the operational semantics of CoTensorExchange.

Definition CoComposExchangeUnder n :=
  co_composs n CoComposExchange.

Lemma cwf_CoComposExchangeUnder:
  forall n,
  cwf (CoComposExchangeUnder n).

Proof.

unfold CoComposExchangeUnder. eauto using cwf_co_composs, cwf_CoComposExchange.
Qed.