move subst/opening lemmas to separate file

This commit is contained in:
Michael Sippel 2024-09-20 19:41:27 +02:00
parent b97cb84caf
commit c4f4e56fee
3 changed files with 201 additions and 197 deletions

View file

@ -5,8 +5,11 @@ FiniteSets.v
FSetNotin.v
Atom.v
Metatheory.v
terms.v
terms_debruijn.v
subst_lemmas_debruijn.v
terms.v
equiv.v
subst.v
subtype.v

197
coq/subst_lemmas_debruijn.v Normal file
View file

@ -0,0 +1,197 @@
Require Import terms_debruijn.
Require Import Atom.
Require Import Metatheory.
Require Import FSetNotin.
(*
* 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 τ) ->
([ x ~> σ ] τ) = τ
.
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.
Qed.
Lemma open_rec_lc_core : forall τ i σ1 j σ2,
i <> j ->
{i ~> σ1} τ = {j ~> σ2} ({i ~> σ1} τ) ->
({j ~> σ2} τ) = τ.
Proof with eauto*.
induction τ;
intros i σ1 j σ2 Neq H.
(* id *)
- reflexivity.
(* free var *)
- reflexivity.
(* 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.
(* 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 σ τ,
type_lc τ ->
({ k ~> σ } τ) = τ
.
Proof.
intros.
generalize dependent k.
induction H.
(* id *)
- auto.
(* free var *)
- auto.
(* univ *)
- simpl.
intro k.
f_equal.
unfold type_open in *.
pick fresh x for L.
apply open_rec_lc_core with
(i := 0) (σ1 := (ty_fvar x))
(j := S k) (σ2 := σ).
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.
Qed.
Lemma type_subst_open_rec : forall τ σ1 σ2 x k,
type_lc σ2 ->
[x ~> σ2] ({k ~> σ1} τ)
=
{k ~> [x ~> σ2] σ1} ([x ~> σ2] τ).
Proof.
induction τ;
intros; simpl; f_equal; auto.
(* free var *)
- destruct (x == a).
subst.
apply eq_sym, type_open_rec_lc.
assumption.
trivial.
(* bound var *)
- destruct (k === n).
reflexivity.
trivial.
Qed.

View file

@ -7,7 +7,6 @@ Local Open Scope nat_scope.
Require Import Atom.
Require Import Metatheory.
Require Import FSetNotin.
Require Import terms.
Inductive type_DeBruijn : Type :=
| ty_id : string -> type_DeBruijn
@ -130,198 +129,3 @@ Fixpoint type_named2debruijn (τ:type_term) {struct τ} : type_DeBruijn :=
Coercion type_named2debruijn : type_term >-> type_DeBruijn.
*)
(*
* Substitution has no effect if the variable is not free
*)
Lemma subst_fresh_type : forall (x : atom) (τ:type_DeBruijn) (σ:type_DeBruijn),
x `notin` (type_fv τ) ->
([ x ~> σ ] τ) = τ
.
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.
Qed.
Lemma open_rec_lc_core : forall τ i σ1 j σ2,
i <> j ->
{i ~> σ1} τ = {j ~> σ2} ({i ~> σ1} τ) ->
({j ~> σ2} τ) = τ.
Proof with eauto*.
induction τ;
intros i σ1 j σ2 Neq H.
(* id *)
- reflexivity.
(* free var *)
- reflexivity.
(* 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.
(* 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 σ τ,
type_lc τ ->
({ k ~> σ } τ) = τ
.
Proof.
intros.
generalize dependent k.
induction H.
(* id *)
- auto.
(* free var *)
- auto.
(* univ *)
- simpl.
intro k.
f_equal.
unfold type_open in *.
pick fresh x for L.
apply open_rec_lc_core with
(i := 0) (σ1 := (ty_fvar x))
(j := S k) (σ2 := σ).
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.
Qed.
Lemma type_subst_open_rec : forall τ σ1 σ2 x k,
type_lc σ2 ->
[x ~> σ2] ({k ~> σ1} τ)
=
{k ~> [x ~> σ2] σ1} ([x ~> σ2] τ).
Proof.
induction τ;
intros; simpl; f_equal; auto.
(* free var *)
- destruct (x == a).
subst.
apply eq_sym, type_open_rec_lc.
assumption.
trivial.
(* bound var *)
- destruct (k === n).
reflexivity.
trivial.
Qed.