From Undecidability.L Require Export Enumerable InterpreterResults DecidableRecognisable Rice Por.

(** * Markov's principle *)

Lemma re_exists p : enumerable p -> enumerable (fun t => exists s : term, p (s t)).
Proof.
(* Goal: forall _ : enumerable p, enumerable (fun t : term => @ex term (fun s : term => p (app s t))) *)
  intros (u & proc_u & spec_u & corr_u).
(* Goal: enumerable (fun t : term => @ex term (fun s : term => p (app s t))) *)
  exists (lambda (u 0 (lambda (0 (lambda none) (lambda (lambda (some 0))) (lambda none))) none)).
(* Goal: and (proc (lambda (app (app (app u (var Datatypes.O)) (lambda (app (app (app (var Datatypes.O) (lambda none)) (lambda (lambda (app some (var Datatypes.O))))) (lambda none)))) none))) (and (forall n : nat, or (equiv (app (lambda (app (app (app u (var Datatypes.O)) (lambda (app (app (app (var Datatypes.O) (lambda none)) (lambda (lambda (app some (var Datatypes.O))))) (lambda none)))) none)) (enc n)) none) (@ex term (fun s : term => and (equiv (app (lambda (app (app (app u (var Datatypes.O)) (lambda (app (app (app (var Datatypes.O) (lambda none)) (lambda (lambda (app some (var Datatypes.O))))) (lambda none)))) none)) (enc n)) (oenc (@Some term s))) (@ex term (fun s0 : term => p (app s0 s)))))) (forall (s : term) (_ : @ex term (fun s0 : term => p (app s0 s))), @ex nat (fun n : nat => equiv (app (lambda (app (app (app u (var Datatypes.O)) (lambda (app (app (app (var Datatypes.O) (lambda none)) (lambda (lambda (app some (var Datatypes.O))))) (lambda none)))) none)) (enc n)) (oenc (@Some term s))))) *)
  repeat split; value.
  - intros n.  destruct (spec_u n).
    + left. solveeq.
    + destruct H as ([] & ? & ?).
(* Goal: evaluates (app (lambda (app (app (app (var Datatypes.O) (lambda (app (app (app (app E (var Datatypes.O)) (tenc t)) (lambda (lambda (lambda (var (S Datatypes.O)))))) (lambda (lambda (var Datatypes.O)))))) (lambda (lambda (lambda (lambda (var Datatypes.O)))))) (lambda (lambda (lambda (var Datatypes.O)))))) (tenc (lambda s))) (lambda (lambda (var Datatypes.O))) *)
      * left; solveeq.
(* Goal: evaluates (app (lambda (app (app (app (var Datatypes.O) (lambda (app (app (app (app E (var Datatypes.O)) (tenc t)) (lambda (lambda (lambda (var (S Datatypes.O)))))) (lambda (lambda (var Datatypes.O)))))) (lambda (lambda (lambda (lambda (var Datatypes.O)))))) (lambda (lambda (lambda (var Datatypes.O)))))) (tenc (lambda s))) (lambda (lambda (var Datatypes.O))) *)
      * right. exists t. split. solveeq. eauto.
(* Goal: evaluates (app (lambda (app (app (app (var Datatypes.O) (lambda (app (app (app (app E (var Datatypes.O)) (tenc t)) (lambda (lambda (lambda (var (S Datatypes.O)))))) (lambda (lambda (var Datatypes.O)))))) (lambda (lambda (lambda (lambda (var Datatypes.O)))))) (lambda (lambda (lambda (var Datatypes.O)))))) (tenc (lambda s))) (lambda (lambda (var Datatypes.O))) *)
      * left; solveeq.
  - intros s [t [n H] % corr_u]. exists n. solveeq.
Qed.

Lemma DA p : recognisable p -> recognisable (fun _ => exists t, p t).
Proof.
(* Goal: forall s : term, iff (not (@ex term (fun t : term => p t))) (eva (app D (tenc s))) *)
  intros. eapply enumerable_recognisable.
(* Goal: enumerable (fun _ : term => @ex term (fun t : term => p t)) *)
  change (enumerable (fun t => exists s, (fun x => match x with app s t => p s | _ => False end) (app s t))).
(* Goal: enumerable (fun t : term => @ex term (fun s : term => (fun x : term => match x with | var n => False | app s0 t0 => p s0 | lambda s0 => False end) (app s t))) *)
  eapply re_exists. eapply recognisable_enumerable.
(* Goal: recognisable (fun x : term => match x with | var n => False | app s t => p s | lambda s => False end) *)
  destruct H as (u & pu & Hu).
(* Goal: recognisable (fun x : term => match x with | var n => False | app s t => p s | lambda s => False end) *)
  pose (v := (lambda (0 (lambda Omega) (lambda (lambda (u 1))) (lambda Omega)))).
(* Goal: recognisable (fun x : term => match x with | var n => False | app s t => p s | lambda s => False end) *)
  exists v.
(* Goal: and (not (q (lambda s))) (evaluates (app (lambda (app (app (app (var Datatypes.O) (lambda (app (app (app (app E (var Datatypes.O)) (tenc t)) (lambda (lambda (lambda (var (S Datatypes.O)))))) (lambda (lambda (var Datatypes.O)))))) (lambda (lambda (lambda (lambda (var Datatypes.O)))))) (lambda (lambda (lambda (var Datatypes.O)))))) (tenc (lambda s))) (lambda (lambda (var Datatypes.O)))) *)
  split. subst v; value. destruct s; unfold pi.
  - assert (v (tenc n) ≡ Omega). solveeq. rewrite H. firstorder using eva_Omega.
  - assert (v (tenc (s1 s2)) ≡ u (tenc s1)). solveeq. now rewrite H, Hu.
  - assert (v (tenc (lambda s)) ≡ Omega). solveeq. rewrite H. firstorder using eva_Omega.
Qed.
  
Definition Markov_Post:= forall p, recognisable p -> recognisable (complement p) -> decidable p.
Definition Markov_Sat := forall p, decidable p -> (~~ exists t, p t) -> exists t, p t.
Definition Markov_Eva := forall s, closed s -> ~~ eva s -> eva s.

Lemma Markov_Post_to_Sat : Markov_Post -> Markov_Sat.
Proof.
(* Goal: forall _ : Markov_Post, Markov_Sat *)
  intros post p dec_p H.
(* Goal: @ex term (fun t : term => p t) *)
  assert (recognisable (fun _ => exists t, p t)). {
(* Goal: recognisable (fun _ : term => @ex term (fun t : term => p t)) *)
    eapply DA. now eapply dec_recognisable. }
(* Goal: not (eva (app v (tenc t))) *)
(* Goal: False *)
  assert (recognisable (fun _ => ~ exists t, p t)). {
(* Goal: forall s : term, iff (not (@ex term (fun t : term => p t))) (eva (app D (tenc s))) *)
    exists D. split; value. intros. firstorder using D_pi. }
(* Goal: @ex term (fun t : term => p t) *)
  destruct (dec_pdec (post _ H0 H1) I); tauto.
Qed.

Lemma Markov_Sat_to_Eva : Markov_Sat -> Markov_Eva.
Proof.
(* Goal: forall _ : Markov_Sat, Markov_Eva *)
  intros markov t cls_t Ht.
(* Goal: eva t *)
  pose (q := fun s => exists n, s = var n /\ eval n t <> None).
  
(* Goal: not (eva (app v (tenc t))) *)
(* Goal: False *)
  assert (decp : decidable q). {
(* Goal: decidable q *)
    exists (.\ "s" ; "s" (.\ "n" ; !E "n" !(tenc t) !(lambda T) !F) !(lambda (lambda F)) !(lambda F)).
(* Goal: and (proc (convert (blambda (String (Ascii.Ascii true true false false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString)) (blambda (String (Ascii.Ascii false true true true false true true false) EmptyString) (bapp (bapp (bapp (bapp (bter E) (bvar (String (Ascii.Ascii false true true true false true true false) EmptyString))) (bter (tenc t))) (bter (lambda T))) (bter F)))) (bter (lambda (lambda F)))) (bter (lambda F)))))) (decides (convert (blambda (String (Ascii.Ascii true true false false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString)) (blambda (String (Ascii.Ascii false true true true false true true false) EmptyString) (bapp (bapp (bapp (bapp (bter E) (bvar (String (Ascii.Ascii false true true true false true true false) EmptyString))) (bter (tenc t))) (bter (lambda T))) (bter F)))) (bter (lambda (lambda F)))) (bter (lambda F))))) q) *)
    split; value. intros s.
