Compare commits
2 commits
f8effc45ad
...
3c86dde677
Author | SHA1 | Date | |
---|---|---|---|
3c86dde677 | |||
4b76d6a982 |
2 changed files with 104 additions and 116 deletions
|
@ -8,7 +8,7 @@ Require Import FSetNotin.
|
|||
*)
|
||||
Lemma type_subst_fresh : forall (x : atom) (τ:type_DeBruijn) (σ:type_DeBruijn),
|
||||
x `notin` (type_fv τ) ->
|
||||
([ x ~> σ ] τ) = τ
|
||||
([ x ~tt~> σ ] τ) = τ
|
||||
.
|
||||
Proof.
|
||||
intros.
|
||||
|
@ -48,25 +48,68 @@ Proof.
|
|||
reflexivity.
|
||||
simpl type_fv in H; fsetdec.
|
||||
simpl type_fv in H; fsetdec.
|
||||
|
||||
Qed.
|
||||
|
||||
(*
|
||||
* Substitution has no effect if the variable is not free
|
||||
*)
|
||||
Lemma expr_subst_fresh : forall (x : atom) (t:expr_DeBruijn) (e:expr_DeBruijn),
|
||||
x `notin` (expr_fv e) ->
|
||||
([ x ~ee~> t ] e) = e
|
||||
.
|
||||
Proof.
|
||||
intros.
|
||||
induction e.
|
||||
|
||||
- unfold expr_fv in H.
|
||||
apply AtomSetNotin.elim_notin_singleton in H.
|
||||
simpl.
|
||||
case_eq (x == a).
|
||||
congruence.
|
||||
reflexivity.
|
||||
|
||||
- reflexivity.
|
||||
|
||||
- simpl. rewrite IHe.
|
||||
all: auto.
|
||||
|
||||
- simpl; rewrite IHe.
|
||||
auto. auto.
|
||||
- simpl; rewrite IHe.
|
||||
auto. auto.
|
||||
- simpl; rewrite IHe.
|
||||
auto. auto.
|
||||
|
||||
- simpl. rewrite IHe1, IHe2.
|
||||
reflexivity.
|
||||
simpl expr_fv in H; fsetdec.
|
||||
simpl expr_fv in H; fsetdec.
|
||||
|
||||
- simpl. rewrite IHe1, IHe2.
|
||||
reflexivity.
|
||||
simpl expr_fv in H; fsetdec.
|
||||
simpl expr_fv in H; fsetdec.
|
||||
|
||||
- simpl; rewrite IHe.
|
||||
auto. auto.
|
||||
- simpl; rewrite IHe.
|
||||
auto. auto.
|
||||
Qed.
|
||||
|
||||
|
||||
|
||||
Lemma open_rec_lc_core : forall τ i σ1 j σ2,
|
||||
Lemma type_open_lc_core : forall (τ:type_DeBruijn) i (σ1:type_DeBruijn) j (σ2:type_DeBruijn),
|
||||
i <> j ->
|
||||
{i ~> σ1} τ = {j ~> σ2} ({i ~> σ1} τ) ->
|
||||
({j ~> σ2} τ) = τ.
|
||||
|
||||
{i ~tt~> σ1} τ = {j ~tt~> σ2} ({i ~tt~> σ1} τ) ->
|
||||
({j ~tt~> σ2} τ) = τ
|
||||
.
|
||||
Proof with eauto*.
|
||||
induction τ;
|
||||
intros i σ1 j σ2 Neq H.
|
||||
intros i σ1 j σ2 Neq H;
|
||||
simpl in *;
|
||||
inversion H;
|
||||
f_equal; eauto.
|
||||
|
||||
(* id *)
|
||||
- reflexivity.
|
||||
|
||||
(* free var *)
|
||||
- reflexivity.
|
||||
|
||||
(* bound var *)
|
||||
- simpl in *.
|
||||
destruct (j === n).
|
||||
|
@ -83,102 +126,45 @@ Proof with eauto*.
|
|||
reflexivity.
|
||||
contradict n1.
|
||||
reflexivity.
|
||||
|
||||
(* univ *)
|
||||
- simpl in *.
|
||||
inversion H.
|
||||
f_equal.
|
||||
apply IHτ with (i:=S i) (j:=S j) (σ1:=σ1).
|
||||
auto.
|
||||
apply H1.
|
||||
|
||||
(* spec *)
|
||||
- simpl in *.
|
||||
inversion H.
|
||||
f_equal.
|
||||
* apply IHτ1 with (i:=i) (j:=j) (σ1:=σ1).
|
||||
auto.
|
||||
apply H1.
|
||||
* apply IHτ2 with (i:=i) (j:=j) (σ1:=σ1).
|
||||
auto.
|
||||
apply H2.
|
||||
|
||||
(* func *)
|
||||
- simpl in *.
|
||||
inversion H.
|
||||
f_equal.
|
||||
* apply IHτ1 with (i:=i) (j:=j) (σ1:=σ1).
|
||||
auto.
|
||||
apply H1.
|
||||
* apply IHτ2 with (i:=i) (j:=j) (σ1:=σ1).
|
||||
auto.
|
||||
apply H2.
|
||||
|
||||
|
||||
(* morph *)
|
||||
- simpl in *.
|
||||
inversion H.
|
||||
f_equal.
|
||||
* apply IHτ1 with (i:=i) (j:=j) (σ1:=σ1).
|
||||
auto.
|
||||
apply H1.
|
||||
* apply IHτ2 with (i:=i) (j:=j) (σ1:=σ1).
|
||||
auto.
|
||||
apply H2.
|
||||
|
||||
(* ladder *)
|
||||
- simpl in *.
|
||||
inversion H.
|
||||
f_equal.
|
||||
* apply IHτ1 with (i:=i) (j:=j) (σ1:=σ1).
|
||||
auto.
|
||||
apply H1.
|
||||
* apply IHτ2 with (i:=i) (j:=j) (σ1:=σ1).
|
||||
auto.
|
||||
apply H2.
|
||||
|
||||
Qed.
|
||||
|
||||
|
||||
Lemma type_open_rec_lc : forall k σ τ,
|
||||
(*
|
||||
* opening is idempotent on locally closed types
|
||||
*)
|
||||
Lemma type_open_lc : forall k σ τ,
|
||||
type_lc τ ->
|
||||
({ k ~> σ } τ) = τ
|
||||
({ k ~tt~> σ } τ) = τ
|
||||
.
|
||||
Proof.
|
||||
intros.
|
||||
generalize dependent k.
|
||||
induction H.
|
||||
|
||||
(* id *)
|
||||
- auto.
|
||||
|
||||
(* free var *)
|
||||
- auto.
|
||||
induction H; eauto; simpl in *; intro k.
|
||||
|
||||
(* univ *)
|
||||
- simpl.
|
||||
intro k.
|
||||
f_equal.
|
||||
unfold type_open in *.
|
||||
pick fresh x for L.
|
||||
apply open_rec_lc_core with
|
||||
f_equal.
|
||||
unfold type_open in *.
|
||||
pick fresh x for L.
|
||||
apply type_open_lc_core with
|
||||
(i := 0) (σ1 := (ty_fvar x))
|
||||
(j := S k) (σ2 := σ).
|
||||
trivial.
|
||||
apply eq_sym, H0, Fr.
|
||||
trivial.
|
||||
apply eq_sym, H0, Fr.
|
||||
|
||||
- simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
|
||||
- simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
|
||||
- simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
|
||||
- simpl. intro. rewrite IHtype_lc1. rewrite IHtype_lc2. reflexivity.
|
||||
(* rest *)
|
||||
all: rewrite IHtype_lc1; rewrite IHtype_lc2; reflexivity.
|
||||
Qed.
|
||||
|
||||
Lemma type_subst_open_rec : forall τ σ1 σ2 x k,
|
||||
|
||||
(*
|
||||
* type substitution distributes over opening
|
||||
*)
|
||||
Lemma type_subst_open : forall τ σ1 σ2 x k,
|
||||
type_lc σ2 ->
|
||||
|
||||
[x ~> σ2] ({k ~> σ1} τ)
|
||||
[x ~tt~> σ2] ({k ~tt~> σ1} τ)
|
||||
=
|
||||
{k ~> [x ~> σ2] σ1} ([x ~> σ2] τ).
|
||||
{k ~tt~> [x ~tt~> σ2] σ1} ([x ~tt~> σ2] τ).
|
||||
Proof.
|
||||
induction τ;
|
||||
intros; simpl; f_equal; auto.
|
||||
|
@ -186,7 +172,7 @@ Proof.
|
|||
(* free var *)
|
||||
- destruct (x == a).
|
||||
subst.
|
||||
apply eq_sym, type_open_rec_lc.
|
||||
apply eq_sym, type_open_lc.
|
||||
assumption.
|
||||
trivial.
|
||||
|
||||
|
|
|
@ -152,8 +152,8 @@ Fixpoint type_open_rec (k:nat) (σ:type_DeBruijn) (τ:type_DeBruijn) {struct τ}
|
|||
| ty_ladder τ1 τ2 => ty_ladder (type_open_rec k σ τ1) (type_open_rec k σ τ2)
|
||||
end.
|
||||
|
||||
Notation "'[' z '~>' u ']' e" := (subst_type z u e) (at level 68).
|
||||
Notation "'{' k '~>' σ '}' τ" := (type_open_rec k σ τ) (at level 67).
|
||||
Notation "'[' z '~tt~>' u ']' e" := (subst_type z u e) (at level 68).
|
||||
Notation "'{' k '~tt~>' σ '}' τ" := (type_open_rec k σ τ) (at level 67).
|
||||
Definition type_open σ τ := type_open_rec 0 σ τ.
|
||||
|
||||
(* is the type locally closed ? *)
|
||||
|
@ -188,33 +188,33 @@ Fixpoint expr_fv (e : expr_DeBruijn) {struct e} : atoms :=
|
|||
end.
|
||||
|
||||
(* substitute free variable x with expression s in t *)
|
||||
Fixpoint ex_subst (x:atom) (s:expr_DeBruijn) (t:expr_DeBruijn) {struct t} : expr_DeBruijn :=
|
||||
Fixpoint expr_subst (x:atom) (s:expr_DeBruijn) (t:expr_DeBruijn) {struct t} : expr_DeBruijn :=
|
||||
match t with
|
||||
| ex_fvar n => if x == n then s else t
|
||||
| ex_bvar y => ex_bvar y
|
||||
| ex_ty_abs t' => ex_ty_abs (ex_subst x s t')
|
||||
| ex_ty_app t' σ => ex_ty_app (ex_subst x s t') σ
|
||||
| ex_morph σ t' => ex_morph σ (ex_subst x s t')
|
||||
| ex_abs σ t' => ex_abs σ (ex_subst x s t')
|
||||
| ex_app t1 t2 => ex_app (ex_subst x s t1) (ex_subst x s t2)
|
||||
| ex_let t1 t2 => ex_let (ex_subst x s t1) (ex_subst x s t2)
|
||||
| ex_ascend τ t' => ex_ascend τ (ex_subst x s t')
|
||||
| ex_descend τ t' => ex_descend τ (ex_subst x s t')
|
||||
| ex_ty_abs t' => ex_ty_abs (expr_subst x s t')
|
||||
| ex_ty_app t' σ => ex_ty_app (expr_subst x s t') σ
|
||||
| ex_morph σ t' => ex_morph σ (expr_subst x s t')
|
||||
| ex_abs σ t' => ex_abs σ (expr_subst x s t')
|
||||
| ex_app t1 t2 => ex_app (expr_subst x s t1) (expr_subst x s t2)
|
||||
| ex_let t1 t2 => ex_let (expr_subst x s t1) (expr_subst x s t2)
|
||||
| ex_ascend τ t' => ex_ascend τ (expr_subst x s t')
|
||||
| ex_descend τ t' => ex_descend τ (expr_subst x s t')
|
||||
end.
|
||||
|
||||
(* substitute free type-variable α with type τ in e *)
|
||||
Fixpoint ex_subst_type (α:atom) (τ:type_DeBruijn) (e:expr_DeBruijn) {struct e} : expr_DeBruijn :=
|
||||
Fixpoint expr_subst_type (α:atom) (τ:type_DeBruijn) (e:expr_DeBruijn) {struct e} : expr_DeBruijn :=
|
||||
match e with
|
||||
| ex_fvar n => ex_fvar n
|
||||
| ex_bvar y => ex_bvar y
|
||||
| ex_ty_abs e' => ex_ty_abs (ex_subst_type α τ e')
|
||||
| ex_ty_app e' σ => ex_ty_app (ex_subst_type α τ e') (subst_type α τ σ)
|
||||
| ex_morph σ e' => ex_morph (subst_type α τ σ) (ex_subst_type α τ e')
|
||||
| ex_abs σ e' => ex_abs (subst_type α τ σ) (ex_subst_type α τ e')
|
||||
| ex_app e1 e2 => ex_app (ex_subst_type α τ e1) (ex_subst_type α τ e2)
|
||||
| ex_let e1 e2 => ex_let (ex_subst_type α τ e1) (ex_subst_type α τ e2)
|
||||
| ex_ascend σ e' => ex_ascend (subst_type α τ σ) (ex_subst_type α τ e')
|
||||
| ex_descend σ e' => ex_descend (subst_type α τ σ) (ex_subst_type α τ e')
|
||||
| ex_ty_abs e' => ex_ty_abs (expr_subst_type α τ e')
|
||||
| ex_ty_app e' σ => ex_ty_app (expr_subst_type α τ e') (subst_type α τ σ)
|
||||
| ex_morph σ e' => ex_morph (subst_type α τ σ) (expr_subst_type α τ e')
|
||||
| ex_abs σ e' => ex_abs (subst_type α τ σ) (expr_subst_type α τ e')
|
||||
| ex_app e1 e2 => ex_app (expr_subst_type α τ e1) (expr_subst_type α τ e2)
|
||||
| ex_let e1 e2 => ex_let (expr_subst_type α τ e1) (expr_subst_type α τ e2)
|
||||
| ex_ascend σ e' => ex_ascend (subst_type α τ σ) (expr_subst_type α τ e')
|
||||
| ex_descend σ e' => ex_descend (subst_type α τ σ) (expr_subst_type α τ e')
|
||||
end.
|
||||
|
||||
(* replace a free variable with a new (dangling) bound variable *)
|
||||
|
@ -247,10 +247,6 @@ Fixpoint expr_open_rec (k:nat) (t:expr_DeBruijn) (e:expr_DeBruijn) {struct e} :
|
|||
| ex_descend σ e' => ex_descend σ (expr_open_rec k t e')
|
||||
end.
|
||||
|
||||
Definition expr_open t e := expr_open_rec 0 t e.
|
||||
|
||||
|
||||
|
||||
(* replace (dangling) index with another expression *)
|
||||
Fixpoint expr_open_type_rec (k:nat) (τ:type_DeBruijn) (e:expr_DeBruijn) {struct e} : expr_DeBruijn :=
|
||||
match e with
|
||||
|
@ -266,6 +262,12 @@ Fixpoint expr_open_type_rec (k:nat) (τ:type_DeBruijn) (e:expr_DeBruijn) {struct
|
|||
| ex_descend σ e' => ex_descend σ (expr_open_type_rec k τ e')
|
||||
end.
|
||||
|
||||
Notation "'[' z '~ee~>' u ']' e" := (expr_subst z u e) (at level 68).
|
||||
Notation "'[' z '~et~>' u ']' e" := (expr_subst_type z u e) (at level 68).
|
||||
Notation "'{' k '~ee~>' t '}' e" := (expr_open_rec k t e) (at level 67).
|
||||
Notation "'{' k '~et~>' τ '}' e" := (expr_open_type_rec k τ e) (at level 67).
|
||||
|
||||
Definition expr_open t e := expr_open_rec 0 t e.
|
||||
Definition expr_open_type τ e := expr_open_type_rec 0 τ e.
|
||||
|
||||
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue