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.
(* Goal: forall _ : satis (app u) n, ok n *)
    intros. exists n. rewrite H_rec, H0; eauto. split. solveeq. eauto.
  Qed.

  Lemma H_n_Sn n : ok (S n) -> ok n.
(* Goal: satis (app u) n *)
  Proof with eauto.
    intros H_Sk. destruct (test_u n).
(* Goal: forall _ : satis (app u) n, ok n *)
    - intros. exists n.
(* Goal: and (evaluates (app (app H (enc n)) u) (enc n)) (satis (app u) n) *)
      rewrite H_rec, H0; eauto. split. solveeq. eauto.
    - destruct (H_Sk) as (k & ?). exists k.
(* Goal: and (evaluates (app (app H (enc n)) u) (enc n)) (satis (app u) n) *)
      rewrite H_rec, H0; eauto. split. eapply evaluates_equiv. split; value.
(* Goal: equiv (app C u) (app (app H (enc O)) u) *)
(* Goal: equiv (app (app H (enc O)) u) (enc k) *)
      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.
(* Goal: forall (_ : test u) (_ : ok n), ok O *)
    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.
(* Goal: satis (app u) n *)
    intros sat % H_ok. destruct (H_0_n test_u sat) as [k [H_sat % evaluates_equiv ?]]; eauto. exists k.
(* Goal: satis (app u) n *)
    split; eauto.
    eapply evaluates_equiv; split; value. transitivity (H (enc 0) u).
(* Goal: equiv (app C u) (app (app H (enc O)) u) *)
(* Goal: equiv (app (app H (enc O)) u) (enc k) *)
    solveeq. firstorder.
  Qed.

  Lemma H_correct n k v : H (enc n) u ▷^k v -> exists n, satis u n.
  Proof.
(* Goal: forall _ : evaluatesin k (app (app H (enc n)) u) v, @ex nat (fun n : nat => satis (app u) n) *)
    revert n v.
(* Goal: forall (n : nat) (v : term) (_ : evaluatesin k (app (app H (enc n)) u) v), @ex nat (fun n0 : nat => satis (app u) n0) *)
    eapply complete_induction with (x := k). clear k.
(* Goal: forall (x : nat) (_ : forall (y : nat) (_ : lt y x) (n : nat) (v : term) (_ : evaluatesin y (app (app H (enc n)) u) v), @ex nat (fun n0 : nat => satis (app u) n0)) (n : nat) (v : term) (_ : evaluatesin x (app (app H (enc n)) u) v), @ex nat (fun n0 : nat => satis (app u) n0) *)
    intros k IHn n v He.

(* Goal: @ex nat (fun n : nat => satis (app u) n) *)
    destruct (test_u n).
    - firstorder.
    - assert (H (enc n) u ≻^+ H (enc (S n)) u).
(* Goal: stepplus (app (app H (enc n)) u) (app (app H (enc (S n))) u) *)
(* Goal: @ex nat (fun n : nat => satis (app u) n) *)
      eapply (stepplus_star_stepplus (H_rec _)).
(* Goal: star (app (app (app (app u (enc n)) (lambda (enc n))) (lambda (app (app H (app Succ (enc n))) u))) I) (app (app H (enc (S n))) u) *)
(* Goal: @ex nat (fun n : nat => satis (app u) n) *)
      eapply evaluates_star in H0 as []. rewrite H0.
(* Goal: star (app (app (app F (lambda (enc n))) (lambda (app (app H (app Succ (enc n))) u))) I) (app (app H (enc (S n))) u) *)
(* Goal: @ex nat (fun n : nat => satis (app u) n) *)
      transitivity (H (Succ (enc n)) u). solvered. now rewrite Succ_correct.
(* Goal: @ex nat (fun n : nat => satis (app u) n) *)
      now destruct (triangle He H1) as (? & ? & ? % IHn).
  Qed.

  Lemma C_sound : eva (C u) -> exists n, satis u n.
(* Goal: satis (app u) n *)
  Proof with eauto.
(* Goal: equiv (app C u) (app (app H (enc O)) u) *)
(* Goal: equiv (app (app H (enc O)) u) (enc k) *)
    assert (He : C u ≡ H (enc 0) u). solveeq. rewrite He.
    intros [v [[k Hv] % star_stepn lam_v] % evaluates_star].
(* Goal: and (evaluates (app (app (app T (lambda (enc n))) (lambda (app (app H (app Succ (enc n))) u))) I) (enc n)) (satis (app u) n) *)
    eapply H_correct. split...
  Qed.

End fix_u.
