# Library Markov

Require Export Acceptability DA.

Definition Post:= forall M, lacc M -> lacc (complement M) -> ldec M.

Definition Convergence := forall s, closed s -> ~~ converges s -> converges s.

Definition DnAcc := forall M, lacc M -> forall t, ~~ M t -> M t.

Definition Markov := forall (P : term -> Prop), ldec P -> (~~ exists t, P t) -> exists t, P t.

Lemma Post_To_Convergence : Post -> Convergence.

Proof.

intros A s cls_s B.

assert (H1 : lacc (fun _ => converges s)).

exists (lam s).
split; value. intros t. split; intros [r Hr].
exists r.
transitivity s. crush. eassumption.
exists r.
symmetry. symmetry in Hr. crush.

assert (H2 : lacc (complement (fun _ => converges s))).

exists (lam Omega).
split; value. unfold complement.
intros t1; split.

tauto.
intros C. exfalso.
destruct C.
eapply Omega_diverges. rewrite <- H.
symmetry.
clear H. crush.

destruct (A _ H1 H2) as [u [[lam_u cls_u] Hu]].

destruct (Hu s); tauto.

Qed.

Proof.

intros C P [u [[lam_u cls_u] Hu]] H.

assert (A : lacc (fun _ => exists t, P t)).
eapply DA.
exists u; split; value; intuition.

destruct A as [v [[lam_v cls_v] Hv]].

rewrite Hv.
eapply C. value. unfold pi in Hv.
rewrite <- Hv.

eassumption.

Grab Existential Variables.
repeat constructor.
Qed.

Definition unenc' t := match unenc t with None => 0 | Some n => n end.

Definition Unenc := R (lam (lam (
#0 (lam none)
(lam(lam none))
(lam (#0 (lam none)
(lam (lam none))
(lam (#0 (lam(EqN (enc 1) #0 (some (enc 0)) none))
(lam(lam( #1 (lam(EqN (enc 0) #0 (lam ((#7 #2) (lam(some (Succ #0))) none )) (lam none) I ))
(lam(lam none))
(lam none))))
(lam none)
)
)
)
)
))).

Definition Unenc' := lam (Unenc #0 I Zero).

Lemma Unenc_correct s : Unenc (tenc s) == match unenc s with None => none | Some n => lam(lam(#1 (enc n))) end.

Proof.

eapply size_induction with (f := size) (x := s).
clear s.
intros s.
intros IH.
destruct s; [crush.. | idtac].

destruct s; [crush.. | idtac].

destruct s.

- destruct n.

+ crush.

+ destruct n; crush.

- destruct s1.

+ destruct n.

* assert (H : size s2 < size (Î» (Î» # 0 s2))) by (simpl; omega).

specialize (IH s2 H).
simpl in *; destruct (unenc s2); crush.
* crush.

+ crush.

+ crush.

- crush.

Qed.

Lemma Unenc'_correct s : Unenc'(tenc s) == enc(unenc' s).

Proof.

unfold Unenc', unenc'.

transitivity (Unenc (tenc s) I Zero).
crush.
rewrite Unenc_correct.
destruct (unenc s); crush.
Qed.

Lemma MarkovDnAcc : Markov -> DnAcc.

Proof.
unfold Markov.
intros markov M [u [[lam_u cls_u] Hu]] t nnMt.

pose (P := fun s => exists t', eva (unenc' s) (u (tenc t)) = Some t').

assert (decP : ldec P). {

exists (lam ((Eva (Unenc' #0) (tenc (u (tenc t)))) (lam true) false)).

split; value.

intros s; destruct (eva (unenc' s) (u (tenc t))) eqn:A;
[left|right]; split; (try eexists; eauto); (try intros []; try congruence);
transitivity (Eva (Unenc' (tenc s)) (tenc (u (tenc t))) (lam true) false); [crush| | crush | ];
rewrite Unenc'_correct, Eva_correct, A; crush.

}

eapply markov in decP.
destruct decP. unfold P in H.
destruct H as [t' H].
unfold unenc' in *.
destruct (eva_lam H).

destruct (unenc x).

rewrite Hu.
exists x0.
eapply eva_equiv.
subst. eassumption. inv H.

intros C.
eapply nnMt. intros D. rewrite Hu in D.
eapply C.
destruct D. eapply equiv_eva in H. destruct H as [n H].
exists (enc n).
unfold P. exists (lam x).

unfold unenc'.
rewrite unenc_correct. eassumption.
Qed.

Lemma DnAcc_To_Post : DnAcc -> Post.

Proof.

intros H M [u [[lam_u cls_u] Hu]] [v [[lam_v cls_v] Hv]].

pose (por_u_v := lam (Por ((App (tenc u) (Q #0))) ((App (tenc v) (Q #0))))).

exists por_u_v.

split; value.
intros t.

assert (A : converges (Por (tenc (u (tenc t))) (tenc (v (tenc t))))).

eapply H; value.
exists (lam (Eval #0)). split; value. intros s.
split.
intros A. assert (converges (Eval (tenc s))). rewrite <- Eval_converges. eassumption. destruct H0. exists x.
transitivity (Eval (tenc s)).
crush. eassumption.
intros A.
rewrite Eval_converges. destruct A. exists x. transitivity ((Î» Eval # 0) (tenc s)). symmetry. clear H0. crush. eassumption.
intros A.

assert (Hnu : ~ converges (u (tenc t))).
intros B. eapply Por_correct_1a in B. eauto.
assert (Hnv : ~ converges (v (tenc t))).
intros B. eapply Por_correct_1b in B. eauto.
unfold pi in *.

rewrite <- Hu in Hnu.
rewrite <- Hv in Hnv. unfold complement in *. tauto.

eapply Por_correct_2 in A.

assert (Q1 := Q_correct t).
assert (A1 := App_correct u (tenc t)). assert (A2 := App_correct v (tenc t)).
destruct A as [[A B] | [A B]]; unfold por_u_v.

- left; split; eauto.
rewrite Hu. tauto. crush.
- right; split; eauto.
unfold complement in *. rewrite Hv. tauto. crush.
Qed.