From Undecidability.L Require Import InterpreterResults.

(** ** Parallel or *)

Definition H (s t : term) : term := Eval cbv in (.\ "z"; !E "z" !s !(lambda T) (!E "z" !t !(lambda T) !F)).
Definition O : term := Eval cbv in .\ "x", "y";
                        (.\ "z"; !E "z" "x" !(lambda T) (!E "z" "y" !(lambda F) !I)) (!C !(H 2 1)).

Lemma H_proc s t : proc (H (tenc s) (tenc t)).
Proof.
(* Goal: proc (H (tenc s) (tenc t)) *)
  value.
Qed.

Lemma H_rec s t n : (H (tenc s) (tenc t) (enc n) ≡ E (enc n) (tenc s) (lambda T) (E (enc n) (tenc t) (lambda T) F)).
Proof.
(* 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)) (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) *)
(* Goal: equiv (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) (app (app O (tenc (app u (tenc t)))) (tenc (app v (tenc t)))) *)
  solveeq.
Qed.

Lemma H_test s t : test (H (tenc s) (tenc t)).
Proof.
(* Goal: test (H (tenc s) (tenc t)) *)
  intros n. destruct (eval n s) eqn:Eq, (eval n t) eqn:Eq2; rewrite H_rec, !E_correct, Eq, Eq2;
(* 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)) (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) *)
(* Goal: equiv (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) (app (app O (tenc (app u (tenc t)))) (tenc (app v (tenc t)))) *)
              [ left .. | right]; solveeq.
Qed.

Lemma H_inv n s t : satis ( H (tenc s) (tenc t) ) n <-> eval n s <> None \/ eval n t <> None.
Proof.
(* Goal: iff (satis (app (H (tenc s) (tenc t))) n) (or (not (@eq (option term) (eval n s) (@None term))) (not (@eq (option term) (eval n t) (@None term)))) *)
  split.
  - intros.
(* Goal: or (not (@eq (option term) (eval n s) (@None term))) (not (@eq (option term) (eval n t) (@None term))) *)
    destruct (eval n s) eqn:Eq, (eval n t) eqn:Eq2; try firstorder congruence.
(* Goal: or (not (@eq (option term) (@None term) (@None term))) (not (@eq (option term) (@None term) (@None term))) *)
    exfalso. unfold satis in H0.
(* Goal: False *)
    rewrite H_rec, !E_correct, Eq, Eq2 in H0.
(* Goal: proc (H (tenc s) (tenc t)) *)
    setoid_rewrite none_correct at 2 in H0; value. rewrite none_correct in H0; value. inv H0.
(* 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)) (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) *)
(* Goal: equiv (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) (app (app O (tenc (app u (tenc t)))) (tenc (app v (tenc t)))) *)
  - intros. destruct (eval n s) eqn:Eq, (eval n t) eqn:Eq2; (try firstorder congruence); unfold satis; rewrite H_rec, !E_correct, Eq, Eq2;  solveeq.
Qed.

Lemma O_rec s t : O (tenc s) (tenc t) ≡ (lambda (E 0 (tenc s) (lambda T) (E 0 (tenc t) (lambda F) I))) (C (H (tenc s) (tenc t))).
Proof.
(* Goal: equiv (app (app O (tenc s)) (tenc t)) (app (lambda (app (app (app (app E (var Datatypes.O)) (tenc s)) (lambda T)) (app (app (app (app E (var Datatypes.O)) (tenc t)) (lambda F)) I))) (app C (H (tenc s) (tenc t)))) *)
  solvered.
Qed.

Lemma O_complete s t : eva s \/ eva t -> eva (O (tenc s) (tenc t)).
Proof.
  intros [ [v [n Hv] % evaluates_eval] | [v [n Hv] % evaluates_eval] ];
  rewrite O_rec; edestruct (C_complete (n := n) (H_proc s t) (H_test s t)) as [k []]; unfold satis.
  - rewrite H_rec, !E_correct, Hv.
