(* Rule reduction for 1RB1RA_0LC0RF_1LD1LC_1RE1LB_---0RA_1RF0RD
   and its mirror twin 1RB1RA_1LC1RE_---0LD_1LE1LD_0RA0LF_1LF0LB.

   THIS IS NOT A NON-HALTING PROOF.  It is a rule reduction in the style of
   AntiHydra.v: it proves the low-level rules of one bounce, the no-00
   invariant, and that halting is equivalent to an explicitly stated open
   property ("the chaotic edge eats the 1-block down to at most 3 cells").
   That property is stated as a Definition and is NOT proved here.

   Tape notation (busycoq, directed head):
     l <* <[a;b] <{{C}} r   is the tape  l a b <C r  (C reads b),
     l {{A}}> [a;b] *> r    is the tape  l A> a b r  (A reads a).
*)

From BusyCoq Require Import Individual62.
Require Import Lia.
Require Import String.

Definition tm := Eval compute in (TM_from_str "1RB1RA_0LC0RF_1LD1LC_1RE1LB_---0RA_1RF0RD").

Notation "c --> c'" := (c -[ tm ]-> c')   (at level 40).
Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).
Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).

Open Scope list.

(* ------------------------------------------------------------------ *)
(** * Part 1. Low-level rules of one bounce *)

(* walks: A runs right over 1s, C runs left over 1s *)
Lemma walkA k : forall l r,
  l {{A}}> [1]^^k *> r -->* l <* [1]^^k {{A}}> r.
Proof. es. Qed.

Lemma walkC k : forall l r,
  l <* [1]^^k <{{C}} r -->* l <{{C}} [1]^^k *> r.
Proof. es. Qed.

(* bounce at the right end:  x A> 1^n 0^inf  -->  x <C 1^(n+1) 0^inf *)
Lemma bounce n l :
  l {{A}}> [1]^^n *> const 0 -->* l <{{C}} [1]^^(n+1) *> const 0.
Proof.
  follow (walkA n l (const 0)). do 2 step.
  follow (walkC (S n) l (const 0)).
  finish.
Qed.

(* C reading 0: the three cases (left context 0, 01, 11) *)

(* T turn:   x 0 0 <C y  -->  x 1 0 A> y        (3 steps) *)
Lemma rule_T l r :
  l <* <[0;0] <{{C}} r -->* l <* <[1;0] {{A}}> r.
Proof. es. Qed.

(* Ca carry: x 0 1 0 <C y  -->  x <C 0 1 1 y      (3 steps) *)
Lemma rule_Ca l r :
  l <* <[0;1;0] <{{C}} r -->* l <{{C}} [0;1;1] *> r.
Proof. es. Qed.

(* Fo fold:  x 1 1 0 <C y  -->  x 0 <C 0 1 y      (6 steps) *)
Lemma rule_Fo l r :
  l <* <[1;1;0] <{{C}} r -->* l <* <[0] <{{C}} [0;1] *> r.
Proof. es. Qed.

(* the same, one step further:  x 1 1 0 <C y --> x <D 1 0 1 y  (7 steps) *)
Lemma rule_Fo7 l r :
  l <* <[1;1;0] <{{C}} r -->* l <{{D}} [1;0;1] *> r.
Proof. es. Qed.

(* A reading 0 (right contexts allowed by the no-00 invariant) *)

(* E1 re-dive: x A> 0 1 1 1 y  -->  x 1 0 <C 0 1 y     (5 steps) *)
Lemma rule_E1 l r :
  l {{A}}> [0;1;1;1] *> r -->* l <* <[1;0] <{{C}} [0;1] *> r.
Proof. es. Qed.

(* E2 re-dive: x A> 0 1 0 1 1 y  -->  x 1 0 <C 1 0 1 y   (7 steps) *)
Lemma rule_E2 l r :
  l {{A}}> [0;1;0;1;1] *> r -->* l <* <[1;0] <{{C}} [1;0;1] *> r.
Proof. es. Qed.

(* P1 pass: x A> 0 1 1 0 1 y  -->  x 1 0 0 1 0 A> y     (5 steps) *)
Lemma rule_P1 l r :
  l {{A}}> [0;1;1;0;1] *> r -->* l <* <[1;0;0;1;0] {{A}}> r.
Proof. es. Qed.

