Kleene-Post Theorem


From SyntheticComputability Require Import TuringReducibility.OracleComputability partial.
Require Import Lia List.
Import ListNotations.

Section Part.

(* Assumptions *)

Context {Part : partiality}.

Notation "R <<= S" := ( x y, R x y S x y) (at level 30).
Notation "R == S" := ( x y, R x y S x y) (at level 30).

Variable lenum : list bool .
Variable lenum' : list bool.
Hypothesis lenum_lenum' : s, lenum' (lenum s) = s.

Variable : Functional bool bool.
Hypothesis Xi_comp : n, OracleComputable ( n).
Hypothesis Xi_enum : F, OracleComputable F c, R, c R == F R.

Lemma Xi_func e p :
  functional p functional ( e p).
Proof.
  apply OracleComputable_functional. apply Xi_comp.
Qed.


Lemma Xi_bound e p n b :
   e p n b N, (q : bool Prop), ( n b, n < N p n b q n b) e q n b.
Proof.
  intros H. apply cont_to_cont in H as [L HL]; try apply Xi_comp.
  exists (S (list_max L)). intros q Hq. apply HL.
  intros n' b' Hn. apply Hq. apply list_max_spec in Hn. .
Qed.


Lemma Xi_mono e (p q : bool Prop) :
  p q e p e q.
Proof.
  intros H n b [N HN] % Xi_bound. apply HN. intros n' b' _. apply H.
Qed.


(* Prelims *)

Lemma lenum_inj s t :
  lenum s = lenum t s = t.
Proof.
  rewrite (lenum_lenum' s) at 2. rewrite (lenum_lenum' t) at 2. now intros .
Qed.


Definition char_rel' (P : Prop) : FunRel bool.
Proof.
  exists (char_rel P). apply char_rel_functional.
Defined.


Lemma nat_even_odd n :
  { k | n = 2 * k } + { k | n = S (2 * k) }.
Proof.
  induction n.
  - left. exists 0. reflexivity.
  - destruct IHn as [[k Hk]|[k Hk]].
    + right. exists k. .
    + left. exists (S k). .
Qed.


Definition bools_to_funrel (L : list bool) : FunRel bool.
Proof.
  exists ( n b nth_error L n = Some b).
  abstract (intros n ; congruence).
Defined.


Definition prefix (sigma tau : list bool) :=
   rho, = .

Lemma prefix_refl sigma :
  prefix .
Proof.
  exists nil. apply app_nil_r.
Qed.


Lemma prefix_trans s t u :
  prefix s t prefix t u prefix s u.
Proof.
  intros [t' ] [u' ]. exists (t' u'). apply app_assoc.
Qed.


Lemma prefix_dec s t :
  {prefix s t} + { prefix s t}.
Proof.
  induction s in t |- *.
  - left. exists t. reflexivity.
  - destruct t as [|[] t].
    + right. intros [t Ht]. cbn in Ht. congruence.
    + destruct a.
      * destruct (IHs t) as [H|H].
        -- left. destruct H as [u Hu]. exists u. cbn. congruence.
        -- right. intros [u Hu]. apply H. exists u. cbn in Hu. congruence.
      * right. intros [u Hu]. cbn in Hu. congruence.
    + destruct a.
      * right. intros [u Hu]. cbn in Hu. congruence.
      * destruct (IHs t) as [H|H].
        -- left. destruct H as [u Hu]. exists u. cbn. congruence.
        -- right. intros [u Hu]. apply H. exists u. cbn in Hu. congruence.
Qed.


Lemma prefix_length s t :
  prefix s t length s length t.
Proof.
  intros [u ]. rewrite app_length. .
Qed.


Lemma prefix_sub s t :
  prefix s t bools_to_funrel s bools_to_funrel t.
Proof.
  intros [u ] n b Hn. unfold bools_to_funrel. cbn in *. rewrite nth_error_app1; trivial.
  apply nth_error_Some. intros H. rewrite H in Hn. discriminate.
Qed.


(* Degree construction *)

Inductive sigtau : list bool list bool Prop :=
| base : sigtau 0 nil nil
| even_step1 e sigma tau rho b : sigtau (2 * e) prefix
                            ( rho' b, prefix lenum < lenum
                                         e (bools_to_funrel ) (length ) b)
                            e (bools_to_funrel ) (length ) b
                            sigtau (S (2 * e)) ( [negb b])
