improve notation for opening/substitution & add proof for expr_subst_fresh

This commit is contained in:
Michael Sippel 2024-09-21 01:43:25 +02:00
parent 4b76d6a982
commit 3c86dde677
Signed by: senvas
GPG key ID: F96CF119C34B64A6
2 changed files with 80 additions and 32 deletions

View file

@ -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,14 +48,60 @@ 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 type_open_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 τ;
@ -88,7 +134,7 @@ Qed.
*)
Lemma type_open_lc : forall k σ τ,
type_lc τ ->
({ k ~> σ } τ) = τ
({ k ~tt~> σ } τ) = τ
.
Proof.
intros.
@ -116,9 +162,9 @@ Qed.
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.

View file

@ -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.