Set Implicit Arguments.
Require Import Coq.Relations.Relations.
Require Import Coq.Wellfounded.Inclusion.
Require Import Coq.Wellfounded.Inverse_Image.
Require Import MyTactics.
Require Import Arithmetic.
Require Import DeBruijn.
Require Import Coercions.
Require Import Store.
Require Import Layers.
Require Import Programs.
Require Import RawPrograms.
Require Import Erasure.
Require Import Canonical.
Require Import PathSemantics.
Require Import RevelationDefinition.
Require Import SemanticsValues.
Require Import Semantics.
Require Import RawSemantics.
Require Import ValueReductionTerminates.
Require Import Environments.
Require Import WellLayeredness.
Require Import Lexicographic.
Require Import ErasureSimulationValues.
-------------------------------------------------------------------------
We know that value reduction is terminating, so we ignore the structure of
values in the following definitions.
The measure hideous counts how many THide constructs appear in an
evaluation position. These constructs are about to extrude, via RedTHide,
in the next reduction steps. The extrusion of a THide construct causes a
decrease in hideous. Because it creates new coercions along the path up
to the root, it does not preserve measure.
The measure measure decreases at every non-computational step, that is,
at every stuttering term reduction step, except for RedTHide steps.
As a result, a lexicographic ordering of hideous and measure decreases
at every stuttering term reduction step.
Fixpoint hideous (
t :
term) :
nat :=
match t with
|
TVal _
|
TLetPair Physical Physical _ _
|
TPrimApp _ _ =>
0
|
TApp _ t
|
TMixPair t _
|
TTyAbs t
|
TCoApp _ t
|
TLetBang _ t
|
TLetUnpack _ t
|
TLetPair Physical Logical _ t
|
TLetPair Logical Physical _ t
|
TLetPair Logical Logical _ t =>
hideous t
|
THide _ t =>
1 +
hideous t
end.
Fixpoint measure (
t :
term) :
nat :=
match t with
|
TVal _
|
TLetPair Physical Physical _ _ =>
0
|
TPrimApp _ _ =>
1
|
TApp _ t
|
TMixPair t _
|
TTyAbs t
|
TCoApp _ t
|
TLetBang _ t
|
TLetUnpack _ t
|
TLetPair Physical Logical _ t
|
TLetPair Logical Physical _ t
|
TLetPair Logical Logical _ t
|
THide _ t =>
1 +
measure t
end.
-------------------------------------------------------------------------
Because the definitions of hideous and measure ignore values, they are
insensitive to substitution of values for variables, and insensitive to
value reduction at any position in the term.
Lemma hideous_subst:
forall t w k,
hideous (
subst_term w k t) =
hideous t.
Proof.
induction t; simpl; layers; intros; eauto.
Qed.
Lemma hideous_redvt:
forall t1 t2,
redvt t1 t2 ->
hideous t2 =
hideous t1.
Proof.
induction 1; simpl; congruence.
Qed.
Lemma hideous_CoMixPairCompossExchange:
forall nh t,
hideous (
CoMixPairCompossExchange nh t) =
hideous t.
Proof.
induction nh; simpl; eauto.
Qed.
Local Hint Resolve hideous_subst.
Lemma measure_subst:
forall t w k,
measure (
subst_term w k t) =
measure t.
Proof.
induction t; simpl; layers; intros; eauto.
Qed.
Lemma measure_redvt:
forall t1 t2,
redvt t1 t2 ->
measure t2 =
measure t1.
Proof.
induction 1; simpl; congruence.
Qed.
-------------------------------------------------------------------------
When a term stutters, either (a) the measure of the term, as measured by the
functions hideous and measure, decreases; or (b) a value reduction step
is taken.
Definition mredvt t1 t2 :=
hideous t1 >
hideous t2 \/
(
hideous t1 =
hideous t2 /\
measure t1 >
measure t2) \/
redvt t1 t2.
This is a well-founded relation.
Lemma mredvt_wf:
well_founded (
transpose mredvt).
Proof.
-------------------------------------------------------------------------
When a term reduces, it either: (i) stutters; or (ii) takes an actual
computational step.
In the second case, where actual computation is performed, we allow this
computation to require several steps in the raw semantics. Thus, one step
in the instrumented semantics can be reflected by several steps in the
raw semantics. This offers some flexibility, e.g. some of the primitive
operations of the instrumented semantics can be compiled away into more
elementary basic operations of the raw semantics.
The following two lemmas describe two distinct cases: (i) a case where no
active hide extrudes, nh = 0; and (ii) a case where at least one active
hide extrudes, nh > 0.
The well-layeredness hypothesis is used only in the cases that concern the
reduction of TLetPair. Considering how we have defined the erasure
function -- a logical variable is replaced with RawVErased -- the
simulation property can hold only if a variable that was deemed logical
actually becomes bound to a logical value.
Lemma erasure_simulation_zero:
forall s1 t1 nh s2 t2,
red s1 t1 nh s2 t2 ->
nh = 0 ->
wls s1 ->
wlt nil t1 ->
erase_store s1 =
erase_store s2 /\
erase_term t1 =
erase_term t2 /\
hideous t1 =
hideous t2 /\
(
redvt t1 t2 \/
measure t1 >
measure t2)
\/
rredplus (
erase_store s1) (
erase_term t1) (
erase_store s2) (
erase_term t2).
Ltac case_ii :=
right;
solve [
constructor |
eauto ].
Ltac case_ia :=
left;
splits; [
congruence |
congruence |
eauto |
left;
eauto ].
Ltac case_ib :=
left;
splits; [
congruence |
congruence |
eauto |
right;
eauto ].
Local Hint Extern 1 (
_ =
_) =>
congruence.
Proof.
induction 1;
simpl;
intros;
layers;
try prim;
ectx;
simpl;
wl_inversion;
Simplify the goal.
repeat rewrite (
pi3 erase_subst);
repeat rewrite (
pi1 erase_lift);
repeat rewrite measure_subst;
repeat rewrite erase_reveal_value;
repeat rewrite fold_erase_reveal;
Recognize the steps that involve value reduction.
try match goal with h:
redv ?
v1 ?
v2 |-
_ =>
unpack (
values_stutter h);
case_ia
end;
Recognize the steps that involve plugging (de-focusing).
try match goal with h:
plug _ _ _ _ |-
_ =>
rewrite (
plugging_respects_erasure h)
end;
Simplify. Destruct the induction hypothesis, if there is one.
intuition eauto;
In the three cases that correspond to pairs with one or two
logical components, the following works.
try solve [
erase_logical_value;
try erase_logical_value;
left;
splits;
repeat rewrite hideous_subst;
eauto with f_equal
];
Try everything.
simpl;
try solve [
case_ii |
case_ia |
case_ib ].
The remaining cases involve references.
PNewAffine
right;
do 2
econstructor.
rewrite <-
transform_extend.
congruence.
PReadAffine
Here, we must check that our somewhat elaborate implementation of PReadAffine
in terms of the ordinary raw read is correct.
right.
eapply RredplusMore.
The first reduction step is a read in memory, under a context.
do 2
econstructor.
unfold transform.
match goal with h: ?
m ?
l =
Some ?
v |-
_ =>
rewrite h end.
eauto.
The next reduction step is the let-redex.
eapply RredplusOne.
equates 1.
econstructor.
simpl.
rewrite subst_var_identity.
eauto.
PWriteAffine
right.
eapply RredplusMore.
The first reduction step is a write in memory, under a context.
do 2
econstructor.
instantiate (1 :=
erase_value v1).
eauto with transform.
rewrite <-
transform_extend.
eauto.
The next reduction step is the let-redex.
eapply RredplusMore.
econstructor.
simpl.
rewrite raw_subst_lift_value.
rewrite subst_var_miss_1;
eauto 2.
The last reduction step is the pair projection.
eapply RredplusOne.
equates 1.
econstructor.
simpl.
rewrite subst_var_identity.
eauto.
PNewCap
right;
do 2
econstructor.
rewrite <-
transform_extend.
congruence.
PReadCap
right.
match goal with h:
erase_value _ =
RawVLoc _ |-
_ =>
rewrite h end.
do 2
econstructor.
unfold transform.
match goal with h: ?
m ?
l =
Some ?
v |-
_ =>
rewrite h end.
congruence.
PWriteCap
right.
match goal with h:
erase_value _ =
RawVLoc _ |-
_ =>
rewrite h end.
do 2
econstructor.
instantiate (1 :=
erase_value v1).
eauto with transform.
rewrite <-
transform_extend.
congruence.
Qed.
Lemma erasure_simulation_nonzero:
forall s1 t1 nh s2 t2,
red s1 t1 nh s2 t2 ->
nh > 0 ->
wls s1 ->
wlt nil t1 ->
erase_store s1 =
erase_store s2 /\
erase_term t1 =
erase_term t2 /\
hideous t1 >
hideous t2.
Proof.
The main lemma puts everything together.
Lemma erasure_simulation:
forall s1 t1 nh s2 t2,
red s1 t1 nh s2 t2 ->
wlconf s1 t1 ->
(
erase_store s1 =
erase_store s2 /\
erase_term t1 =
erase_term t2 /\
mredvt t1 t2
)
\/
rredplus (
erase_store s1) (
erase_term t1) (
erase_store s2) (
erase_term t2).
Proof.