(** Arbitrarily long common prefixes with opposite halting outcomes for
    1RB0LD_0RC1RA_1LD1RC_1LE0RF_---1LA_1LF0LA.
    The configurations are constructed inputs; no blank-start claim is made.
    AI assistance: this proof sketch, the scripts and the checks were
    produced with the help of GPT-6 Astra (OpenAI). *)

From BusyCoq Require Import Individual62.
From AstraLocal Require Import LocalRules LocalSweep.
Require Import Lia List.
Open Scope list.

Lemma C_triples l r n :
  l {{C}}> [1;1;1]^^n *> r -->*
  l <* [1;1;1]^^n {{C}}> r.
Proof. shift_rule. intros. es. Qed.

Lemma first_reflection_bridge l r :
  l {{C}}> [1;0;1;1;1;1;0;0] *> r -->+
  l <* <[1;1;0] {{C}}> [1;1;1;1;1] *> r.
Proof. es. Qed.

(** The input is 1^(3q+1)00, with C on its first cell.  The endpoint
    scans the immediately preceding cell in A; both exterior streams
    are arbitrary.  Triple blocks consist entirely of ones. *)
Lemma short_A_exit l r q :
  l {{C}}> [1;1;1]^^q *> [1;0;0] *> r -->+
  l <{{A}} [0;1;1]^^q *> [1;1;1] *> r.
Proof.
  follow C_triples.
  follow10 (C_first_double_zero [] scan_nil).
  apply A_triples.
Qed.

Lemma triples_one n r :
  [1;1;1]^^n *> [1] *> r = [1] *> [1;1;1]^^n *> r.
Proof.
  induction n; [reflexivity |].
  change ([1;1;1] *> ([1;1;1]^^n *> [1] *> r) =
    [1;1;1;1] *> [1;1;1]^^n *> r).
  rewrite IHn. reflexivity.
Qed.

Lemma two_reflection_bridge l r m :
  l {{C}}> [1;0;1;1;1;1;0;0] *> [1;1;1]^^m *> [0;0] *> r -->+
  l <* [1] <{{A}} [1;1;0] *> [0;1;1]^^(S m) *> [1;1;1] *> r.
Proof.
  follow10 first_reflection_bridge.
  change (l <* <[1;1;0] {{C}}>
    [1;1] *> [1;1;1] *> [1;1;1]^^m *> [0;0] *> r -->*
    l <* [1] <{{A}} [1;1;0] *> [0;1;1]^^(S m) *> [1;1;1] *> r).
  rewrite <- lpow_shift'.
  follow100 C_1.
  follow100 C_1.
  follow C_triples.
  follow100 C_1.
  follow100 C_1.
  follow100 (C_first_double_zero [] scan_nil).
  change ([1] *> [1] *> [1;1;1]^^m *> [1;1;0;1;1] *> l
    <{{A}} [1;1;1] *> r -->*
    l <* [1] <{{A}} [1;1;0] *> [0;1;1]^^(S m) *> [1;1;1] *> r).
  rewrite <- (triples_one m ([1;1;0;1;1] *> l)).
  rewrite <- (triples_one m ([1] *> [1;1;0;1;1] *> l)).
  follow A_triples.
  rewrite lpow_S, Str_app_assoc.
  follow100 A_111.
  apply progress_evstep, A_101.
Qed.

(** The input is 1^(3q+1)0 1111 00 1^(3m)00.  The endpoint scans the
    immediately preceding cell in D, with the displayed zero on its right.
    This includes the zero-parameter cases as well. *)
Lemma long_D_exit l r q m :
  l {{C}}> [1;1;1]^^q *> [1;0;1;1;1;1;0;0] *>
    [1;1;1]^^m *> [0;0] *> r -->+
  l <{{D}} [0] *> [0;1;1]^^q *> [1;1;0] *>
    [0;1;1]^^(S m) *> [1;1;1] *> r.
Proof.
  follow C_triples.
  follow10 two_reflection_bridge.
  rewrite <- triples_one.
  follow A_triples.
  es.
Qed.

(** Give the boundary cell the value one and put blanks farther left.
    The A endpoint halts; the D endpoint escapes through the F blank sweep. *)
Lemma short_halts r q :
  halts tm (0inf <* [1] {{C}}> [1;1;1]^^q *> [1;0;0] *> r).
Proof.
  eapply halts_evstep with
    (c' := 0inf <* [1] <{{A}} [0;1;1]^^q *> [1;1;1] *> r).
  - exact (A_zero_prefix_halt ([0;1;1]^^q *> [1;1;1] *> r)).
  - apply progress_evstep, short_A_exit.
Qed.

Lemma long_nonhalts r q m :
  ~halts tm (0inf <* [1] {{C}}> [1;1;1]^^q *>
    [1;0;1;1;1;1;0;0] *> [1;1;1]^^m *> [0;0] *> r).
Proof.
  eapply multistep_nonhalt.
  - apply progress_evstep, long_D_exit.
  - exact (D_zero_prefix_nonhalt
      ([0;1;1]^^q *> [1;1;0] *> [0;1;1]^^(S m) *> [1;1;1] *> r)).
Qed.

Definition shared_prefix (q : nat) : list sym :=
  [1;1;1]^^q ++ [1;0].
Definition long_suffix (m : nat) : list sym :=
  [1;1;1;1;0;0] ++ [1;1;1]^^m ++ [0;0].

Lemma shared_prefix_length q : List.length (shared_prefix q) = 3*q+2.
Proof.
  unfold shared_prefix. rewrite length_app.
  induction q; cbn [lpow List.app List.length] in *; lia.
Qed.

Theorem opposite_outcomes_shared_prefix q m :
  (forall r, halts tm
    (0inf <* [1] {{C}}> (shared_prefix q ++ [0]) *> r)) /\
  (forall r, ~halts tm
    (0inf <* [1] {{C}}> (shared_prefix q ++ long_suffix m) *> r)).
Proof.
  unfold shared_prefix, long_suffix.
  split; intros r; rewrite !Str_app_assoc.
  - apply short_halts.
  - apply long_nonhalts.
Qed.

(** A single prefix can be longer than any prescribed bound while both
    halting and non-halting continuations exist, uniformly for every tail. *)
Theorem arbitrarily_long_common_prefix n :
  exists u v1 v2 : list sym,
    n <= List.length u /\
    (forall r, halts tm (0inf <* [1] {{C}}> (u ++ v1) *> r)) /\
    (forall r, ~halts tm (0inf <* [1] {{C}}> (u ++ v2) *> r)).
Proof.
  exists (shared_prefix n), [0], (long_suffix 1).
  split.
  - rewrite shared_prefix_length. lia.
  - apply opposite_outcomes_shared_prefix.
Qed.

Print Assumptions short_A_exit.
Print Assumptions two_reflection_bridge.
Print Assumptions long_D_exit.
Print Assumptions short_halts.
Print Assumptions long_nonhalts.
Print Assumptions opposite_outcomes_shared_prefix.
Print Assumptions arbitrarily_long_common_prefix.