(* Rule reduction for 1RB1RA_0LC0RF_1LD1LC_1RE1LB_---0RA_1RF0RD (Bouncer + Chaotic Edge)
   and its mirror twin 1RB1RA_1LC1RE_---0LD_1LE1LD_0RA0LF_1LF0LB.

   NOT a non-halting proof.  In the style of AntiHydra.v this file proves
   - the bounce rules (two walks, the end-of-block turn, and the seven rules T, Ca, Fo, E1,
     E2, P1, P2 of one bounce) as -->+ / -->* lemmas for arbitrary sides,
   - that these rules (plus one degenerate "runaway" rule) form a deterministic rule system
     [rstep] on the configuration family [conf (mode, l, v)], every step of which is a
     -->+ run of the machine ([rstep_sound]),
   - the no-00 invariant: the word v right of the head always lies in (1 | 01)*, i.e. it has
     no factor 00 and does not end in 0 ([GM], [rstep_GM], [GM_no00]),
   - that under the invariant the rule system is total except at the two "eaten" shapes
       A> 0 1 1 0^inf      and      A> 0 1 0 1 0^inf
     (the edge has eaten the 1-block down to two cells), which halt ([rstep_progress],
     [eaten_halts]),
   - [reduction]: the open edge condition [EdgeNeverEats a0] implies ~ halts tm c0, and
     [reduction_iff]: the two are equivalent.  The condition is a premise, never proved.
   - [reduction_twin] / [reduction_twin_iff]: the same for the twin, via busycoq's
     flip_halts / perm_halts; the twin is the machine started in state C on the blank tape.

   Tape notation (busycoq, directed head; wiki notation in comments):
     l <* <[a;b] <{{C}} r   is   x a b <C y   (C reads b),
     l {{A}}> [a;b] *> r    is   x A> a b y   (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.

(* ------------------------------------------------------------------ *)
(** * 1. The bounce rules *)

(** Walks: A runs right over 1s, C runs left over 1s. *)

(* x A> 1^n y  -->*  x 1^n A> y   (n steps) *)
Lemma A_walk n : forall l r, l {{A}}> [1]^^n *> r -->* l <* [1]^^n {{A}}> r.
Proof. es. Qed.

(* x 1^k <C y  -->*  x <C 1^k y   (k steps) *)
Lemma C_walk k : forall l r, l <* [1]^^k <{{C}} r -->* l <{{C}} [1]^^k *> r.
Proof. es. Qed.

(* end of the block:  x A> 0^inf  -->+  x 1 <C 0^inf   (2 steps) *)
Lemma End_turn l : l {{A}}> const 0 -->+ l <* <[1] <{{C}} const 0.
Proof. es. Qed.

(* Bounce:  x A> 1^n 0^inf  -->+  x <C 1^(n+1) 0^inf   (2n+3 steps) *)
Lemma Bounce n l : l {{A}}> [1]^^n *> const 0 -->+ l <{{C}} [1]^^(S n) *> const 0.
Proof.
  eapply evstep_progress_trans; [apply A_walk|].
  eapply progress_evstep_trans; [apply End_turn|].
  change (l <* [1]^^n <* <[1]) with (l <* [1]^^(S n)).
  apply C_walk.
Qed.

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

(* T turn:   x 0 0 <C y  -->+  x 1 0 A> y        (3 steps) *)
Lemma T_rule 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 Ca_rule 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 Fo_rule l r : l <* <[1;1;0] <{{C}} r -->+ l <* <[0] <{{C}} [0;1] *> r.
Proof. es. Qed.

(* the notes' form of Fo, one step further:  x 1 1 0 <C y  -->+  x <D 1 0 1 y  (7 steps) *)
Lemma Fo7_rule l r : l <* <[1;1;0] <{{C}} r -->+ l <{{D}} [1;0;1] *> r.
Proof. es. Qed.

(** A reading 0: the four right contexts the invariant allows. *)

(* E1 re-dive: x A> 0 1 1 1 y  -->+  x 1 0 <C 0 1 y      (5 steps) *)
Lemma E1_rule 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 E2_rule 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 P1_rule 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 P2_rule l r : l {{A}}> [0;1;0;1;0;1] *> r -->+ l <* <[1;0;1;0;1;0] {{A}}> r.
Proof. es. Qed.

(** Degenerate end shapes (block of 1 or 2 cells). *)

(* runaway: x A> 0 1 0^inf  -->+  x 1 0 F> 0^inf, and F then sweeps right forever *)
Lemma Run_rule l : l {{A}}> [0;1] *> const 0 -->+ l <* <[1;0] {{F}}> const 0.
Proof. es. Qed.

Lemma F_sweep l : l {{F}}> const 0 -->+ l <* <[1] {{F}}> const 0.
Proof. es. Qed.

(* F walks right over 0s, writing 1s *)
Lemma F_walk 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 after j+5 steps
   (A0 B1 F0^j F1 D0, then E reads 0).  E0 is the only halting transition. *)
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 F_walk. do 2 step. apply evstep_refl. }
  apply halted_halts. reflexivity.
Qed.

Lemma Halt_011 l : halts tm (l {{A}}> [0;1;1] *> const 0).
Proof.
  pose proof (Door_halts 0 l (const 0)) as H.
  rewrite (const_unfold _ S0), (const_unfold _ S0). exact H.
Qed.

Lemma Halt_0101 l : halts tm (l {{A}}> [0;1;0;1] *> const 0).
Proof.
  pose proof (Door_halts 1 l (const 0)) as H.
  rewrite (const_unfold _ S0), (const_unfold _ S0). exact H.
Qed.

(* ------------------------------------------------------------------ *)
(** * 2. The configuration family and the rule system *)

(* Modes: A returning right, C diving left, F in the runaway sweep. *)
Inductive mode := MA | MC | MF.

(* (m, l, v): left side l (any stream), finite word v right of the head, then 0^inf.
   In mode A the head reads the first cell of v (or the blank if v = []);
   in mode C it reads the cell next to the head on the left, hd l. *)
Definition ast : Type := (mode * side * list Sym)%type.

Definition conf (a : ast) : Q * tape :=
  match a with
  | (MA, l, v) => l {{A}}> v *> const 0
  | (MC, l, v) => l <{{C}} v *> const 0
  | (MF, l, v) => l {{F}}> v *> const 0
  end.

(* One rule of the system. *)
Inductive rstep : ast -> ast -> Prop :=
  (* C walks left over a 1 *)
  | r_Cwalk l v : rstep (MC, l <* <[1], v) (MC, l, 1 :: v)
  (* C reads 0 *)
  | r_T  l v : rstep (MC, l <* <[0;0], v)   (MA, l <* <[1;0], v)
  | r_Ca l v : rstep (MC, l <* <[0;1;0], v) (MC, l, 0 :: 1 :: 1 :: v)
  | r_Fo l v : rstep (MC, l <* <[1;1;0], v) (MC, l <* <[0], 0 :: 1 :: v)
  (* A walks right over a 1, and turns at the end of the block *)
  | r_Awalk l v : rstep (MA, l, 1 :: v) (MA, l <* <[1], v)
  | r_End   l   : rstep (MA, l, []) (MC, l <* <[1], [])
  (* A reads 0 inside the tape *)
  | r_E1 l v : rstep (MA, l, 0 :: 1 :: 1 :: 1 :: v)           (MC, l <* <[1;0], 0 :: 1 :: v)
  | r_E2 l v : rstep (MA, l, 0 :: 1 :: 0 :: 1 :: 1 :: v)      (MC, l <* <[1;0], 1 :: 0 :: 1 :: v)
  | r_P1 l v : rstep (MA, l, 0 :: 1 :: 1 :: 0 :: 1 :: v)      (MA, l <* <[1;0;0;1;0], v)
  | r_P2 l v : rstep (MA, l, 0 :: 1 :: 0 :: 1 :: 0 :: 1 :: v) (MA, l <* <[1;0;1;0;1;0], v)
  (* block of one cell: F sweeps right forever *)
  | r_Run l : rstep (MA, l, [0;1]) (MF, l <* <[1;0], [])
  | r_F   l : rstep (MF, l, []) (MF, l <* <[1], []).

Lemma rstep_sound a a' : rstep a a' -> conf a -->+ conf a'.
Proof.
  intros H. destruct H; cbn [conf].
  - apply progress_base. prove_step.
  - exact (T_rule l (v *> const 0)).
  - exact (Ca_rule l (v *> const 0)).
  - exact (Fo_rule l (v *> const 0)).
  - apply progress_base. prove_step.
  - exact (End_turn l).
  - exact (E1_rule l (v *> const 0)).
  - exact (E2_rule l (v *> const 0)).
  - exact (P1_rule l (v *> const 0)).
  - exact (P2_rule l (v *> const 0)).
  - exact (Run_rule l).
  - exact (F_sweep l).
Qed.

Lemma rstep_deterministic a a1 a2 : rstep a a1 -> rstep a a2 -> a1 = a2.
Proof.
  intros H1 H2.
  destruct H1; inversion H2; subst; try reflexivity;
  repeat match goal with
         | H : _ >> _ = _ >> _ |- _ => injection H as ? ?; subst
         end;
  try discriminate; reflexivity.
Qed.

(* ------------------------------------------------------------------ *)
(** * 3. The no-00 invariant *)

(* GM v: v is in (1 | 01)*, i.e. golden-mean words ending in 1. *)
Inductive GM : list Sym -> Prop :=
  | GM_nil : GM []
  | GM_1 v : GM v -> GM (1 :: v)
  | GM_01 v : GM v -> GM (0 :: 1 :: v).

Lemma GM_no00 v : GM v -> forall x y, v <> x ++ 0 :: 0 :: y.
Proof.
  induction 1 as [| v H IH | v H IH]; intros x y E.
  - destruct x; discriminate.
  - destruct x as [|s x]; [discriminate|]. injection E as _ E. exact (IH x y E).
  - destruct x as [|s x]; [discriminate|]. injection E as _ E.
    destruct x as [|t x]; [discriminate|]. injection E as _ E. exact (IH x y E).
Qed.

Lemma GM_no_trailing0 v : GM v -> forall x, v <> x ++ [0].
Proof.
  induction 1 as [| v H IH | v H IH]; intros x E.
  - destruct x; discriminate.
  - destruct x as [|s x]; [discriminate|].
    injection E as _ E. exact (IH x E).
  - destruct x as [|s x]; [discriminate|]. injection E as _ E.
    destruct x as [|t x]; [discriminate|]. injection E as _ E. exact (IH x E).
Qed.

(* The invariant on the family: in modes A and C the right word is in GM
   (so no 00 lies right of the head, and in mode A not even from the head on);
   in mode F the right side is blank. *)
Definition Inv (a : ast) : Prop :=
  match a with
  | (MF, _, v) => v = []
  | (_, _, v) => GM v
  end.

Lemma rstep_GM a a' : Inv a -> rstep a a' -> Inv a'.
Proof.
  intros HI H. destruct H; cbn in *.
  - constructor. exact HI.
  - exact HI.
  - constructor. constructor. exact HI.
  - constructor. exact HI.
  - inversion HI; subst. assumption.
  - constructor.
  - inversion HI as [|? H1|? H1]; subst. inversion H1 as [|? H2|]; subst.
    inversion H2 as [|? H3|]; subst. constructor. exact H3.
  - inversion HI as [|? H1|? H1]; subst. inversion H1 as [|? H2|? H2]; subst.
    inversion H2 as [|? H3|]; subst. constructor. constructor. exact H3.
  - inversion HI as [|? H1|? H1]; subst. inversion H1 as [|? H2|]; subst.
    inversion H2 as [|? H3|? H3]; subst. exact H3.
  - inversion HI as [|? H1|? H1]; subst. inversion H1 as [|? H2|? H2]; subst.
    inversion H2 as [|? H3|? H3]; subst. exact H3.
  - reflexivity.
  - reflexivity.
Qed.

(* ------------------------------------------------------------------ *)
(** * 4. Completeness: under the invariant only the eaten shapes are stuck *)

(* The edge has eaten the block down to two cells. *)
Definition eaten (a : ast) : Prop :=
  match a with
  | (MA, _, v) => v = [0;1;1] \/ v = [0;1;0;1]
  | _ => False
  end.

Lemma eaten_halts a : eaten a -> halts tm (conf a).
Proof.
  destruct a as [[[] l] v]; cbn; try contradiction.
  intros [-> | ->]; [apply Halt_011 | apply Halt_0101].
Qed.

Lemma rstep_progress a : Inv a -> ~ eaten a -> exists a', rstep a a'.
Proof.
  destruct a as [[m l] v]. intros HI Hn. destruct m; cbn in HI.
  - (* mode A *)
    inversion HI as [|v1 H1|v1 H1]; subst.
    + eexists. apply r_End.
    + eexists. apply r_Awalk.
    + inversion H1 as [|v2 H2|v2 H2]; subst.
      * eexists. apply r_Run.
      * inversion H2 as [|v3 H3|v3 H3]; subst.
        -- exfalso. apply Hn. cbn. auto.
        -- eexists. apply r_E1.
        -- eexists. apply r_P1.
      * inversion H2 as [|v3 H3|v3 H3]; subst.
        -- exfalso. apply Hn. cbn. auto.
        -- eexists. apply r_E2.
        -- eexists. apply r_P2.
  - (* mode C: case split on the three cells left of the head *)
    destruct l as [x [y [z l]]].
    destruct x.
    + destruct y.
      * eexists. exact (r_T (z >> l) v).
      * destruct z.
        -- eexists. exact (r_Ca l v).
        -- eexists. exact (r_Fo l v).
    + eexists. exact (r_Cwalk (y >> z >> l) v).
  - (* mode F *)
    subst v. eexists. apply r_F.
Qed.

(* ------------------------------------------------------------------ *)
(** * 5. The open condition and the reduction *)

Inductive reach (s : ast) : ast -> Prop :=
  | reach_refl : reach s s
  | reach_step a a' : reach s a -> rstep a a' -> reach s a'.

(* THE OPEN EDGE CONDITION (not proved here): started from s, the rule system never
   reaches A> 0 1 1 0^inf or A> 0 1 0 1 0^inf, i.e. 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 about 0.04 cells per bounce; no deterministic erosion bound is known. *)
Definition EdgeNeverEats (s : ast) : Prop := forall a, reach s a -> ~ eaten a.

Lemma reach_Inv s a : Inv s -> reach s a -> Inv a.
Proof. intros H0 H. induction H; eauto using rstep_GM. Qed.

Lemma reach_evstep s a : reach s a -> conf s -->* conf a.
Proof.
  induction 1 as [|a a' _ IH Hs].
  - apply evstep_refl.
  - eapply evstep_trans; [exact IH|]. apply progress_evstep, rstep_sound, Hs.
Qed.

Lemma reduction_from s : Inv s -> EdgeNeverEats s -> ~ halts tm (conf s).
Proof.
  intros H0 Hn.
  apply progress_nonhalt_cond with (P := reach s).
  - intros a Ha.
    destruct (rstep_progress a (reach_Inv s a H0 Ha) (Hn a Ha)) as [a' Hs].
    exists a'. split; [apply rstep_sound, Hs | eapply reach_step; eassumption].
  - apply reach_refl.
Qed.

Lemma reduction_from_iff s : Inv s -> (~ halts tm (conf s) <-> EdgeNeverEats s).
Proof.
  intros H0. split.
  - intros Hnh a Ha He. apply Hnh.
    exact (halts_evstep _ _ _ (eaten_halts a He) (reach_evstep s a Ha)).
  - apply reduction_from, H0.
Qed.

(* The machine's start: 0^inf A> 0^inf. *)
Definition a0 : ast := (MA, const 0, []).

Lemma conf_a0 : conf a0 = c0.
Proof. reflexivity. Qed.

Theorem reduction : EdgeNeverEats a0 -> ~ halts tm c0.
Proof. rewrite <- conf_a0. apply reduction_from. constructor. Qed.

Theorem reduction_iff : ~ halts tm c0 <-> EdgeNeverEats a0.
Proof. rewrite <- conf_a0. apply reduction_from_iff. constructor. Qed.

(* The same condition read directly on the machine. *)
Corollary reduction_tm :
  (forall l, ~ c0 -->* l {{A}}> [0;1;1] *> const 0) ->
  (forall l, ~ c0 -->* l {{A}}> [0;1;0;1] *> const 0) ->
  ~ halts tm c0.
Proof.
  intros H1 H2. apply reduction. intros [[m l] v] Ha He.
  apply reach_evstep in Ha. rewrite conf_a0 in Ha.
  destruct m; cbn in He; try contradiction.
  destruct He as [-> | ->]; [exact (H1 l Ha) | exact (H2 l Ha)].
Qed.

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

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

(* The twin's table mirrored (L <-> R) is tm's table with states renamed by phi
   (twin state q plays tm's state phi q). *)
Definition phi (q : Q) : Q :=
  match q with A => C | B => D | C => E | D => A | E => B | F => F end.

Lemma perm_twin : Perm (flip tm26) tm phi.
Proof.
  split.
  - intros [] [] H; cbn in *; try discriminate; reflexivity.
  - intros [] [] s' d q' H; cbn in *; inversion H; subst; reflexivity.
Qed.

(* and back: tm mirrored is the twin with states renamed by psi = phi^-1
   (used for the converse, so that no flip_involutive / funext is needed) *)
Definition psi (q : Q) : Q :=
  match q with A => D | B => E | C => A | D => B | E => C | F => F end.

Lemma perm_twin' : Perm (flip tm) tm26 psi.
Proof.
  split.
  - intros [] [] H; cbn in *; try discriminate; reflexivity.
  - intros [] [] s' d q' H; cbn in *; inversion H; subst; reflexivity.
Qed.

(* The twin runs tm from 0^inf <C 0^inf (C reading a blank). *)
Definition a0_twin : ast := (MC, const 0, []).

Lemma conf_a0_twin : conf a0_twin = C;; tape0.
Proof. reflexivity. Qed.

Lemma twin_halts_iff : halts tm26 c0 <-> halts tm (conf a0_twin).
Proof.
  rewrite conf_a0_twin. split.
  - intros H. apply flip_halts in H.
    change (halts (flip tm26) (A;; tape0)) in H.
    exact (perm_halts _ _ _ _ _ perm_twin H).
  - intros H. apply flip_halts in H.
    change (halts (flip tm) (C;; tape0)) in H.
    exact (perm_halts _ _ _ _ _ perm_twin' H).
Qed.

Theorem reduction_twin : EdgeNeverEats a0_twin -> ~ halts tm26 c0.
Proof.
  intros Hn H. apply twin_halts_iff in H. revert H.
  apply reduction_from; [constructor | exact Hn].
Qed.

Theorem reduction_twin_iff : ~ halts tm26 c0 <-> EdgeNeverEats a0_twin.
Proof.
  rewrite twin_halts_iff. apply reduction_from_iff. constructor.
Qed.

(* ------------------------------------------------------------------ *)
Check reduction.
Check reduction_iff.
Check reduction_tm.
Check reduction_twin.
Check reduction_twin_iff.
Print Assumptions reduction.
Print Assumptions reduction_iff.
Print Assumptions reduction_tm.
Print Assumptions reduction_twin.
Print Assumptions reduction_twin_iff.