(* Goal: equiv (app (app O (tenc s)) (tenc t)) (app (lambda (app (app (app (app E (var Datatypes.O)) (tenc s)) (lambda T)) (app (app (app (app E (var Datatypes.O)) (tenc t)) (lambda F)) I))) (app C (H (tenc s) (tenc t)))) *)
    destruct (eval n t) eqn:E2; solvered.
  - rewrite H0. eapply H_inv in H1.
(* Goal: eva (app (lambda (app (app (app (app E (var Datatypes.O)) (tenc s)) (lambda T)) (app (app (app (app E (var Datatypes.O)) (tenc t)) (lambda F)) I))) (enc k)) *)
    destruct (eval k s) eqn:E1; try firstorder congruence.
(* Goal: proc (H (tenc s) (tenc t)) *)
    + exists T. 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)) (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) *)
(* Goal: equiv (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) (app (app O (tenc (app u (tenc t)))) (tenc (app v (tenc t)))) *)
      transitivity (E (enc k) (tenc s) (lambda T) (E (enc k) (tenc t) (lambda F) I)). solveeq.
(* 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)) (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) *)
(* Goal: equiv (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) (app (app O (tenc (app u (tenc t)))) (tenc (app v (tenc t)))) *)
      rewrite !E_correct, E1. destruct (eval k t); solveeq.
    + destruct (eval k t) eqn:E2; try firstorder congruence.
(* Goal: proc (H (tenc s) (tenc t)) *)
      exists F. 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)) (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) *)
(* Goal: equiv (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) (app (app O (tenc (app u (tenc t)))) (tenc (app v (tenc t)))) *)
      transitivity (E (enc k) (tenc s) (lambda T) (E (enc k) (tenc t) (lambda F) I)). solveeq.
(* 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)) (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) *)
(* Goal: equiv (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) (app (app O (tenc (app u (tenc t)))) (tenc (app v (tenc t)))) *)
      rewrite !E_correct, E1, E2. solveeq.
  - rewrite H_rec, !E_correct, Hv.
(* Goal: equiv (app (app O (tenc s)) (tenc t)) (app (lambda (app (app (app (app E (var Datatypes.O)) (tenc s)) (lambda T)) (app (app (app (app E (var Datatypes.O)) (tenc t)) (lambda F)) I))) (app C (H (tenc s) (tenc t)))) *)
    destruct (eval n s) eqn:E2; solvered.
  - rewrite H0. eapply H_inv in H1.
(* Goal: eva (app (lambda (app (app (app (app E (var Datatypes.O)) (tenc s)) (lambda T)) (app (app (app (app E (var Datatypes.O)) (tenc t)) (lambda F)) I))) (enc k)) *)
    destruct (eval k s) eqn:E1; try firstorder congruence.
(* Goal: proc (H (tenc s) (tenc t)) *)
    + exists T. 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)) (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) *)
(* Goal: equiv (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) (app (app O (tenc (app u (tenc t)))) (tenc (app v (tenc t)))) *)
      transitivity (E (enc k) (tenc s) (lambda T) (E (enc k) (tenc t) (lambda F) I)). solveeq.
(* 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)) (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) *)
(* Goal: equiv (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) (app (app O (tenc (app u (tenc t)))) (tenc (app v (tenc t)))) *)
      rewrite !E_correct, E1. destruct (eval k t); solveeq.
    + destruct (eval k t) eqn:E2; try firstorder congruence.
(* Goal: proc (H (tenc s) (tenc t)) *)
      exists F. 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)) (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) *)
(* Goal: equiv (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) (app (app O (tenc (app u (tenc t)))) (tenc (app v (tenc t)))) *)
      transitivity (E (enc k) (tenc s) (lambda T) (E (enc k) (tenc t) (lambda F) I)). solveeq.