(* P2 pass: x A> 0 1 0 1 0 1 y  -->  x 1 0 1 0 1 0 A> y (6 steps) *)
Lemma rule_P2 l r :
  l {{A}}> [0;1;0;1;0;1] *> r -->* l <* <[1;0;1;0;1;0] {{A}}> r.
Proof. es. Qed.

(* F sweeps right over 0s, writing 1s *)
Lemma walkF j : forall l r,
  l {{F}}> [0]^^j *> r -->* l <* [1]^^j {{F}}> r.
Proof. es. Qed.

(* halting door: x A> 0 1 0^j 1 0 0 y halts (A0 B1 F0^j F1 D0, then E reads 0) *)
Lemma door_halts j l r :
  halts tm (l {{A}}> [0;1] *> [0]^^j *> [1;0;0] *> r).
Proof.
  eapply halts_evstep.
  2:{ do 2 step. follow walkF. do 2 step. apply evstep_refl. }
  apply halted_halts. reflexivity.
Qed.

(* ------------------------------------------------------------------ *)
(** * Part 2. The no-00 invariant *)

(* Rg r: the side r is a word without 00, followed by 0^inf
   (the golden-mean language, padded with blanks). *)
Inductive Rg : side -> Prop :=
  | Rg_0 : Rg (const 0)
  | Rg_1 r : Rg r -> Rg (1 >> r)
  | Rg_01 r : Rg r -> Rg (0 >> 1 >> r).

Lemma Str_eta (r : side) : hd r >> tl r = r.
Proof. destruct r; reflexivity. Qed.

Lemma Rg_tl r : Rg r -> Rg (tl r).
Proof.
  intros H. destruct H; cbn.
  - constructor.
  - exact H.
  - constructor. exact H.
Qed.

Lemma Rg_1_inv x : Rg (1 >> x) -> Rg x.
Proof.
  intros H. remember (1 >> x) as r eqn:Er. destruct H.
  - rewrite const_unfold in Er. discriminate.
  - injection Er as <-. exact H.
  - discriminate.
Qed.

Lemma Rg_0_inv x : Rg (0 >> x) -> x = const 0 \/ exists y, x = 1 >> y /\ Rg y.
Proof.
  intros H. remember (0 >> x) as r eqn:Er. destruct H.
  - rewrite const_unfold in Er. injection Er as <-. left. reflexivity.
  - discriminate.
  - injection Er as <-. right. eauto.
Qed.

(* The invariant: no 00 between the head (exclusive) and the rightmost 1;
   in state B also the head cell itself starts such a word; and D is
   never at a 1 with both a 1 to its left and a 0 to its right.
   (Inv was checked to 1e9 steps by simulation; here it is proved.) *)
Definition Inv (c : Q * tape) : Prop :=
  match c with
  | (q, (l, s, r)) =>
    Rg r /\ (q = B -> Rg (s >> r)) /\ (q = D -> hd r = 1 \/ hd l = 0)
  end.

Lemma Inv_c0 : Inv c0.
Proof. cbn. repeat split; intros; try discriminate. constructor. Qed.

Lemma Inv_step c c' : Inv c -> c --> c' -> Inv c'.
Proof.
  intros HI Hs.
  destruct Hs as [q q' s s' l r Htm | q q' s s' l r Htm];
  destruct HI as [HR [HB HD]];
  destruct q, s; cbn in Htm; inversion Htm; subst; clear Htm; cbn;
  repeat split; try intros Hq; try discriminate;
  try (apply Rg_tl; assumption);
  try (rewrite Str_eta; assumption);
  try (constructor; assumption);
  try (left; reflexivity); try (right; reflexivity);
  (* B0 -> C writes 0 to the left; B1 -> F; D1 -> B *)
  solve [ apply HB; reflexivity
        | apply Rg_tl, Rg_1_inv, HB; reflexivity
        | destruct (hd l); repeat constructor; assumption ].
Qed.

Lemma Inv_evstep c c' : Inv c -> c -->* c' -> Inv c'.
Proof.
  intros HI H. induction H; eauto using Inv_step.
Qed.

(* A reading 0 in the middle of the tape with 0 to its right: turn. *)
Lemma rule_turnA l r :
  l {{A}}> [0;0] *> r -->* l <{{C}} [1;0] *> r.
Proof. es. Qed.

(* Case split for A reading 0 (head cell 0, right side r) is complete under
   the invariant: turn (r starts with 0, including the blank end), the
   degenerate "A> 0 1 0^inf" (F then sweeps right forever), the two door
   shapes, or one of E1, P1, E2, P2. *)