(* Goal: or (and (q s) (evaluates (app (convert (blambda (String (Ascii.Ascii true true false false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString)) (blambda (String (Ascii.Ascii false true true true false true true false) EmptyString) (bapp (bapp (bapp (bapp (bter E) (bvar (String (Ascii.Ascii false true true true false true true false) EmptyString))) (bter (tenc t))) (bter (lambda T))) (bter F)))) (bter (lambda (lambda F)))) (bter (lambda F))))) (tenc s)) T)) (and (not (q s)) (evaluates (app (convert (blambda (String (Ascii.Ascii true true false false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString)) (blambda (String (Ascii.Ascii false true true true false true true false) EmptyString) (bapp (bapp (bapp (bapp (bter E) (bvar (String (Ascii.Ascii false true true true false true true false) EmptyString))) (bter (tenc t))) (bter (lambda T))) (bter F)))) (bter (lambda (lambda F)))) (bter (lambda F))))) (tenc s)) F)) *)
    cbn. destruct s.
    - destruct (eval n t) eqn:Eq.
      + left. split. exists n; firstorder congruence. eapply evaluates_equiv; split; value.
(* Goal: evaluates (app (lambda (app (app (app (var Datatypes.O) (lambda (app (app (app (app E (var Datatypes.O)) (tenc t)) (lambda (lambda (lambda (var (S Datatypes.O)))))) (lambda (lambda (var Datatypes.O)))))) (lambda (lambda (lambda (lambda (var Datatypes.O)))))) (lambda (lambda (lambda (var Datatypes.O)))))) (tenc (lambda s))) (lambda (lambda (var Datatypes.O))) *)
        transitivity (E (enc n) (tenc t) (lambda T) F). solveeq. rewrite E_correct, Eq. solveeq.
      + right. split. intros (n' & Hn & E'). inv Hn. congruence. eapply evaluates_equiv; split; value.
