Require Export LC.
Open Scope LC_scope.

Definition evalBeta p q:=
  match p,q with
    |clos (lam s) sigma,clos (lam t) tau ⇒ Some (clos s (clos (lam t) tau::sigma))
    |_,_ ⇒ None
  end.

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

Functional Scheme evalLC_ind := Induction for evalLC Sort Prop.

Lemma evalBeta_sound p q r: evalBeta p q = Some r → p q >[]> r ∧ value p ∧ value q.

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

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

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

Lemma eval_complete p k q: p >[]^k q → value q → ∃ l, ∀ l', l' ≥l → evalLC l' p = Some q.

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