Library LC_eval

Require Export LC.
Open Scope LC_scope.


Definition evalBeta p q:=
  match p,q with
    |clos (lam s) sigma,clos (lam t) tauSome (clos s (clos (lam t) tau::sigma))

Fixpoint evalLC k (p:term) : option term:=
  match k with
      S k
      match p with
      | app p q
        match evalBeta p q with
          match (evalLC k p),(evalLC k q) with
            Some p', Some q'evalLC k (p' q')
          | _ ,_None
        | Some p'evalLC k p'
      | clos ( s t) AevalLC k ((clos s A) (clos t A))
      | clos (L.var x) AevalLC k (nth x A (var x))
      | uSome u
    | 0 ⇒ None

Functional Scheme evalLC_ind := Induction for evalLC Sort Prop.


Lemma evalBeta_sound p q r: evalBeta p q = Some rp q >[]> rvalue pvalue q.

Lemma evalBeta_complete s t: evalBeta s t = None → ¬ (value svalue t).

Lemma eval_sound p k q : evalLC k p = Some qp >[]* q.


Lemma eval_app (p q r:term) k: (p q) >[]^k rvalue r
                         l1 l2 l' p' q', p >[]^l1 p'q >[]^l2 q'
                                            value p'value q'
                                            (p' q') >[]^l' rk=l1+l2+l'.

Lemma eval_complete p k q: p >[]^k qvalue q l, l', l'levalLC l' p = Some q.

Benchmark term

Fixpoint b n :=
  match n with
    0 ⇒ I
  | S nlam ((b n) (L.var 0))