Set Implicit Arguments.
Require Import MyTactics.
Require Import DeBruijn.
Require Import Types.
Require Import TypeEquality.
Require Import Programs.
Require Import Typing.
Require Import Environments.
Require Import Multiplicity.
Require Import MultiplicityEnvironments.
Require Import PreliminaryLemmas.
Require Import Resources.
Require Import ResourcesContinued.
Require Import ResourcesReconfiguration.
Require Import Closed.
-------------------------------------------------------------------------
Stability of typing by term substitution.
-------------------------------------------------------------------------
Hints.
Local Hint Resolve jenv_neutral_zero jenv_neutral_one jenv_neutral_infinity.
Local Hint Extern 1 =>
rewrite neutral_remove.
Hint Extern 1 =>
rewrite remove_env_entry_simpl :
remove_env_entry_simpl.
-------------------------------------------------------------------------
In the right-hand side of THide, substitutions simply disappear, because
the right-hand side of hide x = v in t is closed -- it has no free
variables other than x.
Ltac hide_rhs :=
let r :=
fresh "
r"
in
forwards r:
subst_term_overshoot; [
eassumption |
idtac |
rewrite r;
eassumption ];
simpl;
omega.
-------------------------------------------------------------------------
First comes the vacuous substitution lemma: if the variable that we are
substituting for has multiplicity zero, then, without any hypotheses on
the term that is substituted for this variable, the result is well-typed.
This is really a weakening lemma in disguise.
Lemma j_value_term_substitution_zero:
(
forall R1 M1 E v T,
jv R1 M1 E v T ->
mark_ih (
forall k,
jenv M1 k MZero ->
forall w :
value,
jv R1 (
remove_env_entry k M1) (
remove_env_entry k E) (
subst_value w k v)
T
)
) /\ (
forall R vs T,
ji R vs T ->
True
) /\ (
forall R1 M1 E t T,
jt R1 M1 E t T ->
mark_ih (
forall k,
jenv M1 k MZero ->
forall w :
value,
jt R1 (
remove_env_entry k M1) (
remove_env_entry k E) (
subst_term w k t)
T
)
).
Proof.
By induction...
apply jvit_ind;
intros_ih;
simpl;
Identify the cases that split the resource/multiplicity environment.
try match goal with
|
h1:
jenv ?
M ?
k MZero,
h2:
star ?
M1 ?
M2 ?
M |-
_ =>
unpack (
split_zero h1 h2)
end;
Set aside or solve several special cases.
try match goal with
fail 1 causes this match goal to fail, and thanks to
the enclosing try, we fall out.
| |-
jv _ _ _ (
VVar _)
_ =>
fail 1
| |-
jv _ _ _ (
VInhabitant _)
_ =>
rewrite closed_value_subst;
eauto
| |-
jt _ _ _ (
THide _ _)
_ =>
econstructor;
eauto 2;
hide_rhs
The following is the general case.
|
_ =>
Apply the same typing rule as in the original derivation; discharge any easy premises.
econstructor;
eauto 2;
If the goal is a star hypothesis, it is easily solved like this:
try solve [
eapply split_as_dictated;
eassumption ];
Rewrite, so as to make the induction hypothesis applicable.
repeat rewrite remove_lift_env;
repeat rewrite remove_env_entry_simpl;
repeat rewrite neutral_remove;
Apply the induction hypothesis and conclude.
use_ih;
eauto
end.
Deal with the cases that were set aside.
VVar
unfold subst_var.
inspect_cases;
intro.
eauto using jenv_substitution_recent.
subst.
jenv_uniqueness.
match goal with h:
nonzero MZero |-
_ =>
inversion h end.
eauto using jenv_substitution_old.
Qed.
Lemma j_value_substitution_zero:
forall R1 M1 E v T,
jv R1 M1 E v T ->
forall k,
jenv M1 k MZero ->
forall w,
jv R1 (
remove_env_entry k M1) (
remove_env_entry k E) (
subst_value w k v)
T.
Proof.
Lemma j_term_substitution_zero:
forall R1 M1 E t T,
jt R1 M1 E t T ->
forall k,
jenv M1 k MZero ->
forall w,
jt R1 (
remove_env_entry k M1) (
remove_env_entry k E) (
subst_term w k t)
T.
Proof.
Lemma j_term_substitution_zero_0:
forall R1 M1 E t T U,
jt R1 (
M1;;
MZero) (
E;;
U)
t T ->
forall v,
jt R1 M1 E (
subst_term v 0
t)
T.
Proof.
-------------------------------------------------------------------------
Next comes the linear substitution lemma, where the variable that we are
substituting for has multiplicity one.
Local Hint Resolve jenv_lift j_value_substitution_zero
j_term_substitution_zero j_value_weakening_remove
j_ty_weakening_value_remove j_value_resource_weakening
j_term_resource_weakening :
j_substitution_one.
Lemma j_value_term_substitution_one:
(
forall R1 M1 E v T,
jv R1 M1 E v T ->
mark_ih (
forall k U,
jenv M1 k MOne ->
jenv E k U ->
forall R2 M2 u M R,
star R1 R2 R ->
star (
remove_env_entry k M1)
M2 M ->
jv R2 M2 (
remove_env_entry k E)
u U ->
jv R M (
remove_env_entry k E) (
subst_value u k v)
T
)
) /\ (
forall R vs T,
ji R vs T ->
True
) /\ (
forall R1 M1 E t T,
jt R1 M1 E t T ->
mark_ih (
forall k U,
jenv M1 k MOne ->
jenv E k U ->
forall R2 M2 u M R,
star R1 R2 R ->
star (
remove_env_entry k M1)
M2 M ->
jv R2 M2 (
remove_env_entry k E)
u U ->
jt R M (
remove_env_entry k E) (
subst_term u k t)
T
)
).
Proof.
By induction...
apply jvit_ind;
intros_ih;
simpl;
Identify the cases that split the resource/multiplicity environment.
try match goal with
|
h1:
star _ _ ?
R,
h2:
star ?
R _ _ |-
_ =>
The variable of interest, k, has multiplicity one, so it is used
either on the left-hand side, or on the right-hand side. This gives
rise to two sub-cases.
In the sub-case 0+1, M1 is split as M1a + M1b. Furthermore, M1\k + M2 is
M. The variables in M2 must be sent into the right-hand side, so we must
write M1a\k + (M1b\k + M2) = M. The sub-case 1+0 is symmetric.
Once this is done, we will apply a vanishing substitution on
one side, and the induction hypothesis on the other side.
split_one; [
1+0
rotate_right_remove;
rotate_right
0+1
|
permute_left_remove;
permute_left
]
end;
Identify several special cases.
try match goal with
The following special cases are dealt with directly, because they
have short proofs.
| |-
context[
TyAt] =>
econstructor;
try rewrite closed_value_subst;
eauto with resources
| |-
jv _ _ _ (
VRegionCap _)
_ =>
eapply j_value_resource_weakening;
try eassumption;
eauto 2
| |-
jv _ _ _ (
VRegionCapPunched _)
_ =>
eapply j_value_resource_weakening;
try eassumption;
eauto 2
| |-
jv _ _ _ (
VLoc _ _)
_ =>
eapply j_value_resource_weakening;
try eassumption;
eauto 2
| |-
jt _ _ _ (
THide _ _)
_ =>
permute_left;
econstructor;
try solve [
hide_rhs ];
eauto 2
The following special cases are set aside, because they have
more intricate proofs. fail 1 causes this match goal to
fail, and thanks to the enclosing try, we fall out.
| |-
jv _ _ _ (
VVar _)
_ =>
fail 1
| |-
jv _ _ _ (
VBang _)
_ =>
fail 1
The following is the general case.
|
_ =>
Apply the same typing rule as in the original derivation; discharge any easy premises.
econstructor;
eauto 2;
Rewrite, so as to make the induction hypothesis applicable.
repeat rewrite remove_lift_env;
repeat rewrite remove_env_entry_simpl;
Apply the induction hypothesis, if necessary, and conclude.
try solve [
use_ih;
eauto 3
with j_substitution_one |
eauto 4
with j_substitution_one ]
end.
Deal with the cases that were set aside.
VVar
unfold subst_var.
inspect_cases;
intro.
forwards [ ? [ ? ? ]] :
present_substitution_recent;
eauto.
eauto using jenv_substitution_recent.
subst.
jenv_uniqueness.
eapply j_resource_multiplicity_weakening;
eauto using (@
star_commutative resource), (@
star_commutative menv).
forwards [ ? [ ? ? ]] :
present_substitution_old;
eauto.
eauto using jenv_substitution_old.
VBang
A value that has been boxed using VBang does not use any linear
variable, so it must be the case that k is not used in v. As
a result, we can use the earlier lemma j_value_term_substitution_zero,
and we don't need the resources in M2, so we throw them away via
an application of the resource/multiplicity weakening lemma.
eapply j_resource_multiplicity_weakening;
eauto 2.
eauto using j_value_substitution_zero.
Qed.
-------------------------------------------------------------------------
Last comes the non-linear substitution lemma, where the variable
that we are substituting for has multiplicity infinity.
The following tactic helps deal with environment splitting. The variable of
interest, k, has multiplicity infinity, so it is sent down into both
sides. The replacement term u requires the resources in M2, a duplicable
multiplicity environment. We have (M1a\k + M1b\k) + M2 = M, which implies
(M1a\k + M2) + (M1b\k + M2) = M. This is the new split, to be used in the new
typing derivation.
Similarly, we have R1a * R1b = R1 and R1 * R2 = R, where R2 is duplicable.
The new split is based on the identity (R1a * R2) * (R1b * R2) = R.
Local Hint Resolve j_value_weakening_remove jenv_lift
j_ty_weakening_value_remove star_neutral_bang
j_term_substitution_infinity_bang :
infinity.
Ltac split_infinity :=
match goal with h1:
jenv ?
M1 ?
k MInfinity,
h2:
star ?
M1a ?
M1b ?
M1,
h3:
star ?
M1k ?
M2 ?
M,
h4:
duplicable ?
M2,
i1:
star ?
R1a ?
R1b ?
R1,
i2:
star ?
R1 ?
R2 ?
R,
i3:
duplicable ?
R2 |-
_ =>
unpack (
split_infinity h1 h2);
unpack (
send_down_both_ways (@
split_as_dictated k _ _ _ h2)
h3 h4);
unpack (
send_down_both_ways i1 i2 i3)
end.
Lemma j_value_term_substitution_infinity:
(
forall R1 M1 E v T,
jv R1 M1 E v T ->
mark_ih (
forall k U,
jenv M1 k MInfinity ->
jenv E k U ->
forall R2 M2 u,
jv R2 M2 (
remove_env_entry k E)
u U ->
forall M R,
star R1 R2 R ->
star (
remove_env_entry k M1)
M2 M ->
duplicable R2 ->
duplicable M2 ->
jv R M (
remove_env_entry k E) (
subst_value u k v)
T
)
) /\ (
forall R vs T,
ji R vs T ->
True
) /\ (
forall R1 M1 E t T,
jt R1 M1 E t T ->
mark_ih (
forall k U,
jenv M1 k MInfinity ->
jenv E k U ->
forall R2 M2 u,
jv R2 M2 (
remove_env_entry k E)
u U ->
forall M R,
star R1 R2 R ->
star (
remove_env_entry k M1)
M2 M ->
duplicable R2 ->
duplicable M2 ->
jt R M (
remove_env_entry k E) (
subst_term u k t)
T
)
).
Proof.
-------------------------------------------------------------------------
Backward style reformulations.
Lemma j_value_term_substitution_one_backward:
(
forall R1 R2 R M1 M2 M E F v T k u U,
jv R1 M1 E v T ->
jv R2 M2 F u U ->
jenv M1 k MOne ->
jenv E k U ->
F =
remove_env_entry k E ->
star R1 R2 R ->
star (
remove_env_entry k M1)
M2 M ->
jv R M F (
subst_value u k v)
T
) /\ (
forall R1 R2 R M1 M2 M E F t T k u U,
jt R1 M1 E t T ->
jv R2 M2 F u U ->
jenv M1 k MOne ->
jenv E k U ->
F =
remove_env_entry k E ->
star R1 R2 R ->
star (
remove_env_entry k M1)
M2 M ->
jt R M F (
subst_term u k t)
T
).
Proof.
Lemma j_value_term_substitution_infinity_backward:
(
forall R1 R2 R M1 E F v T k U M2 u M,
jv R1 M1 E v T ->
jenv M1 k MInfinity ->
jenv E k U ->
duplicable R2 ->
duplicable M2 ->
jv R2 M2 F u U ->
F =
remove_env_entry k E ->
star R1 R2 R ->
star (
remove_env_entry k M1)
M2 M ->
jv R M F (
subst_value u k v)
T
) /\ (
forall R1 R2 R M1 E F t T k U M2 u M,
jt R1 M1 E t T ->
jenv M1 k MInfinity ->
jenv E k U ->
duplicable R2 ->
duplicable M2 ->
F =
remove_env_entry k E ->
jv R2 M2 F u U ->
star R1 R2 R ->
star (
remove_env_entry k M1)
M2 M ->
jt R M F (
subst_term u k t)
T
).
Proof.
-------------------------------------------------------------------------
Special cases.
Lemma j_value_substitution_infinity_0:
forall R1 R2 R M1 M2 M E T1 v2 T2 v1,
jv R1 (
M1;;
MInfinity) (
E;;
T1)
v2 T2 ->
duplicable R2 ->
duplicable M2 ->
jv R2 M2 E v1 T1 ->
star R1 R2 R ->
star M1 M2 M ->
jv R M E (
subst_value v1 0
v2)
T2.
Proof.
Lemma j_term_substitution_infinity_0:
forall R1 R2 R M1 M2 M E T1 t T2 v,
jt R1 (
M1;;
MInfinity) (
E;;
T1)
t T2 ->
duplicable R2 ->
duplicable M2 ->
jv R2 M2 E v T1 ->
star R1 R2 R ->
star M1 M2 M ->
jt R M E (
subst_term v 0
t)
T2.
Proof.
Lemma j_term_substitution_one_0:
forall R1 R2 R M1 M2 M E T1 t T2 v,
jt R1 (
M1;;
MOne) (
E;;
T1)
t T2 ->
jv R2 M2 E v T1 ->
star R1 R2 R ->
star M1 M2 M ->
jt R M E (
subst_term v 0
t)
T2.
Proof.
Lemma j_term_substitution_one_1:
forall R1 R2 R M1 m M2 n M E T1 t T2 v U,
jt R1 (
M1;;
MOne;;
m) (
E;;
T1;;
U)
t T2 ->
jv R2 (
M2;;
n) (
E;;
U)
v T1 ->
star R1 R2 R ->
star (
M1;;
m) (
M2;;
n)
M ->
jt R M (
E;;
U) (
subst_term v 1
t)
T2.
Proof.
Lemma j_term_substitution_one_1_rebind:
forall R E T1 t T2 v U,
jt R (
nil;;
MOne;;
MZero) (
E;;
T1;;
U)
t T2 ->
jv (
neutral R) (
nil;;
MOne) (
E;;
U)
v T1 ->
jt R (
nil;;
MOne) (
E;;
U) (
subst_term v 1
t)
T2.
Proof.