From Undecidability.L Require Import Interpreter Encodings.

Definition test (u : term) := forall n, u (enc n) ▷ T \/ u (enc n) ▷ F.
Definition satis u n := u (enc n) ▷ T.

Hint Unfold test.

Section fix_u.

  Variable u : term.
  Hypothesis proc_u : proc u.
  Hypothesis test_u : test u.

  Definition H := rho (.\"H", "n", "u"; "u" "n" (.\ "_"; "n") (.\ "_"; "H" (!Succ "n") "u") !I).
  Hint Unfold H : cbv.

  Lemma H_rec n : H (enc n) u ≻^+ u (enc n) (lambda (enc n)) (lambda (H (Succ (enc n)) u)) I.
  Proof.
    eexists. split; solvered.
  Qed.

  Definition ok n := exists k, H (enc n) u ▷ enc k /\ satis u k.

  Lemma H_ok n : satis u n -> ok n.
  Proof.
    intros. exists n. rewrite H_rec, H0; eauto. split. solveeq. eauto.
  Qed.

  Lemma H_n_Sn n : ok (S n) -> ok n.
  Proof with eauto.
    intros H_Sk. destruct (test_u n).
    - intros. exists n.
      rewrite H_rec, H0; eauto. split. solveeq. eauto.
    - destruct (H_Sk) as (k & ?). exists k.
      rewrite H_rec, H0; eauto. split. eapply evaluates_equiv. split; value.
      transitivity (H (Succ (enc n)) u). solveeq.
      rewrite Succ_correct. now eapply evaluates_equiv. firstorder.
  Qed.

  Lemma H_0_n n : test u -> ok n -> ok 0.
  Proof.
    induction n; eauto using H_n_Sn.
  Qed.

  Definition C := lambda (H (enc 0) 0).

  Lemma C_complete n : satis u n -> exists n, C u ▷ enc n /\ satis u n.
  Proof.
    intros sat % H_ok. destruct (H_0_n test_u sat) as [k [H_sat % evaluates_equiv ?]]; eauto. exists k.
    split; eauto.
    eapply evaluates_equiv; split; value. transitivity (H (enc 0) u).
    solveeq. firstorder.
  Qed.

  Lemma H_correct n k v : H (enc n) u ▷^k v -> exists n, satis u n.
  Proof.
    revert n v.
    eapply complete_induction with (x := k). clear k.
    intros k IHn n v He.

    destruct (test_u n).
    - firstorder.
    - assert (H (enc n) u ≻^+ H (enc (S n)) u).
      eapply (stepplus_star_stepplus (H_rec _)).
      eapply evaluates_star in H0 as []. rewrite H0.
      transitivity (H (Succ (enc n)) u). solvered. now rewrite Succ_correct.
      now destruct (triangle He H1) as (? & ? & ? % IHn).
  Qed.

  Lemma C_sound : eva (C u) -> exists n, satis u n.
  Proof with eauto.
    assert (He : C u ≡ H (enc 0) u). solveeq. rewrite He.
    intros [v [[k Hv] % star_stepn lam_v] % evaluates_star].
    eapply H_correct. split...
  Qed.

End fix_u.