Set Implicit Arguments.
Require Import DeBruijn.
Require Import MyTactics.
Require Import Types.
Require Import TypeEquality.
Require Import TypeContexts.
Require Import FocusPaths.
Require Import Focus.
Require Import Coercions.
Require Import Store.
Require Import Programs.
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 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 Monotonicity.
Require Import Closed.
Require Import RegionAllocation.
Require Import RegionAccess.
Require Import Erasure.
Require Import ValueLists.
Require Import LittleFacts.
Require Import ProgressValues.
Require Import ResourcesReconfiguration.
Require Import AntiFrameSwitch.
-------------------------------------------------------------------------
A configuration of a store s and a term t is acceptable if either t
is a value or the configuration is able to make one step.
When the anti-frame rule is disabled, we can assert that no active hide
constructs extrude, that is, nh is zero. This is required for induction
to go through.
Inductive acceptable :
store ->
term ->
Prop :=
|
AcceptableValue:
forall s t v,
canonical v ->
t =
TVal v ->
acceptable s t
|
AcceptableStep:
forall s t nh s'
t',
red s t nh s'
t' ->
(
anti_frame_disabled ->
nh = 0) ->
acceptable s t.
Hint Constructors acceptable.
Ltac acceptable :=
match goal with h:
acceptable _ _ |-
_ =>
depelim h;
subst end.
-------------------------------------------------------------------------
Progress.
Lemma progress:
forall R s,
jsto R s ->
forall R1 t T,
jt R1 nil nil t T ->
forall R2,
star R2 R1 R ->
acceptable s t.
Ltac progress_ih :=
If a resource reconfiguration is required before the induction hypothesis
can be applied, perform it.
match goal with
|
h1:
star ?
R1 ?
R2 ?
R12,
h2:
star ?
R3 ?
R12 ?
R,
IHhj:
forall R2p,
star R2p ?
R1 ?
R ->
acceptable _ _ |-
_ =>
reconfigure R (
Node (
Node (
Leaf R2) (
Leaf R3)) (
Leaf R1))
|
h1:
star ?
R1 ?
R2 ?
R12,
h2:
star ?
R3 ?
R12 ?
R,
IHhj:
forall R2p,
star R2p ?
R2 ?
R ->
acceptable _ _ |-
_ =>
reconfigure R (
Node (
Node (
Leaf R1) (
Leaf R3)) (
Leaf R2))
|
_ =>
idtac
end;
Apply the induction hypothesis and conclude.
match goal with
|
IHhj:
forall R2p,
_ ->
acceptable _ _ |-
_ =>
forwards :
IHhj; [
eassumption |
acceptable; [
classify_and_invert;
eauto 2
|
solve [
eapply AcceptableStep;
eauto 3
with red_context ]
]]
|
_ =>
eauto 3
using (
anti_frame_switch_contradiction (1 = 0))
end.
Ltac progress_values :=
match goal with
|
h:
jv _ nil nil _ _ |-
_ =>
generalize (
progress_values h);
intros [ ? | [ ? ? ]]; [
idtac |
solve [
eapply AcceptableStep;
eauto ]]
end.
Proof.
introv ?
hj;
dependent induction hj;
introv ?;
try solve [
eauto 2 ];
Simplify.
try nil;
nilnil;
try jp_inversion;
If we have a judgement about a value, then either this value is
canonical, or it reduces. In the former case, a classification
lemma may apply to this value. In the latter case, the whole term
should reduce, via reduction under a context.
try progress_values;
Classify and invert.
classify_and_invert;
If possible, apply the induction hypothesis.
progress_ih.
TTyAbs
forwards :
IHhj; [
eassumption |
acceptable; [
eauto 2 |
idtac ]].
There is no interaction between TTyAbs and THide, because one
is enabled only when the other is disabled. More precisely, in the
present case, we know that anti-frame must be disabled, so nh
must be zero. In that case, and in that case only, the operational
semantics permits reduction under TTyAbs.
assert (
nh = 0).
tauto.
subst.
eauto 3.
Only the cases of primitive operations should remain.
Ltac conclude :=
eapply AcceptableStep;
econstructor;
eauto.
PDefocusDuplicable
There exists a value VInhabitant v at path pi.
forwards [
v ? ]:
defocus_progress_select;
try eassumption.
There exists a value w that is an inhabitant of the region
and can be plugged at path pi -- that is, its erasure is
that of v.
forwards [
w [
v1p [ ? ? ]]]:
defocus_duplicable_progress_plug;
try eassumption.
eapply JVRegionCap_flexible;
eauto using pwe_reflexive.
w is canonical.
forwards:
each_canonical_member;
try eassumption.
w has type TyBang T.
forwards:
ji_inversion;
try eassumption.
Hence w is of the form VBang _.
classify_and_invert.
This allows us to conclude.
eapply AcceptableStep;
eauto 3.
PFocus
forwards:
focus_progress;
try eassumption;
unpack.
conclude.
PFocusGroup
forwards:
group_inhabitation.
eassumption.
eauto with resources.
unpack.
eapply AcceptableStep;
eauto.
PNewAffine
match goal with s:
store |-
_ =>
destruct s end.
conclude.
PReadAffine
The only difficulty is to prove that this memory location is allocated
and holds a value that is equal (up to erasure) to the shadow value
carried by the memory location.
match goal with s:
store |-
_ =>
destruct s end.
star_owned_locations.
forwards:
jsto_inversion.
eassumption.
eassumption.
eauto 2
with resources.
unpack.
conclude.
PWriteAffine. As above.
match goal with s:
store |-
_ =>
destruct s end.
star_owned_locations.
forwards:
jsto_inversion.
eassumption.
eassumption.
eauto 2
with resources.
unpack.
conclude.
PNewCap
match goal with s:
store |-
_ =>
destruct s end.
conclude.
PReadCap
match goal with s:
store |-
_ =>
destruct s end.
star_owned_locations.
forwards:
jsto_inversion.
eassumption.
eassumption.
eauto 2
with resources.
unpack.
We must show that the inhabitant of the region is indeed our location.
forwards:
singleton_inhabitation_preliminary_variant;
eauto 2
with resources.
conclude.
PWriteCap.
match goal with s:
store |-
_ =>
destruct s end.
star_owned_locations.
forwards:
jsto_inversion.
eassumption.
eassumption.
eauto 2
with resources.
unpack.
forwards:
singleton_inhabitation_preliminary_variant;
eauto 2
with resources.
conclude.
Qed.
-------------------------------------------------------------------------
As a corollary, we obtain progress for configurations.
Lemma progress_configurations:
forall s t T,
jconf s t T ->
acceptable s t.
Proof.