Subject reduction for values.
Subject reduction for values was initially stated under arbitrary
environments M and E. However, some cases were added, , which require
an empty environment, because they deal with regions and closed values.
CoDefocusDuplicable was one of them, but is no longer here
because it is no longer a coercion; instead, it is a primitive operation.
Not sure whether other cases remain.
Proof.
apply jvit_ind;
intros;
subst;
try nil;
Eliminate the case of JVEq.
try solve [
eauto 3 ];
Analyze the reduction; perform simplifications.
match goal with
|
hr:
redv _ _ |-
_ =>
generalize hr;
clear hr
|
hr:
redvs _ _ |-
_ =>
generalize hr;
clear hr
end;
intro hr;
dependent induction hr;
simpl;
try solve [
eauto 3 ];
try match goal with h:
jco ?
E ?
c ?
T |-
_ =>
depelim h end;
try match goal with h:
cwf ?
c |-
_ =>
depelim h end.
RedCoId
eauto.
RedCoSeq
eauto.
RedCoForallIntro
eauto using j_ty_weakening_value.
RedCoForallElim
jv_inversion.
eauto using (
proj1 j_type_substitution_0).
RedCoExistsIntro
eauto.
RedCoExistsElim
econstructor;
eauto.
eapply JTLetUnpack with (
R1 :=
neutral R) (
R2 :=
R) (
M1 := (
nil;;
MOne)) (
M2 := (
nil;;
MZero));
eauto using (@
star_commutative resource), (@
star_neutral resource).
jv_inversion.
jv_inversion.
eapply j_term_weakening_general;
eauto.
RedCoExistsElim
jv_inversion.
match goal with h:
jv _ _ _ _ (
subst_ty _ _ _) |-
_ =>
rewrite subst_lift_ty in h end.
assumption.
RedCoArrow
jv_inversion.
constructor;
eauto.
econstructor;
eauto.
eapply j_term_substitution_one_1_rebind.
eapply j_term_weakening;
eassumption.
eauto.
RedCoPair
jv_inversion.
eauto.
RedCoForall
jv_inversion.
eauto.
RedCoExists
jv_inversion.
eauto 6
using jco_type_substitution_nil_arrow.
RedCoBang
jv_inversion.
eauto.
RedCoRegionCap
jv_inversion.
sigma.
econstructor;
eauto 2
using ji_coapp,
pwe_vmap_coapp with region_compatibility.
RedCoRegionCapPunched
jv_inversion.
sigma.
econstructor;
eauto 3
using ji_coapp,
pwe_vmap_coapp with region_compatibility.
RedCoRef
jv_inversion.
eauto 3.
RedCoDereliction
jv_inversion.
eapply j_resource_multiplicity_weakening;
eauto using (@
star_neutral resource), (@
star_commutative resource).
RedCoBangIdempotent
jv_inversion.
eauto with resources.
RedCoPairBang
jv_inversion.
jv_inversion.
jv_inversion.
eauto with resources.
RedCoBangPair
jv_inversion.
jv_inversion.
constructor.
econstructor;
eauto with duplicable.
RedCoUnitBang
jv_inversion.
eauto.
RedCoAtBang
eauto using classification_at_neutral.
RedCoDistrib
jv_inversion.
jv_inversion.
constructor~.
constructor;
eauto 1.
simpl.
eapply j_value_term_substitution_one_backward
with (
M1 :=
nil;;
MOne;;
MZero)
(
M2 :=
nil;;
MOne)
(
R2 :=
neutral R)
(
E :=
nil;;
T1;;
TyForall (
lift_ty 1
T1));
eauto using (@
star_neutral resource);
try solve [
constructor;
eauto ].
eapply j_term_weakening_general;
eauto.
eauto 6
using JCoForallElimPun.
RedCoSingletonToGroup
jv_inversion.
sigma.
eauto using ji_singleton_construction.
RedCoForallPair
jv_inversion.
jv_inversion.
econstructor;
eauto 2.
RedCoForallBang
jv_inversion.
jv_inversion.
econstructor;
eauto 2.
RedCoForallRef
jv_inversion.
jv_inversion.
econstructor;
eauto 2.
RedCoForallRegionCap
jv_inversion.
jv_inversion.
tyeq_region_lift.
sigma.
econstructor;
eauto 2
using pwe_vmap_vtyabs,
ji_vtyabs with region_compatibility.
RedCoForallRegionCapPunched
jv_inversion.
jv_inversion.
do 2
tyeq_region_lift.
sigma.
econstructor;
eauto 3
using pwe_vmap_vtyabs,
ji_vtyabs with region_compatibility.
RedCoSingletonRegionCapExists
jv_inversion.
jv_inversion.
econstructor.
simpl.
rewrite subst_lift_ty.
eapply JVRegionCap_flexible_singleton;
eauto with resources.
wf.
wf.
RedCoPairExistsLeft
jv_inversion.
jv_inversion.
econstructor;
eauto 3.
econstructor;
try rewrite subst_lift_ty;
eauto.
RedCoPairExistsRight
jv_inversion.
jv_inversion.
econstructor;
eauto 3.
econstructor;
try rewrite subst_lift_ty;
eauto.
RedCoBangExists
jv_inversion.
jv_inversion.
econstructor.
simpl.
eauto 2.
wf.
wf.
RedCoRefExists
jv_inversion.
jv_inversion.
econstructor.
simpl.
eauto 2.
wf.
wf.
RedCoDefocus
jv_inversion.
forwards:
defocus_sr;
try eassumption.
intuition eauto 2.
RedCoDefocusGroup
eauto using defocus_group_sr.
RedCoStarCommutative
jv_inversion.
eauto 3
using (@
star_commutative resource), (@
star_commutative menv).
RedCoStarAssociative
jv_inversion.
jv_inversion.
star_associative.
econstructor;
eauto 2.
RedCoStarRef
jv_inversion.
jv_inversion.
rotate_right.
econstructor;
eauto 3
with resources.
RedCoRefStar
jv_inversion.
jv_inversion.
rotate_left.
econstructor;
eauto 3
with resources.
RedCoStarSingleton
jv_inversion.
jv_inversion.
rotate_right.
eapply JVRegionCap_flexible_singleton;
eauto with resources.
RedCoSingletonStar
jv_inversion.
jv_inversion.
rotate_left.
econstructor;
eauto 1.
eapply JVRegionCap_flexible_singleton;
eauto with resources.
RedCoTensorExchangeVAbs
We have a lambda-abstraction, so its type must be an arrow.
prediction.
We have an application of tensor that results in an arrow. Thus,
the type within the tensors must itself be an arrow.
if_tensor_exhibits_tycon.
This allows us to modify the typing judgement that forms our hypothesis.
We use the following tactic to prove the required type equality. This
tactic is polymorphic, in that it works not just for arrow, but also
for other type constructors.
Ltac eqq :=
do 2
rewrite fold_tensors;
tyeq_under_tensor; [
eapply tyeq_symmetric;
eassumption
|
tyred_tensors
|
eapply wf_tensors;
wf
].
jveq_forward eqq.
We can now invert this typing judgement.
jv_inversion.
Build a new type derivation. The derivation ends with a type equality
argument, which is symmetric to the one that we just made about our
hypothesis.
jveq eqq.
simpl.
econstructor; [
idtac |
wf ].
coComposExchangeUnder.
eapply j_term_substitution_one_1_rebind.
eapply j_term_weakening.
eassumption.
coComposExchangeUnder.
repeat econstructor;
eauto.
RedCoTensorExchangeVPair
prediction.
if_tensor_exhibits_tycon.
jveq_forward eqq.
jv_inversion.
jveq eqq.
simpl.
econstructor;
eauto.
RedCoTensorExchangeVUnit
prediction.
if_tensor_exhibits_tycon.
jveq eqq.
econstructor.
RedCoTensorExchangeVTyAbs
Slightly harder, because lift is involved.
prediction.
if_tensor_exhibits_tycon.
jveq_forward eqq.
eapply wf_tensors; [
eapply wfs_map;
eauto |
eauto ].
jv_inversion.
jveq eqq.
simpl.
econstructor.
econstructor.
eassumption.
econstructor;
eauto 3.
rewrite map_length.
assumption.
eauto.
RedCoTensorExchangeVPack
Slightly harder yet, because lift and subst are involved.
prediction.
if_tensor_exhibits_tycon.
jveq_forward eqq.
eapply wf_tensors; [
eapply wfs_map;
eauto |
eauto ].
jv_inversion.
jveq eqq.
simpl.
econstructor.
rewrite subst_tensors in *.
simpl in *.
econstructor.
eassumption.
econstructor;
eauto.
repeat rewrite map_length.
assumption.
eauto.
eapply wf_tensors; [
eapply wfs_map;
eauto |
wf ].
wf.
RedCoTensorExchangeVBang
prediction.
if_tensor_exhibits_tycon.
jveq_forward eqq.
jv_inversion.
jveq eqq.
simpl.
econstructor;
eauto.
RedCoTensorExchangeVLoc
prediction.
if_tensor_exhibits_tycon.
jveq_forward eqq.
jv_inversion.
jveq eqq.
simpl.
econstructor;
eauto.
RedCoTensorExchangeVRegionCap
prediction.
if_tensor_exhibits_tycon.
jveq_forward eqq.
jv_inversion.
jveq eqq.
simpl.
TEMPORARY sigma should do this, but fails.
eapply JVEq; [
idtac
|
eapply tyeq_regioncap; [
eassumption |
eapply tyeq_reflexive;
wf ]
|
wf
].
econstructor;
eauto 3
using pwe_vmap_coapp,
ji_coapp with region_compatibility.
RedCoTensorExchangeVRegionCapPunched
prediction.
if_tensor_exhibits_tycon.
jveq_forward eqq.
jv_inversion.
jveq eqq.
simpl.
TEMPORARY sigma should do this, but fails.
eapply JVEq; [
idtac
|
eapply tyeq_regioncappunched; [
eassumption |
eapply tyeq_reflexive;
wf |
eassumption ]
|
wf
].
econstructor;
eauto 3
using pwe_vmap_coapp,
ji_coapp with region_compatibility.
RedCoTensorExchangeVInhabitant
prediction.
if_tensor_exhibits_tycon.
jveq_forward eqq.
jveq eqq.
assumption.
RedCoMu
econstructor;
eauto using cwf_cunfold.
unfold cunfold.
eapply jco_substitution_0;
eauto 6.
RedVRegionCapContext
forwards:
values_stutter_yup.
eassumption.
econstructor;
eauto 2
with region_compatibility.
RedVRegionCapPunchedContext
forwards:
values_stutter_yup.
eassumption.
econstructor;
eauto 3
with region_compatibility.
RedVLocContext
forwards:
values_stutter.
eassumption.
econstructor;
eauto 2.
congruence.
Qed.
Proof.