Set Implicit Arguments.
Require Import MyTactics.
Require Import DeBruijn.
Require Import Coercions.
Require Import Programs.
Require Import RawPrograms.
Require Import Canonical.
Require Import SemanticsValues.
Require Import Semantics.
Require Import RawSemantics.
Require Import ValueReductionTerminates.
Require Import Erasure.
Require Import ErasureSimulation.
Require Import Types.
Require Import Typing.
Require Import Environments.
Require Import InversionClassification.
Require Import SubjectReduction.
Require Import Progress.
Require Import WellLayeredness.
-------------------------------------------------------------------------
Type soundness results for the raw calculus.
-------------------------------------------------------------------------
A raw configuration is well-typed if it reduces (in an arbitrary number of
steps) to the erasure of some well-typed and well-layered configuration.
One could wish to be more strict and require equality rather than reduction
in an arbitrary number of steps. This would in turn require a tighter
statement of erasure_simulation: we would have to require that one step
in the instrumented semantics be either a stuttering step or simulated by
exactly one step in the raw semantics. This version offers greater
flexibility.
Inductive well_typed (
rs :
raw_store) (
rt :
raw_term) (
T :
ty) :
Prop :=
|
WellTypedCons:
forall s t,
jconf s t T ->
wlconf s t ->
rredstar rs rt (
erase_store s) (
erase_term t) ->
well_typed rs rt T.
Hint Constructors well_typed.
-------------------------------------------------------------------------
The following is the main step in proving that the above notion of
well-typedness is preserved by reduction.
It is, in a sense, a reciprocal of the erasure simulation statement,
as it relates one step of reduction at the raw level to a number of
reduction steps at the instrumented level.
One could make the statement more precise by expanding the definition
of well_typed rs2 rt2 T in the conclusion and adding that rs2/rt2
is the erasure of a configuration s2/t2 such that redplus s1 t1 s2 t2
holds.
Lemma erasure_reverse_simulation:
forall T t1 s1,
jconf s1 t1 T ->
wlconf s1 t1 ->
forall rs2 rt2,
rred (
erase_store s1) (
erase_term t1)
rs2 rt2 ->
well_typed rs2 rt2 T.
Proof.
intro.
We work by well-founded induction over t1 with respect to mredvt.
intro t1.
induction_wf ih:
mredvt_wf t1.
intro s1.
introv ? ?
raw_step.
Either the term t1 is a canonical value, or the configuration
s1/t1 reduces.
forwards a:
progress_configurations.
eassumption.
inversion a as [ | ? ? ?
s2 t2 step ];
subst;
clear a.
If the former, then the erasure of t1 is also a value; impossible,
since raw values do not reduce.
false.
exact (
values_do_not_reduce raw_step).
So, s1/t1 must reduce to some new configuration s2/t2.
By subject reduction, s2/t2 is well-typed.
forwards:
subject_reduction_configurations.
eassumption.
eassumption.
Now, this is either a stuttering step, or a computational step.
forwards [[
stutter_store [
stutter_term ? ]] | ? ] :
erasure_simulation;
try eassumption.
If the former, apply the induction hypothesis. By well-founded induction,
we cannot stutter forever.
forwards wt:
ih.
eassumption.
eassumption.
eauto using wlconf_preserved.
rewrite <-
stutter_store.
rewrite <-
stutter_term.
eassumption.
inversion wt.
eauto.
If the latter, then s2/t2 is the desired configuration. We exploit the
determinism of the (raw) semantics to ensure that the erasure of s2/t2
is indeed rs2/rt2. That is, we started with a raw step out of the
erasure of s1/t1, constructed a typed step out of s1/t1, and must now
check that the erasure of the latter is indeed the former.
econstructor.
eassumption.
eauto using wlconf_preserved.
eauto using rred_and_rredplus.
Qed.
The reverse simulation property allows transporting Subject Reduction down to
the level of raw terms.
Lemma raw_subject_reduction:
forall rs1 rt1 rs2 rt2 T,
well_typed rs1 rt1 T ->
rred rs1 rt1 rs2 rt2 ->
well_typed rs2 rt2 T.
Proof.
inversion 1;
intros.
There is a well-typed point somewhere ahead of us, and we are taking one
step. So, either (1) the well-typed point is still ahead of us, and all is
well; or (2) we were at a well-typed point, and we have to prove that there
is a new well-typed point ahead of us; in that case, the reverse simulation
lemma is all we need.
forwards [ ? | [ ? ? ]]:
rred_and_rredstar;
try eassumption.
Case 1.
eauto.
Case 2.
subst.
eauto using erasure_reverse_simulation.
Qed.
-------------------------------------------------------------------------
The simulation property allows transporting Progress down to the level of
raw configurations.
Lemma raw_progress_preliminary:
forall rs1 rt1 T t1 s1,
jconf s1 t1 T ->
wlconf s1 t1 ->
erase_store s1 =
rs1 ->
erase_term t1 =
rt1 ->
(
exists rv,
rt1 =
RawTVal rv) \/
(
exists rs2 rt2,
rred rs1 rt1 rs2 rt2).
Proof.
do 3
intro.
intro t1.
induction_wf ih:
mredvt_wf t1.
intro s1.
introv hjconf ?
here_store here_term.
By progress, either t1 is a canonical value, or s1/t1 reduces to
some configuration s2/t2.
forwards a:
progress_configurations;
try eassumption.
inversion a as [ | ? ? ?
s2 t2 ? ];
clear a;
subst.
If the former, then we are done. Well-layeredness guarantees that
the final value is not RawVErased.
left.
wl_inversion.
simpl.
eauto.
If the latter, then, this is either a stuttering step or a computational step.
forwards [[ ? [ ? ? ]] |
steps ] :
erasure_simulation;
try eassumption.
If the former, apply the induction hypothesis.
forwards:
subject_reduction_configurations;
try eassumption.
eapply ih.
eassumption.
eassumption.
eauto using wlconf_preserved.
congruence.
congruence.
If the latter, then we are done.
We prove, on the fly, that a term that can take one or more steps can take
one step.
right.
inversion steps;
subst;
intuition eauto.
Qed.
Lemma raw_progress:
forall rs1 rt1 T,
well_typed rs1 rt1 T ->
(
exists rv,
rt1 =
RawTVal rv) \/
(
exists rs2 rt2,
rred rs1 rt1 rs2 rt2).
Proof.
inversion 1.
There is a well-typed point somewhere ahead of us. Then, either (1) we are at
this well-typed point, and the previous lemma applies; or (2) we can take at
least one step towards this well-typed point, and we are done.
match goal with h:
rredstar _ _ _ _ |-
_ =>
depelim h end.
Case 1.
eauto using raw_progress_preliminary.
Case 2.
eauto.
Qed.
-------------------------------------------------------------------------
Towards the final type soundness theorem.
If a well-typed raw configuration is unable to reach a value, then it
must diverge. This formulation is amenable to an intuitionistic
co-inductive proof.
Lemma type_soundness_preliminary:
forall rs1 rt1 T,
well_typed rs1 rt1 T ->
(
forall rs2 rv2, ~ (
rredstar rs1 rt1 rs2 (
RawTVal rv2))) ->
diverges rs1 rt1.
Proof.
cofix.
introv wt noval.
rs1/rt1 is well-typed, so either it is value, or it steps.
forwards [ ? | ? ]:
raw_progress;
try eassumption;
unpack;
subst.
In the former case, we have a contradiction, since we have assumed
that rs1/rt1 is unable to reach a value.
false.
eapply noval.
eauto.
In the latter case, we have produced one step, and the co-inductive
hypothesis provides the rest.
econstructor.
eassumption.
intuition eauto using raw_subject_reduction.
Qed.
A reformulation in classical logic: a well-typed raw configuration must
either eventually yield a value or diverge.
Require Import Classical.
Lemma type_soundness:
forall rs1 rt1 T,
well_typed rs1 rt1 T ->
(
exists rs2 rv2,
rredstar rs1 rt1 rs2 (
RawTVal rv2)) \/
diverges rs1 rt1.
Proof.
intros.
Assume the negation of the left-hand disjunct, and prove the right-hand disjunct.
match goal with |- ?
A \/ ?
B =>
destruct (
classic A)
end.
tauto.
right.
Apply the previous result.
eapply type_soundness_preliminary;
try eassumption.
A tautology remains.
unfold not in *.
eauto.
Qed.
-------------------------------------------------------------------------
We could stop here, but, for the sake of completeness, we prove one more result.
If the erasure of t1 is a value, then it can only take a stuttering step.
Lemma erasure_value_stutter:
forall rv1 s1 t1 nh s2 t2,
red s1 t1 nh s2 t2 ->
wlconf s1 t1 ->
erase_term t1 =
RawTVal rv1 ->
erase_store s1 =
erase_store s2 /\
erase_term t1 =
erase_term t2 /\
mredvt t1 t2.
Proof.
There follows that, if the erasure of t1 is a value, then t1 reduces in
zero or more steps to a value.
Lemma erasure_value_reduces_value:
forall T t1 s1,
jconf s1 t1 T ->
wlconf s1 t1 ->
forall rv1,
erase_term t1 =
RawTVal rv1 ->
exists s2 v2,
redstar s1 t1 s2 (
TVal v2) /\
jconf s2 (
TVal v2)
T /\
wlconf s2 (
TVal v2) /\
erase_store s2 =
erase_store s1 /\
erase_value v2 =
rv1.
Proof.
intro.
We work by well-founded induction over t1.
intro t1.
induction_wf ih:
mredvt_wf t1.
intro s1.
introv hjconf ?
here.
Either the term t1 either is a canonical value v1, or the configuration
s1/t1 reduces to s2/t2.
forwards a:
progress_configurations.
eassumption.
inversion a as [ | ? ? ?
s2 t2 ? ];
clear a;
subst.
If the former, then we are done.
simpl in here.
inversion here.
intuition eauto 8.
If the latter, then this must be a stuttering step.
forwards [
stutter_store [
stutter_term ? ]]:
erasure_value_stutter;
try eassumption.
By subject reduction, s2/t2 is well-typed.
forwards :
subject_reduction_configurations;
try eassumption.
Apply the induction hypothesis.
forwards:
ih.
eassumption.
eassumption.
eauto using wlconf_preserved.
rewrite <-
stutter_term.
eassumption.
unpack.
rewrite stutter_store.
intuition eauto 10.
Qed.