Set Implicit Arguments.
Require Import List.
Require Import MyTactics.
Require Import DeBruijn.
Require Import Layers.
Require Import Types.
Require Import TypeEquality.
-------------------------------------------------------------------------
We now wish to define a notion of head constructor and to prove that tensor
does not affect the head constructor, that is, for instance, if TyTensor T
U is an arrow, then T itself is an arrow. This requires quite a lot of
preparatory work.
Iterated application of tensor.
Definition tensors (
T :
ty) (
Us :
list ty) :
ty :=
fold_left (
fun T U =>
TyTensor T U)
Us T.
Definition composs (
T :
ty) (
Us :
list ty) :
ty :=
fold_left (
fun T U =>
TyCompos T U)
Us T.
Lemmas used as rewriting rules.
Lemma fold_tensors:
forall T A Us,
tensors (
TyTensor T A)
Us =
tensors T (
A ::
Us).
Proof.
auto.
Qed.
Lemma fold_composs:
forall T A Us,
composs (
TyCompos T A)
Us =
composs T (
A ::
Us).
Proof.
auto.
Qed.
Lemma composs_app:
forall T Ts Us,
composs (
composs T Ts)
Us =
composs T (
Ts ++
Us).
Proof.
tensors preserves well-formedness and type equality.
Lemma wf_tensors:
forall Us,
wfs Us ->
forall T,
wf T ->
wf (
tensors T Us).
Proof.
induction 1; simpl; eauto.
Qed.
Lemma wf_composs:
forall Us,
wfs Us ->
forall T,
wf T ->
wf (
composs T Us).
Proof.
induction 1; simpl; eauto.
Qed.
Hint Resolve wf_tensors wf_composs.
Lemma lift_tensors:
forall Us k T,
lift_ty k (
tensors T Us) =
tensors (
lift_ty k T) (
map (
lift_ty k)
Us).
Proof.
induction Us; simpl; intros; eauto.
rewrite IHUs. reflexivity.
Qed.
Lemma subst_tensors:
forall Us U k T,
subst_ty U k (
tensors T Us) =
tensors (
subst_ty U k T) (
map (
subst_ty U k)
Us).
Proof.
induction Us; simpl; intros; eauto.
rewrite IHUs. reflexivity.
Qed.
Lemma tyeq_tensors:
forall Us,
wfs Us ->
forall T1 T2,
tyeq T1 T2 ->
tyeq (
tensors T1 Us) (
tensors T2 Us).
Proof.
Lemma tyeq_composs:
forall Us,
wfs Us ->
forall T1 T2,
tyeq T1 T2 ->
tyeq (
composs T1 Us) (
composs T2 Us).
Proof.
tensors satisfies the equational theory of tensor. The following statements
unfortunately duplicate the definition of the equational theory. The proof is
shared via a tactic; it requires an induction to push the tensors down, one
after the other.
Ltac push_tensors :=
induction 1;
simpl;
intros; [
eauto
|
eapply tyeq_transitive; [
eapply tyeq_tensors; [
eassumption |
tyred_tyeq ]
|
eauto 6
|
eauto 8
]].
Lemma tensors_arrow:
forall Us,
wfs Us ->
forall T1 T2,
wf T1 ->
wf T2 ->
tyeq (
tensors (
TyArrow T1 T2)
Us) (
TyArrow (
composs T1 Us) (
composs T2 Us)).
Proof.
push_tensors.
Qed.
Lemma tensors_pair:
forall Us,
wfs Us ->
forall layer1 layer2 T1 T2,
wf T1 ->
wf T2 ->
tyeq (
tensors (
TyPair layer1 layer2 T1 T2)
Us) (
TyPair layer1 layer2 (
tensors T1 Us) (
tensors T2 Us)).
Proof.
push_tensors.
Qed.
Lemma tensors_unit:
forall Us,
wfs Us ->
forall layer,
tyeq (
tensors (
TyUnit layer)
Us) (
TyUnit layer).
Proof.
push_tensors.
Qed.
Lemma tensors_q:
forall Us,
wfs Us ->
forall q T,
wf T ->
tyeq (
tensors (
TyQ q T)
Us) (
TyQ q (
tensors T (
map (
lift_ty 0)
Us))).
Proof.
push_tensors.
Qed.
Lemma tensors_bang:
forall Us,
wfs Us ->
forall T,
wf T ->
tyeq (
tensors (
TyBang T)
Us) (
TyBang (
tensors T Us)).
Proof.
push_tensors.
Qed.
Lemma tensors_ref:
forall Us,
wfs Us ->
forall T,
wf T ->
tyeq (
tensors (
TyRef T)
Us) (
TyRef (
tensors T Us)).
Proof.
push_tensors.
Qed.
Lemma tensors_at:
forall Us,
wfs Us ->
forall T,
wf T ->
tyeq (
tensors (
TyAt T)
Us) (
TyAt T).
Proof.
push_tensors.
Qed.
Lemma tensors_regioncap:
forall Us,
wfs Us ->
forall rk sigma T,
wf sigma ->
wf T ->
tyeq (
tensors (
TyRegionCap rk sigma T)
Us) (
TyRegionCap rk sigma (
tensors T Us)).
Proof.
push_tensors.
Qed.
Lemma tensors_regioncappunched:
forall Us,
wfs Us ->
forall rho T sigma,
wf rho ->
wf T ->
wf sigma ->
tyeq (
tensors (
TyRegionCapPunched rho T sigma)
Us) (
TyRegionCapPunched rho (
tensors T Us)
sigma).
Proof.
push_tensors.
Qed.
Ltac tyred_tensors :=
first [
eapply tensors_arrow;
solve [
eauto ]
|
eapply tensors_pair;
solve [
eauto ]
|
eapply tensors_unit;
solve [
eauto ]
|
eapply tensors_q;
solve [
eauto ]
|
eapply tensors_bang;
solve [
eauto ]
|
eapply tensors_ref;
solve [
eauto ]
|
eapply tensors_at;
solve [
eauto ]
|
eapply tensors_regioncap;
solve [
eauto ]
|
eapply tensors_regioncappunched;
solve [
eauto ]
].
This tactic looks for a type equality hypothesis and reduces its right-hand
side via one step of tyred_tensors. It then argues that the equality is
impossible.
Ltac tyeq_reduce_impossible :=
match goal with h:
tyeq ?
T (
tensors _ _) |-
_ =>
let U :=
fresh "
U"
in
evar (
U :
ty);
assert (
tyeq T U);
unfold U; [
eapply tyeq_transitive; [
eexact h |
tyred_tensors |
wf ]
|
impossible
]
end.
Goal
forall U1 U2 Us layer1 layer2 T1 T2,
wfs Us ->
wf T1 ->
wf T2 ->
tyeq (
TyArrow U1 U2) (
tensors (
TyPair layer1 layer2 T1 T2)
Us) ->
False.
Proof.
intros. tyeq_reduce_impossible.
Qed.
Some types exhibit a head constructor, which is reliable, in the sense
that applications of tensor cannot change this head constructor.
Inductive tycon :=
|
TyConArrow:
tycon
|
TyConPair:
layer ->
layer ->
tycon
|
TyConUnit:
layer ->
tycon
|
TyConQ:
quantifier ->
tycon
|
TyConBang:
tycon
|
TyConRef:
tycon
|
TyConAt:
tycon
|
TyConRegionCap:
region_kind ->
tycon
|
TyConRegionCapPunched:
tycon.
Inductive has_tycon:
tycon ->
ty ->
Prop :=
|
HasArrow:
forall T1 T2,
has_tycon TyConArrow (
TyArrow T1 T2)
|
HasPair:
forall layer1 layer2 T1 T2,
has_tycon (
TyConPair layer1 layer2) (
TyPair layer1 layer2 T1 T2)
|
HasUnit:
forall layer,
has_tycon (
TyConUnit layer) (
TyUnit layer)
|
HasQ:
forall q T,
has_tycon (
TyConQ q) (
TyQ q T)
|
HasBang:
forall T,
has_tycon TyConBang (
TyBang T)
|
HasRef:
forall T,
has_tycon TyConRef (
TyRef T)
|
HasAt:
forall T,
has_tycon TyConAt (
TyAt T)
|
HasRegionCap:
forall rk T1 T2,
has_tycon (
TyConRegionCap rk) (
TyRegionCap rk T1 T2)
|
HasRegionCapPunched:
forall T1 T2 t3,
has_tycon TyConRegionCapPunched (
TyRegionCapPunched T1 T2 t3)
.
Inductive exhibits_tycon:
tycon ->
ty ->
Prop :=
|
ExhibitsTyCon:
forall tc T U,
tyeq U T ->
has_tycon tc U ->
wf U ->
exhibits_tycon tc T.
Hint Constructors has_tycon exhibits_tycon.
Lemma has_exhibits:
forall tc T,
wf T ->
has_tycon tc T ->
exhibits_tycon tc T.
Proof.
Lemma exhibits_tyeq:
forall tc T,
exhibits_tycon tc T ->
forall U,
tyeq T U ->
wf T ->
exhibits_tycon tc U.
Proof.
Ltac htc :=
match goal with h:
has_tycon _ _ |-
_ =>
depelim h;
hereditary wf end.
Lemma exhibits_tensor:
forall tc T U,
exhibits_tycon tc T ->
wf U ->
exhibits_tycon tc (
TyTensor T U).
Proof.
Hint Resolve has_exhibits exhibits_tyeq.
Some constructors are inert, in the sense that tensor does not react with
them. This includes TyVar and TyRegion. (We could have stipulated that
tensor vanishes at TyRegion, but it did not seem useful to do so.) As a
result, the following types are inert, in the sense that the equational
theory does not allow them to be simplified.
Inductive inert:
ty ->
Prop :=
|
InertVar:
forall x,
inert (
TyVar x)
|
InertRegion:
forall r,
inert (
TyRegion r)
|
InertTensor:
forall T U,
inert T ->
inert (
TyTensor T U).
Hint Constructors inert.
Lemma inert_tensors:
forall Us T,
inert T ->
inert (
tensors T Us).
Proof.
induction Us; simpl; eauto.
Qed.
Local Hint Resolve inert_tensors.
Lemma tyred_inert:
forall T,
inert T ->
forall U,
tyred T U ->
False.
Proof.
induction 1 as [ | | ? ? it ]; introv h.
eauto with tyred.
eauto with tyred.
tyred; dependent destruction it; eauto with tyred.
Qed.
Hint Resolve tyred_inert :
tyred.
An inert type cannot exhibit a head constructor.
Lemma exhibits_tycon_inert:
forall tc T U,
tyeq T U ->
inert U ->
has_tycon tc T ->
False.
Proof.
introv e i htc.
specializes e 1.
dependent destruction e; dependent destruction i; dependent destruction htc; eauto 3 with tyred.
Qed.
Goal
forall T1 T2 U,
inert U ->
tyeq (
TyArrow T1 T2)
U ->
False.
Proof.
The ordering tmo is used in the proof of the main result. It allows
descending into the left-hand side of a tensor and unfolding recursive
types. Its well-foundedness derives from the fact that tmo is included
within tto. In fact, it is included within the first level of tto.
Inductive tmo:
ty ->
ty ->
Prop :=
|
TmoTensor:
forall T1 T2,
wf T1 ->
tmo T1 (
TyTensor T1 T2)
|
TmoMu:
forall T1 T2,
tyredmu T1 T2 ->
wf T2 ->
tmo T2 T1.
Hint Constructors tmo.
Lemma tmo_tto:
forall kt,
Acc tto kt ->
forall T,
kt = (1,
T) ->
Acc tmo T.
Proof.
induction 1 as [ kt ? IH ]. intros. subst kt.
econstructor. intros ? h. dependent destruction h; eauto.
Qed.
Lemma tmo_well_founded:
well_founded tmo.
Proof.
This is the main result: if tensors U Us is an arrow, then U itself is
an arrow. More generally, if tensors U Us exhibits some head constructor
tc, then U exhibits the same head constructor.
The proof is by well-founded induction over tmo. In the tensor case, the
list Us grows -- which explains why induction over Us would not make
sense, and also explains why we need to introduce tensors in the first
place.
Ltac quantifiers :=
match goal with
|
quantifier:
quantifier |-
_ =>
destruct quantifier;
quantifiers
|
_ =>
idtac
end.
Ltac region_kinds :=
match goal with
|
rk:
region_kind |-
_ =>
destruct rk;
region_kinds
|
_ =>
idtac
end.
Lemma if_tensor_exhibits_tycon_preliminary:
forall U,
Acc tmo U ->
wf U ->
forall tc Us,
exhibits_tycon tc (
tensors U Us) ->
wfs Us ->
exhibits_tycon tc U.
Proof.
Reason by induction over the fact that U is tmo-accessible.
induction 1
as [
U ?
IH ];
introv hwf hx;
intros.
Reason by cases over U. The cases TyMu and TyTensor are difficult
and can be done without further case analysis, so we set them aside.
All other cases require case analysis over tc, and each sub-case is
then either trivial or impossible.
destruct hwf;
match goal with
| |-
exhibits_tycon _ (
TyMu _) =>
idtac
| |-
exhibits_tycon _ (
TyTensor _ _) =>
idtac
|
_ =>
dependent destruction hx;
Perform case analysis over the head constructor tc.
htc;
Furthermore, if the head constructor involves layers, quantifiers,
or region kinds, perform case analysis over these. This is
quite dumb and expensive, but avoids some tedious reasoning.
layers;
quantifiers;
region_kinds;
try solve [
false;
eauto 3
using exhibits_tycon_inert
|
eauto 3
|
tyeq_reduce_impossible
]
end.
Two goals should remain.
TyMu
The idea is to unfold the recursive type and continue. By the induction
hypothesis, the unfolded type exhibits the desired head constructor; so
the original type exhibits this head constructor as well.
dependent destruction hx.
forwards f:
IH.
eauto using wf_unfold.
eauto using wf_unfold.
econstructor.
eapply tyeq_transitive.
eassumption.
eapply tyeq_tensors.
eassumption.
eauto using tyeq_unfold.
wf.
eassumption.
wf.
wf.
eapply exhibits_tyeq.
eassumption.
eauto using tyeq_symmetric,
tyeq_unfold.
eauto using wf_unfold.
TyTensor T1 T2
The idea is to descend into the left-hand side T1 of the tensor, pushing its
right-hand side T2 onto the stack Us. By the induction hypothesis, T1
exhibits the desired head constructor; so TyTensor T1 T2 exhibits it as well.
forwards: (>>>
IH (
T2 ::
Us)).
eauto.
wf.
eassumption.
wf.
eauto using exhibits_tensor.
Qed.
Lemma if_tensor_exhibits_tycon:
forall U tc Us,
exhibits_tycon tc (
tensors U Us) ->
wf U ->
wfs Us ->
exhibits_tycon tc U.
Proof.
The following tactic simplifies a hypothesis of the form
exhibits_tycon _
[TyTensor _ _)]. The hypothesis is transformed into one that no longer
involves the tensor. This is repeated if necessary; when this process is
over, the hypothesis is inverted. *)
Ltac if_tensor_exhibits_tycon :=
match goal with
| h: exhibits_tycon _ (TyTensor _ ?U) |- _ =>
forwards: (>>> if_tensor_exhibits_tycon (U :: nil)); [
simpl; eexact h | wf | wf | clear h; if_tensor_exhibits_tycon
]
| h: exhibits_tycon _ (tensors _ _) |- _ =>
forwards: if_tensor_exhibits_tycon; [
eexact h | wf | wf | clear h; if_tensor_exhibits_tycon
]
| h: exhibits_tycon _ _ |- _ =>
depelim h; htc
end.
(* A corollary, just for the paper. *)
Lemma if_tensor_exhibits_arrow:
forall T1 T2,
wf T1 ->
wf T2 ->
(exists U1 U2, tyeq (TyTensor T1 T2) (TyArrow U1 U2) /\ wf U1 /\ wf U2) ->
(exists U1 U2, tyeq T1 (TyArrow U1 U2) /\ wf U1 /\ wf U2).
Proof.
intros. unpack.
assert (exhibits_tycon TyConArrow (TyTensor T1 T2)).
eauto using tyeq_symmetric.
if_tensor_exhibits_tycon.
intuition eauto 6 using tyeq_symmetric.
Qed.
(* ------------------------------------------------------------------------- *)
(* Iterated application of tensor, the other way round. *)
Definition srosnet (T : ty) (Us : list ty) : ty :=
fold_right (fun U T => TyTensor T U) T Us.
Lemma tensors_srosnet:
forall T Us,
tensors T Us = srosnet T (rev Us).
Proof.
intros. unfold tensors, srosnet. symmetry. eapply fold_left_rev_right.
Qed.
Lemma tensors_snoc:
forall T Us U,
TyTensor (tensors T Us) U = tensors T (Us ++ U :: nil).
Proof.
intros. repeat rewrite tensors_srosnet. rewrite distr_rev. simpl. reflexivity.
Qed.
Definition ssopmoc (T : ty) (Us : list ty) : ty :=
fold_right (fun U T => TyCompos T U) T Us.
Lemma composs_ssopmoc:
forall T Us,
composs T Us = ssopmoc T (rev Us).
Proof.
intros. unfold composs, ssopmoc. symmetry. eapply fold_left_rev_right.
Qed.
Lemma composs_snoc:
forall T Us U,
TyCompos (composs T Us) U = composs T (Us ++ U :: nil).
Proof.
intros. repeat rewrite composs_ssopmoc. rewrite distr_rev. simpl. reflexivity.
Qed.
(* ------------------------------------------------------------------------- *)
(* Commutative pairs. *)
Definition commutative_pair T U T' U' :=
wf T' /\ wf U' /\
tyeq T' (TyTensor T U') /\
tyeq U' (TyTensor U T').
(* Basic properties of commutative pairs. *)
Lemma commutative_pair_wf_first:
forall A B A' B',
commutative_pair A B A' B' ->
wf A'.
Proof.
unfold commutative_pair; intuition eauto.
Qed.
Lemma commutative_pair_wf_second:
forall A B A' B',
commutative_pair A B A' B' ->
wf B'.
Proof.
unfold commutative_pair; intuition eauto.
Qed.
Hint Resolve commutative_pair_wf_first commutative_pair_wf_second.
Lemma commutative_pair_symmetric:
forall A B A' B',
commutative_pair A B A' B' ->
commutative_pair B A B' A'.
Proof.
unfold commutative_pair. intuition eauto.
Qed.
Hint Immediate commutative_pair_symmetric.
Lemma lift_commutative_pair:
forall A B A' B',
commutative_pair A B A' B' ->
forall k,
commutative_pair (lift_ty k A) (lift_ty k B) (lift_ty k A') (lift_ty k B').
Proof.
intros U V U' V'; unfold commutative_pair; intuition eauto.
eapply tyeq_lift with (U := TyTensor U V'). assumption.
eapply tyeq_lift with (U := TyTensor V U'). assumption.
Qed.
Lemma subst_commutative_pair:
forall A B A' B',
commutative_pair A B A' B' ->
forall U k,
wf U ->
commutative_pair (subst_ty U k A) (subst_ty U k B) (subst_ty U k A') (subst_ty U k B').
Proof.
intros U V U' V'; unfold commutative_pair; intros ? T k ?; intuition eauto.
eapply tyeq_subst with (T2 := TyTensor U V'); auto.
eapply tyeq_subst with (T2 := TyTensor V U'); auto.
Qed.
Hint Resolve lift_commutative_pair subst_commutative_pair.
(* Out of two types [T] and [U], the commutative pair lemma produces two new
types [T'] and [U'], which are characterized by two mutually recursive
equations. This lemma plays a key role in the revelation lemma, in the case
of the anti-frame rule. *)
Lemma commutative_pair_existence:
forall T U,
wf T ->
wf U ->
exists T' U',
commutative_pair T U T' U'.
Ltac cp_simpl :=
unfold unfold; simpl; repeat rewrite subst_lift_ty; repeat rewrite subst_var_identity.
Proof.
generalize contractive_lift_3; intros.
exists (TyMu (TyTensor (lift_ty 0 T) (TyTensor (lift_ty 0 U) (TyVar 0)))).
exists (TyMu (TyTensor (lift_ty 0 U) (TyTensor (lift_ty 0 T) (TyVar 0)))).
intuition idtac. wf. wf.
(* We are comparing two different finite expressions of a single infinite type.
Here, the usual fold/unfold rules are not powerful enough: we must use the
uniqueness of solutions of contractive fixed point equations. *)
eapply tyeq_symmetric.
eapply contractive_type_equations_have_solution_mu; [ wf | cp_simpl | wf ].
eapply tyeq_tensor; eauto.
equates 1. eapply tyeq_unfold; wf. cp_simpl; reflexivity.
(* The two equations are symmetric, so we duplicate the above four-line
proof. It would also be possible to use the fact that the the second
equation follows from the first one by substitution. *)
eapply tyeq_symmetric.
eapply contractive_type_equations_have_solution_mu; [ wf | cp_simpl | wf ].
eapply tyeq_tensor; eauto.
equates 1. eapply tyeq_unfold; wf. cp_simpl; reflexivity.
Qed.
(* This lemma unfolds the definition of composition, distributes
tensor over a pair, and exploits the definition of commutative
pairs in order to replace [TyTensor A B'] with [A']. *)
Lemma exploit_commutative_pair_2:
forall T A B A' B',
commutative_pair A B A' B' ->
wf A ->
wf B ->
wf T ->
tyeq (TyTensor (TyCompos T B) A') (TyMixPair (TyTensor (TyTensor T B) A') B').
Proof.
introv [ ? [ ? [ ? ? ]]]; intros.
eapply tyeq_transitive; [ eapply tyeq_tensor_pair; wf | idtac | wf ].
eapply tyeq_pair; eauto using tyeq_symmetric.
Qed.
Lemma exploit_commutative_pair:
forall T A B A' B',
commutative_pair A B A' B' ->
wf T ->
wf A ->
wf B ->
tyeq (TyMixPair (TyMixPair (TyTensor (TyTensor T A) B') A') B')
(TyCompos (TyCompos T A) B').
Proof.
eauto 6 using tyeq_pair, tyeq_symmetric, exploit_commutative_pair_2.
Qed.