LambdaCal.v

Require Import ZArith.
Open Scope Z_scope.

Definition var := Z.

Inductive term : Set :=
    | t_var : var -> term
    | t_abs : term -> term 
    | t_app : term -> term -> term.

Fixpoint shift (d c : var) (t : term) : term :=
    match t with 
    | t_var k =>
        if Z.leb c k then t_var (k + d) else t_var k
    | t_abs t' => t_abs shift d (c + 1) t'     
    | t_app f v => t_app (shift d c f) (shift d c v)
    end.

Fixpoint substitute (j : var) (s t : term) : term :=
    match t with 
    | t_var i => if Z.eqb i j then s else t 
    | t_abs t' => t_abs (substitute (j + 1) (shift 1 0 s) t')
    | t_app f v => t_app (substitute j s f) (substitute j s v)
    end.

Notation "[ t | x → s ]" := (substitute x s t)(at level 30).

Inductive val : term -> Prop :=
    | v_abs t : val (t_abs t).

Reserved Notation "t1 ⟶ t2" (at level 80).

Inductive eval : term -> term -> Prop :=
    | e_app1 f f' v : f ⟶ f' -> (t_app f v) ⟶ (t_app f' v)
    | e_app2 f v v' : val f -> v ⟶ v' -> (t_app f v) ⟶ (t_app f v')
    | e_appabs t v : val v -> (t_app (t_abs t) v)  ⟶  (shift (-1) 0 ([t | 0 → shift 1 0 v]))
    where "t1 ⟶ t2" := (eval t1 t2).