From SyntheticComputability Require Import TuringReducibility.OracleComputability partial.
Require Import Lia List.
Import ListNotations.
Section Part.
(* Assumptions *)
Context {Part : partiality}.
Notation "R <<= S" := (forall x y, R x y -> S x y) (at level 30).
Notation "R == S" := (forall x y, R x y <-> S x y) (at level 30).
Variable lenum : list bool -> nat.
Variable lenum' : nat -> list bool.
Hypothesis lenum_lenum' : forall s, lenum' (lenum s) = s.
Variable Xi : nat -> Functional nat bool nat bool.
Hypothesis Xi_comp : forall n, OracleComputable (Xi n).
Hypothesis Xi_enum : forall F, OracleComputable F -> exists c, forall R, Xi c R == F R.
Lemma Xi_func e p :
functional p -> functional (Xi e p).
Proof.
apply OracleComputable_functional. apply Xi_comp.
Qed.
Lemma Xi_bound e p n b :
Xi e p n b -> exists N, forall (q : nat -> bool -> Prop), (forall n b, n < N -> p n b -> q n b) -> Xi 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. lia.
Qed.
Lemma Xi_mono e (p q : nat -> bool -> Prop) :
p <<= q -> Xi e p <<= Xi 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 : nat -> Prop) : FunRel nat 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. lia.
+ left. exists (S k). lia.
Qed.
Definition bools_to_funrel (L : list bool) : FunRel nat bool.
Proof.
exists (fun n b => nth_error L n = Some b).
abstract (intros n H1 H2; congruence).
Defined.
Definition prefix (sigma tau : list bool) :=
exists rho, sigma ++ rho = tau.
Lemma prefix_refl sigma :
prefix sigma sigma.
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. lia.
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 : nat -> list bool -> list bool -> Prop :=
| base : sigtau 0 nil nil
| even_step1 e sigma tau rho b : sigtau (2 * e) sigma tau -> prefix sigma rho
-> (forall rho' b, prefix sigma rho' -> lenum rho' < lenum rho
-> ~ Xi e (bools_to_funrel rho') (length tau) b)
-> Xi e (bools_to_funrel rho) (length tau) b
-> sigtau (S (2 * e)) rho (tau ++ [negb b])
| even_step2 e sigma tau : sigtau (2 * e) sigma tau
-> (~ exists rho b, prefix sigma rho /\ Xi e (bools_to_funrel rho) (length tau) b)
-> sigtau (S (2 * e)) sigma (tau ++ [false])
| odd_step1 e sigma tau rho b : sigtau (S (2 * e)) sigma tau -> prefix tau rho
-> (forall rho' b, prefix tau rho' -> lenum rho' < lenum rho
-> ~ Xi e (bools_to_funrel rho') (length sigma) b)
-> Xi e (bools_to_funrel rho) (length sigma) b
-> sigtau (S (S (2 * e))) (sigma ++ [negb b]) rho
| odd_step2 e sigma tau : sigtau (S (2 * e)) sigma tau
-> (~ exists rho b, prefix tau rho /\ Xi e (bools_to_funrel rho) (length sigma) b)
-> sigtau (S (S (2 * e))) (sigma ++ [false]) tau.
Definition A n :=
exists k, forall s t, sigtau k s t -> nth_error s n = Some true.
Definition B n :=
exists k, forall 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 sigma tau -> sigtau n sig' tau' -> sigma = sig' /\ tau = tau'.
Proof.
induction 1 in sig', tau' |- *.
- inversion 1; auto.
- inversion 1; subst; try lia; assert (e = e0) as -> by lia.
+ apply IHsigtau in H5 as [-> ->].
destruct (PeanoNat.Nat.lt_total (lenum rho) (lenum sig')) as [Hr|[Hr|Hr]].
* exfalso. now apply (H7 rho b).
* apply lenum_inj in Hr. subst. split; trivial. repeat f_equal.
eapply Xi_func; eauto. apply the_func_proof.
* exfalso. now apply (H1 sig' b0).
+ apply IHsigtau in H5 as [-> ->]. contradict H6. eauto.
- inversion 1; subst; try lia; assert (e = e0) as -> by lia.
+ apply IHsigtau in H3 as [-> ->]. contradict H0. eauto.
+ apply IHsigtau in H3 as [-> ->]. tauto.
- inversion 1; subst; try lia; assert (e = e0) as -> by lia.
+ apply IHsigtau in H5 as [-> ->].
destruct (PeanoNat.Nat.lt_total (lenum rho) (lenum tau')) as [Hr|[Hr|Hr]].
* exfalso. now apply (H7 rho b).
* apply lenum_inj in Hr. subst. split; trivial. repeat f_equal.
eapply Xi_func; eauto. apply the_func_proof.
* exfalso. now apply (H1 tau' b0).
+ apply IHsigtau in H5 as [-> ->]. contradict H6. eauto.
- inversion 1; subst; try lia; assert (e = e0) as -> by lia.
+ apply IHsigtau in H3 as [-> ->]. contradict H0. eauto.
+ apply IHsigtau in H3 as [-> ->]. tauto.
Qed.
Lemma wf_ind (P : nat -> Prop) :
(forall n, (forall k, k < n -> P k) -> P n) -> forall n, P n.
Proof.
intros HI n. apply HI. induction n.
- lia.
- intros k H. apply HI. intros k' H'. apply IHn. lia.
Qed.
Definition DNLEM P :
~ ~ (P \/ ~ P).
Proof.
tauto.
Qed.
Lemma least_doubleneg (P : nat -> Prop) :
(exists n, P n) -> ~ ~ exists n, P n /\ forall k, k < n -> ~ P k.
Proof.
intros [n Hn]. induction n as [n IH] using wf_ind.
intros HL. apply (@DNLEM (exists k, k < n /\ P k)). intros [[k Hk]|H].
- apply (IH k); tauto.
- apply HL. exists n. split; trivial. intros k H1 H2. apply H. exists k. tauto.
Qed.
Lemma least_termination (f : Functional nat bool nat bool) sigma n :
(exists rho b, prefix sigma rho /\ f (bools_to_funrel rho) n b) ->
~ ~ (exists rho b, prefix sigma rho /\ f (bools_to_funrel rho) n b
/\ forall rho' b, prefix sigma rho' -> lenum rho' < lenum rho
-> ~ f (bools_to_funrel rho') n b).
Proof.
intros H1 H2.
apply (@least_doubleneg (fun k => exists rho, k = lenum rho /\ prefix sigma rho /\ exists b, f (bools_to_funrel rho) n b)).
- destruct H1 as [rho[b H]]. exists (lenum rho), rho. intuition eauto.
- intros [k [[rho[-> [H[b Hb]]]] H']]. apply H2. exists rho, b. repeat split; trivial.
intros rho' b'. intros H3 H4 H5. apply (H' (lenum rho')); eauto.
Qed.
Lemma sigtau_tot n :
~ ~ exists sigma tau, sigtau n sigma tau.
Proof.
induction n.
- intros H. apply H. exists nil, nil. constructor.
- intros H. apply IHn. intros (sigma & tau & Hn).
destruct (nat_even_odd n) as [[e He]|[e He]].
+ apply (@DNLEM (exists rho b, prefix sigma rho /\ Xi e (bools_to_funrel rho) (length tau) b)).
intros [Hr|Hr]; subst n.
* apply (least_termination Hr). intros [rho[b Hb]]. apply H.
exists rho, (tau ++ [negb b]). eapply even_step1; intuition eauto.
* apply H. exists sigma, (tau ++ [false]). apply (even_step2 Hn). firstorder.
+ apply (@DNLEM (exists rho b, prefix tau rho /\ Xi e (bools_to_funrel rho) (length sigma) b)).
intros [Hr|Hr]; subst n.
* apply (least_termination Hr). intros [rho[b Hb]]. apply H.
exists (sigma ++ [negb b]), rho. eapply odd_step1; intuition eauto.
* apply H. exists (sigma ++ [false]), tau. apply (odd_step2 Hn). firstorder.
Qed.
Lemma sigtau_step n sigma tau sig' tau' :
sigtau n sigma tau -> sigtau (S n) sig' tau' -> prefix sigma sig' /\ prefix tau tau'.
Proof.
intros H1 H2. inversion H2; subst.
- assert (sigma0 = sigma /\ tau0 = tau) as [-> ->] by apply (sigtau_fun H0 H1).
split; try tauto. now exists [negb b].
- assert (sig' = sigma /\ tau0 = tau) as [-> ->] by apply (sigtau_fun H0 H1).
split; try apply prefix_refl. now exists [false].
- assert (sigma0 = sigma /\ tau0 = tau) as [-> ->] by apply (sigtau_fun H0 H1).
split; try tauto. now exists [negb b].
- assert (sigma0 = sigma /\ tau' = tau) as [-> ->] by apply (sigtau_fun H0 H1).
split; try apply prefix_refl. now exists [false].
Qed.
Lemma sigtau_cum n k sigma tau sig' tau' :
sigtau n sigma tau -> n <= k -> sigtau k sig' tau' -> prefix sigma sig' /\ prefix tau tau'.
Proof.
intros Hn H Hk. induction H in sig', tau', Hk |- *.
- assert (sig' = sigma /\ tau' = tau) as [-> ->] by apply (sigtau_fun Hk Hn). split; apply prefix_refl.
- destruct (prefix_dec sigma sig') as [Hs|Hs], (prefix_dec tau tau') 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 lia.
- 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 lia.
- 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 lia.
assert (S (n + S (n + 0)) = S (S (2 * n))) as -> by lia.
inversion 1; subst; try lia; inversion H1; subst; try lia; assert (n = e0) as <- by lia.
- apply IHn in H6. split.
+ rewrite app_length. cbn. apply prefix_length in H7. lia.
+ apply prefix_length in H2. rewrite app_length in H2. cbn in H2. lia.
- apply IHn in H6. split.
+ rewrite app_length. cbn. lia.
+ apply prefix_length in H2. rewrite app_length in H2. cbn in H2. lia.
- apply IHn in H4. split.
+ rewrite app_length. cbn. apply prefix_length in H5. lia.
+ rewrite app_length. cbn. lia.
- apply IHn in H4. split.
+ rewrite app_length. cbn. lia.
+ rewrite app_length. cbn. lia.
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'. lia.
- apply H. assert (length s' <= length s) by apply prefix_length, (sigtau_cum Hst' Hk Hst).
apply sigtau_length in Hst'. lia.
- apply H'. assert (length t' <= length t) by apply prefix_length, (sigtau_cum Hst' Hk Hst).
apply sigtau_length in Hst'. lia.
Qed.
(* Obtained functional relations *)
Definition sigmas (n : nat) : FunRel nat bool.
Proof.
exists (fun k b => forall sigma tau, sigtau n sigma tau -> bools_to_funrel sigma k b).
intros k [] [] H1 H2; trivial; exfalso.
all: apply (@sigtau_tot n); intros (sigma & tau & H).
- enough (true = false) by congruence. apply (the_func_proof (H1 sigma tau H) (H2 sigma tau H)).
- enough (false = true) by congruence. apply (the_func_proof (H1 sigma tau H) (H2 sigma tau H)).
Defined.
Definition taus (n : nat) : FunRel nat bool.
Proof.
exists (fun k b => forall sigma tau, sigtau n sigma tau -> bools_to_funrel tau k b).
intros k [] [] H1 H2; trivial; exfalso.
all: apply (@sigtau_tot n); intros (sigma & tau & H).
- enough (true = false) by congruence. apply (the_func_proof (H1 sigma tau H) (H2 sigma tau H)).
- enough (false = true) by congruence. apply (the_func_proof (H1 sigma tau H) (H2 sigma tau 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 sigma tau -> bools_to_funrel sigma <<= 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 sigma tau -> bools_to_funrel tau <<= 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 :
~ ~ exists 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 :
~ ~ exists 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. lia.
- 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 :
Xi e (char_rel' A) n b -> exists k, ~ ~ Xi 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 sigma tau -> Xi e (bools_to_funrel sigma) n b -> ~ ~ Xi e (char_rel' A) n b.
Proof.
intros H1 H2. destruct (Xi_bound H2) as [N HN].
intros Hr. apply (@sigtau_tot (k + 2 * N)). intros (s & t & Hst).
apply Hr, HN. intros n' b' _. apply (A_sigmas H1).
Qed.
Lemma B_disc e sigma tau sig' tau' b :
sigtau (2 * e) sigma tau -> sigtau (S (2 * e)) sig' tau'
-> char_rel' B (length tau) b -> ~ Xi e (char_rel' A) (length tau) b.
Proof.
intros H. inversion 1; subst; try lia.
- intros HB HA. assert (e = e0) as <- by lia.
assert (sigma = sigma0 /\ tau = tau0) as [<- <-] by apply (sigtau_fun H H2). assert (b = negb b0) as ->.
{ apply (the_func_proof HB), (B_taus H0). cbn. now rewrite nth_error_app2, PeanoNat.Nat.sub_diag. }
apply (A_mono H0) in H5. apply H5. intros H5'.
apply (Bool.no_fixpoint_negb b0). eapply Xi_func; eauto. apply the_func_proof.
- intros _ [k Hk] % A_prefix. apply Hk. intros Hk'. assert (e = e0) as <- by lia.
assert (sigma = sig' /\ tau = tau0) as [<- <-] by apply (sigtau_fun H H2).
apply (@sigtau_tot k). intros (s & t & Hst).
assert (k <= 2 * e \/ 2 * e <= k) as [H'|H'] by lia.
+ apply H3. exists sigma, 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 H3. 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 <<= Xi e (char_rel' A).
Proof.
intros H. apply (@sigtau_tot (2 * e)). intros (sigma & tau & Hst).
apply (@sigtau_tot (S (2 * e))). intros (sig' & tau' & Hst').
specialize (H (length tau)). apply (@B_tot (length tau)). 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. lia.
- 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 :
Xi e (char_rel' B) n b -> exists k, ~ ~ Xi 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 sigma tau -> Xi e (bools_to_funrel tau) n b -> ~ ~ Xi e (char_rel' B) n b.
Proof.
intros H1 H2. destruct (Xi_bound H2) as [N HN].
intros Hr. apply (@sigtau_tot (k + 2 * N)). intros (s & t & Hst).
apply Hr, HN. intros n' b' _. apply (B_taus H1).
Qed.
Lemma A_disc e sigma tau sig' tau' b :
sigtau (S (2 * e)) sigma tau -> sigtau (S (S (2 * e))) sig' tau'
-> char_rel' A (length sigma) b -> ~ Xi e (char_rel' B) (length sigma) b.
Proof.
intros H. inversion 1; subst; try lia.
- intros HB HA. assert (e = e0) as <- by lia.
assert (sigma = sigma0 /\ tau = tau0) as [<- <-] by apply (sigtau_fun H H2). assert (b = negb b0) as ->.
{ apply (the_func_proof HB), (A_sigmas H0). cbn. now rewrite nth_error_app2, PeanoNat.Nat.sub_diag. }
apply (B_mono H0) in H5. apply H5. intros H5'.
apply (Bool.no_fixpoint_negb b0). eapply Xi_func; eauto. apply the_func_proof.
- intros _ [k Hk] % B_prefix. apply Hk. intros Hk'. assert (e = e0) as <- by lia.
assert (sigma = sigma0 /\ tau = tau') as [<- <-] by apply (sigtau_fun H H2).
apply (@sigtau_tot k). intros (s & t & Hst).
assert (k <= S (2 * e) \/ S (2 * e) <= k) as [H'|H'] by lia.
+ apply H3. exists tau, 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 H3. 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 <<= Xi e (char_rel' B).
Proof.
intros H. apply (@sigtau_tot (S (2 * e))). intros (sigma & tau & Hst).
apply (@sigtau_tot (S (S (2 * e)))). intros (sig' & tau' & Hst').
specialize (H (length sigma)). apply (@A_tot (length sigma)). intros [b Hb].
specialize (H b). apply (A_disc Hst Hst' Hb). apply H, Hb.
Qed.
(* Main result *)
Theorem KleenePost :
exists (A B : nat -> Prop), ~ (A ⪯ᴛ B) /\ ~ (B ⪯ᴛ A).
Proof.
exists A, B. split.
- intros [F [HF1 HF2]]. destruct (Xi_enum HF1) as [e He].
apply (Kleene_Post2 (e:=e)). intros n b. cbn. now rewrite HF2, He.
- intros [F [HF1 HF2]]. destruct (Xi_enum HF1) as [e He].
apply (Kleene_Post1 (e:=e)). intros n b. cbn. now rewrite HF2, He.
Qed.
Print Assumptions KleenePost.
End Part.