Lemma A0_cover r : Rg r ->
  (exists y, r = 0 >> y) \/ r = 1 >> const 0 \/
  r = [1;1] *> const 0 \/ r = [1;0;1] *> const 0 \/
  exists z, r = [1;1;1] *> z \/ r = [1;1;0;1] *> z \/
            r = [1;0;1;1] *> z \/ r = [1;0;1;0;1] *> z.
Proof.
  intros H. destruct H as [| r1 H1 | r1 H1].
  - left. exists (const 0). apply const_unfold.
  - destruct H1 as [| r2 H2 | r2 H2].
    + right; left; reflexivity.
    + destruct H2 as [| r3 _ | r3 _].
      * right; right; left; reflexivity.
      * right; right; right; right. exists r3. left; reflexivity.
      * right; right; right; right. exists r3. right; left; reflexivity.
    + destruct H2 as [| r3 _ | r3 _].
      * right; right; right; left; reflexivity.
      * right; right; right; right. exists r3. right; right; left; reflexivity.
      * right; right; right; right. exists r3. right; right; right; reflexivity.
  - left. exists (1 >> r1). reflexivity.
Qed.

(* ------------------------------------------------------------------ *)
(** * Part 3. Halting goes through the door, and the door needs a tiny block *)

(* FDoor s: F at the start of s halts without returning to A:
   s = 0^j 1 0 0 y. *)
Inductive FDoor : side -> Prop :=
  | FD_end x : FDoor (1 >> 0 >> 0 >> x)
  | FD_0 x : FDoor x -> FDoor (0 >> x).

(* Configurations strictly inside the halting door (states B, F, D, E). *)
Definition Door (c : Q * tape) : Prop :=
  match c with
  | (q, (l, s, r)) =>
    match q with
    | E => s = 0
    | D => s = 0 /\ hd r = 0
    | F => FDoor (s >> r)
    | B => s = 1 /\ FDoor r
    | _ => False
    end
  end.

(* A at the entrance of the door:  A> 0 1 0^j 1 0 0 y *)
Definition ADoor (c : Q * tape) : Prop :=
  match c with
  | (q, (l, s, r)) => q = A /\ s = 0 /\ exists y, r = 1 >> y /\ FDoor y
  end.

Lemma halted_Door c : halted tm c -> Door c.
Proof.
  destruct c as [q [[l s] r]]. unfold halted.
  destruct q, s; cbn; intros H; try discriminate; reflexivity.
Qed.

Lemma Door_back c c' : Inv c -> c --> c' -> Door c' -> Door c \/ ADoor c.
Proof.
  intros HI Hs.
  destruct Hs as [q q' s s' l r Htm | q q' s s' l r Htm];
  destruct HI as [HR [HB HD]];
  destruct q, s; cbn in Htm; inversion Htm; subst; clear Htm; cbn;
  intros Hd; try contradiction.
  - (* C0 -> D *) destruct Hd as [_ H]. discriminate.
  - (* D1 -> B *)
    destruct Hd as [H1 H2].
    destruct (HD eq_refl) as [H|H]; [|congruence].
    inversion H2; subst. cbn in H. discriminate.
  - (* A0 -> B *)
    destruct Hd as [H1 H2]. right. repeat split.
    exists (tl r). split; [|exact H2]. rewrite <- H1. symmetry. apply Str_eta.
  - (* B1 -> F *) left. split; [reflexivity|]. rewrite Str_eta in Hd. exact Hd.
  - (* D0 -> E *) left. split; [reflexivity|]. exact Hd.
  - (* F0 -> F *) left. constructor. rewrite Str_eta in Hd. exact Hd.
  - (* F1 -> D *)
    destruct Hd as [H1 H2]. left.
    rewrite <- (Str_eta r), <- (Str_eta (tl r)), H1, H2. constructor.
Qed.

Lemma halts_in_door n : forall c,
  Inv c -> halts_in tm c n -> Door c \/ exists c', c -->* c' /\ ADoor c'.
