Set Implicit Arguments.
Require Import Morphisms Setoid std calculus.prelim
    calculus.semantics calculus.confluence calculus.normalisation.

Section Evaluator.

  Context {X: Const}.

  Definition xi := evaluator.E (@rho X) _.

  Lemma xi_correct s t:
    s ▷ t <-> exists n, xi n s = Some t.
  Proof.
    split; intros ?; eapply E_correct_tak; try eapply tak_fun_rho.
    all: eauto using sandwich_step, sandwich_steps.
    all: typeclasses eauto.
  Qed.

  Lemma xi_monotone n m s t:
    n <= m -> xi n s = Some t -> xi m s = Some t.
  Proof.
    intros ??; eapply E_monotone; eauto.
  Qed.

  Lemma compute_evaluation_step (s: exp X):
    (exists t, s ▷ t) -> { t | s ▷ t }.
  Proof.
    intros; eapply compute_evaluation with (S := par) (rho := rho); eauto using tak_fun_rho.
    all: typeclasses eauto.
  Qed.

  Definition eta (s: exp X) {Gamma A} (H: Gamma ⊢ s : A) :=
    proj1_sig (compute_evaluation_step (termination_steps H)).

  Definition eta₀ (s: exp X) {Gamma n A} (H: Gamma ⊢(n) s : A) :=
    proj1_sig (compute_evaluation_step (ordertyping_termination_steps H)).

  Arguments eta _ {_} {_} _.
  Arguments eta₀ _ {_} {_} {_} _.

  Section Correctness.
    Variable (Gamma: ctx) (n: nat) (s: exp X) (A: type) (H: Gamma ⊢ s : A) (H₀: Gamma ⊢(n) s : A).

    Lemma eta_correct: s ▷ eta s H.
    Proof.
      unfold eta. destruct compute_evaluation_step; cbn; eauto.
    Qed.

    Lemma eta₀_correct: s ▷ eta₀ s H₀.
    Proof.
      unfold eta₀. destruct compute_evaluation_step; cbn; eauto.
    Qed.

    Lemma eta_normal: normal (eta s H).
    Proof.
      destruct eta_correct; eauto.
    Qed.

    Lemma eta₀_normal: normal (eta₀ s H₀).
    Proof.
      destruct eta₀_correct; eauto.
    Qed.

    Lemma eta_typing: Gamma ⊢ eta s H : A.
    Proof.
      eapply preservation_under_steps. rewrite <-eta_correct. all: eauto.
    Qed.

    Lemma eta₀_typing: Gamma ⊢(n) eta₀ s H₀ : A.
    Proof.
      eapply ordertyping_preservation_under_steps. rewrite <-eta₀_correct. all: eauto.
    Qed.


  End Correctness.

End Evaluator.

Arguments eta {_} _ {_} {_} _.
Arguments eta₀ {_} _ {_} {_} {_} _.