Set Implicit Arguments.
Require Import MyTactics.
Require Import DeBruijn.
Require Import Types.
Require Import TypeContexts.
Require Import FocusPaths.
Require Import TypeEquality.
Require Import MoreTypeEquality.
Require Import Coercions.
Require Import Programs.
Require Import Subtyping.
Require Import Typing.
Require Import Environments.
Require Import Multiplicity.
Require Import MultiplicityEnvironments.
Require Import Resources.
Require Import ResourcesContinued.
Require Import ResourcesReconfiguration.
Require Import ValueLists.
Require Import Erasure.
Hint Extern 1 =>
rewrite env_lift_lift :
weaken_ty.
Hint Extern 1 =>
rewrite <-
lift_lift_ty :
weaken_ty.
Hint Extern 1 =>
rewrite <-
lift_lift_ty_ctx :
weaken_ty.
-------------------------------------------------------------------------
A type that appears in the right-hand side of a judgement is well-formed.
Lemma jco_wf:
forall C c T,
jco C c T ->
wf T.
Proof.
induction 1; eauto; eauto 8; eauto 10.
Qed.
Lemma jco_wf_left:
forall C c T U,
jco C c (
T -->
U) ->
wf T.
Proof.
introv h.
generalize (
jco_wf h).
eauto.
Qed.
Lemma jco_wf_right:
forall C c T U,
jco C c (
T -->
U) ->
wf U.
Proof.
introv h.
generalize (
jco_wf h).
eauto.
Qed.
Lemma jp_wf_1:
forall p T1 T2,
jp p T1 T2 ->
wf T1.
Proof.
induction 1; eauto 6.
Qed.
Lemma jp_wf_2:
forall p T1 T2,
jp p T1 T2 ->
wf T2.
Proof.
induction 1; eauto 6.
Qed.
Hint Resolve jp_wf_1 jp_wf_2.
Lemma jvit_wf:
(
forall R M E v T,
jv R M E v T ->
wf T
) /\ (
forall R vs T,
ji R vs T ->
wf T
) /\ (
forall R M E t T,
jt R M E t T ->
wf T
).
Proof.
Ltac jwf :=
match goal with
|
h:
jco _ _ _ |-
_ =>
generalize (
jco_wf h);
clear h;
jwf
|
h:
jv _ _ _ _ _ |-
_ =>
generalize (
pi1 jvit_wf _ _ _ _ _ h);
clear h;
jwf
|
h:
ji _ _ _ |-
_ =>
generalize (
pi2 jvit_wf _ _ _ h);
clear h;
jwf
|
h:
jt _ _ _ _ _ |-
_ =>
generalize (
pi3 jvit_wf _ _ _ _ _ h);
clear h;
jwf
|
_ =>
idtac
end.
Hint Extern 1 (
wf _) =>
jwf.
-------------------------------------------------------------------------
The region inhabitation judgement is compatible with type equality.
Lemma ji_tyeq:
forall R vs T,
ji R vs T ->
forall U,
tyeq T U ->
wf U ->
ji R vs U.
Proof.
induction 1; intros; eauto.
Qed.
-------------------------------------------------------------------------
Typing is compatible with environment equality.
Lemma jvit_enveq:
(
forall R M E2 v T,
jv R M E2 v T ->
forall E1,
enveq E1 E2 ->
jv R M E1 v T
) /\ (
forall R vs T,
ji R vs T ->
True
) /\ (
forall R M E2 t T,
jt R M E2 t T ->
forall E1,
enveq E1 E2 ->
jt R M E1 t T
).
Local Hint Extern 0 =>
match goal with
| |- (
enveq (
_;; ?
T) (
_;; ?
T)) =>
econstructor; [
idtac |
apply tyeq_reflexive;
eauto 3 |
eauto 3 ]
end.
Proof.
By induction...
apply jvit_ind;
simpl in *;
intros;
match goal with
| |-
jv _ _ _ (
VVar _)
_ =>
VVar is the interesting case.
jenv_enveq;
eauto
|
_ =>
Every other case is trivial.
econstructor;
simpl;
eauto using enveq_lift
end.
Qed.
-------------------------------------------------------------------------
Weakening by introducing a new type variable binding.
Hint Resolve tyeq_lift jenv_lift jpath_lift :
weaken_ty.
Hint Extern 3 =>
rewrite lift_subst_2_ty :
weaken_ty.
Hint Extern 3 =>
rewrite <-
lift_subst_2_ty :
weaken_ty.
Hint Extern 1 =>
rewrite map_length :
weaken_ty.
Lemma jco_ty_weakening:
forall C c T,
jco C c T ->
forall k,
jco (
lift_ty_env k C)
c (
lift_ty k T).
Proof.
induction 1;
simpl in *;
intro;
CoDefocus:
repeat rewrite lift_fill;
simpl;
eauto 7
with weaken_ty.
CoTensorExchange
repeat rewrite lift_tensors;
simpl.
econstructor;
eauto with weaken_ty.
Qed.
Lemma jco_ty_weakening_arrow:
forall C c T1 T2,
jco C c (
T1 -->
T2) ->
forall k,
jco (
lift_ty_env k C)
c (
lift_ty k T1 -->
lift_ty k T2).
Proof.
Lemma jco_ty_weakening_nil_arrow:
forall c T1 T2,
jco nil c (
T1 -->
T2) ->
forall k,
jco nil c (
lift_ty k T1 -->
lift_ty k T2).
Proof.
Hint Resolve jco_ty_weakening_nil_arrow :
weaken_ty.
Hint Extern 3 =>
rewrite lift_lift_ty :
weaken_ty.
Lemma jp_ty_weakening:
forall p T1 T2,
jp p T1 T2 ->
forall k,
jp p (
lift_ty k T1) (
lift_ty k T2).
Proof.
induction 1;
simpl;
intros;
repeat rewrite lift_fill;
simpl;
eauto 6
with weaken_ty.
Qed.
Hint Resolve jp_ty_weakening :
weaken_ty.
Hint Extern 1 =>
rewrite <-
lift_env_tensor :
weaken_ty.
Lemma j_ty_weakening_general:
(
forall R M E v T,
jv R M E v T ->
forall k,
jv R M (
lift_ty_env k E)
v (
lift_ty k T)
) /\ (
forall R vs T,
ji R vs T ->
forall k,
ji R vs (
lift_ty k T)
) /\ (
forall R M E t T,
jt R M E t T ->
forall k,
jt R M (
lift_ty_env k E)
t (
lift_ty k T)
).
Proof.
apply jvit_ind;
intros;
simpl in *;
econstructor;
simpl in *;
eauto 3
with weaken_ty.
Qed.
Lemma j_ty_weakening_value:
forall R M E v T,
jv R M E v T ->
jv R M (
E!)
v (
lift_ty 0
T).
Proof.
Lemma j_ty_weakening_value_remove:
forall R M E v T k,
jv R M (
remove_env_entry k E)
v T ->
jv R M (
remove_env_entry k (
E!))
v (
lift_ty 0
T).
Proof.
Lemma j_ty_weakening_term:
forall R M E t T,
jt R M E t T ->
jt R M (
E!)
t (
lift_ty 0
T).
Proof.
-------------------------------------------------------------------------
Weakening by introducing a new term variable binding.
Lemma j_term_weakening_general:
(
forall R N F v T,
jv R N F v T ->
forall k M E,
N =
remove_env_entry k M ->
F =
remove_env_entry k E ->
jv R M E (
lift_value k v)
T
) /\ (
forall R vs T,
ji R vs T ->
True
) /\ (
forall R N F t T,
jt R N F t T ->
forall k M E,
N =
remove_env_entry k M ->
F =
remove_env_entry k E ->
jt R M E (
lift_term k t)
T
).
Local Hint Extern 1 ((
_;;
_) = (
_;;
_)) =>
f_equal.
Local Hint Extern 1 ((
_;;
_) =
remove_env_entry _ (
_;;
_)) =>
simpl.
Local Hint Extern 1 (
_ =
_) =>
congruence.
Proof.
Lemma j_value_weakening:
forall R M m E T u U,
jv R M E u U ->
jv R (
M;;
m) (
E;;
T) (
lift_value 0
u)
U.
Proof.
Lemma j_value_weakening_remove:
forall R M m Mm k E T u U,
jv R M (
remove_env_entry k E)
u U ->
Mm = (
M;;
m) ->
jv R Mm (
remove_env_entry (
S k) (
E;;
T)) (
lift_value 0
u)
U.
Proof.
Lemma j_value_weakening_insert:
forall R M E v T k m U,
jv R M E v T ->
jv R (
insert_env k m M) (
insert_env k U E) (
lift_value k v)
T.
Proof.
Lemma j_term_weakening:
forall R M m E T t U,
jt R M E t U ->
jt R (
M;;
m) (
E;;
T) (
lift_term 0
t)
U.
Proof.
Lemma j_term_weakening_2:
forall R M E m0 T0 m1 T1 m2 T2 u U,
jt R (
M;;
m1;;
m0) (
E;;
T1;;
T0)
u U ->
jt R (
M;;
m2;;
m1;;
m0) (
E;;
T2;;
T1;;
T0) (
lift_term 2
u)
U.
Proof.
Lemma j_term_weakening_insert:
forall R M E t T k m U,
jt R M E t T ->
jt R (
insert_env k m M) (
insert_env k U E) (
lift_term k t)
T.
Proof.
-------------------------------------------------------------------------
Weakening by introducing a new coercion variable binding.
Hint Extern 1 =>
simpl :
j_term_substitution.
Hint Extern 2 =>
rewrite remove_lift_env :
j_term_substitution.
Hint Extern 2 =>
rewrite <-
remove_lift_env :
j_term_substitution.
Lemma jco_weakening_general:
forall D c T,
jco D c T ->
forall k C,
D =
remove_env_entry k C ->
jco C (
lift_co k c)
T.
Proof.
induction 1;
simpl;
intros;
subst;
eauto using jenv_weakening with j_term_substitution.
Qed.
Lemma jco_weakening:
forall C T c U,
jco C c U ->
jco (
C;;
T) (
lift_co 0
c)
U.
Proof.
-------------------------------------------------------------------------
A resource weakening lemma.
This lemma shows that the system is affine: judgements remain valid as more
resources are added.
Lemma j_resource_weakening:
(
forall R1 M E v T,
jv R1 M E v T ->
forall R2 R,
star R1 R2 R ->
jv R M E v T
) /\ (
forall R vs T,
ji R vs T ->
True
) /\ (
forall R1 M E t T,
jt R1 M E t T ->
forall R2 R,
star R1 R2 R ->
jt R M E t T
).
Proof.
apply jvit_ind;
intros;
simpl;
eauto 4
with resources;
In the cases where the resource is split, we must split
the excess resources, and can do so in an arbitrary way.
try solve [
star_associative;
eauto 4
with resources ].
JVRegionCap
permute_left.
econstructor;
eauto 3
with resources.
JVRegionCapPunched
permute_left.
econstructor;
eauto 3
with resources.
Qed.
Definition j_value_resource_weakening :=
pi1 j_resource_weakening.
Definition j_term_resource_weakening :=
pi3 j_resource_weakening.
-------------------------------------------------------------------------
A multiplicity weakening lemma.
This lemma shows that the system is affine: judgements remain valid as more
variables are introduced.
Lemma j_multiplicity_weakening:
(
forall R M1 E v T,
jv R M1 E v T ->
forall M2 M,
star M1 M2 M ->
jv R M E v T
) /\ (
forall R vs T,
ji R vs T ->
True
) /\ (
forall R M1 E t T,
jt R M1 E t T ->
forall M2 M,
star M1 M2 M ->
jt R M E t T
).
Proof.
apply jvit_ind;
intros;
simpl;
eauto;
In the cases where the multiplicity environment is split, we must split
the excess resources, and can do so in an arbitrary way.
try solve [
star_associative;
eauto ].
VVar
forwards [ ? [ ? ? ]] :
present_star;
eauto.
Qed.
-------------------------------------------------------------------------
A combination of the above two lemmas.
Lemma j_resource_multiplicity_weakening:
(
forall R1 M1 E v T,
jv R1 M1 E v T ->
forall R2 R M2 M,
star R1 R2 R ->
star M1 M2 M ->
jv R M E v T
) /\ (
forall R1 M1 E t T,
jt R1 M1 E t T ->
forall R2 R M2 M,
star R1 R2 R ->
star M1 M2 M ->
jt R M E t T
).
Proof.
Lemma j_resource_multiplicity_weakening_term:
forall R1 M1 E t T,
jt R1 M1 E t T ->
forall R2 R M2 M,
star R1 R2 R ->
star M1 M2 M ->
jt R M E t T.
Proof.