(* Goal: evaluates (app (lambda (app (app (app (var Datatypes.O) (lambda (app (app (app (app E (var Datatypes.O)) (tenc t)) (lambda (lambda (lambda (var (S Datatypes.O)))))) (lambda (lambda (var Datatypes.O)))))) (lambda (lambda (lambda (lambda (var Datatypes.O)))))) (lambda (lambda (lambda (var Datatypes.O)))))) (tenc (lambda s))) (lambda (lambda (var Datatypes.O))) *)
        transitivity (E (enc n) (tenc t) (lambda T) F). solveeq. rewrite E_correct, Eq. solveeq.
    - right. split. intros (n' & Hn & E'). inv Hn. solveeq.
    - right. split. intros (n' & Hn & E'). inv Hn. solveeq.
  }

(* Goal: eva t *)
  destruct (markov _ decp) as [t' [v H]].
  - assert (forall P Q : Prop, (P -> Q) -> (~~ P -> ~~ Q)) by tauto. eapply H; try eassumption; eauto.
(* Goal: forall _ : eva t, @ex term (fun t : term => q t) *)
    intros [v [n Hn] % evaluates_eval].
(* Goal: q (var n) *)
    exists n. exists n. firstorder congruence.
  - destruct H. subst. destruct (eval v t) eqn:Eq; try congruence.
(* Goal: eva t *)
    eapply eval_evaluates in Eq. eauto.
Qed.

Lemma Markov_Eva_to_Post : Markov_Eva -> Markov_Post.
Proof.
(* Goal: forall _ : Markov_Eva, Markov_Post *)
  intros H p [u [[lam_u cls_u] Hu]] [v [[lam_v cls_v] Hv]].
(* Goal: decidable p *)
  pose (por_u_v := lambda (O ((App (tenc u) (Q 0))) ((App (tenc v) (Q 0))))).
(* Goal: decidable p *)
  exists por_u_v.
(* Goal: and (proc por_u_v) (decides por_u_v p) *)
  split; subst por_u_v; value. intros t. 

(* Goal: not (eva (app v (tenc t))) *)
(* Goal: False *)
  assert (A : eva (O (tenc (u (tenc t))) (tenc (v (tenc t))))). {
(* Goal: eva (app (app O (tenc (app u (tenc t)))) (tenc (app v (tenc t)))) *)
    eapply H; value.

(* Goal: not (not (eva (app (app O (tenc (app u (tenc t)))) (tenc (app v (tenc t)))))) *)
    intros A.
(* Goal: not (eva (app v (tenc t))) *)
(* Goal: False *)
    assert (Hnu : ~ eva (u (tenc t))). { intros B. eapply A, O_complete. tauto. }
(* Goal: not (eva (app v (tenc t))) *)
(* Goal: False *)
    assert (Hnv : ~ eva (v (tenc t))). { intros B. eapply A, O_complete. tauto. }
    rewrite <- Hu in Hnu. rewrite <- Hv in Hnv. unfold complement in *. tauto.
  } 

(* Goal: or (and (p t) (evaluates (app (lambda (app (app O (app (app App (tenc u)) (app Q (var Datatypes.O)))) (app (app App (tenc v)) (app Q (var Datatypes.O))))) (tenc t)) T)) (and (not (p t)) (evaluates (app (lambda (app (app O (app (app App (tenc u)) (app Q (var Datatypes.O)))) (app (app App (tenc v)) (app Q (var Datatypes.O))))) (tenc t)) F)) *)
  eapply O_sound in A.

(* Goal: or (and (p t) (evaluates (app (lambda (app (app O (app (app App (tenc u)) (app Q (var Datatypes.O)))) (app (app App (tenc v)) (app Q (var Datatypes.O))))) (tenc t)) T)) (and (not (p t)) (evaluates (app (lambda (app (app O (app (app App (tenc u)) (app Q (var Datatypes.O)))) (app (app App (tenc v)) (app Q (var Datatypes.O))))) (tenc t)) F)) *)
  destruct A as [[A [B ?] %evaluates_equiv] | [A [B ?] %evaluates_equiv]].
  - left; split; eauto. rewrite Hu. tauto. eapply evaluates_equiv; split; value.
(* Goal: equiv (app (lambda (app (app O (app (app App (tenc u)) (app Q (var Datatypes.O)))) (app (app App (tenc v)) (app Q (var Datatypes.O))))) (tenc t)) T *)
    dobeta. now rewrite Q_correct, !App_correct, B.
  - right; split; eauto. unfold complement in *. rewrite Hv. tauto.
(* Goal: and (proc (convert (blambda (String (Ascii.Ascii true true false false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString)) (blambda (String (Ascii.Ascii false true true true false true true false) EmptyString) (bapp (bapp (bapp (bapp (bter E) (bvar (String (Ascii.Ascii false true true true false true true false) EmptyString))) (bter (tenc t))) (bter (lambda T))) (bter F)))) (bter (lambda (lambda F)))) (bter (lambda F)))))) (decides (convert (blambda (String (Ascii.Ascii true true false false true true true false) EmptyString) (bapp (bapp (bapp (bvar (String (Ascii.Ascii true true false false true true true false) EmptyString)) (blambda (String (Ascii.Ascii false true true true false true true false) EmptyString) (bapp (bapp (bapp (bapp (bter E) (bvar (String (Ascii.Ascii false true true true false true true false) EmptyString))) (bter (tenc t))) (bter (lambda T))) (bter F)))) (bter (lambda (lambda F)))) (bter (lambda F))))) q) *)
    eapply evaluates_equiv; split; value. dobeta; now rewrite Q_correct, !App_correct, B.
Qed.
