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.


  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.

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

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

  destruct (Hu s); tauto.


Lemma Convergence_To_Markov : Convergence -> Markov.


   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.


   Grab Existential Variables.
repeat constructor.

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.


  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.


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


  unfold Unenc', unenc'.

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

Lemma MarkovDnAcc : Markov -> DnAcc.

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.

Lemma DnAcc_To_Post : DnAcc -> Post.


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