Library LambdaES_Defs
Grammar of pre-terms.
Inductive pterm : Set :=
| pterm_bvar : nat -> pterm
| pterm_fvar : var -> pterm
| pterm_abs : pterm -> pterm
| pterm_app : pterm -> pterm -> pterm
| pterm_sub : pterm -> pterm -> pterm .
Notation "t [ u ]" := (pterm_sub t u) (at level 70).
| pterm_bvar : nat -> pterm
| pterm_fvar : var -> pterm
| pterm_abs : pterm -> pterm
| pterm_app : pterm -> pterm -> pterm
| pterm_sub : pterm -> pterm -> pterm .
Notation "t [ u ]" := (pterm_sub t u) (at level 70).
Opening up abstractions and substitutions
Fixpoint open_rec (k : nat) (u : pterm) (t : pterm) {struct t} : pterm :=
match t with
| pterm_bvar i => if k === i then u else (pterm_bvar i)
| pterm_fvar x => pterm_fvar x
| pterm_abs t1 => pterm_abs (open_rec (S k) u t1)
| pterm_app t1 t2 => pterm_app (open_rec k u t1) (open_rec k u t2)
| pterm_sub t1 t2 => pterm_sub (open_rec (S k) u t1) (open_rec k u t2)
end.
Definition open t u := open_rec 0 u t.
Notation "{ k ~> u } t" := (open_rec k u t) (at level 67).
Notation "t ^^ u" := (open t u) (at level 67).
Notation "t ^ x" := (open t (pterm_fvar x)).
match t with
| pterm_bvar i => if k === i then u else (pterm_bvar i)
| pterm_fvar x => pterm_fvar x
| pterm_abs t1 => pterm_abs (open_rec (S k) u t1)
| pterm_app t1 t2 => pterm_app (open_rec k u t1) (open_rec k u t2)
| pterm_sub t1 t2 => pterm_sub (open_rec (S k) u t1) (open_rec k u t2)
end.
Definition open t u := open_rec 0 u t.
Notation "{ k ~> u } t" := (open_rec k u t) (at level 67).
Notation "t ^^ u" := (open t u) (at level 67).
Notation "t ^ x" := (open t (pterm_fvar x)).
Variable closing
Fixpoint close_rec (k : nat) (x : var) (t : pterm) {struct t} : pterm :=
match t with
| pterm_bvar i => pterm_bvar i
| pterm_fvar x' => if x' == x then (pterm_bvar k) else pterm_fvar x'
| pterm_abs t1 => pterm_abs (close_rec (S k) x t1)
| pterm_app t1 t2 => pterm_app (close_rec k x t1) (close_rec k x t2)
| pterm_sub t1 t2 => pterm_sub (close_rec (S k) x t1) (close_rec k x t2)
end.
Definition close t x := close_rec 0 x t.
Fixpoint fv (t : pterm) {struct t} : vars :=
match t with
| pterm_bvar i => {}
| pterm_fvar x => {{x}}
| pterm_abs t1 => (fv t1)
| pterm_app t1 t2 => (fv t1) \u (fv t2)
| pterm_sub t1 t2 => (fv t1) \u (fv t2)
end.
match t with
| pterm_bvar i => pterm_bvar i
| pterm_fvar x' => if x' == x then (pterm_bvar k) else pterm_fvar x'
| pterm_abs t1 => pterm_abs (close_rec (S k) x t1)
| pterm_app t1 t2 => pterm_app (close_rec k x t1) (close_rec k x t2)
| pterm_sub t1 t2 => pterm_sub (close_rec (S k) x t1) (close_rec k x t2)
end.
Definition close t x := close_rec 0 x t.
Fixpoint fv (t : pterm) {struct t} : vars :=
match t with
| pterm_bvar i => {}
| pterm_fvar x => {{x}}
| pterm_abs t1 => (fv t1)
| pterm_app t1 t2 => (fv t1) \u (fv t2)
| pterm_sub t1 t2 => (fv t1) \u (fv t2)
end.
Terms are locally-closed pre-terms
Inductive term : pterm -> Prop :=
| term_var : forall x,
term (pterm_fvar x)
| term_abs : forall L t1,
(forall x, x \notin L -> term (t1 ^ x)) ->
term (pterm_abs t1)
| term_app : forall t1 t2,
term t1 ->
term t2 ->
term (pterm_app t1 t2)
| term_sub : forall L t1 t2,
(forall x, x \notin L -> term (t1 ^ x)) ->
term t2 ->
term (pterm_sub t1 t2).
| term_var : forall x,
term (pterm_fvar x)
| term_abs : forall L t1,
(forall x, x \notin L -> term (t1 ^ x)) ->
term (pterm_abs t1)
| term_app : forall t1 t2,
term t1 ->
term t2 ->
term (pterm_app t1 t2)
| term_sub : forall L t1 t2,
(forall x, x \notin L -> term (t1 ^ x)) ->
term t2 ->
term (pterm_sub t1 t2).