Library LambdaES_Defs

Set Implicit Arguments.
Require Import Metatheory.

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).

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)).

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.

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).