From BusyCoq Require Import Individual62 Longitudinal DivModCases.
Require Import ZifyNat Lia.
Require Import ZArith.
Require Import String.
Require Import List.

Ltac esc :=
  (apply BoundedConfig.segRLs_c_spec with (T:=10^3); reflexivity) ||
  (apply BoundedConfig.sideRLs_c_spec with (T:=10^3); reflexivity) ||
  (eapply sideRLs_c_spec with (T:=10^6); [vm_compute; reflexivity | st; reflexivity]).

Ltac ec := econstructor.

Ltac am a a' k b b' :=
  applys_eq (segRLs_addmul_v2 a a' k b b'); unfold DH0; flia; esc.

Definition tm := Eval compute in (TM_from_str "1RB0RA_1LC0RE_0LC0LD_1RD1LB_0RF1RA_0RB---").

Notation ld := [1;1;0].
Notation d0 := [0;0;0].
Notation d1 := [1;0;0].
Notation w1ld := [1;1;1;0].
Notation hR := (B,@nil Sym).
Notation hR' := (D,[1]).
Notation hL := (C,@nil Sym).
Notation h := [(hR,hL)].
Notation h' := [(hR',hL)].

(* DS = the stray: one cell holding 1 *)
Inductive RD := LD|D0|D1|DS.
Inductive H := hx|h1.

Fixpoint toRC ls :=
match ls with
| [] => 0inf
| LD::ls => ld*>toRC ls
| D0::ls => d0*>toRC ls
| D1::ls => d1*>toRC ls
| DS::ls => [1]*>toRC ls
end.

Definition toH' x := match x with | hx => [] | h1 => [1] end.
Definition toH x := match x with | hx => h' | h1 => [] end.

