Section Evalf.

Fixpoint evalf (n : nat) (s : recipe) (l : stack) : option term :=
  match n with
  | 0 => None
  | n.+1 =>
    match s, l with
    | Zero, [::] => Some FBot
    | Top, [::] => Some FTop
    | Imp s f, [::] => omap (FImp f) (evalf n s [::])
    | And s t, l =>
        match evalf n s l, evalf n t l with
        | Some f, Some g => Some (FAnd f g)
        | _, _ => None
        end
    | Box s, l => evalf n s l
    | Neu s, l => evalf n (neu s) l
    | TLam s, T t :: l => evalf n s.|[t/] l
    | TAll s, [::] => omap FAll (evalf n s [::])
    | Lam s _, R r :: l => evalf n s.[Box r/] l
    | App s t, l => evalf n s (R t :: l)
    | TApp s t, l => evalf n s (T t :: l)
    | _, _ => None
    end
  end.

Lemma evalf_sound n s l f :
  evalf n s l = Some f ->
  eval s l f.
Proof.
  elim: n s l f=> [|n] ih s l f //=.
  case: s=> //=; try by (move=> > /ih h; constructor).
  - case: l=> //=.
    move=> [<-].
    by constructor.
  - case: l=> //=.
    move=> [<-].
    by constructor.
  - move=> s t.
    case e1: (evalf n s l)=> [?|] //.
    case e2: (evalf n t l)=> [?|] //.
    move=> [<-].
    by constructor; apply ih.
  - move=> s U.
    case: l=> [|[?|?] ?] //= /ih h.
    by constructor.
  - move=> s g.
    case: l=> //=.
    case e: (evalf n s [::])=> [?|] //.
    move=> [<-].
    by constructor; apply ih.
  - move=> s.
    case: l=> [|[?|?] ?] //= /ih h.
    by constructor.
  - move=> s.
    case: l=> //=.
    case e: (evalf n s [::])=> [?|] //.
    move=> [<-].
    by constructor; apply ih.
Qed.

Lemma evalf_mono n m s l f :
  n <= m ->
  evalf n s l = Some f ->
  evalf m s l = Some f.
Proof.
  elim: n m s l f=> [|n ih] [|m] s l f //=.
  rewrite ltnS=> hnm.
  case: s=> //=; try by (move=> >; apply ih).
  - move=> s t.
    case e1: (evalf n s l)=> [?|] //.
    case e2: (evalf n t l)=> [?|] //.
    by rewrite (ih _ _ _ _ hnm e1) (ih _ _ _ _ hnm e2).
  - move=> s ?.
    case: l=> [|[?|?] ?] //=.
    by apply ih.
  - move=> s ?.
    case: l=> //=.
    case e: (evalf n s [::])=> [?|] //.
    by rewrite (ih _ _ _ _ hnm e).
  - move=> s.
    case: l=> [|[?|?] ?] //=.
    by apply ih.
  - move=> s.
    case: l=> //=.
    case e: (evalf n s [::])=> [?|] //.
    by rewrite (ih _ _ _ _ hnm e).
Qed.

Lemma evalf_complete s l f :
  eval s l f ->
  exists n, evalf n s l = Some f.
Proof.
  elim; try by (move=> > _ [n h]; exists n.+1).
  - by exists 1.
  - by exists 1.
  - move=> > _ [n h].
    exists n.+1=>/=.
    by rewrite h.
  - move=> > _ [n1 h1] _ [n2 h2].
    exists (maxn n1 n2).+1=>/=.
    rewrite (evalf_mono (leq_maxl _ _) h1).
    rewrite (evalf_mono (leq_maxr _ _) h2).
    done.
  - move=> > _ [n h].
    exists n.+1=>/=.
    by rewrite h.
Qed.

Theorem evalf_def s :
  complete s ->
  exists n f, evalf n s [::] = Some f.
Proof.
  move=> /exists_unique_eval [f [h _]].
  have [n hn] := evalf_complete h.
  by exists n, f.
Qed.

Theorem evalf_unique s n m f g :
  complete s ->
  evalf n s [::] = Some f ->
  evalf m s [::] = Some g ->
  f = g.
Proof.
  move=> h /evalf_sound hf /evalf_sound hg.
  by apply (uniqueness_eval h).
Qed.

End Evalf.