Proof.
  induction n as [|n IH]; intros c HI [ch [Hm Hh]].
  - inversion Hm; subst. left. apply halted_Door. exact Hh.
  - inversion Hm as [|? ? c1 ? Hs Hm']; subst.
    destruct (IH c1 (Inv_step _ _ HI Hs)) as [Hd | [c' [He Ha]]].
    + exists ch. split; assumption.
    + destruct (Door_back _ _ HI Hs Hd) as [H|H].
      * left. exact H.
      * right. exists c. split; [apply evstep_refl | exact H].
    + right. exists c'. split; [eapply evstep_step; eassumption | exact Ha].
Qed.

Lemma FDoor_not_const y : FDoor y -> y <> const 0.
Proof.
  induction 1; intros E; rewrite const_unfold in E; injection E; intros.
  - discriminate.
  - apply IHFDoor. assumption.
Qed.

Lemma Rg_00 x : Rg (0 >> 0 >> x) -> 0 >> x = const 0.
Proof.
  intros H. apply Rg_0_inv in H. destruct H as [H | [y [H _]]].
  - exact H.
  - discriminate.
Qed.

(* Under the invariant only j <= 1 with nothing after the door is possible. *)
Lemma FDoor_Rg y : FDoor y -> Rg y ->
  y = 1 >> const 0 \/ y = 0 >> 1 >> const 0.
Proof.
  intros Hf HR. destruct Hf as [x | x Hf].
  - left. apply Rg_1_inv, Rg_00 in HR. rewrite HR.
    rewrite <- const_unfold. reflexivity.
  - right. apply Rg_0_inv in HR. destruct HR as [Hx | [z [Hz HRz]]].
    + exfalso. exact (FDoor_not_const _ Hf Hx).
    + subst x. inversion Hf; subst.
      apply Rg_00 in HRz. rewrite HRz. rewrite <- const_unfold. reflexivity.
Qed.

(* ------------------------------------------------------------------ *)
(** * Part 4. The open property and the reduction *)

(* BlockGone c: A stands on the last 0 of the edge and the 1-block has
   been eaten down to "1 1" (or to "1 0 1"):
       0^inf ... A> 0 1 1 0^inf      or      0^inf ... A> 0 1 0 1 0^inf. *)
Definition BlockGone (c : Q * tape) : Prop :=
  exists l,
    c = l {{A}}> [0;1;1] *> const 0 \/
    c = l {{A}}> [0;1;0;1] *> const 0.

(* THE OPEN PROPERTY (not proved here).  From configuration c, the chaotic
   left edge never eats the right 1-block down to two cells.  Empirically
   the block gains 1 cell per bounce while the edge eats ~0.04-0.06 cells
   per bounce, but no deterministic bound on the erosion is known. *)
Definition erosion_open (c : Q * tape) : Prop :=
  forall c', c -->* c' -> ~ BlockGone c'.

Lemma ADoor_BlockGone c : Inv c -> ADoor c -> BlockGone c.
Proof.
  destruct c as [q [[l s] r]]. cbn.
  intros [HR _] [Hq [Hs [y [Hr Hf]]]]. subst q s r.
  apply Rg_1_inv in HR.
  exists l. destruct (FDoor_Rg _ Hf HR) as [H|H]; subst y.
  - left. reflexivity.
  - right. reflexivity.
Qed.

Lemma BlockGone_halts c : BlockGone c -> halts tm c.
Proof.
  intros [l [H|H]]; subst c;
  rewrite const_unfold; rewrite const_unfold.
  - exact (door_halts 0 l (const 0)).
  - exact (door_halts 1 l (const 0)).
Qed.

(* general form: from any non-door configuration satisfying Inv *)
Lemma reduction_gen c :
  Inv c -> ~ Door c -> erosion_open c -> ~ halts tm c.
Proof.
  intros HI HD Ho [n Hh].
  destruct (halts_in_door n c HI Hh) as [H | [c' [He Ha]]].
  - exact (HD H).
  - apply (Ho c' He). apply ADoor_BlockGone; [|exact Ha].
    exact (Inv_evstep _ _ HI He).
Qed.

Lemma reduction : erosion_open c0 -> ~ halts tm c0.
Proof.
  apply reduction_gen.
  - exact Inv_c0.
  - cbn. tauto.
Qed.

(* and the converse: the open property is exactly non-halting *)
Lemma nonhalt_iff_erosion_open : ~ halts tm c0 <-> erosion_open c0.
Proof.
  split.
  - intros Hn c' He Hg. apply Hn.
    exact (halts_evstep _ _ _ (BlockGone_halts _ Hg) He).
  - exact reduction.
Qed.

(* ------------------------------------------------------------------ *)
(** * Part 5. The mirror twin 1RB1RA_1LC1RE_---0LD_1LE1LD_0RA0LF_1LF0LB *)

Definition tm26 := Eval compute in (TM_from_str "1RB1RA_1LC1RE_---0LD_1LE1LD_0RA0LF_1LF0LB").

(* tm26 is the mirror image of tm with states renamed;
   twin state q plays the role of tm state (sigma q). *)
Definition sigma (q : Q) : Q :=
  match q with
  | A => C | B => D | C => E | D => A | E => B | F => F
  end.

Lemma perm_twin : Perm tm26 (flip tm) sigma.
Proof.
  split.
  - intros q s H. destruct q, s; cbn in *; congruence.
  - intros q s s' d q' H. destruct q, s; cbn in *; inversion H; subst; reflexivity.
Qed.

(* The twin starts (in tm-coordinates, mirrored) at C on the blank tape. *)
Definition c0_twin : Q * tape := C;; tape0.

Lemma reduction_twin : erosion_open c0_twin -> ~ halts tm26 c0.
Proof.
  intros Ho.
  change c0 with (A;; tape0).
  apply (perm_nonhalt tm26 (flip tm) sigma A tape0 perm_twin).
  cbn [sigma]. intros Hh.
  apply flip_halts in Hh. rewrite flip_involutive in Hh.
  revert Hh. apply reduction_gen.
  - cbn. repeat split; intros; try discriminate. constructor.
  - cbn. tauto.
  - exact Ho.
Qed.

Lemma nonhalt_twin_iff_erosion_open : ~ halts tm26 c0 <-> erosion_open c0_twin.
Proof.
  split.
  - intros Hn c' He Hg. apply Hn.
    change c0 with (A;; tape0).
    apply (perm_halts' tm26 (flip tm) sigma A tape0 perm_twin).
    exact (flip_halts tm c0_twin (halts_evstep _ _ _ (BlockGone_halts _ Hg) He)).
  - exact reduction_twin.
Qed.

(* The twin's own low-level rules (mirror images of Part 1). *)
Notation "c ==>* c'" := (c -[ tm26 ]->* c') (at level 40).

Lemma tw_walkA k : forall l r,
  l {{A}}> [1]^^k *> r ==>* l <* [1]^^k {{A}}> r.
Proof. es. Qed.

Lemma tw_walkD k : forall l r,
  l <* [1]^^k <{{D}} r ==>* l <{{D}} [1]^^k *> r.
Proof. es. Qed.

Lemma tw_bounce n r :
  const 0 <* [1]^^n <{{D}} r ==>* const 0 <* [1]^^(n+1) {{A}}> r.
Proof.
  follow (tw_walkD n (const 0) r). do 2 step.
  follow (tw_walkA (S n) (const 0) r).
  finish.
Qed.

Lemma tw_T l r : l {{A}}> [0;0] *> r ==>* l <{{D}} [0;1] *> r.
Proof. es. Qed.

Lemma tw_Ca l r : l {{A}}> [0;1;0] *> r ==>* l <* <[1;1;0] {{A}}> r.
Proof. es. Qed.

Lemma tw_Fo l r : l {{A}}> [0;1;1] *> r ==>* l <* <[1;0] {{A}}> [0] *> r.
Proof. es. Qed.

Lemma tw_E1 l r : l <* <[1;1;1;0] <{{D}} r ==>* l <* <[1;0] {{A}}> [0;1] *> r.
Proof. es. Qed.

Lemma tw_E2 l r : l <* <[1;1;0;1;0] <{{D}} r ==>* l <* <[1;0;1] {{A}}> [0;1] *> r.
Proof. es. Qed.

Lemma tw_P1 l r : l <* <[1;0;1;1;0] <{{D}} r ==>* l <{{D}} [0;1;0;0;1] *> r.
Proof. es. Qed.

Lemma tw_P2 l r : l <* <[1;0;1;0;1;0] <{{D}} r ==>* l <{{D}} [0;1;0;1;0;1] *> r.
Proof. es. Qed.

(* ------------------------------------------------------------------ *)
Check reduction.
Check nonhalt_iff_erosion_open.
Check reduction_twin.
Check nonhalt_twin_iff_erosion_open.
Print Assumptions nonhalt_iff_erosion_open.
Print Assumptions nonhalt_twin_iff_erosion_open.