| even_step2 e sigma tau : sigtau (2 * e)
                        ( rho b, prefix e (bools_to_funrel ) (length ) b)
                        sigtau (S (2 * e)) ( [false])
| odd_step1 e sigma tau rho b : sigtau (S (2 * e)) prefix
                           ( rho' b, prefix lenum < lenum
                                         e (bools_to_funrel ) (length ) b)
                           e (bools_to_funrel ) (length ) b
                           sigtau (S (S (2 * e))) ( [negb b])
| odd_step2 e sigma tau : sigtau (S (2 * e))
                       ( rho b, prefix e (bools_to_funrel ) (length ) b)
                       sigtau (S (S (2 * e))) ( [false]) .

Definition A n :=
   k, s t, sigtau k s t nth_error s n = Some true.

Definition B n :=
   k, s t, sigtau k s t nth_error t n = Some true.

(* Properties of sigtau: functionality, totality, cumulativity, agreement, unboundedness *)

Lemma sigtau_fun n sigma tau sig' tau' :
  sigtau n sigtau n sig' = sig' = .
Proof.
  induction 1 in sig', |- *.
  - inversion 1; auto.
  - inversion 1; subst; try ; assert (e = ) as by .
    + apply IHsigtau in as [ ].
      destruct (PeanoNat.Nat.lt_total (lenum ) (lenum sig')) as [Hr|[Hr|Hr]].
      * exfalso. now apply ( b).
      * apply lenum_inj in Hr. subst. split; trivial. repeat f_equal.
        eapply Xi_func; eauto. apply the_func_proof.
      * exfalso. now apply ( sig' ).
    + apply IHsigtau in as [ ]. contradict . eauto.
  - inversion 1; subst; try ; assert (e = ) as by .
    + apply IHsigtau in as [ ]. contradict . eauto.
    + apply IHsigtau in as [ ]. tauto.
  - inversion 1; subst; try ; assert (e = ) as by .
    + apply IHsigtau in as [ ].
      destruct (PeanoNat.Nat.lt_total (lenum ) (lenum )) as [Hr|[Hr|Hr]].
      * exfalso. now apply ( b).
      * apply lenum_inj in Hr. subst. split; trivial. repeat f_equal.
        eapply Xi_func; eauto. apply the_func_proof.
      * exfalso. now apply ( ).
    + apply IHsigtau in as [ ]. contradict . eauto.
  - inversion 1; subst; try ; assert (e = ) as by .
    + apply IHsigtau in as [ ]. contradict . eauto.
    + apply IHsigtau in as [ ]. tauto.
Qed.


Lemma wf_ind (P : Prop) :
  ( n, ( k, k < n P k) P n) n, P n.
Proof.
  intros HI n. apply HI. induction n.
  - .
  - intros k H. apply HI. intros k' H'. apply IHn. .
Qed.


Definition DNLEM P :
   (P P).
Proof.
  tauto.
Qed.


Lemma least_doubleneg (P : Prop) :
  ( n, P n) n, P n k, k < n P k.
Proof.
  intros [n Hn]. induction n as [n IH] using wf_ind.
  intros HL. apply (@DNLEM ( k, k < n P k)). intros [[k Hk]|H].
  - apply (IH k); tauto.
  - apply HL. exists n. split; trivial. intros k . apply H. exists k. tauto.
Qed.


Lemma least_termination (f : Functional bool bool) sigma n :
  ( rho b, prefix f (bools_to_funrel ) n b)
   ( rho b, prefix f (bools_to_funrel ) n b
             rho' b, prefix lenum < lenum
                         f (bools_to_funrel ) n b).
Proof.
  intros .
  apply (@least_doubleneg ( k rho, k = lenum prefix b, f (bools_to_funrel ) n b)).
  - destruct as [[b H]]. exists (lenum ), . intuition eauto.
  - intros [k [[[ [H[b Hb]]]] H']]. apply . exists , b. repeat split; trivial.
    intros b'. intros . apply (H' (lenum )); eauto.
Qed.


Lemma sigtau_tot n :
   sigma tau, sigtau n .
Proof.
  induction n.
  - intros H. apply H. exists nil, nil. constructor.
  - intros H. apply IHn. intros ( & & Hn).
    destruct (nat_even_odd n) as [[e He]|[e He]].
    + apply (@DNLEM ( rho b, prefix e (bools_to_funrel ) (length ) b)).
      intros [Hr|Hr]; subst n.
      * apply (least_termination Hr). intros [[b Hb]]. apply H.
        exists , ( [negb b]). eapply even_step1; intuition eauto.
      * apply H. exists , ( [false]). apply (even_step2 Hn). firstorder.
    + apply (@DNLEM ( rho b, prefix e (bools_to_funrel ) (length ) b)).
      intros [Hr|Hr]; subst n.
      * apply (least_termination Hr). intros [[b Hb]]. apply H.
        exists ( [negb b]), . eapply odd_step1; intuition eauto.
      * apply H. exists ( [false]), . apply (odd_step2 Hn). firstorder.
Qed.


Lemma sigtau_step n sigma tau sig' tau' :
  sigtau n sigtau (S n) sig' prefix sig' prefix .
Proof.
  intros . inversion ; subst.
  - assert ( = = ) as [ ] by apply (sigtau_fun ).
    split; try tauto. now exists [negb b].
  - assert (sig' = = ) as [ ] by apply (sigtau_fun ).
    split; try apply prefix_refl. now exists [false].
  - assert ( = = ) as [ ] by apply (sigtau_fun ).
    split; try tauto. now exists [negb b].
  - assert ( = = ) as [ ] by apply (sigtau_fun ).
    split; try apply prefix_refl. now exists [false].
Qed.


Lemma sigtau_cum n k sigma tau sig' tau' :
  sigtau n n k sigtau k sig' prefix sig' prefix .
Proof.
  intros Hn H Hk. induction H in sig', , Hk |- *.
  - assert (sig' = = ) as [ ] by apply (sigtau_fun Hk Hn). split; apply prefix_refl.
  - destruct (prefix_dec sig') as [Hs|Hs], (prefix_dec ) as [Ht|Ht]; try tauto; exfalso.
    all: apply (@sigtau_tot m); intros (s & t & Hst); eapply sigtau_step in Hk; eauto.
    all: apply IHle in Hst; intuition eauto using prefix_trans.
Qed.


Lemma sigma_agree k s t k' s' t' n b b' :
  sigtau k s t sigtau k' s' t' bools_to_funrel s n b bools_to_funrel s' n b' b = b'.
Proof.
  intros Hk Hk' Hb Hb'. assert (k k' k' k) as [H|H] by .
  - apply (prefix_sub (t:=s')) in Hb; try apply (sigtau_cum Hk H Hk'). apply (the_func_proof Hb Hb').
  - apply (prefix_sub (t:=s)) in Hb'; try apply (sigtau_cum Hk' H Hk). apply (the_func_proof Hb Hb').
Qed.


Lemma tau_agree k s t k' s' t' n b b' :
  sigtau k s t sigtau k' s' t' bools_to_funrel t n b bools_to_funrel t' n b' b = b'.
Proof.
  intros Hk Hk' Hb Hb'. assert (k k' k' k) as [H|H] by .
  - apply (prefix_sub (t:=t')) in Hb; try apply (sigtau_cum Hk H Hk'). apply (the_func_proof Hb Hb').
  - apply (prefix_sub (t:=t)) in Hb'; try apply (sigtau_cum Hk' H Hk). apply (the_func_proof Hb Hb').
Qed.


Lemma sigtau_length n s t :
  sigtau (2 * n) s t n length s n length t.
Proof.
  induction n in s, t |- *; cbn; try .
  assert (S (n + S (n + 0)) = S (S (2 * n))) as by .
  inversion 1; subst; try ; inversion ; subst; try ; assert (n = ) as by .
  - apply IHn in . split.
    + rewrite app_length. cbn. apply prefix_length in . .
    + apply prefix_length in . rewrite app_length in . cbn in . .
  - apply IHn in . split.
    + rewrite app_length. cbn. .
    + apply prefix_length in . rewrite app_length in . cbn in . .
  - apply IHn in . split.
    + rewrite app_length. cbn. apply prefix_length in . .
    + rewrite app_length. cbn. .
  - apply IHn in . split.
    + rewrite app_length. cbn. .
    + rewrite app_length. cbn. .
Qed.


Lemma sigtau_length' k n s t :
  2 * n k sigtau k s t n length s n length t.
Proof.
  intros Hk Hst. destruct (Compare_dec.le_dec n (length s)) as [H|H], (Compare_dec.le_dec n (length t)) as [H'|H'].
  all: try tauto. all: exfalso; apply (@sigtau_tot (2 * n)); intros (s' & t' & Hst').
  - apply H'. assert (length t' length t) by apply prefix_length, (sigtau_cum Hst' Hk Hst).
    apply sigtau_length in Hst'. .
  - apply H. assert (length s' length s) by apply prefix_length, (sigtau_cum Hst' Hk Hst).
    apply sigtau_length in Hst'. .
  - apply H'. assert (length t' length t) by apply prefix_length, (sigtau_cum Hst' Hk Hst).
    apply sigtau_length in Hst'. .
Qed.


(* Obtained functional relations *)

Definition sigmas (n : ) : FunRel bool.
Proof.
  exists ( k b sigma tau, sigtau n bools_to_funrel k b).
  intros k [] [] ; trivial; exfalso.
  all: apply (@sigtau_tot n); intros ( & & H).
  - enough (true = false) by congruence. apply (the_func_proof ( H) ( H)).
  - enough (false = true) by congruence. apply (the_func_proof ( H) ( H)).
Defined.


Definition taus (n : ) : FunRel bool.
Proof.
  exists ( k b sigma tau, sigtau n bools_to_funrel k b).
  intros k [] [] ; trivial; exfalso.
  all: apply (@sigtau_tot n); intros ( & & H).
  - enough (true = false) by congruence. apply (the_func_proof ( H) ( H)).
  - enough (false = true) by congruence. apply (the_func_proof ( H) ( H)).
Defined.


Lemma sigtau_sigmas s t n :
  sigtau n s t bools_to_funrel s == sigmas n.
Proof.
  intros Hn k b. split; intros H.
  - now intros s' t' [ ] % (sigtau_fun Hn).
  - apply (H s t Hn).
Qed.


Lemma sigtau_taus s t n :
  sigtau n s t bools_to_funrel t == taus n.
Proof.
  intros Hn k b. split; intros H.
  - now intros s' t' [ ] % (sigtau_fun Hn).
  - apply (H s t Hn).
Qed.


(* Simple properties of degrees A and B *)

Lemma A_sigmas n sigma tau :
  sigtau n bools_to_funrel char_rel A.
Proof.
  intros Hn k b Hk. destruct b; cbn.
  - exists n. now intros s t [ ] % (sigtau_fun Hn).
  - intros [l Hl]. apply (@sigtau_tot l). intros (s & t & Hs).
    enough (false = true) by congruence. apply (sigma_agree Hn Hs (n:=k)).
    + apply Hk.
    + eapply Hl, Hs.
Qed.


Lemma B_taus n sigma tau :
  sigtau n bools_to_funrel char_rel B.
Proof.
  intros Hn k b Hk. destruct b; cbn.
  - exists n. now intros s t [ ] % (sigtau_fun Hn).
  - intros [l Hl]. apply (@sigtau_tot l). intros (s & t & Hs).
    enough (false = true) by congruence. apply (tau_agree Hn Hs (n:=k)).
    + apply Hk.
    + eapply Hl, Hs.
Qed.


Lemma A_tot n :
   b, char_rel A n b.
Proof.
  intros H. apply (@sigtau_tot (2 * (S n))).
  intros (s & t & Hst). destruct (sigtau_length Hst) as [Hs _].
  destruct (nth_error s n) as [|] eqn : Hn.
  - apply H. exists b. destruct b; cbn.
    + exists (2 * (S n)). intros s' t' Hst'. apply (sigtau_fun Hst) in Hst' as [ ]. apply Hn.
    + intros [k Hk]. apply (@sigtau_tot k). intros (s' & t' & Hst').
      specialize (Hk s' t' Hst'). enough (true = false) by congruence.
      apply (sigma_agree Hst' Hst (n:=n)); eauto.
  - eapply nth_error_Some; eauto.
Qed.


Lemma B_tot n :
   b, char_rel B n b.
Proof.
  intros H. apply (@sigtau_tot (2 * (S n))).
  intros (s & t & Hst). destruct (sigtau_length Hst) as [_ Ht].
  destruct (nth_error t n) as [|] eqn : Hn.
  - apply H. exists b. destruct b; cbn.
    + exists (2 * (S n)). intros s' t' Hst'. apply (sigtau_fun Hst) in Hst' as [ ]. apply Hn.
    + intros [k Hk]. apply (@sigtau_tot k). intros (s' & t' & Hst').
      specialize (Hk s' t' Hst'). enough (true = false) by congruence.
      apply (tau_agree Hst' Hst (n:=n)); eauto.
  - eapply nth_error_Some; eauto.
Qed.


(* Remaining verification using continuity *)

Lemma A_agree N k n b :
   2 * N k n < N char_rel' A n b sigmas k n b.
Proof.
  intros Hk Hn. split; intros H.
  - intros s t Hst. unfold bools_to_funrel. cbn. destruct nth_error as [|] eqn : Hs'.
    + f_equal. symmetry. now apply (the_func_proof H), (A_sigmas Hst).
    + exfalso. eapply nth_error_Some; eauto. apply (sigtau_length' Hk) in Hst. .
  - destruct b; cbn.
    + exists k. now intros s t Hst % H.
    + intros [l Hl]. apply (@sigtau_tot l). intros (s & t & Hst).
      apply (@sigtau_tot k). intros (s' & t' & Hst').
      enough (false = true) by congruence. apply (sigma_agree Hst' Hst (n:=n)).
      * now apply (sigtau_sigmas Hst').
      * eapply Hl, Hst.
Qed.


Lemma A_prefix e n b :
   e (char_rel' A) n b k, e (sigmas k) n b.
Proof.
  intros He. destruct (Xi_bound He) as [N HN]. exists (2 * N).
  intros Hn. apply (@sigtau_tot (2 * N)). intros (s & t & Hst).
  apply Hn. apply HN. intros k b'. now apply A_agree.
Qed.


Lemma A_mono e k sigma tau n b :
  sigtau k e (bools_to_funrel ) n b e (char_rel' A) n b.
Proof.
  intros . destruct (Xi_bound ) as [N HN].
  intros Hr. apply (@sigtau_tot (k + 2 * N)). intros (s & t & Hst).
  apply Hr, HN. intros n' b' _. apply (A_sigmas ).
Qed.


Lemma B_disc e sigma tau sig' tau' b :
  sigtau (2 * e) sigtau (S (2 * e)) sig'
   char_rel' B (length ) b e (char_rel' A) (length ) b.
Proof.
  intros H. inversion 1; subst; try .
  - intros HB HA. assert (e = ) as by .
    assert ( = = ) as [ ] by apply (sigtau_fun H ). assert (b = negb ) as .
    { apply (the_func_proof HB), (B_taus ). cbn. now rewrite nth_error_app2, PeanoNat.Nat.sub_diag. }
    apply (A_mono ) in . apply . intros .
    apply (Bool.no_fixpoint_negb ). eapply Xi_func; eauto. apply the_func_proof.
  - intros _ [k Hk] % A_prefix. apply Hk. intros Hk'. assert (e = ) as by .
    assert ( = sig' = ) as [ ] by apply (sigtau_fun H ).
    apply (@sigtau_tot k). intros (s & t & Hst).
    assert (k 2 * e 2 * e k) as [H'|H'] by .
    + apply . exists , b. split; try apply prefix_refl. eapply Xi_mono; try apply Hk'.
      intros l b' Hl. apply prefix_sub with s; try apply (sigtau_cum Hst H' H).
      apply (sigtau_sigmas Hst), Hl.
    + apply . exists s, b. split; try apply (sigtau_cum H H' Hst).
      eapply Xi_mono; try apply Hk'. intros n' b'. apply (sigtau_sigmas Hst).
Qed.


Lemma Kleene_Post1 e :
   char_rel' B e (char_rel' A).
Proof.
  intros H. apply (@sigtau_tot (2 * e)). intros ( & & Hst).
  apply (@sigtau_tot (S (2 * e))). intros (sig' & & Hst').
  specialize (H (length )). apply (@B_tot (length )). intros [b Hb].
  specialize (H b). apply (B_disc Hst Hst' Hb). apply H, Hb.
Qed.


Lemma B_agree N k n b :
   2 * N k n < N char_rel' B n b taus k n b.
Proof.
  intros Hk Hn. split; intros H.
  - intros s t Hst. unfold bools_to_funrel. cbn. destruct nth_error as [|] eqn : Hs'.
    + f_equal. symmetry. now apply (the_func_proof H), (B_taus Hst).
    + exfalso. eapply nth_error_Some; eauto. apply (sigtau_length' Hk) in Hst. .
  - destruct b; cbn.
    + exists k. now intros s t Hst % H.
    + intros [l Hl]. apply (@sigtau_tot l). intros (s & t & Hst).
      apply (@sigtau_tot k). intros (s' & t' & Hst').
      enough (false = true) by congruence. apply (tau_agree Hst' Hst (n:=n)).
      * now apply (sigtau_taus Hst').
      * eapply Hl, Hst.
Qed.


Lemma B_prefix e n b :
   e (char_rel' B) n b k, e (taus k) n b.
Proof.
  intros He. destruct (Xi_bound He) as [N HN]. exists (2 * N).
  intros Hn. apply (@sigtau_tot (2 * N)). intros (s & t & Hst).
  apply Hn. apply HN. intros k b'. now apply B_agree.
Qed.


Lemma B_mono e k sigma tau n b :
  sigtau k e (bools_to_funrel ) n b e (char_rel' B) n b.
Proof.
  intros . destruct (Xi_bound ) as [N HN].
  intros Hr. apply (@sigtau_tot (k + 2 * N)). intros (s & t & Hst).
  apply Hr, HN. intros n' b' _. apply (B_taus ).
Qed.


Lemma A_disc e sigma tau sig' tau' b :
  sigtau (S (2 * e)) sigtau (S (S (2 * e))) sig'
   char_rel' A (length ) b e (char_rel' B) (length ) b.
Proof.
  intros H. inversion 1; subst; try .
  - intros HB HA. assert (e = ) as by .
    assert ( = = ) as [ ] by apply (sigtau_fun H ). assert (b = negb ) as .
    { apply (the_func_proof HB), (A_sigmas ). cbn. now rewrite nth_error_app2, PeanoNat.Nat.sub_diag. }
    apply (B_mono ) in . apply . intros .
    apply (Bool.no_fixpoint_negb ). eapply Xi_func; eauto. apply the_func_proof.
  - intros _ [k Hk] % B_prefix. apply Hk. intros Hk'. assert (e = ) as by .
    assert ( = = ) as [ ] by apply (sigtau_fun H ).
    apply (@sigtau_tot k). intros (s & t & Hst).
    assert (k S (2 * e) S (2 * e) k) as [H'|H'] by .
    + apply . exists , b. split; try apply prefix_refl. eapply Xi_mono; try apply Hk'.
      intros l b' Hl. apply prefix_sub with t; try apply (sigtau_cum Hst H' H).
      apply (sigtau_taus Hst), Hl.
    + apply . exists t, b. split; try apply (sigtau_cum H H' Hst).
      eapply Xi_mono; try apply Hk'. intros n' b'. apply (sigtau_taus Hst).
Qed.


Lemma Kleene_Post2 e :
   char_rel' A e (char_rel' B).
Proof.
  intros H. apply (@sigtau_tot (S (2 * e))). intros ( & & Hst).
  apply (@sigtau_tot (S (S (2 * e)))). intros (sig' & & Hst').
  specialize (H (length )). apply (@A_tot (length )). intros [b Hb].
  specialize (H b). apply (A_disc Hst Hst' Hb). apply H, Hb.
Qed.


(* Main result *)

Theorem KleenePost :
   (A B : Prop), (A ⪯ᴛ B) (B ⪯ᴛ A).
Proof.
  exists A, B. split.
  - intros [F [ ]]. destruct (Xi_enum ) as [e He].
    apply (Kleene_Post2 (e:=e)). intros n b. cbn. now rewrite , He.
  - intros [F [ ]]. destruct (Xi_enum ) as [e He].
    apply (Kleene_Post1 (e:=e)). intros n b. cbn. now rewrite , He.
Qed.


Print Assumptions KleenePost.

End Part.