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.
Proof with try now repeat (auto || congruence || subst || simpl in × || intuition).
  intros eq. destruct p,q; inv eq. destruct s... destruct s,s0... inv H0. repeat constructor...
  destruct s...
Qed.

Lemma evalBeta_complete s t: evalBeta s t = None → ¬ (value s ∧ value t).
Proof.
  intros eq. intros [H1 H2]. inv H1;inv H2;discriminate eq.
Qed.

Lemma eval_sound p k q : evalLC k p = Some q → p >[]* q.
Proof.
  revert q;functional induction (evalLC k p);intros r eq;inv eq;eauto using star.
  -apply evalBeta_sound in e1 as [R _]. eauto using star.
  -apply IHo in e2. apply IHo0 in e3. apply IHo1 in H0. rewrite <- H0. now apply star_step_app_proper.
Qed.

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'.
Proof.
  revert p q r;induction k;intros ? ? ? R n.
  -inv R. inv n.
  -destruct R as (r'&R1&R2). change (it (rcomp step) k eq r' r) with (pow step k r' r) in R2. inv R1.
   +destruct (IHk _ _ _ R2 n) as (?&?&?&?&?&?&?&?&?&?&?). destruct H1. destruct H3.
    repeat eexists. apply (pow_add _ 1). eexists. split. apply (rcomp_1 step). eauto. eauto. eauto. eauto. omega.
   +destruct (IHk _ _ _ R2 n) as (?&?&?&?&?&?&?&?&?&?&?). destruct H1. destruct H3.
    repeat eexists. eauto. apply (pow_add _ 1). eexists. split. apply (rcomp_1 step). eauto. eauto. eauto. omega.
   +eexists 0, 0, (1+k),_,_. repeat split. apply (pow_add _ 1). eexists. split. apply (rcomp_1 step). auto. auto.
Qed.

Lemma eval_complete p k q: p >[]^k q → value q → ∃ l, ∀ l', l' ≥l → evalLC l' p = Some q.
Proof.
  revert p q;apply complete_induction with (x:=k);clear ;intros k IH ? ? R v. destruct k.
  -inv R. inv v. ∃ 1. intros l' ?. destruct l'. omega. reflexivity.
  -destruct p.
   +destruct R as (?&R&_). inv R.
   +apply (pow_add _ 1) in R as [p [S R]]. apply rcomp_1 in S. inv S.
    ×apply IH in R as (k'&eq');[|omega|auto].
     ∃ (1+k');intros l ?. destruct l. omega. simpl. apply eq'. omega.
    ×apply IH in R as (k'&eq');[|omega|auto].
     ∃ (1+k');intros l ?. destruct l. omega. simpl. apply eq'. omega.
   +destruct (eval_app R v) as (l1&l2&l'&?&?&?R1&R2&n1&n2&R'&eq).
    assert (l'>0).
    {destruct l'. inv R'. inv v. omega. }
    destruct (evalBeta p1 p2) eqn:eq''.
    ×apply evalBeta_sound in eq'' as (_&v1&v2).
     apply irred_pow in R1. apply irred_pow in R2. subst l1. subst l2. inv v1. inv v2.
     apply (pow_add _ 1) in R as [p [S R]]. apply rcomp_1 in S. inv S. inv H3. inv H3.
     apply IH in R as [l H'];[|omega|auto].
     ∃ (1+l). intros. destruct l'0. omega. simpl in ×.
     apply H'. omega. inv v2. inversion 1. inv v1. inversion 1.
    ×specialize (evalBeta_complete eq'');intro.
     assert (l1+l2>0).
     {destruct l1;[|omega]. destruct l2;[|omega]. inv R1. inv R2. tauto. }
     apply IH in R1 as (k1&eq1);[|omega|auto].
     apply IH in R2 as (k2&eq2);[|omega|auto].
     apply IH in R' as (k'&eq');[|omega|auto].
     ∃ (1+k1+k2+k');intros l ?. destruct l. omega. simpl.
     rewrite eq''. rewrite eq1. rewrite eq2. apply eq'. omega. omega. omega.
Qed.

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