Set Implicit Arguments.
Require Import DeBruijn.
Require Import MyTactics.
Require Import Types.
Require Import TypeEquality.
Require Import MoreTypeEquality.
Require Import TypeContexts.
Require Import FocusPaths.
Require Import Focus.
Require Import Coercions.
Require Import Store.
Require Import Programs.
Require Import RawPrograms.
Require Import Subtyping.
Require Import DerivedSubtyping.
Require Import Typing.
Require Import DerivedTyping.
Require Import Environments.
Require Import Multiplicity.
Require Import MultiplicityEnvironments.
Require Import Canonical.
Require Import PathSemantics.
Require Import RevelationDefinition.
Require Import Revelation.
Require Import SemanticsValues.
Require Import Semantics.
Require Import PreliminaryLemmas.
Require Import TypeSubstitution.
Require Import TermSubstitution.
Require Import CoercionSubstitution.
Require Import InversionClassification.
Require Import Resources.
Require Import ResourcesContinued.
Require Import ResourcesReconfiguration.
Require Import Sigma.
Require Import Monotonicity.
Require Import Closed.
Require Import RegionAllocation.
Require Import RegionAccess.
Require Import Erasure.
Require Import ValueLists.
Require Import LittleFacts.
Require Import SubjectReductionValues.
Require Import ReferenceAllocation.
Require Import ReferenceAccess.
-------------------------------------------------------------------------
Properties of evaluation contexts.
Let us first read this statement in the case where nh is zero and Us
is the empty list.
If efill EC t1 has type T under a resource R1, then t1 has some
type U under some resource R1b. The rest of the resource, R1a,
corresponds to the part owned by the evaluation context EC.
Furthermore, if we replace t1 with a term t2 that has type U under
R2b, where R2b is compatible with an evolution R2a of R1a along
rio, then efill EC t2 has type T under R2, where R2 is the
conjunction of R2a and R2b.
Now, when nh is nonzero, this means that the active term t1 has just
executed an instance of the anti-frame rule, and wishes to reveal it to the
evaluation context. So, the new term t2 does not have type U; instead,
it has type composs U Us, where Us is a stack of invariants. (In
reality, we only use the case where nh is 1, but never mind.) So, the
evaluation context must adapt. Instead of efill EC t2, the conclusion of
the theorem mentions reveal_ectx nh EC t2, which represents the term
obtained by first applying revelation to the evaluation context EC, then
plugging the term t in the hole. And the theorem claims that this term
has type composs T Us, that is, the original type T, modified with the
invariants Us that continue to extrude.
Careful if modifying this lemma -- it is manually duplicated in the paper.
Lemma evaluation_contexts:
forall EC R1 t1 T,
jt R1 nil nil (
efill EC t1)
T ->
exists R1a R1b U,
star R1a R1b R1 /\
jt R1b nil nil t1 U /\
forall t2 R2a R2b R2 nh Us,
jt R2b nil nil t2 (
composs U Us) ->
rio R1a R2a ->
star R2a R2b R2 ->
length Us =
nh ->
wfs Us ->
jt R2 nil nil (
reveal_ectx nh EC t2) (
composs T Us).
Proof.
-------------------------------------------------------------------------
Subject reduction for terms.
This tactic performs various kinds of inversion.
Ltac sr_invert :=
try inversion_tval;
try jv_inversion.
This tactic splits the conclusion of the theorem.
Ltac sr_flatten :=
do 3
eexists;
split; [
idtac |
split; [
idtac |
split ]].
This tactic asserts that no active hide is emitted, so the list Us is
nil.
Ltac nohide :=
exists (
nil :
list ty);
simpl;
split; [
eauto |
split; [
eauto |
idtac ]].
This tactic asserts that there is no state change.
Ltac pure :=
nohide;
sr_flatten; [
idtac |
eassumption |
eapply rio_reflexive |
eassumption ].
This tactic first asserts that there is no state change, then performs an
auxiliary induction over the typing judgement j, in order to get rid of
any trailing applications of JTEq.
Ltac purej :=
pure;
dependent induction j;
try nil;
nilnil; [
sr_invert |
solve [
eauto ]].
This tactic asserts that there is a state change -- we have built an rxo
statement -- and we now wish to impose this state change on the evaluation
context.
Ltac istep :=
rxo_star;
sr_flatten; [
idtac |
idtac |
eassumption |
eassumption ];
[
idtac |
eauto 2
using fictitious_jsto ].
This tactic performs an auxiliary induction over the typing derivation, in
order to get rid of any trailing applications of JTEq.
Ltac srj IHj :=
dependent induction j;
introv hstar;
try nil;
nilnil; [
sr_invert |
solve [
forwards:
IHj;
eauto 2;
unpack;
eauto 10 ]].
Careful if modifying this lemma -- it is manually duplicated in the paper.
Lemma subject_reduction:
forall s1 t1 nh s2 t2,
red s1 t1 nh s2 t2 ->
forall R1,
jsto R1 s1 ->
forall R1a T,
jt R1a nil nil t1 T ->
exists Us,
wfs Us /\
length Us =
nh /\
forall R1b,
star R1a R1b R1 ->
exists R2a R2b R2,
jt R2a nil nil t2 (
composs T Us) /\
jsto R2 s2 /\
rio R1b R2b /\
star R2a R2b R2.
Proof.
Proceed by induction over the reduction judgement.
induction 1;
introv hsto j;
Deal with the cases that follow directly from the subject reduction property
for values. In these cases, there is no state change.
try solve [
match goal with
|
h:
redv _ _ |-
_ =>
purej;
eauto 3
using subject_reduction_value
end ].
RedBeta
purej.
eauto using j_term_substitution_one_0.
RedMixPair
purej.
eauto.
RedLetBang
There is an implicit weakening in the typing rule for VBang v.
The value v is substituted into t using the infinity substitution
lemma; the weakening step remains at the root of t.
purej.
eapply j_resource_multiplicity_weakening; [
idtac |
eapply star_commutative;
eassumption |
eauto ].
eapply j_term_substitution_infinity_0;
eauto 2
using star_neutral_generalized with resources.
RedLetPair
purej.
clear IHj.
match goal with
|
hv1:
jv ?
Rv1 nil nil v1 _,
hv2:
jv ?
Rv2 nil nil v2 _,
ht:
jt ?
Rt _ _ _ _ |-
_ =>
reconfigure R (
Node (
Leaf Rv1) (
Node (
Leaf Rv2) (
Leaf Rt)))
end.
do 2 (
eapply j_term_substitution_one_0;
eauto using (@
star_commutative resource)).
eauto using j_value_weakening.
RedTyAbs
nohide.
srj IHj.
intuition eauto 10
using (@
rio_reflexive resource).
RedUnpack
purej.
eapply j_term_substitution_one_0;
try eassumption.
eapply j_term_type_substitution_unpack;
eassumption.
eauto using (@
star_commutative resource).
eauto using (@
star_commutative menv).
RedCoApp
nohide.
srj IHj.
intuition eauto 10
using (@
rio_reflexive resource).
RedDefocusDuplicable
purej.
jp_inversion.
jv_inversion.
econstructor.
econstructor.
eassumption.
eauto.
eapply defocus_duplicable_sr;
eassumption.
assumption.
RedFocus
nohide.
srj IHj.
jp_inversion.
forwards:
focus_sr;
try eassumption.
unpack.
istep.
auto.
RedNewGroup
nohide.
srj IHj.
jp_inversion.
match goal with s:
star ?
R1a _ _ |-
_ =>
forwards: (
group_region_allocation R1a);
unpack
end.
istep.
constructor.
match goal with h:
context[
TyRegion ?
r] |-
_ =>
the existential witness is the region that was just allocated
eapply JVPack with (
U :=
TyRegion r);
eauto;
simpl
end.
eapply JVPairDupLeft;
eauto.
RedAdopt
nohide.
srj IHj.
jp_inversion.
jv_inversion.
forwards:
adoption;
try eassumption.
unpack.
istep.
constructor.
eapply JVPairDupLeft;
eauto.
RedFocusGroup
nohide.
srj IHj.
jp_inversion.
jv_inversion.
pair_inhabitant.
jv_inversion.
jv_inversion.
forwards:
ji_focus;
try eassumption.
unpack.
forwards:
singleton_region_allocation.
eassumption.
unpack.
rxo_star.
rxo_star.
rotate_left.
istep.
econstructor.
match goal with h:
context[
TyRegion ?
r] |-
_ =>
the existential witness is the region that was just allocated
eapply JVPack with (
U :=
TyRegion r); [
simpl |
repeat constructor;
eauto |
eauto 2 ]
end.
repeat rewrite subst_lift_ty.
rewrite subst_var_identity.
eapply JVPairDupLeft.
eapply inhabitant_compatible.
eassumption.
eauto with resources.
eauto.
eauto.
econstructor.
apply star_commutative.
eassumption.
eauto.
eassumption.
sigma.
eapply JVRegionCapPunched with (
w :=
w).
eauto 3
with resources.
jv_inversion.
jv_inversion.
eauto 3
with resources.
This is messy. In principle eauto with resources should do it, but
the search space is too large.
intros.
eapply reordering_1;
eauto 2.
match goal with h:
forall rv,
_ ->
some _ _ |-
_ =>
eapply h end.
eapply region_map_neutral.
eapply region_map_rio_reverse;
eauto 3
with resources.
neutral_eq.
End of this messy side condition.
intros.
forwards:
reordering_2;
try eassumption.
eauto 4
with resources.
eassumption.
eapply j_rio;
eassumption.
jv_inversion.
eauto 3
with resources.
eauto using well_typed_closed_value.
eauto 3
with resources.
RedNewAffine
nohide.
srj IHj.
jp_inversion.
eauto using new_reference_allocation.
RedReadAffine
purej.
jp_inversion.
jv_inversion.
jv_inversion.
constructor.
eapply JVPairDupLeft.
constructor.
equates 5.
eassumption.
eauto 3
with resources.
eauto 3.
RedWriteAffine
nohide.
srj IHj.
jp_inversion.
eauto using reference_write.
RedNewCap
nohide.
srj IHj.
jp_inversion.
Allocate a linearly-typed location.
forwards:
new_reference_allocation;
try eassumption.
unpack.
inversion_tval.
Focus on the new location, so as to create a new singleton region.
forwards: (@
focus_sr PathRoot).
eauto.
rewrite fill_hole.
eassumption.
eauto.
eauto.
unpack.
rewrite fill_hole in *.
Conclude.
rxo_star.
sr_flatten.
constructor.
eassumption.
eapply fictitious_jsto;
eassumption.
eapply rio_transitive;
eassumption.
eassumption.
RedReadCap
purej.
jp_inversion.
jv_inversion.
pair_inhabitant.
match goal with h:
jv _ _ _ (
VRegionCap _)
_ |-
_ =>
generalize h end.
classify_and_invert.
intro.
constructor.
eapply JVPairDupLeft.
constructor.
equates 5.
eassumption.
eauto 3
with resources.
assumption.
RedWriteCap
nohide.
srj IHj.
jp_inversion.
eauto using controlled_reference_write.
RedContext
intros.
forwards:
evaluation_contexts.
eassumption.
unpack.
In this case, we are looking at a term-in-context of the form efill EC t1.
The right-hand side makes a non-trivial step that causes a state change;
the left-hand side must follow. When the term t1 steps, the piece of the
store owned by EC is framed out. Thus, we have to (1) fold the resource
that corresponds to EC into the resource R1b, which describes the
framed-out resource; (2) invoke the induction hypothesis; (3) perform the
reverse maneuver. It is really quite simple, but as usual, our formalization
of star as a 3-place relation makes things quite obscure.
If the reduction of t1 causes active hide constructs to be emitted, we
can find out about their types right now. This simplifies both the induction
hypothesis and the goal.
forwards [
Us [ ? [ ?
IH ]]]:
IHred.
eassumption.
eassumption.
exists Us.
split.
eauto.
split.
eauto.
intros.
Combine the resource for EC, say REC, with R1b, in preparation for the
application of the induction hypothesis. We get an extended resource, say
R1bx.
permute_left.
Apply the induction hypothesis.
forwards:
IH.
eauto using (@
star_commutative resource).
unpack.
Out of this, we get, in particular, that R1bx evolves along rio and
becomes (say) R1bxi. Since R1bx was a composite resource, each of its
components has evolved along rio as well. Thus, REC has evolved to
(say) RECi and R1b has evolved to (say) R1bi.
rio_star.
We now perform the reverse resource re-arrangement, and we are ready to
establish the conclusion of the theorem.
rotate_left.
sr_flatten.
Reconstruct a typing judgement for the term reveal_ectx nh EC t2.
eauto using (@
star_commutative resource).
The store is well-typed.
eassumption.
The resource that describes the unknown part of the store has evolved
along rio.
eassumption.
The pieces fall together.
eassumption.
RedTTyAbsContext
nohide.
srj IHj.
forwards [
Us [ ? [ ?
IH ]]]:
IHred;
try eassumption.
match goal with h:
length ?
Us = 0 |-
_ =>
destruct Us;
simpl in *; [
clear h |
discriminate h ]
end.
forwards:
IH.
eassumption.
unpack.
intuition eauto 10.
TEMPORARY the induction over j has to be repeated in many cases, why not do it once at the beginning?
RedTHide
dependent induction j.
Sub-case: JTCoApp
clear IHj.
This reduction creates one active hide construct.
match goal with h:
jt _ _ _ _ (
TyCompos _ ?
U) |-
_ =>
exists (
U ::
nil)
end.
split.
eauto.
split.
eauto.
intros.
do 3
eexists.
intuition idtac.
eapply j_term_substitution_one_0;
eauto using revelation_values_nil, (@
star_commutative resource).
eassumption.
eauto using (@
rio_reflexive resource).
eassumption.
Sub-case: JTEq
forwards [
Us [ ? [ ?
IH ]]]:
IHj;
eauto 2.
exists Us.
split.
eauto.
split.
eauto.
intros.
forwards:
IH;
try eassumption.
unpack.
intuition eauto 10
using tyeq_composs.
Qed.
-------------------------------------------------------------------------
As a corollary, we obtain subject reduction for configurations.
Lemma subject_reduction_configurations:
forall s1 t1 T,
jconf s1 t1 T ->
forall nh s2 t2,
red s1 t1 nh s2 t2 ->
jconf s2 t2 T.
Proof.