Set Implicit Arguments.
Require Import Morphisms Setoid.
From Undecidability.HOU Require Import std.std.
From Undecidability.HOU.calculus Require Import
  prelim terms syntax semantics confluence typing order normalisation.
Import ArsInstances.

Section Evaluator.

  Context {X: Const}.


  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₀ {_} _ {_} {_} {_} _.