Set Implicit Arguments.
Require Import MyTactics.
Require Import DeBruijn.
Require Import Types.
Require Import TypeContexts.
Require Import TypeEquality.
Require Import Coercions.
Require Import Store.
Require Import Programs.
Require Import Multiplicity.
Require Import Environments.
Require Import Typing.
Require Import Subtyping.
Require Import Resources.
Require Import ResourcesContinued.
Require Import ValueLists.
Require Import Erasure.
Require Import PreliminaryLemmas.
Require Import InversionClassification.
-------------------------------------------------------------------------
The side conditions in JVRegionCap are compatible with equality up to
erasure.
Lemma region_compatibility_1b:
forall R r vs1 vs2,
(
forall rv,
region_map R r rv ->
some (
fun v =>
erase_value v =
rv)
vs1) ->
pwe vs1 vs2 ->
(
forall rv,
region_map R r rv ->
some (
fun v =>
erase_value v =
rv)
vs2).
Proof.
intros.
eapply pwe_some;
eauto.
congruence.
Qed.
Lemma region_compatibility_1bs:
forall R r vh vs1 vs2,
(
forall rv,
region_map R r rv ->
erase_value vh =
rv \/
some (
fun v =>
erase_value v =
rv)
vs1) ->
pwe vs1 vs2 ->
(
forall rv,
region_map R r rv ->
erase_value vh =
rv \/
some (
fun v =>
erase_value v =
rv)
vs2).
Proof.
Lemma region_compatibility_1:
forall R r v1 v2,
(
forall rv,
region_map R r rv ->
some (
fun v =>
erase_value v =
rv) (
VCons v1 VNil)) ->
erase_value v1 =
erase_value v2 ->
(
forall rv,
region_map R r rv ->
some (
fun v =>
erase_value v =
rv) (
VCons v2 VNil)).
Proof.
Lemma region_compatibility_2b:
forall R r vs1 vs2,
(
forall v,
member v vs1 ->
region_map R r (
erase_value v)) ->
pwe vs1 vs2 ->
(
forall v,
member v vs2 ->
region_map R r (
erase_value v)).
Proof.
introv h1 h2; generalize h2 h1; clear h2 h1.
unfold member. induction 1; simpl. tauto. intros ih ? [ ? | ? ].
subst. forwards: (ih v1). auto. congruence.
eauto.
Qed.
Lemma region_compatibility_2:
forall R r v1 v2,
(
forall v,
member v (
VCons v1 VNil) ->
region_map R r (
erase_value v)) ->
erase_value v1 =
erase_value v2 ->
(
forall v,
member v (
VCons v2 VNil) ->
region_map R r (
erase_value v)).
Proof.
Lemma region_compatibility_3b:
forall rk vs1 vs2,
(
rk =
Singleton ->
count vs1 = 1) ->
pwe vs1 vs2 ->
(
rk =
Singleton ->
count vs2 = 1).
Proof.
intros.
forwards:
pwe_count.
eassumption.
intuition congruence.
Qed.
Hint Resolve region_compatibility_1b region_compatibility_1bs
region_compatibility_1 region_compatibility_2b
region_compatibility_2 region_compatibility_3b :
region_compatibility.
-------------------------------------------------------------------------
Application of a coercion to all inhabitants of a region.
Lemma ji_coapp:
forall c T1 T2,
jco nil c (
T1 -->
T2) ->
cwf c ->
forall R vs,
ji R vs T1 ->
ji R (
vmap (
VCoApp c)
vs)
T2.
Proof.
induction 3; simpl; eauto.
Qed.
Application of VTyAbs to all inhabitants of a region.
Lemma ji_vtyabs:
forall R vs T,
ji R vs T ->
ji R (
vmap VTyAbs vs) (
TyForall T).
Proof.
induction 1; simpl; eauto.
Qed.
Inhabitance in a region is compatible with equality up to erasure.
Lemma inhabitant_compatible:
forall R1 v1 R2 v2 r,
jv R1 nil nil (
VInhabitant v1) (
TyAt (
TyRegion r)) ->
R1 =
R2 ->
erase_value v1 =
erase_value v2 ->
closed_value v2 ->
jv R2 nil nil (
VInhabitant v2) (
TyAt (
TyRegion r)).
Proof.
intros. subst. jv_inversion. econstructor. eauto. congruence. eauto.
Qed.
-------------------------------------------------------------------------
When typechecking a pair whose left-hand component is a region inhabitant,
there is no need to split the resource -- all of it can be sent into the
right-hand component. This fact helps simplify the analysis of a typing
derivation.
Lemma pair_inhabitant:
forall R1 R2 R v1 rho v2 T2,
star R1 R2 R ->
jv R1 nil nil (
VInhabitant v1) (
TyAt rho) ->
jv R2 nil nil v2 T2 ->
jv (
neutral R)
nil nil (
VInhabitant v1) (
TyAt rho) /\
jv R nil nil v2 T2.
Proof.
Implicit Arguments pair_inhabitant [
R1 R2 R v1 rho v2 T2 ].
Ltac pair_inhabitant :=
match goal with
|
h1:
star ?
R1 ?
R2 ?
R,
h2:
jv ?
R1 nil nil (
VInhabitant ?
v1) (
TyAt ?
rho),
h3:
jv ?
R2 nil nil ?
v2 ?
T2 |-
_ =>
unpack (
pair_inhabitant h1 h2 h3);
clear h1 h2 h3;
clear R1 R2
end.
-------------------------------------------------------------------------
This little lemma is useful in hoisting TyBang out of some other type
constructor.
Lemma jv_duplicable:
forall R M E v T,
jv R M E v T ->
duplicable R ->
duplicable M ->
jv (
neutral R) (
neutral M)
E v T.
Proof.
Hint Resolve jv_duplicable (@
duplicable_split resource)
(@
duplicable_split_2 resource) (@
duplicable_split menv)
(@
duplicable_split_2 menv) :
duplicable.
-------------------------------------------------------------------------
A fictitious change to a resource does not affect a store typing judgment.
Lemma fictitious_jsto:
forall R1 s,
jsto R1 s ->
forall R2,
fictitious R1 R2 ->
jsto R2 s.
Proof.
intros [ ? ? ] [ limit m ] [ h1 h2 ] [ ? ? ] [ ? ? ]. subst. split; eauto.
Qed.
If the resource R describes the current store, then location_map R
is (the erasure of) the store.
Lemma jsto_inversion_preliminary:
forall R limit m,
jsto R (
Store limit m) ->
forall l,
l <
reflimit R ->
location_map R l =
transform erase_value m l.
Proof.
introv [ ? h ] ?. rewrite h; eauto.
Qed.
If the resource R describes the current store, and if R says we
own some location l, then the location exists in the store, and
its content is as predicted by R (up to erasure).
Lemma jsto_inversion:
forall R limit m,
jsto R (
Store limit m) ->
forall l rv,
location_map R l =
Some rv ->
l <
reflimit R ->
exists v,
rv =
erase_value v /\
m l =
Some v.
Proof.
introv ?
hs ?.
forwards j:
jsto_inversion_preliminary.
eassumption.
eassumption.
rewrite j in hs.
clear j.
unfold transform in hs.
remember (
m l)
as ml;
destruct ml; [
injection hs;
intro |
discriminate hs ].
eauto.
Qed.