2024-09-20 19:41:27 +02:00
|
|
|
|
Require Import Atom.
|
|
|
|
|
Require Import Metatheory.
|
|
|
|
|
Require Import FSetNotin.
|
2024-09-21 13:00:57 +02:00
|
|
|
|
Require Import debruijn.
|
2024-09-20 19:41:27 +02:00
|
|
|
|
|
|
|
|
|
(*
|
|
|
|
|
* Substitution has no effect if the variable is not free
|
|
|
|
|
*)
|
|
|
|
|
Lemma type_subst_fresh : forall (x : atom) (τ:type_DeBruijn) (σ:type_DeBruijn),
|
|
|
|
|
x `notin` (type_fv τ) ->
|
2024-09-21 01:43:25 +02:00
|
|
|
|
([ x ~tt~> σ ] τ) = τ
|
2024-09-20 19:41:27 +02:00
|
|
|
|
.
|
|
|
|
|
Proof.
|
|
|
|
|
intros.
|
|
|
|
|
induction τ.
|
|
|
|
|
|
|
|
|
|
- reflexivity.
|
|
|
|
|
|
|
|
|
|
- unfold type_fv in H.
|
|
|
|
|
apply AtomSetNotin.elim_notin_singleton in H.
|
|
|
|
|
simpl.
|
|
|
|
|
case_eq (x == a).
|
|
|
|
|
congruence.
|
|
|
|
|
reflexivity.
|
|
|
|
|
|
|
|
|
|
- reflexivity.
|
|
|
|
|
|
|
|
|
|
- simpl. rewrite IHτ.
|
|
|
|
|
reflexivity.
|
|
|
|
|
apply H.
|
|
|
|
|
|
|
|
|
|
- simpl; rewrite IHτ1, IHτ2.
|
|
|
|
|
reflexivity.
|
|
|
|
|
simpl type_fv in H; fsetdec.
|
|
|
|
|
simpl type_fv in H; fsetdec.
|
|
|
|
|
|
|
|
|
|
- simpl. rewrite IHτ1, IHτ2.
|
|
|
|
|
reflexivity.
|
|
|
|
|
simpl type_fv in H; fsetdec.
|
|
|
|
|
simpl type_fv in H; fsetdec.
|
|
|
|
|
|
|
|
|
|
- simpl. rewrite IHτ1, IHτ2.
|
|
|
|
|
reflexivity.
|
|
|
|
|
simpl type_fv in H; fsetdec.
|
|
|
|
|
simpl type_fv in H; fsetdec.
|
|
|
|
|
|
|
|
|
|
- simpl. rewrite IHτ1, IHτ2.
|
|
|
|
|
reflexivity.
|
|
|
|
|
simpl type_fv in H; fsetdec.
|
|
|
|
|
simpl type_fv in H; fsetdec.
|
2024-09-21 01:43:25 +02:00
|
|
|
|
|
2024-09-20 19:41:27 +02:00
|
|
|
|
Qed.
|
|
|
|
|
|
2024-09-21 01:43:25 +02:00
|
|
|
|
(*
|
|
|
|
|
* 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.
|
2024-09-20 19:41:27 +02:00
|
|
|
|
|
|
|
|
|
|
2024-09-21 01:43:25 +02:00
|
|
|
|
Lemma type_open_lc_core : forall (τ:type_DeBruijn) i (σ1:type_DeBruijn) j (σ2:type_DeBruijn),
|
2024-09-20 19:41:27 +02:00
|
|
|
|
i <> j ->
|
2024-09-21 01:43:25 +02:00
|
|
|
|
{i ~tt~> σ1} τ = {j ~tt~> σ2} ({i ~tt~> σ1} τ) ->
|
|
|
|
|
({j ~tt~> σ2} τ) = τ
|
2024-09-21 01:05:28 +02:00
|
|
|
|
.
|
2024-09-20 19:41:27 +02:00
|
|
|
|
Proof with eauto*.
|
|
|
|
|
induction τ;
|
2024-09-21 01:05:28 +02:00
|
|
|
|
intros i σ1 j σ2 Neq H;
|
|
|
|
|
simpl in *;
|
|
|
|
|
inversion H;
|
|
|
|
|
f_equal; eauto.
|
2024-09-20 19:41:27 +02:00
|
|
|
|
|
|
|
|
|
(* bound var *)
|
|
|
|
|
- simpl in *.
|
|
|
|
|
destruct (j === n).
|
|
|
|
|
destruct (i === n).
|
|
|
|
|
3:reflexivity.
|
|
|
|
|
|
|
|
|
|
rewrite e,e0 in Neq.
|
|
|
|
|
contradiction Neq.
|
|
|
|
|
reflexivity.
|
|
|
|
|
|
|
|
|
|
rewrite H,e.
|
|
|
|
|
simpl.
|
|
|
|
|
destruct (n===n).
|
|
|
|
|
reflexivity.
|
|
|
|
|
contradict n1.
|
|
|
|
|
reflexivity.
|
|
|
|
|
Qed.
|
|
|
|
|
|
|
|
|
|
|
2024-09-21 01:05:28 +02:00
|
|
|
|
(*
|
|
|
|
|
* opening is idempotent on locally closed types
|
|
|
|
|
*)
|
|
|
|
|
Lemma type_open_lc : forall k σ τ,
|
2024-09-20 19:41:27 +02:00
|
|
|
|
type_lc τ ->
|
2024-09-21 01:43:25 +02:00
|
|
|
|
({ k ~tt~> σ } τ) = τ
|
2024-09-20 19:41:27 +02:00
|
|
|
|
.
|
|
|
|
|
Proof.
|
|
|
|
|
intros.
|
|
|
|
|
generalize dependent k.
|
2024-09-21 01:05:28 +02:00
|
|
|
|
induction H; eauto; simpl in *; intro k.
|
2024-09-20 19:41:27 +02:00
|
|
|
|
|
|
|
|
|
(* univ *)
|
2024-09-21 01:05:28 +02:00
|
|
|
|
f_equal.
|
|
|
|
|
unfold type_open in *.
|
|
|
|
|
pick fresh x for L.
|
|
|
|
|
apply type_open_lc_core with
|
2024-09-20 19:41:27 +02:00
|
|
|
|
(i := 0) (σ1 := (ty_fvar x))
|
|
|
|
|
(j := S k) (σ2 := σ).
|
2024-09-21 01:05:28 +02:00
|
|
|
|
trivial.
|
|
|
|
|
apply eq_sym, H0, Fr.
|
2024-09-20 19:41:27 +02:00
|
|
|
|
|
2024-09-21 01:05:28 +02:00
|
|
|
|
(* rest *)
|
|
|
|
|
all: rewrite IHtype_lc1; rewrite IHtype_lc2; reflexivity.
|
2024-09-20 19:41:27 +02:00
|
|
|
|
Qed.
|
|
|
|
|
|
2024-09-21 01:05:28 +02:00
|
|
|
|
|
|
|
|
|
(*
|
|
|
|
|
* type substitution distributes over opening
|
|
|
|
|
*)
|
|
|
|
|
Lemma type_subst_open : forall τ σ1 σ2 x k,
|
2024-09-20 19:41:27 +02:00
|
|
|
|
type_lc σ2 ->
|
|
|
|
|
|
2024-09-21 01:43:25 +02:00
|
|
|
|
[x ~tt~> σ2] ({k ~tt~> σ1} τ)
|
2024-09-20 19:41:27 +02:00
|
|
|
|
=
|
2024-09-21 01:43:25 +02:00
|
|
|
|
{k ~tt~> [x ~tt~> σ2] σ1} ([x ~tt~> σ2] τ).
|
2024-09-20 19:41:27 +02:00
|
|
|
|
Proof.
|
|
|
|
|
induction τ;
|
|
|
|
|
intros; simpl; f_equal; auto.
|
|
|
|
|
|
|
|
|
|
(* free var *)
|
|
|
|
|
- destruct (x == a).
|
|
|
|
|
subst.
|
2024-09-21 01:05:28 +02:00
|
|
|
|
apply eq_sym, type_open_lc.
|
2024-09-20 19:41:27 +02:00
|
|
|
|
assumption.
|
|
|
|
|
trivial.
|
|
|
|
|
|
|
|
|
|
(* bound var *)
|
|
|
|
|
- destruct (k === n).
|
|
|
|
|
reflexivity.
|
|
|
|
|
trivial.
|
|
|
|
|
Qed.
|