Set Implicit Arguments.
Require Import MyTactics.
Require Import DeBruijn.
Require Import Store.
Require Import Coercions.
Require Import Layers.
Require Import FocusPaths.
-------------------------------------------------------------------------
Primitive operations.
Inductive primitive :
Set :=
|
PDefocusDuplicable:
path ->
primitive
|
PFocus:
path ->
primitive
|
PNewGroup:
primitive
|
PAdopt:
primitive
|
PFocusGroup:
primitive
|
PNewAffine:
primitive
|
PReadAffine:
primitive
|
PWriteAffine:
primitive
|
PNewCap:
primitive
|
PReadCap:
primitive
|
PWriteCap:
primitive
tex: primitive operations
.
Ltac prim :=
match goal with p:
primitive |-
_ =>
destruct p;
simpl end.
-------------------------------------------------------------------------
Values.
VInhabitant could have a raw value as its argument, as no reduction takes
place under it, and the argument is used only as a key in a region.
Inductive value :=
|
VVar:
nat ->
value
|
VAbs:
term ->
value
|
VPair:
layer ->
layer ->
value ->
value ->
value
|
VUnit:
layer ->
value
|
VTyAbs:
value ->
value
|
VPack:
value ->
value
|
VCoApp:
coercion ->
value ->
value
|
VBang:
value ->
value
|
VLoc:
location ->
value ->
value
|
VRegionCap:
values ->
value
|
VRegionCapPunched:
values ->
value
|
VInhabitant:
value ->
value
tex: values
with values :=
|
VNil:
values
|
VCons:
value ->
values ->
values
tex: lists of values
-------------------------------------------------------------------------
Terms.
TMixPair is a physical/logical pair of a term and a value. It is just
what we need to encode the frame rule. One could go further and define
a general TPair construct that allows all four layer combinations,
but that would be overkill and more noisy.
THide v t is syntax for an as-yet-inactive instance of the anti-frame
rule.
In nominal style, this construct would be written hide x = v in t. We
impose the requirement that t has no free variable other than x. In de
Bruijn style, this means that t has no free variable other than 0. The
value v can be arbitrary, and is substituted for x when the hide
statement begins its execution. By requiring that x.t be closed, we are
able to precisely identify the boundary of the hide construct. This helps
simplify the definition of substitution. (More precisely, substitution into
hide x = v in t construct only requires substitution into v, whereas,
if t was not closed, it would require revelation and substitution into
t. The definition of substitution would then become dependent upon the
definition of revelation.) This also helps define revelation for hide
constructs, where coercions must be applied to each of the free variables.
In a higher-level language, one could introduce a simpler construct hide t,
where t may have free variables; this would then be viewed as syntactic
sugar for hide xs = xs in t, where the xs are the free variables of t.
The construct hide xs = vs in t could itself be viewed as sugar for hide
x = (vs) in let (xs) = x in t, so that requiring t to have exactly one
free variable is not restrictive.
with term :=
|
TVal:
value ->
term
|
TApp:
value ->
term ->
term
|
TMixPair:
term ->
value ->
term
|
TTyAbs:
term ->
term
|
TCoApp:
coercion ->
term ->
term
|
TLetUnpack:
value ->
term ->
term
|
TLetBang:
value ->
term ->
term
|
TLetPair:
layer ->
layer ->
value ->
term ->
term
|
TPrimApp:
primitive ->
value ->
term
|
THide:
value ->
term ->
term
tex: terms
.
Notation VPhyPair :=
(
VPair Physical Physical).
Notation VMixPair :=
(
VPair Physical Logical).
Notation VLogPair :=
(
VPair Logical Logical).
Notation VPhyUnit :=
(
VUnit Physical).
Notation VLogUnit :=
(
VUnit Logical).
Notation TLetMixPair :=
(
TLetPair Physical Logical).
Notation TLet t1 t2 :=
(
TApp (
VAbs t2)
t1).
-------------------------------------------------------------------------
Stores.
Definition store :=
gstore value.
-------------------------------------------------------------------------
Construct an appropriate mutual induction scheme for values and terms.
Scheme value_term_ind_v :=
Induction for value Sort Prop
with value_term_ind_vs :=
Induction for values Sort Prop
with value_term_ind_t :=
Induction for term Sort Prop.
Combined Scheme value_term_ind from value_term_ind_v,
value_term_ind_vs,
value_term_ind_t.
-------------------------------------------------------------------------
De Bruijn operations over terms.
The closed values carried by VRegionCap are unaffected by lifting
or substitution. They are erased anyway, so this does not compromise
the lemmas erase_lift and erase_subst. In fact, this has the
unexpected side effect of simplifying some proofs, such as stability
of typing through term substitution.
The value carried by VInhabitant is also closed, so one might
wish to follow the same route, but that would break erase_lift
and erase_subst, because this value is not erased. So, we perform
lifting and substitution as usual, even though we know that this
value should be closed. Same remark about the term carried by
THide.
Fixpoint lift_value (
k :
nat) (
v :
value) :
value :=
match v with
|
VVar x =>
VVar (
lift_var k x)
|
VAbs t =>
VAbs (
lift_term (1 +
k)
t)
|
VPair layer1 layer2 v1 v2 =>
VPair layer1 layer2 (
lift_value k v1) (
lift_value k v2)
|
VUnit layer =>
VUnit layer
|
VTyAbs v =>
VTyAbs (
lift_value k v)
|
VPack v =>
VPack (
lift_value k v)
|
VCoApp c v =>
VCoApp c (
lift_value k v)
|
VBang v =>
VBang (
lift_value k v)
|
VLoc l v =>
VLoc l v
|
VRegionCap vs =>
VRegionCap vs
|
VRegionCapPunched vs =>
VRegionCapPunched vs
|
VInhabitant v =>
VInhabitant (
lift_value k v)
end
with lift_term (
k :
nat) (
t :
term) :
term :=
match t with
|
TVal v =>
TVal (
lift_value k v)
|
TApp v t =>
TApp (
lift_value k v) (
lift_term k t)
|
TMixPair t1 v2 =>
TMixPair (
lift_term k t1) (
lift_value k v2)
|
TTyAbs t =>
TTyAbs (
lift_term k t)
|
TCoApp c t =>
TCoApp c (
lift_term k t)
|
TLetBang v t =>
TLetBang (
lift_value k v) (
lift_term (1 +
k)
t)
|
TLetUnpack v t =>
TLetUnpack (
lift_value k v) (
lift_term (1 +
k)
t)
|
TLetPair layer1 layer2 v t =>
TLetPair layer1 layer2 (
lift_value k v) (
lift_term (2 +
k)
t)
|
TPrimApp p v =>
TPrimApp p (
lift_value k v)
|
THide v t =>
THide (
lift_value k v) (
lift_term (1 +
k)
t)
end.
Substitutions of values for variables within values and terms. By design of
the syntax, substitution of terms for variables is not possible.
Fixpoint subst_value (
v :
value) (
k :
nat) (
w :
value) :
value :=
match w with
|
VVar x =>
subst_var VVar v k x
|
VAbs u =>
VAbs (
subst_term (
lift_value 0
v) (1 +
k)
u)
|
VPair layer1 layer2 w1 w2 =>
VPair layer1 layer2 (
subst_value v k w1) (
subst_value v k w2)
|
VUnit layer =>
VUnit layer
|
VTyAbs w =>
VTyAbs (
subst_value v k w)
|
VPack w =>
VPack (
subst_value v k w)
|
VCoApp c w =>
VCoApp c (
subst_value v k w)
|
VBang w =>
VBang (
subst_value v k w)
|
VLoc l v =>
VLoc l v
|
VRegionCap vs =>
VRegionCap vs
|
VRegionCapPunched vs =>
VRegionCapPunched vs
|
VInhabitant w =>
VInhabitant (
subst_value v k w)
end
with subst_term (
v :
value) (
k :
nat) (
u :
term) :
term :=
match u with
|
TVal w =>
TVal (
subst_value v k w)
|
TApp w u =>
TApp (
subst_value v k w) (
subst_term v k u)
|
TMixPair t1 v2 =>
TMixPair (
subst_term v k t1) (
subst_value v k v2)
|
TTyAbs u =>
TTyAbs (
subst_term v k u)
|
TCoApp c u =>
TCoApp c (
subst_term v k u)
|
TLetBang w u =>
TLetBang (
subst_value v k w) (
subst_term (
lift_value 0
v) (1 +
k)
u)
|
TLetUnpack w u =>
TLetUnpack (
subst_value v k w) (
subst_term (
lift_value 0
v) (1 +
k)
u)
|
TLetPair layer1 layer2 w u =>
TLetPair layer1 layer2 (
subst_value v k w) (
subst_term (
lift_value 0 (
lift_value 0
v)) (2 +
k)
u)
|
TPrimApp p w =>
TPrimApp p (
subst_value v k w)
|
THide w t =>
THide (
subst_value v k w) (
subst_term (
lift_value 0
v) (1 +
k)
t)
end.
-------------------------------------------------------------------------
De Bruijn lemmas.
Lemma subst_lift_value_term:
(
forall w v k,
subst_value v k (
lift_value k w) =
w) /\
(
forall vs :
values,
True) /\
(
forall t v k,
subst_term v k (
lift_term k t) =
t).
Proof.
Lemma subst_lift_value:
subst_lift lift_value subst_value.
Proof.
Lemma subst_lift_term:
subst_lift lift_term subst_term.
Proof.
Local Hint Resolve subst_lift_value subst_lift_term.
Lemma lift_lift_value_term:
(
forall v k1 s1,
k1 <=
s1 ->
lift_value k1 (
lift_value s1 v) =
lift_value (
S s1) (
lift_value k1 v)) /\
(
forall vs :
values,
True) /\
(
forall t k1 s1,
k1 <=
s1 ->
lift_term k1 (
lift_term s1 t) =
lift_term (
S s1) (
lift_term k1 t)).
Proof.
apply value_term_ind;
intros;
simpl;
f_equal;
eauto with lift_lift_db.
Qed.
Lemma lift_lift_value:
lift_lift lift_value.
Proof.
Lemma lift_lift_term:
lift_lift lift_term.
Proof.
Local Hint Resolve lift_lift_value lift_lift_term.
Lemma lift_zero_lift_value:
lift_zero_lift lift_value.
Proof.
lift_zero_lift_tac.
Qed.
Lemma lift_zero_lift_term:
lift_zero_lift lift_term.
Proof.
lift_zero_lift_tac.
Qed.
Ltac lzl_value :=
lzl lift_value lift_zero_lift_value.
Hint Extern 1 =>
lzl_value :
lift_subst_1_db.
Hint Extern 1 =>
lzl_value :
lift_subst_2_db.
Hint Extern 1 =>
lzl_value :
subst_subst_db.
Lemma lift_subst_1_value_term:
(
forall w k1 v s1,
k1 <=
s1 ->
lift_value k1 (
subst_value v s1 w) =
subst_value (
lift_value k1 v) (
S s1) (
lift_value k1 w)
) /\ (
forall vs :
values,
True
) /\ (
forall t k1 v s1,
k1 <=
s1 ->
lift_term k1 (
subst_term v s1 t) =
subst_term (
lift_value k1 v) (
S s1) (
lift_term k1 t)
).
Proof.
apply value_term_ind;
simpl;
intros;
eauto 6
with lift_subst_1_db.
Qed.
Lemma lift_subst_1_value:
lift_subst_1 lift_value lift_value subst_value.
Proof.
Lemma lift_subst_1_term:
lift_subst_1 lift_value lift_term subst_term.
Proof.
Local Hint Resolve lift_subst_1_value lift_subst_1_term.
Hint Extern 1 =>
rewrite lift_subst_1_value; [
idtac |
omega ] :
subst_subst_db.
Lemma lift_subst_2_value_term:
(
forall w k1 v s1,
k1 <=
s1 ->
lift_value s1 (
subst_value v k1 w) =
subst_value (
lift_value s1 v)
k1 (
lift_value (
S s1)
w)
) /\ (
forall vs :
values,
True
) /\ (
forall t k1 v s1,
k1 <=
s1 ->
lift_term s1 (
subst_term v k1 t) =
subst_term (
lift_value s1 v)
k1 (
lift_term (
S s1)
t)
).
Proof.
apply value_term_ind;
simpl;
intros;
eauto 6
with lift_subst_2_db.
Qed.
Lemma lift_subst_2_value:
lift_subst_2 lift_value lift_value subst_value.
Proof.
Lemma lift_subst_2_term:
lift_subst_2 lift_value lift_term subst_term.
Proof.
Local Hint Resolve lift_subst_2_value lift_subst_2_term.
Lemma subst_subst_value_term:
(
forall v k1 t u s1,
k1 <=
s1 ->
subst_value t s1 (
subst_value u k1 v) =
subst_value (
subst_value t s1 u)
k1 (
subst_value (
lift_value k1 t) (
S s1)
v)
) /\ (
forall vs :
values,
True
) /\ (
forall v k1 t u s1,
k1 <=
s1 ->
subst_term t s1 (
subst_term u k1 v) =
subst_term (
subst_value t s1 u)
k1 (
subst_term (
lift_value k1 t) (
S s1)
v)
).
Proof.
apply value_term_ind;
simpl;
intros;
eauto with subst_subst_db;
some more difficult cases
f_equal;
eauto 6
with subst_subst_db.
Qed.
Lemma subst_subst_value:
subst_subst lift_value subst_value subst_value.
Proof.
Lemma subst_subst_term:
subst_subst lift_value subst_value subst_term.
Proof.
Lemma pun_1_value_term:
pun_1 VVar lift_value subst_value /\
(
forall vs :
values,
True) /\
pun_1 VVar lift_term subst_term.
Proof.
Definition pun_1_value :=
proj1 pun_1_value_term.
Definition pun_1_term :=
proj2 pun_1_value_term.
Lemma pun_2_value_term:
pun_2 VVar lift_value subst_value /\
(
forall vs :
values,
True) /\
pun_2 VVar lift_term subst_term.
Proof.
Definition pun_2_value :=
proj1 pun_2_value_term.
Definition pun_2_term :=
proj2 pun_2_value_term.
Definition closed_value :
value ->
Prop :=
closed lift_value.
Lemma closed_value_lift:
forall k v,
closed_value v ->
lift_value k v =
v.
Proof.
unfold closed_value, closed, well_scoped_lift.
introv h. eapply h. reflexivity.
Qed.
Lemma closed_value_subst:
forall w k v,
closed_value v ->
subst_value w k v =
v.
Proof.
Ltac closed :=
match goal with c:
closed_value _ |-
_ =>
eapply c;
eauto end.
-------------------------------------------------------------------------
Equality of values / terms is decidable. Not a really interesting property;
it seems to be required by the fact that we effectively use values as keys
within regions. In particular, the semantics of PFocusGroup needs to
identify and remove a certain value in a list of values.
Local Hint Resolve eq_nat_dec.
Lemma eq_layer_dec:
forall layer1 layer2 :
layer, {
layer1 =
layer2 } + {
layer1 <>
layer2 }.
Proof.
decide equality.
Qed.
Local Hint Resolve eq_layer_dec.
Lemma eq_path_dec:
forall pi1 pi2 :
path, {
pi1 =
pi2 } + {
pi1 <>
pi2 }.
Proof.
decide equality.
Qed.
Local Hint Resolve eq_path_dec.
Lemma eq_coercion_dec:
forall c1 c2 :
coercion, {
c1 =
c2 } + {
c1 <>
c2 }.
Proof.
decide equality.
Qed.
Local Hint Resolve eq_coercion_dec.
Lemma eq_primitive_dec:
forall p1 p2 :
primitive, {
p1 =
p2 } + {
p1 <>
p2 }.
Proof.
decide equality.
Qed.
Local Hint Resolve eq_primitive_dec.
Lemma eq_value_dec:
forall v1 v2 :
value, {
v1 =
v2 } + {
v1 <>
v2 }
with eq_values_dec:
forall vs1 vs2 :
values, {
vs1 =
vs2 } + {
vs1 <>
vs2 }
with eq_term_dec:
forall t1 t2 :
term, {
t1 =
t2 } + {
t1 <>
t2 }.
Proof.
decide equality.
decide equality.
decide equality.
Qed.