Library MoreAcc

Require Import Rice Size.

Lemma totality : ~ lacc(fun s => forall t, pi s t).
Proof.
  intros [u [proc_u Hu]].

  pose (w := (.\"x"; !u (!Lam (!App (!App (!App (!App
                              !(tenc Eva)
                              (!App !(tenc Size) !(tenc 0)))
                              (!Q (!App "x" (!Q "x"))))
                              !(tenc (lam Omega)))
                              !(tenc I)))) : term).

  eapply self_div. exists w.

  split; value.

  intros s.

  pose (v_s := (.\"y"; !Eva (!Size "y") !(tenc (s (tenc s))) !(lam Omega) !I) : term ).

  assert (~ pi s s <-> pi u v_s). {
    rewrite <- Hu.
    unfold pi.
    assert (forall t, v_s (tenc t) == ((oenc (eva (size t) (s (tenc s)))) (λ Omega)) I). {
      intros.
      transitivity (Eva (Size (tenc t)) (tenc (s (tenc s))) (lam Omega) I). crush.
      now rewrite Size_correct, Eva_correct.
    }
    split; intros A.
    - intros t. rewrite H.
      destruct (eva (size t) (s (tenc s))) eqn:E.
      + exfalso; eapply A. destruct (eva_lam E). exists x. eapply eva_seval in E. eapply seval_eval in E. eapply star_equiv; subst; firstorder.
      + eexists; crush.
    - intros [v Hv]. eapply equiv_lambda in Hv.
      assert (B : Seval.eval (s (tenc s)) (lam v)) by firstorder.
      destruct (eval_seval B) as [n C]. eapply seval_eva in C.
      destruct n. inv C.
      destruct (size_surj n) as [t Ht].
      specialize (A t); specialize (H t). rewrite <- Ht in C. rewrite C in H. eapply lamOmega.
      destruct A as [v' A]. exists v'.
      rewrite <- A, H. clear A H.
      transitivity Omega. now reduction. symmetry. crush.
  }

  assert (A : w (tenc s) == u (tenc v_s)). {
    transitivity (u (Lam (App (App (App (App
                              (tenc Eva)
                              (App (tenc Size) (tenc 0)))
                              (Q (App (tenc s) (Q (tenc s)))))
                              (tenc (lam Omega)))
                              (tenc I)))). crush.
    now rewrite !Q_correct, !App_correct, !Q_correct, !App_correct, Lam_correct.
  }
  unfold pi; now rewrite A.
Grab Existential Variables. repeat econstructor.
Qed.

Lemma totality_proc : ~ lacc (fun s => proc s /\ ~ forall t, pi s t).
Proof.
  eapply Rice1.
  - firstorder.
  - firstorder intuition. eapply H3. intros t0. rewrite H1. eauto.
  - exists (lam I). repeat split; value. intros [_ H]. eapply H. intros; eexists; crush.
  - exists (lam Omega). split; value. split; value. intros H; eapply lamOmega. eauto.
  - split; value. intros H; eapply lamOmega. eauto.
Grab Existential Variables. repeat econstructor. repeat econstructor.
Qed.

Lemma totality_compl : ~ (lacc (fun s => ~ forall t, pi s t)).
Proof.
  intros H.
  eapply totality_proc.
  eapply lacc_conj.
  - eapply dec_lacc. eapply ldec_proc.
  - eassumption.
Qed.