(** Conditional safety for an unlimited left prefix.
    The scanned cell and the whole right tape are arbitrary. The strict-left
    stream must contain no adjacent zeros. This premise fails on blank tape;
    no blank-start nonhalting theorem is claimed.
    AI assistance: GPT-6 Astra (OpenAI). *)

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

Fixpoint left_symbol (n : nat) (l : side) : sym :=
  match n with
  | O => Streams.hd l
  | S m => left_symbol m (Streams.tl l)
  end.

Definition no00_left (l : side) : Prop :=
  forall n, left_symbol n l = 1 \/ left_symbol (S n) l = 1.

Lemma no00_left_iff l : no00_left l <->
  forall n, ~ (left_symbol n l = 0 /\ left_symbol (S n) l = 0).
Proof.
  split.
  - intros H n [H0 H1]. destruct (H n); congruence.
  - intros H n.
    destruct (left_symbol n l) eqn:H0;
    destruct (left_symbol (S n) l) eqn:H1; auto.
    exfalso. apply (H n). split; assumption.
Qed.

Lemma blank_not_no00_left : ~ no00_left 0inf.
Proof. intros H. destruct (H O); discriminate. Qed.

Lemma no00_left_tail l : no00_left l -> no00_left (Streams.tl l).
Proof. intros H n. exact (H (S n)). Qed.

Lemma no00_left_one l : no00_left l -> no00_left (1 >> l).
Proof.
  intros H [|n]; cbn.
  - left. reflexivity.
  - apply H.
Qed.

Lemma no00_left_zero_one l : no00_left l -> no00_left (0 >> 1 >> l).
Proof.
  intros H [|n]; cbn.
  - right. reflexivity.
  - apply no00_left_one. exact H.
Qed.

Lemma no00_left_not_zero_zero l : ~ no00_left (0 >> 0 >> l).
Proof.
  intros H. destruct (H O) as [H0|H0]; discriminate.
Qed.

Definition safe_AC (c : Q * tape) : Prop :=
  exists q l r, (q = A \/ q = C) /\ no00_left l /\ c = l {{q}}> r.

Lemma safe_AC_right q l r :
  (q = A \/ q = C) -> no00_left l -> safe_AC (l {{q}}> r).
Proof. intros Hq Hl. exists q, l, r. auto. Qed.

Lemma safe_AC_left q l r :
  (q = A \/ q = C) -> no00_left l -> safe_AC (l <{{q}} r).
Proof.
  intros Hq Hl. exists q, (Streams.tl l), (Streams.hd l >> r).
  split; [exact Hq|]. split.
  - apply no00_left_tail. exact Hl.
  - reflexivity.
Qed.

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

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

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

Lemma safe_AC_progress c : safe_AC c ->
  exists c', safe_AC c' /\ c -->+ c'.
Proof.
  intros [q [l [r [Hq [Hl ->]]]]].
  destruct Hq as [-> | ->].
  - destruct r as [x r]. destruct x.
    + destruct r as [y r]. destruct y.
      * exists (l <* <[1;0] {{C}}> r). split.
        -- apply safe_AC_right; [right; reflexivity|].
           apply no00_left_zero_one. exact Hl.
        -- apply safety_A00.
      * exists (l <* <[1;1] {{A}}> r). split.
        -- apply safe_AC_right; [left; reflexivity|].
           apply no00_left_one, no00_left_one. exact Hl.
        -- apply safety_A01.
    + destruct l as [x l]. destruct x.
      * destruct l as [y l]. destruct y.
        -- exfalso. apply (no00_left_not_zero_zero l). exact Hl.
        -- exists (l <{{A}} [1;1;0] *> r). split.
           ++ apply safe_AC_left; [left; reflexivity|].
              exact (no00_left_tail _ (no00_left_tail _ Hl)).
           ++ apply A_101.
      * destruct l as [y l]. destruct y.
        -- destruct l as [z l]. destruct z.
           ++ exfalso. apply (no00_left_not_zero_zero l).
              exact (no00_left_tail _ Hl).
           ++ exists (l <{{A}} [0;1;1;1] *> r). split.
              ** apply safe_AC_left; [left; reflexivity|].
                 exact (no00_left_tail _ (no00_left_tail _ (no00_left_tail _ Hl))).
              ** apply safety_A1011.
        -- exists (l <{{A}} [0;1;1] *> r). split.
           ++ apply safe_AC_left; [left; reflexivity|].
              exact (no00_left_tail _ (no00_left_tail _ Hl)).
           ++ apply A_111.
  - destruct r as [x r]. destruct x.
    + destruct l as [x l]. destruct x.
      * destruct l as [y l]. destruct y.
        -- exfalso. apply (no00_left_not_zero_zero l). exact Hl.
        -- exists (l <{{A}} [1;1;1] *> r). split.
           ++ apply safe_AC_left; [left; reflexivity|].
              exact (no00_left_tail _ (no00_left_tail _ Hl)).
           ++ apply C_100.
      * exists (l <* <[1;0] {{C}}> r). split.
        -- apply safe_AC_right; [right; reflexivity|].
           apply no00_left_zero_one. exact (no00_left_tail _ Hl).
        -- apply C_10.
    + exists (l <* [1] {{C}}> r). split.
      * apply safe_AC_right; [right; reflexivity|].
        apply no00_left_one. exact Hl.
      * apply C_1.
Qed.

Theorem unlimited_left_safe_nonhalt q l r :
  (q = A \/ q = C) -> no00_left l -> ~ halts tm (l {{q}}> r).
Proof.
  intros Hq Hl. apply (progress_nonhalt tm safe_AC).
  - apply safe_AC_progress.
  - apply safe_AC_right; assumption.
Qed.

(** Closest cells first: physical ...011011 is stored as 110110... . *)
CoFixpoint left_011_reserve : side := 1 >> 1 >> 0 >> left_011_reserve.

Lemma left_011_reserve_no00 : no00_left left_011_reserve.
Proof.
  unfold no00_left. fix IH 1. intro n.
  destruct n as [|[|[|n]]]; cbn [left_symbol].
  - left. reflexivity.
  - left. reflexivity.
  - right. reflexivity.
  - apply IH.
Qed.

Corollary unlimited_011_reserve_nonhalt q r :
  (q = A \/ q = C) -> ~ halts tm (left_011_reserve {{q}}> r).
Proof.
  intro Hq. apply unlimited_left_safe_nonhalt.
  - exact Hq.
  - apply left_011_reserve_no00.
Qed.

Print Assumptions unlimited_left_safe_nonhalt.
Print Assumptions unlimited_011_reserve_nonhalt.