(** * 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF never halts

    Machine: 1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF ("Bell eats counter").
    Adapted from verify/BECv5.v, Module TM1 / Module TM2 (same table except F1):
    the right side R n m, the right step and the standard counter are as there;
    the left side is a word W(e,o) (bit d of e on cell 2d, bit d of o on cell 2d+1),
    the left step is the relation PA/PF below, and the counter alternates between a
    standard and a packed encoding.  The informal proof is the accompanying write-up
    (proof.md); the macro rules S0..S3, P0..P4 and the invariant I are its 3.4 and 4.

    Formalized with Claude Code (AI-assisted).
    Checked: compiles against unmodified busycoq BB6 (commit 0940bb9) with Coq 8.20.1;
    Print Assumptions nonhalt: Closed under the global context.
*)

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

Open Scope list.

Definition tmP := Eval compute in (TM_from_str "1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1RC").

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

Definition R n m := [1] *> [1;0]^^(1+n) *> [0] *> [1;0]^^(m) *> const 0.

(** ** Words W(e,o): bit d of e on cell 2d, bit d of o on cell 2d+1 (cell 0 is read by A) *)

Definition bt (x:nat) : Sym := if Nat.odd x then 1 else 0.

Fixpoint wd (n e o : nat) : list Sym :=
  match n with
  | O => []
  | S n' => bt e :: bt o :: wd n' (Nat.div2 e) (Nat.div2 o)
  end.

Definition WS e o : side := wd (e+o) e o *> const 0.

Lemma bt_even e: bt (2*e) = 0.
Proof. unfold bt. rewrite Nat.odd_even. reflexivity. Qed.

Lemma bt_odd e: bt (2*e+1) = 1.
Proof. unfold bt. rewrite Nat.odd_odd. reflexivity. Qed.

Lemma div2_even e: Nat.div2 (2*e) = e.
Proof. apply Nat.div2_double. Qed.

Lemma div2_odd e: Nat.div2 (2*e+1) = e.
Proof. rewrite Nat.add_1_r. apply Nat.div2_succ_double. Qed.

Lemma wd_pad n: forall e o k,
  e < 2^n -> o < 2^n ->
  wd (n+k) e o *> const 0 = wd n e o *> const 0.
Proof.
  induction n; intros e o k He Ho.
  - cbn in He,Ho. assert (e=0)%nat by lia. assert (o=0)%nat by lia. subst.
    cbn. induction k.
    + reflexivity.
    + change (wd (S k) 0 0) with (0 :: 0 :: wd k 0 0). cbn [Str_app]. rewrite IHk. rewrite <-!const_unfold. reflexivity.
  - cbn [wd Nat.add Str_app]. f_equal. f_equal.
    apply IHn.
    + rewrite Nat.div2_div. cbn in He. apply Nat.Div0.div_lt_upper_bound; lia.
    + rewrite Nat.div2_div. cbn in Ho. apply Nat.Div0.div_lt_upper_bound; lia.
Qed.

Lemma lt_pow2_self x: x < 2^x.
Proof. apply Nat.pow_gt_lin_r. lia. Qed.

Lemma wd_WS n e o:
  e < 2^n -> o < 2^n ->
  wd n e o *> const 0 = WS e o.
Proof.
  intros He Ho. unfold WS.
  assert (e < 2^(e+o)). { pose proof (lt_pow2_self (e+o)). pose proof (Nat.pow_le_mono_r 2 e (e+o)). lia. }
  assert (o < 2^(e+o)). { pose proof (lt_pow2_self (e+o)). lia. }
  destruct (Nat.le_ge_cases n (e+o)) as [H1|H1].
  - replace (e+o) with (n+(e+o-n)) by lia. rewrite wd_pad; auto.
  - replace n with ((e+o)+(n-(e+o))) by lia. rewrite wd_pad; auto.
Qed.

Lemma WS_split e o:
  WS e o = [bt e; bt o] *> WS (Nat.div2 e) (Nat.div2 o).
Proof.
  rewrite <-(wd_WS (S (e+o)) e o).
  2,3: pose proof (lt_pow2_self (e+o)); pose proof (Nat.pow_le_mono_r 2 (e+o) (S (e+o))); lia.
  cbn [wd Str_app].
  rewrite (wd_WS (e+o)). 1: reflexivity.
  - rewrite Nat.div2_div. apply Nat.Div0.div_lt_upper_bound.
    pose proof (lt_pow2_self (e+o)). rewrite <-Nat.pow_succ_r'. pose proof (Nat.pow_le_mono_r 2 (e+o) (S (e+o))). lia.
  - rewrite Nat.div2_div. apply Nat.Div0.div_lt_upper_bound.
    pose proof (lt_pow2_self (e+o)). rewrite <-Nat.pow_succ_r'. pose proof (Nat.pow_le_mono_r 2 (e+o) (S (e+o))). lia.
Qed.

