Compare commits
3 commits
cafa9808aa
...
c5a4626551
Author | SHA1 | Date | |
---|---|---|---|
c5a4626551 | |||
d22ae9a682 | |||
7a6ed28c0a |
4 changed files with 436 additions and 198 deletions
|
@ -5,8 +5,12 @@ FiniteSets.v
|
|||
FSetNotin.v
|
||||
Atom.v
|
||||
Metatheory.v
|
||||
terms.v
|
||||
|
||||
terms_debruijn.v
|
||||
equiv_debruijn.v
|
||||
subst_lemmas_debruijn.v
|
||||
|
||||
terms.v
|
||||
equiv.v
|
||||
subst.v
|
||||
subtype.v
|
||||
|
|
180
coq/equiv_debruijn.v
Normal file
180
coq/equiv_debruijn.v
Normal file
|
@ -0,0 +1,180 @@
|
|||
Require Import terms_debruijn.
|
||||
|
||||
Open Scope ladder_type_scope.
|
||||
Open Scope ladder_expr_scope.
|
||||
|
||||
Reserved Notation "S '-->distribute-ladder' T" (at level 40).
|
||||
|
||||
Inductive type_distribute_ladder : type_DeBruijn -> type_DeBruijn -> Prop :=
|
||||
| L_DistributeOverSpec1 : forall x x' y,
|
||||
[< <x~x' y> >]
|
||||
-->distribute-ladder
|
||||
[< <x y>~<x' y> >]
|
||||
|
||||
| L_DistributeOverSpec2 : forall x y y',
|
||||
[< <x y~y'> >]
|
||||
-->distribute-ladder
|
||||
[< <x y>~<x y'> >]
|
||||
|
||||
| L_DistributeOverFun1 : forall x x' y,
|
||||
[< (x~x' -> y) >]
|
||||
-->distribute-ladder
|
||||
[< (x -> y) ~ (x' -> y) >]
|
||||
|
||||
| L_DistributeOverFun2 : forall x y y',
|
||||
[< (x -> y~y') >]
|
||||
-->distribute-ladder
|
||||
[< (x -> y) ~ (x -> y') >]
|
||||
|
||||
| L_DistributeOverMorph1 : forall x x' y,
|
||||
[< (x~x' ->morph y) >]
|
||||
-->distribute-ladder
|
||||
[< (x ->morph y) ~ (x' ->morph y) >]
|
||||
|
||||
| L_DistributeOverMorph2 : forall x y y',
|
||||
[< x ->morph y~y' >]
|
||||
-->distribute-ladder
|
||||
[< (x ->morph y) ~ (x ->morph y') >]
|
||||
|
||||
where "S '-->distribute-ladder' T" := (type_distribute_ladder S T).
|
||||
|
||||
|
||||
Reserved Notation "S '-->condense-ladder' T" (at level 40).
|
||||
Inductive type_condense_ladder : type_DeBruijn -> type_DeBruijn -> Prop :=
|
||||
| L_CondenseOverSpec1 : forall x x' y,
|
||||
[< <x y>~<x' y> >]
|
||||
-->condense-ladder
|
||||
[< <x~x' y> >]
|
||||
|
||||
| L_CondenseOverSpec2 : forall x y y',
|
||||
[< <x y>~<x y'> >]
|
||||
-->condense-ladder
|
||||
[< <x y~y'> >]
|
||||
|
||||
| L_CondenseOverFun1 : forall x x' y,
|
||||
[< (x -> y) ~ (x' -> y) >]
|
||||
-->condense-ladder
|
||||
[< (x~x') -> y >]
|
||||
|
||||
| L_CondenseOverFun2 : forall x y y',
|
||||
[< (x -> y) ~ (x -> y') >]
|
||||
-->condense-ladder
|
||||
[< (x -> y~y') >]
|
||||
|
||||
| L_CondenseOverMorph1 : forall x x' y,
|
||||
[< (x ->morph y) ~ (x' ->morph y) >]
|
||||
-->condense-ladder
|
||||
[< (x~x' ->morph y) >]
|
||||
|
||||
| L_CondenseOverMorph2 : forall x y y',
|
||||
[< (x ->morph y) ~ (x ->morph y') >]
|
||||
-->condense-ladder
|
||||
[< (x ->morph y~y') >]
|
||||
|
||||
where "S '-->condense-ladder' T" := (type_condense_ladder S T).
|
||||
|
||||
Create HintDb type_eq_hints.
|
||||
|
||||
Hint Constructors type_distribute_ladder : type_eq_hints.
|
||||
Hint Constructors type_condense_ladder : type_eq_hints.
|
||||
|
||||
(** Inversion Lemma:
|
||||
`-->distribute-ladder` is the inverse of `-->condense-ladder
|
||||
*)
|
||||
Lemma distribute_inverse :
|
||||
forall x y,
|
||||
x -->distribute-ladder y ->
|
||||
y -->condense-ladder x.
|
||||
Proof.
|
||||
intros.
|
||||
destruct H.
|
||||
all: auto with type_eq_hints.
|
||||
Qed.
|
||||
|
||||
(** Inversion Lemma:
|
||||
`-->condense-ladder` is the inverse of `-->distribute-ladder`
|
||||
*)
|
||||
Lemma condense_inverse :
|
||||
forall x y,
|
||||
x -->condense-ladder y ->
|
||||
y -->distribute-ladder x.
|
||||
Proof.
|
||||
intros.
|
||||
destruct H.
|
||||
all: auto with type_eq_hints.
|
||||
Qed.
|
||||
|
||||
|
||||
(** Define the equivalence relation as reflexive, transitive hull. $\label{coq:type-equiv}$ *)
|
||||
|
||||
Reserved Notation " S '===' T " (at level 40).
|
||||
Inductive type_eq : type_DeBruijn -> type_DeBruijn -> Prop :=
|
||||
| TEq_Refl : forall x,
|
||||
x === x
|
||||
|
||||
| TEq_Trans : forall x y z,
|
||||
x === y ->
|
||||
y === z ->
|
||||
x === z
|
||||
|
||||
| TEq_SubFun : forall x x' y y',
|
||||
x === x' ->
|
||||
y === y' ->
|
||||
[< x -> y >] === [< x' -> y' >]
|
||||
|
||||
| TEq_SubMorph : forall x x' y y',
|
||||
x === x' ->
|
||||
y === y' ->
|
||||
[< x ->morph y >] === [< x' ->morph y' >]
|
||||
|
||||
| TEq_LadderAssocLR : forall x y z,
|
||||
[< (x~y)~z >]
|
||||
===
|
||||
[< x~(y~z) >]
|
||||
|
||||
| TEq_LadderAssocRL : forall x y z,
|
||||
[< x~(y~z) >]
|
||||
===
|
||||
[< (x~y)~z >]
|
||||
|
||||
| TEq_Distribute : forall x y,
|
||||
x -->distribute-ladder y ->
|
||||
x === y
|
||||
|
||||
| TEq_Condense : forall x y,
|
||||
x -->condense-ladder y ->
|
||||
x === y
|
||||
|
||||
where "S '===' T" := (type_eq S T).
|
||||
|
||||
|
||||
|
||||
(** Symmetry of === *)
|
||||
Lemma TEq_Symm :
|
||||
forall x y,
|
||||
(x === y) -> (y === x).
|
||||
Proof.
|
||||
intros.
|
||||
induction H.
|
||||
|
||||
apply TEq_Refl.
|
||||
|
||||
apply TEq_Trans with (y:=y).
|
||||
apply IHtype_eq2.
|
||||
apply IHtype_eq1.
|
||||
|
||||
apply TEq_SubFun.
|
||||
auto. auto.
|
||||
apply TEq_SubMorph.
|
||||
auto. auto.
|
||||
apply TEq_LadderAssocRL.
|
||||
apply TEq_LadderAssocLR.
|
||||
|
||||
apply TEq_Condense.
|
||||
apply distribute_inverse.
|
||||
apply H.
|
||||
|
||||
apply TEq_Distribute.
|
||||
apply condense_inverse.
|
||||
apply H.
|
||||
Qed.
|
197
coq/subst_lemmas_debruijn.v
Normal file
197
coq/subst_lemmas_debruijn.v
Normal 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.
|
|
@ -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
|
||||
|
@ -28,11 +27,64 @@ Inductive expr_DeBruijn : Type :=
|
|||
| ex_abs : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
|
||||
| ex_morph : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
|
||||
| ex_app : expr_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
|
||||
| ex_let : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
|
||||
| ex_let : expr_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
|
||||
| ex_ascend : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
|
||||
| ex_descend : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
|
||||
.
|
||||
|
||||
Declare Scope ladder_type_scope.
|
||||
Declare Scope ladder_expr_scope.
|
||||
Declare Custom Entry ladder_type.
|
||||
Declare Custom Entry ladder_expr.
|
||||
|
||||
Notation "[< t >]" := t
|
||||
(t custom ladder_type at level 99) : ladder_type_scope.
|
||||
Notation "t" := t
|
||||
(in custom ladder_type at level 0, t ident) : ladder_type_scope.
|
||||
Notation "'∀' t" := (ty_univ t)
|
||||
(t custom ladder_type at level 80, in custom ladder_type at level 80).
|
||||
Notation "'<' σ τ '>'" := (ty_spec σ τ)
|
||||
(in custom ladder_type at level 80, left associativity) : ladder_type_scope.
|
||||
Notation "'[' τ ']'" := (ty_spec (ty_id "Seq") τ)
|
||||
(in custom ladder_type at level 70) : ladder_type_scope.
|
||||
Notation "'(' τ ')'" := τ
|
||||
(in custom ladder_type at level 5) : ladder_type_scope.
|
||||
Notation "σ '->' τ" := (ty_func σ τ)
|
||||
(in custom ladder_type at level 75, right associativity) : ladder_type_scope.
|
||||
Notation "σ '->morph' τ" := (ty_morph σ τ)
|
||||
(in custom ladder_type at level 75, right associativity, τ at level 80) : ladder_type_scope.
|
||||
Notation "σ '~' τ" := (ty_ladder σ τ)
|
||||
(in custom ladder_type at level 20, right associativity) : ladder_type_scope.
|
||||
Notation "'$' x" := (ty_id x%string)
|
||||
(in custom ladder_type at level 10, x constr) : ladder_type_scope.
|
||||
Notation "'%' x" := (ty_fvar x)
|
||||
(in custom ladder_type at level 10, x constr) : ladder_type_scope.
|
||||
|
||||
Notation "[{ e }]" := e
|
||||
(e custom ladder_expr at level 99) : ladder_expr_scope.
|
||||
Notation "e" := e
|
||||
(in custom ladder_expr at level 0, e ident) : ladder_expr_scope.
|
||||
Notation "'%' x" := (ex_fvar x)
|
||||
(in custom ladder_expr at level 10, x constr) : ladder_expr_scope.
|
||||
Notation "'Λ' e" := (ex_ty_abs e)
|
||||
(in custom ladder_expr at level 10, e custom ladder_expr at level 80, right associativity) : ladder_expr_scope.
|
||||
Notation "'λ' τ '↦' e" := (ex_abs τ e)
|
||||
(in custom ladder_expr at level 70, τ custom ladder_type at level 90, e custom ladder_expr at level 80, right associativity) :ladder_expr_scope.
|
||||
Notation "'λ' τ '↦morph' e" := (ex_morph τ e)
|
||||
(in custom ladder_expr at level 70, τ custom ladder_type at level 90, e custom ladder_expr at level 80, right associativity) :ladder_expr_scope.
|
||||
Notation "'let' e 'in' t" := (ex_let e t)
|
||||
(in custom ladder_expr at level 60, e custom ladder_expr at level 80, t custom ladder_expr at level 80, right associativity) : ladder_expr_scope.
|
||||
Notation "e 'as' τ" := (ex_ascend τ e)
|
||||
(in custom ladder_expr at level 30, e custom ladder_expr, τ custom ladder_type at level 99) : ladder_expr_scope.
|
||||
Notation "e 'des' τ" := (ex_descend τ e)
|
||||
(in custom ladder_expr at level 30, e custom ladder_expr, τ custom ladder_type at level 99) : ladder_expr_scope.
|
||||
Notation "e1 e2" := (ex_app e1 e2)
|
||||
(in custom ladder_expr at level 90, e2 custom ladder_expr at next level) : ladder_expr_scope.
|
||||
Notation "e '#' τ" := (ex_ty_app e τ)
|
||||
(in custom ladder_expr at level 80, τ custom ladder_type at level 101, left associativity) : ladder_expr_scope.
|
||||
Notation "'(' e ')'" := e
|
||||
(in custom ladder_expr, e custom ladder_expr at next level, left associativity) : ladder_expr_scope.
|
||||
|
||||
(* get the list of all free variables in a type term *)
|
||||
Fixpoint type_fv (τ : type_DeBruijn) {struct τ} : atoms :=
|
||||
match τ with
|
||||
|
@ -130,198 +182,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.
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue