# 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.