Set Implicit Arguments.
Require Import MyTactics.
Require Import DeBruijn.
Require Import Types.
Require Import TypeEquality.
Require Import Programs.
Require Export List.
-------------------------------------------------------------------------
A kind environment assigns kinds to type variables. For the time being,
we have no kinds, so a type environment would be just an integer, and
we can dispense with it.
-------------------------------------------------------------------------
A type environment assigns types to value variables. It is just a list
of types.
A coercion environment assigns coercion types to coercion variables.
It is again just a list of types.
Definition env :=
list ty.
-------------------------------------------------------------------------
When a new type variable is introduced, every type in the type and
coercion environments must be lifted.
Definition lift_ty_env k :
env ->
env :=
map (
lift_ty k).
When a type variable is substituted away, every type in the type
and coercion environments is affected.
Definition subst_ty_env U k :
env ->
env :=
map (
subst_ty U k).
-------------------------------------------------------------------------
Syntax for environments.
Notation "
E ;;
T" := (
T ::
E) (
at level 59,
left associativity) :
env_scope.
Notation "
E !" := (
lift_ty_env 0
E) (
at level 60) :
env_scope.
Open Scope env_scope.
Bind Scope env_scope with env.
-------------------------------------------------------------------------
Environment access.
Inductive jenv (
A :
Type) :
list A ->
nat ->
A ->
Prop :=
|
JEnvNil:
forall E T,
jenv (
E;;
T) 0
T
|
JEnvCons:
forall E U x T,
jenv E x T ->
jenv (
E;;
U) (
S x)
T.
Hint Constructors jenv.
-------------------------------------------------------------------------
Removing a binding in an environment.
Fixpoint remove_env_entry (
A :
Type) (
k :
nat) (
E :
list A) {
struct E } :=
match E,
k with
| (
E;;
T), 0 =>
E
| (
E;;
T),
S k =>
(
remove_env_entry k E);;
T
|
nil,
_ =>
nil
end.
-------------------------------------------------------------------------
Inserting a binding in an environment.
Fixpoint insert_env (
A :
Type)
k (
T :
A) (
E :
list A) :=
match k,
E with
| 0,
_ =>
(
E;;
T)
|
S k,
nil =>
nil
|
S k, (
E;;
U) =>
(
insert_env k T E;;
U)
end.
-------------------------------------------------------------------------
The proposition enveq E1 E2 holds if the type environments E1 and E2
are equal -- up to type equality.
Inductive enveq :
env ->
env ->
Prop :=
|
EnvEqNil:
forall E,
enveq E E
|
EnvEqCons:
forall E1 E2 T1 T2,
enveq E1 E2 ->
tyeq T1 T2 ->
wf T1 ->
enveq (
E1;;
T1) (
E2;;
T2).
Hint Constructors enveq :
enveq.
Lemma enveq_lift:
forall E1 E2,
enveq E1 E2 ->
enveq (
E1!) (
E2!).
Proof.
induction 1;
simpl;
eauto using tyeq_lift with enveq.
Qed.
-------------------------------------------------------------------------
A commutation lemma.
Lemma env_lift_lift:
forall E k,
(
lift_ty_env k E)! =
lift_ty_env (
S k) (
E!).
Proof.
unfold lift_ty_env.
induction E;
simpl;
intros;
f_equal;
eauto.
apply lift_lift_ty.
omega.
Qed.
Lemma env_subst_lift:
forall U E k,
(
subst_ty_env U k E)! =
subst_ty_env (
lift_ty 0
U) (
S k) (
E!).
Proof.
unfold subst_ty_env.
induction E;
simpl;
intros;
f_equal;
eauto.
apply lift_subst_1_ty.
omega.
Qed.
Lemma le_length_map:
forall A k (
xs :
list A) (
f :
A ->
A),
k <=
length xs ->
k <=
length (
map f xs).
Proof.
Lemma lift_ty_env_preserves_length:
forall E,
length (
E!) =
length E.
Proof.
induction E; simpl; auto.
Qed.
Lemma lift_ty_env_preserves_length_le:
forall E k,
k <=
length E ->
k <=
length (
E!).
Proof.
-------------------------------------------------------------------------
Environment access lemmas.
No variable is well-typed in an empty environment.
Lemma jenv_nil:
forall A x T,
~
jenv (
nil :
list A)
x T.
Proof.
introv h. inversion h.
Qed.
Lemma jenv_well_scoped:
forall A E k (
T :
A),
jenv E k T ->
k <
length E.
Proof.
induction 1; simpl; eauto.
Qed.
Environment access is a (partial) function.
Lemma jenv_uniqueness:
forall A E x (
T :
A),
jenv E x T ->
forall U,
jenv E x U ->
T =
U.
Proof.
induction 1; introv h; dependent destruction h; simpl; eauto; false; congruence.
Qed.
Ltac jenv_uniqueness :=
match goal with h1:
jenv ?
E ?
x ?
T1,
h2:
jenv ?
E ?
x ?
T2 |-
_ =>
generalize (
jenv_uniqueness h1 h2);
intro;
subst end.
Environment access is compatible with environment equality.
Lemma jenv_enveq:
forall E2 x T2,
jenv E2 x T2 ->
forall E1,
enveq E1 E2 ->
exists T1,
jenv E1 x T1 /\ ((
wf T1 /\
tyeq T1 T2) \/
T1 =
T2).
Proof.
induction 1; introv e; dependent destruction e; simpl; intuition eauto.
forwards* [ ? [ ? [ [ ? ? ] | ? ]]] : (IHjenv _ e). intuition eauto 6.
Qed.
Ltac jenv_enveq :=
match goal with
|
h1:
jenv ?
E2 _ _,
h2:
enveq _ ?
E2 |-
_ =>
generalize (
jenv_enveq h1 h2);
intros [ ? [ ? [ [ ? ? ] | ? ]]]; [
idtac |
subst ]
end.
Environment access commutes with environment transformations.
Lemma jenv_map:
forall A E x T,
jenv E x T ->
forall B (
f :
A ->
B)
y,
y =
f T ->
jenv (
map f E)
x y.
Proof.
induction 1; simpl; intros; subst; eauto.
Qed.
Lemma jenv_lift:
forall E x T,
jenv E x T ->
forall k,
jenv (
lift_ty_env k E)
x (
lift_ty k T).
Proof.
unfold lift_ty_env.
eauto using jenv_map.
Qed.
Lemma jenv_type_substitution:
forall E x T,
jenv E x T ->
forall k U,
jenv (
subst_ty_env U k E)
x (
subst_ty U k T).
Proof.
unfold subst_ty_env.
eauto using jenv_map.
Qed.
Hint Resolve jenv_type_substitution tyeq_subst :
type_substitution.
Lemma subst_lift_env:
subst_lift lift_ty_env subst_ty_env.
Proof.
unfold subst_lift,
subst_ty_env,
lift_ty_env.
intro E;
induction E;
intros k T;
simpl;
auto.
f_equal;
eauto using subst_lift_ty.
Qed.
Environment access gives rise to a notion of inclusion between environments.
Definition env_inclusion (
A :
Type) (
E F :
list A) :
Prop :=
forall x a,
jenv E x a ->
jenv F x a.
Lemma env_inclusion_extension:
forall A (
E F :
list A) (
a :
A),
env_inclusion E F ->
env_inclusion (
E;;
a) (
F;;
a).
Proof.
unfold env_inclusion. introv ? h. destruct x; dependent destruction h; eauto.
Qed.
Lemma env_inclusion_nil:
forall A (
E :
list A),
env_inclusion nil E.
Proof.
introv h. inversion h.
Qed.
-------------------------------------------------------------------------
Lemmas about the removal (or, conversely, the insertion) of an entry in
the environment.
Lemma remove_env_entry_simpl:
forall A k E (
T :
A),
(
remove_env_entry k E;;
T) =
remove_env_entry (
S k) (
E;;
T).
Proof.
reflexivity.
Qed.
Weakening -- insertion of a new entry in the environment -- requires
adjusting variables via lift_var.
Hint Extern 1 =>
rewrite lift_var_old :
jenv_weakening.
Hint Extern 1 =>
rewrite lift_var_succ :
jenv_weakening.
Lemma jenv_weakening:
forall A E k x (
T :
A),
jenv (
remove_env_entry k E)
x T ->
jenv E (
lift_var k x)
T.
Proof.
intro.
cut (
forall E x (
T :
A),
jenv E x T ->
forall k F,
E =
remove_env_entry k F ->
jenv F (
lift_var k x)
T
).
eauto.
induction 1;
simpl;
introv h;
F must be non-empty; argue so
destruct F;
simpl in h;
try congruence;
analyze k
destruct k;
try (
false;
omega);
decompose the equation; conclude
inversion h;
eauto with jenv_weakening.
Qed.
Removal of a binding commutes with map.
Lemma map_remove:
forall A B (
f :
A ->
B)
E k,
map f (
remove_env_entry k E) =
remove_env_entry k (
map f E).
Proof.
induction E; simpl; intros; auto.
destruct k. auto. simpl. f_equal. auto.
Qed.
Removal of a binding commutes with lifting.
Lemma remove_lift_env:
forall E k,
(
remove_env_entry k E)! =
remove_env_entry k (
E!).
Proof.
induction E; intros.
auto.
destruct k. auto.
simpl. f_equal. auto.
Qed.
Removal of a binding does not affect more recent indices, and requires
adjusting older indices by one.
Lemma jenv_substitution_recent:
forall A E x (
T :
A),
jenv E x T ->
forall k,
x <
k ->
jenv (
remove_env_entry k E)
x T.
Proof.
induction 1; simpl; intros; destruct k; try (false; omega); auto.
Qed.
Lemma jenv_substitution_old:
forall A E x (
T :
A),
jenv E x T ->
forall k,
x >
k ->
jenv (
remove_env_entry k E) (
x - 1)
T.
Proof.
induction E;
introv h ?;
dependent destruction h;
try solve [
false;
omega ].
replace (
S x - 1)
with x;
try omega.
destruct k;
simpl.
assumption.
replace x with (
S (
x - 1));
try omega.
eauto.
Qed.
Provided we have some term (of unknown type A) to substitute for
the variable that is being removed, and provided the judgement j
depends directly on the judgement jenv for variables, the judgement
j is preserved by substitution.
Lemma jenv_substitution:
forall A E x (
T :
A) (
wf :
A ->
Prop),
wf T ->
jenv E x T ->
forall k U,
jenv E k U ->
forall B (
j :
list A ->
B ->
A ->
Prop) (
var :
nat ->
B),
(
forall E x T,
wf T ->
jenv E x T ->
j E (
var x)
T) ->
forall u,
j (
remove_env_entry k E)
u U ->
j (
remove_env_entry k E) (
subst_var var u k x)
T.
Proof.
-------------------------------------------------------------------------
Lemmas about the insertion of an entry in the environment.
Lemma lift_insert_env:
forall k U E,
(
insert_env k U E)! =
insert_env k (
lift_ty 0
U) (
E!).
Proof.
induction k; destruct E; simpl; eauto. f_equal; eauto.
Qed.
Lemma remove_insert_env:
forall (
A :
Type)
k (
T :
A)
E,
E =
remove_env_entry k (
insert_env k T E).
Proof.
induction k; destruct E; simpl; intros; eauto. f_equal; eauto.
Qed.
Lemma jenv_insert:
forall (
A :
Type)
k (
T :
A)
E,
k <=
length E ->
jenv (
insert_env k T E)
k T.
Proof.
induction k; destruct E; simpl; eauto.
intro. false. omega.
Qed.
-------------------------------------------------------------------------
Application of tensor to the typing environment.
Notation env_tensor E U :=
(
map (
fun T =>
TyTensor T U)
E).
Lemma lift_env_tensor:
forall E U k,
lift_ty_env k (
env_tensor E U) =
env_tensor (
lift_ty_env k E) (
lift_ty k U).
Proof.
induction E; simpl; intros; f_equal; eauto.
Qed.
Lemma enveq_env_tensor:
forall U,
wf U ->
forall E1 E2,
enveq E1 E2 ->
enveq (
env_tensor E1 U) (
env_tensor E2 U).
Proof.
induction 2;
simpl;
econstructor;
eauto using tyeq_tensor.
Qed.
Lemma env_tensor_remove_env_entry:
forall U E k,
env_tensor (
remove_env_entry k E)
U =
remove_env_entry k (
env_tensor E U).
Proof.
induction E; destruct k; simpl; f_equal; eauto.
Qed.
Lemma jenv_env_tensor:
forall E k T,
jenv E k T ->
forall U,
jenv (
env_tensor E U)
k (
TyTensor T U).
Proof.
induction 1; simpl; eauto.
Qed.