Inductive Inc: list RD -> list RD -> Prop :=
| Inc_d1 r r': Inc r r' -> Inc (D1::r) (D0::r')
| Inc_d0 r: Inc (D0::r) (D1::r)
| Inc_ld r r': Inc r r' -> Inc (LD::r) (LD::r')
| Inc_nil: Inc [] [D1]
| Inc_s r r': RIncs h1 1 r r' -> Inc (DS::r) r'                    (* NEW: +1 reaching a stray *)
with RIncs: H->nat->(list RD)->(list RD)->Prop :=
| RIncs_hx_ld k r r1 r':                                             (* CHANGED: k, not 1+k *)
  Inc r r1 ->
  RIncs hx k r1 r' ->
  RIncs hx k (LD::r) (LD::r')
| RIncs_hx_d1 k r r':
  RIncs h1 k r r' ->
  RIncs hx k (D1::r) (LD::r')
| RIncs_hx_d0 k r r':
  RIncs hx (1+k) r r' ->
  RIncs hx k (D0::r) (LD::r')
| RIncs_h1_ld k r r1 r':                                             (* CHANGED: hx k, not hx (1+k) *)
  Inc r r1 ->
  RIncs hx k r1 r' ->
  RIncs h1 (1+k) (LD::r) (LD::r')
| RIncs_h1_d1 k r r':
  RIncs h1 k r r' ->
  RIncs h1 (1+k) (D1::r) (LD::r')
| RIncs_h1_d0_0 k r r':
  RIncs h1 k r r' ->
  RIncs h1 (1+k*2) (D0::r) (D0::r')
| RIncs_h1_d0_1 k r r':
  RIncs h1 k r r' ->
  RIncs h1 (2+k*2) (D0::r) (D1::r')
| RIncs_h1_rh_0:
  RIncs h1 0 [] [D1]
| RIncs_h1_rh_1 k r':
  RIncs h1 k [] r' ->
  RIncs h1 (1+k*2) [] (D0::r')
| RIncs_h1_rh_2 k r':
  RIncs h1 k [] r' ->
  RIncs h1 (2+k*2) [] (D1::r')
| RIncs_z r: RIncs h1 0 r (DS::r)                                    (* NEW: replaces Z0/Z1 *)
| RIncs_eq tp k r r0 r':                                             (* NEW (pass 3): re-parse the input *)
  toRC r = toRC r0 ->
  RIncs tp k r0 r' ->
  RIncs tp k r r'
.

Scheme Inc_mut := Induction for Inc Sort Prop
with RIncs_mut := Induction for RIncs Sort Prop.
Combined Scheme Inc_RIncs_mut from Inc_mut, RIncs_mut.

Ltac cat3 :=
  eapply @segRLs_sideRLs_concat with (w1:=[_;_;_]) (w2:=[_;_;_]); [|eauto 1].
Ltac tr1 :=
  rewrite lpow_add,app_assoc;
  eapply segRLs_trans; [esx | ].
Ltac wal :=
  eapply segRLs_wall''; esx.
Ltac tr2 :=
  eapply sideRLs_trans; [esx | ].

Open Scope nat.

(* CHANGED segment facts: TM7 [h';h], parent [h;h';h], twin [h;h'] *)
Lemma seg_hx_ld k: segRLs tm (h' ++ h^^k) (h ++ h' ++ h^^k) ld ld.
Proof.
  change (h ++ h' ++ h^^k) with ((h ++ h') ++ h^^k).
  eapply segRLs_trans; [esx | wal].
Qed.

Lemma seg_h1_ld k: segRLs tm (h^^1 ++ h^^k) (h ++ h' ++ h^^k) w1ld ld.
Proof.
  change (h ++ h' ++ h^^k) with ((h ++ h') ++ h^^k).
  eapply segRLs_trans; [esx | wal].
Qed.

Lemma spec_both:
  (forall r r', Inc r r' -> sideRLs tm h (toRC r) (toRC r')) /\
  (forall tp k r r', RIncs tp k r r' ->
     sideRLs tm (toH tp++h^^k) (toH' tp*>toRC r) (toRC r')).
Proof.
  apply Inc_RIncs_mut; intros; cbn[toH toH' toRC] in *.
  - (* I1 *) cat3. esx.
  - (* I2 *) eapply @segRLs_sideRLs_concat with (w1:=[_;_;_]) (w2:=[_;_;_]) (ls2:=[]); [esx | constructor].
  - (* I3 *) cat3. esx.
  - (* I4 *) esc.
  - (* IS: NEW *) exact H0.
  - (* X1: CHANGED *)
    eapply @segRLs_sideRLs_concat with (w1:=[_;_;_]) (w2:=[_;_;_]);
      [apply seg_hx_ld | eapply sideRLs_trans; [eassumption | eassumption]].
  - tr2.
    cat3; wal.
  - cat3; tr1; wal.
  - (* C1: CHANGED *)
    rewrite lpow_add.
    eapply @segRLs_sideRLs_concat with (w1:=[_;_;_;_]) (w2:=[_;_;_]);
      [apply seg_h1_ld | eapply sideRLs_trans; [eassumption | eassumption]].
  - rewrite lpow_add,app_assoc.
    tr2.
    cat3; wal.
  - cat3.
    rewrite app_nil_l.
    am 2 1 k 1 1.
    rewrite Nat.add_comm,lpow_add,Nat.mul_1_r.
    tr2; eauto 1.
  - cat3.
    rewrite Nat.add_comm.
    am 2 1 k 2 1.
    rewrite Nat.add_comm,lpow_add,Nat.mul_1_r.
    tr2; eauto 1.
  - esc.
  - rewrite lpow_add,app_assoc.
    tr2.
    cat3.
    rewrite app_nil_l.
    am 2 1 k 0 0.
  - change (2+k*2) with (1+(1+k*2)).
    rewrite lpow_add,app_assoc.
    tr2.
    cat3.
    rewrite app_nil_l.
    am 2 1 k 1 0.
  - (* Z: NEW, zero passes *)
    constructor.
  - (* RIncs_eq: NEW (pass 3), one rewrite *)
    match goal with E: toRC _ = toRC _ |- _ => rewrite E end.
    eassumption.
Qed.

(* Canonical end identities (the parent's z1_eq/z0_eq), used through RIncs_eq. *)
Lemma s1_eq: toRC [DS;D1] = toRC [LD].
Proof. cbn. f_equal. f_equal. f_equal. symmetry. apply const_unfold. Qed.

Lemma d0s_eq j: toRC (repeat D0 j) = 0inf.
Proof.
  induction j as [|j IH]; cbn; [reflexivity|].
  rewrite IH. rewrite <- !const_unfold. reflexivity.
Qed.

Lemma s0_eq j: toRC (DS :: repeat D0 j) = toRC [D1].
Proof.
  cbn [toRC]. rewrite d0s_eq. cbn. f_equal. rewrite <- !const_unfold. reflexivity.
Qed.

(* proof.md 3.3.3, Lemma C: the re-parse sits inside the derivation, after the eater's L-run.
   w = L S 0 1 has G, but the only Inc derivation of S01 gives 0 S 1 (IS, C3, Z), and no clause
   lets the eater read S. RIncs_eq re-reads 0 S 1 as 0 L (s1_eq) and the sweep goes through. *)
Example sweep_LS01: RIncs hx 0 [LD;DS;D0;D1] [LD;LD;LD;LD;D0;D1].
Proof.
  eapply RIncs_hx_ld.
  { apply Inc_s. apply (RIncs_h1_d0_0 0). apply RIncs_z. }
  apply (RIncs_eq hx 0 _ [D0;LD]).
  { cbn [toRC]. f_equal. exact s1_eq. }
  apply RIncs_hx_d0.
  eapply RIncs_hx_ld; [apply Inc_nil|].
  apply RIncs_hx_d1.
  apply (RIncs_h1_rh_1 0). apply RIncs_h1_rh_0.
Qed.

Lemma Inc_spec r r': Inc r r' -> sideRLs tm h (toRC r) (toRC r').
Proof. apply spec_both. Qed.

Lemma RIncs_spec tp k r r':
  RIncs tp k r r' ->
  sideRLs tm (toH tp++h^^k) (toH' tp*>toRC r) (toRC r').
Proof. apply spec_both. Qed.

Open Scope sym.
Notation lh := (0inf<*<[1]).
Definition S' r := lh {{{ (hR',R) }}} toH' hx *> toRC r.
Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).

Lemma BigStep r r':
  RIncs hx 0 r r' ->
  S' r -->+ S' r'.
Proof.
  intros H.
  apply RIncs_spec in H.
  unfold S'.
  eapply sideRLs_1 in H.
  follow10 H.
  es.
Qed.

Lemma init: c0 -[ tm ]->* S' [D1].
Proof. esx. Qed.

Print Assumptions RIncs_spec.
Print Assumptions Inc_spec.
Print Assumptions BigStep.
Print Assumptions init.
Print Assumptions sweep_LS01.