(* 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)) (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) *)
(* Goal: equiv (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) (app (app O (tenc (app u (tenc t)))) (tenc (app v (tenc t)))) *)
      rewrite !E_correct, E1, E2. solveeq.
Qed.

Lemma O_sound s t : eva (O (tenc s) (tenc t)) -> eva s /\ O (tenc s) (tenc t) ▷ T \/ eva t /\ O (tenc s) (tenc t) ▷ F.
Proof with eauto.
  rewrite O_rec. intros H0.
  assert (eva (C (H (tenc s) (tenc t)))) by now eapply app_eva in H0.
  eapply C_sound in H1 as [n H1 % H_inv]; value; eauto using H_test.
(* Goal: eva (app (lambda (app (app (app (app E (var Datatypes.O)) (tenc s)) (lambda T)) (app (app (app (app E (var Datatypes.O)) (tenc t)) (lambda F)) I))) (enc k)) *)
  assert (H2 := H1). eapply H_inv in H1.
  eapply C_complete in H1 as (k & H1 & sat); value; eauto using H_test.
  eapply H_inv in sat. destruct (eval k s) eqn:Eq; try congruence.
(* Goal: iff (satis (app (H (tenc s) (tenc t))) n) (or (not (@eq (option term) (eval n s) (@None term))) (not (@eq (option term) (eval n t) (@None term)))) *)
  - left. split. exists t0. eapply eval_evaluates. eauto.
(* Goal: proc (H (tenc s) (tenc t)) *)
    rewrite H1. 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)) (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) *)
(* Goal: equiv (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) (app (app O (tenc (app u (tenc t)))) (tenc (app v (tenc t)))) *)
    transitivity (E (enc k) (tenc s) (lambda T) (E (enc k) (tenc t) (lambda F) I)). solveeq.
(* 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)) (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) *)
(* Goal: equiv (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) (app (app O (tenc (app u (tenc t)))) (tenc (app v (tenc t)))) *)
    rewrite !E_correct, Eq. destruct (eval k t); solveeq.
  - destruct sat; try congruence.
    destruct (eval k t) eqn:E2; try congruence. right.
(* Goal: iff (satis (app (H (tenc s) (tenc t))) n) (or (not (@eq (option term) (eval n s) (@None term))) (not (@eq (option term) (eval n t) (@None term)))) *)
    split. exists t0. eapply eval_evaluates. eauto.
(* Goal: proc (H (tenc s) (tenc t)) *)
    rewrite H1. 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)) (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) *)
(* Goal: equiv (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) (app (app O (tenc (app u (tenc t)))) (tenc (app v (tenc t)))) *)
    transitivity (E (enc k) (tenc s) (lambda T) (E (enc k) (tenc t) (lambda F) I)). solveeq.
(* 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)) (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) *)
(* Goal: equiv (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) (app (app O (tenc (app u (tenc t)))) (tenc (app v (tenc t)))) *)
    rewrite !E_correct, Eq. destruct (eval k t); solveeq.
Qed.

From Undecidability.L Require Import DecidableRecognisable.

(** ** Post's theorem *)

Theorem Post p : (forall x, p x \/ ~ p x) -> recognisable p -> recognisable (complement p) -> decidable p.
Proof.
(* Goal: forall (_ : forall x : term, or (p x) (not (p x))) (_ : recognisable p) (_ : recognisable (complement p)), decidable p *)
  intros pdec_p [u [[cls_u lam_u] Hu]] [v [[cls_v lam_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: proc (H (tenc s) (tenc t)) *)
  split; value. intros t.
(* Goal: or (and (p t) (evaluates (app por_u_v (tenc t)) T)) (and (not (p t)) (evaluates (app por_u_v (tenc t)) F)) *)
  unfold complement,pi in *.
(* Goal: or (and (p t) (evaluates (app por_u_v (tenc t)) T)) (and (not (p t)) (evaluates (app por_u_v (tenc t)) F)) *)
  assert (A : eva (O (tenc (u (tenc t))) (tenc (v (tenc t))))). {
    eapply O_complete. now rewrite <-Hu,<-Hv.
  }
(* Goal: or (and (p t) (evaluates (app por_u_v (tenc t)) T)) (and (not (p t)) (evaluates (app por_u_v (tenc t)) F)) *)
  destruct (O_sound A) as [[B [? C]%evaluates_equiv] | [B [? C]%evaluates_equiv]].
(* Goal: iff (satis (app (H (tenc s) (tenc t))) n) (or (not (@eq (option term) (eval n s) (@None term))) (not (@eq (option term) (eval n t) (@None term)))) *)
  - left; split. now apply Hu.
(* Goal: proc (H (tenc s) (tenc t)) *)
    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)) (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) *)
