Compare commits

...

3 commits

4 changed files with 436 additions and 198 deletions

View file

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