Lemma WS_00 e o: WS (2*e) (2*o) = [0;0] *> WS e o.
Proof. rewrite WS_split, bt_even, bt_even, div2_even, div2_even. reflexivity. Qed.
Lemma WS_10 e o: WS (2*e+1) (2*o) = [1;0] *> WS e o.
Proof. rewrite WS_split, bt_even, bt_odd, div2_even, div2_odd. reflexivity. Qed.
Lemma WS_01 e o: WS (2*e) (2*o+1) = [0;1] *> WS e o.
Proof. rewrite WS_split, bt_even, bt_odd, div2_even, div2_odd. reflexivity. Qed.
Lemma WS_11 e o: WS (2*e+1) (2*o+1) = [1;1] *> WS e o.
Proof. rewrite WS_split, bt_odd, bt_odd, div2_odd, div2_odd. reflexivity. Qed.

Lemma WS_0x e o: WS (2*e) o = [0; bt o] *> WS e (Nat.div2 o).
Proof. rewrite WS_split, bt_even, div2_even. reflexivity. Qed.
Lemma WS_1x e o: WS (2*e+1) o = [1; bt o] *> WS e (Nat.div2 o).
Proof. rewrite WS_split, bt_odd, div2_odd. reflexivity. Qed.

(** ** The left step phi, as a relation (A scanning an E-cell / F scanning an E-cell) *)

Inductive PA : nat -> nat -> nat -> nat -> Prop :=
| PA0 e o : PA (2*e) o (2*e+1) o
| PA1 e o e' o' : PA e o e' o' -> PA (2*e+1) (2*o) (2*e') (2*o')
| PA2 e o e' o' : PF e o e' o' -> PA (2*e+1) (2*o+1) (2*e') (2*o')
with PF : nat -> nat -> nat -> nat -> Prop :=
| PF0 e o : PF (2*e) (2*o) (2*e) (2*o+1)
| PF1 e o e' o' : PF e o e' o' -> PF (2*e) (2*o+1) (2*e') (2*o')
| PF2 e o e' o' : PA e o e' o' -> PF (2*e+1) (2*o) (2*e') (2*o')
| PF3 e o e' o' : PF e o e' o' -> PF (2*e+1) (2*o+1) (2*e') (2*o').

Scheme PA_mind := Induction for PA Sort Prop
with PF_mind := Induction for PF Sort Prop.
Combined Scheme PAF_mind from PA_mind, PF_mind.

Lemma TA0 l a r: [0;a] *> l <{{A}} r -->+ [1;a] *> l {{B}}> r.
Proof. es. Qed.
Lemma TA1 l r: [1;0] *> l <{{A}} r -->+ l <{{A}} [1;1] *> r.
Proof. es. Qed.
Lemma TA2 l r: [1;1] *> l <{{A}} r -->+ l <{{F}} [1;1] *> r.
Proof. es. Qed.
Lemma TF0 l r: [0;0] *> l <{{F}} r -->+ [0;1] *> l {{B}}> r.
Proof. es. Qed.
Lemma TF1 l r: [0;1] *> l <{{F}} r -->+ l <{{F}} [1;1] *> r.
Proof. es. Qed.
Lemma TF2 l r: [1;0] *> l <{{F}} [1] *> r -->+ l <{{A}} [1;1] *> [1] *> r.
Proof. es. Qed.
Lemma TF3 l r: [1;1] *> l <{{F}} [1] *> r -->+ l <{{F}} [1;1] *> [1] *> r.
Proof. es. Qed.
Lemma TB l r: l {{B}}> [1;1] *> r -->+ [0;0] *> l {{B}}> r.
Proof. es. Qed.

Lemma phi_spec:
  (forall e o e' o', PA e o e' o' -> forall r, WS e o <{{A}} r -->+ WS e' o' {{B}}> r) /\
  (forall e o e' o', PF e o e' o' -> forall r, WS e o <{{F}} [1] *> r -->+ WS e' o' {{B}}> [1] *> r).
Proof.
  apply PAF_mind.
  all: intros.
  all: try (rewrite WS_0x, WS_1x; apply TA0).
  all: try (rewrite WS_10, WS_00; eapply progress_trans; [apply TA1|]; eapply progress_trans; [apply H|]; apply TB).
  all: try (rewrite WS_11, WS_00; eapply progress_trans; [apply TA2|]; eapply progress_trans; [apply (H ([1] *> r))|]; apply TB).
  all: try (rewrite WS_00, WS_01; apply TF0).
  all: try (rewrite WS_01, WS_00; eapply progress_trans; [apply TF1|]; eapply progress_trans; [apply (H ([1] *> [1] *> r))|]; apply (TB _ ([1] *> r))).
  all: try (rewrite WS_10, WS_00; eapply progress_trans; [apply TF2|]; eapply progress_trans; [apply H|]; apply (TB _ ([1] *> r))).
  all: try (rewrite WS_11, WS_00; eapply progress_trans; [apply TF3|]; eapply progress_trans; [apply (H ([1] *> [1] *> r))|]; apply (TB _ ([1] *> r))).
Qed.

Definition PA_spec := proj1 phi_spec.