(* Goal: equiv (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) (app (app O (tenc (app u (tenc t)))) (tenc (app v (tenc t)))) *)
    transitivity (((O ((App (tenc u) ( Q (tenc t))))) ((App (tenc v) (Q (tenc t)))))). unfold por_u_v. solveeq.
(* Goal: equiv (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) F *)
    now rewrite !Q_correct, !App_correct.
(* Goal: proc (H (tenc s) (tenc t)) *)
  - right; split. now apply Hv. 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)) (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) *)
(* Goal: equiv (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) (app (app O (tenc (app u (tenc t)))) (tenc (app v (tenc t)))) *)
    transitivity (((O ((App (tenc u) ( Q (tenc t))))) ((App (tenc v) (Q (tenc t)))))). unfold por_u_v; solveeq.
(* Goal: equiv (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) F *)
    now rewrite !Q_correct, !App_correct.
Qed.


(** ** Recognisable classes are closed under union *)

Lemma recognisable_union p q : recognisable p -> recognisable q -> recognisable (union p q).
Proof.
(* Goal: forall (_ : recognisable p) (_ : recognisable q), recognisable (union p q) *)
  intros [u [[lam_u cls_u] Hu]] [v [[lam_v cls_v] Hv]].
(* Goal: recognisable (union p q) *)
  unfold recognisable, union.
(* Goal: @ex term (fun u : term => and (proc u) (forall s : term, iff (or (p s) (q s)) (eva (app u (tenc s))))) *)
  exists (lambda (O ((App (tenc u) (Q 0))) ((App (tenc v) (Q 0))))).
(* Goal: proc (H (tenc s) (tenc t)) *)
  split; value. intros t.

(* Goal: iff (or (p t) (q t)) (eva (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))) *)
  rewrite Hu, Hv; unfold pi.

(* 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)) (app (app O (tenc (app u (tenc t)))) (tenc (app v (tenc t)))) *)
(* Goal: iff (or (eva (app u (tenc t))) (eva (app v (tenc t)))) (eva (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))) *)
  assert (H : (lambda (O ((App (tenc u)) (Q 0)) ((App (tenc v)) (Q 0)))) (tenc t) ≡ O (tenc (u (tenc t))) (tenc (v (tenc t)))). {
(* 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)) (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) *)
(* Goal: equiv (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) (app (app O (tenc (app u (tenc t)))) (tenc (app v (tenc t)))) *)
  transitivity (((O ((App (tenc u) ( Q (tenc t))))) ((App (tenc v) (Q (tenc t)))))). solveeq.
(* Goal: equiv (app (app O (app (app App (tenc u)) (app Q (tenc t)))) (app (app App (tenc v)) (app Q (tenc t)))) (app (app O (tenc (app u (tenc t)))) (tenc (app v (tenc t)))) *)
  now rewrite Q_correct, App_correct, App_correct.
  }
(* Goal: iff (satis (app (H (tenc s) (tenc t))) n) (or (not (@eq (option term) (eval n s) (@None term))) (not (@eq (option term) (eval n t) (@None term)))) *)
  rewrite H; split.
  - intros [A | A]; eapply O_complete; intuition.
  - intros A. eapply O_sound in A; intuition. 
Qed.
