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.
Lemma Convergence_To_Markov : Convergence -> Markov.
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.
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.
Lemma Convergence_To_Markov : Convergence -> Markov.
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.