From BusyCoq Require Import Individual62.
Require Import Lia String List Arith.
Import ListNotations.

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

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).

(* ===================================================================== *)
(* 1. Arrivals on sides: one carry entering a side in state B and        *)
(*    coming back in state C.                                            *)
(* ===================================================================== *)

Definition ArrS (r r' : side) : Prop := forall l, l {{B}}> r -->* l <{{C}} r'.

(* first cell 0: B0 -> 1LC *)
Lemma arr_Z r : ArrS (0 >> r) (1 >> r).
Proof. intros l. execute. Qed.

(* D1: B> 1000 r --> 1111 B> r ~> 1111 <C r' --> <C 0000 r' *)
Lemma arr_D1 r r' : ArrS r r' -> ArrS ([1;0;0;0] *> r) ([0;0;0;0] *> r').
Proof.
  intros H l. cbn [Str_app].
  do 4 step. follow H. execute.
Qed.

(* P: B> 11000 r --> 10111 B> r ~> 10111 <C r' --> <C 11000 r' *)
Lemma arr_P r r' : ArrS r r' -> ArrS ([1;1;0;0;0] *> r) ([1;1;0;0;0] *> r').
Proof.
  intros H l. cbn [Str_app].
  do 5 step. follow H. execute.
Qed.

(* W: B> 111000 r --> 100111 B> r ~> 100111 <C r1 --> 000111 B> r1 ~> ...
      --> 101111 B> r2 ~> 101111 <C r3 --> <C 110000 r3 *)
Lemma arr_W r r1 r2 r3 : ArrS r r1 -> ArrS r1 r2 -> ArrS r2 r3 ->
  ArrS ([1;1;1;0;0;0] *> r) ([1;1;0;0;0;0] *> r3).
Proof.
  intros H1 H2 H3 l. cbn [Str_app].
  do 6 step. follow H1.
  do 11 step. follow H2.
  do 11 step. follow H3.
  execute.
Qed.

(* ===================================================================== *)
(* 2. Units and unit words; one carry (Inc); Theorem U (arrival = Inc).  *)
(* ===================================================================== *)

Inductive unt := uD0 | uD1 | uP | uS1 | uSP | uW.

Definition ucells (u : unt) : list Sym :=
  match u with
  | uD0 => [0;0;0;0]
  | uD1 => [1;0;0;0]
  | uP  => [1;1;0;0;0]
  | uS1 => [0;1;0;0;0]
  | uSP => [0;1;1;0;0;0]
  | uW  => [1;1;1;0;0;0]
  end.

Fixpoint enc (w : list unt) : list Sym :=
  match w with
  | [] => []
  | u :: w' => ucells u ++ enc w'
  end.

Definition Rs (w : list unt) : side := enc w *> const 0.

Lemma Rs_cons u w : Rs (u :: w) = ucells u *> Rs w.
Proof. unfold Rs. cbn [enc]. apply Str_app_assoc. Qed.

Lemma enc_app a b : enc (a ++ b) = enc a ++ enc b.
Proof. induction a as [|u a IH]; cbn; [reflexivity|]. rewrite IH, app_assoc. reflexivity. Qed.

Lemma Rs_app a b : Rs (a ++ b) = enc a *> Rs b.
Proof. unfold Rs. rewrite enc_app. apply Str_app_assoc. Qed.

(* The shift: one extra 0 cell, re-read as units.  It passes D0 units and
   prepends 0 to the head of the first other unit; on S1, SP or W it is a
   hit, which is not a unit word. *)
Fixpoint shift (w : list unt) : option (list unt) :=
  match w with
  | [] => Some []
  | uD0 :: w' =>
      match shift w' with
      | Some w'' => Some (uD0 :: w'')
      | None => None
      end
  | uD1 :: w' => Some (uS1 :: w')
  | uP :: w' => Some (uSP :: w')
  | _ => None
  end.

Lemma shift_spec w w' : shift w = Some w' -> 0 >> Rs w = Rs w'.
Proof.
  revert w'; induction w as [|u w IH]; intros w' H; cbn in H.
  - inversion H; subst. unfold Rs. cbn. symmetry. apply const_unfold.
  - destruct u; try discriminate.
    + destruct (shift w) as [w''|] eqn:E; [|discriminate].
      inversion H; subst. rewrite !Rs_cons. rewrite <- (IH w'' eq_refl). reflexivity.
    + inversion H; subst. rewrite !Rs_cons. reflexivity.
    + inversion H; subst. rewrite !Rs_cons. reflexivity.
Qed.

(* One carry entering a unit word at its left end. *)
Inductive Inc : list unt -> list unt -> Prop :=
| Inc_nil : Inc [] [uD1]
| Inc_D0 w : Inc (uD0 :: w) (uD1 :: w)
| Inc_S1 w : Inc (uS1 :: w) (uP :: w)
| Inc_SP w : Inc (uSP :: w) (uW :: w)
| Inc_D1 w w' : Inc w w' -> Inc (uD1 :: w) (uD0 :: w')
| Inc_P w w' : Inc w w' -> Inc (uP :: w) (uP :: w')
| Inc_W w w1 w2 w3 w4 : Inc w w1 -> Inc w1 w2 -> Inc w2 w3 -> shift w3 = Some w4 ->
    Inc (uW :: w) (uP :: w4).

(* Theorem U *)
Theorem inc_arr w w' : Inc w w' -> ArrS (Rs w) (Rs w').
Proof.
  induction 1.
  - assert (E1 : Rs [] = 0 >> const 0) by (unfold Rs; cbn; apply const_unfold).
    assert (E2 : Rs [uD1] = 1 >> const 0).
    { unfold Rs. cbn. f_equal. rewrite <- !const_unfold. reflexivity. }
    rewrite E1, E2. apply arr_Z.
  - rewrite !Rs_cons. apply arr_Z.
  - rewrite !Rs_cons. apply arr_Z.
  - rewrite !Rs_cons. apply arr_Z.
  - rewrite !Rs_cons. apply arr_D1; auto.
  - rewrite !Rs_cons. apply arr_P; auto.
  - rewrite !Rs_cons. rewrite <- (shift_spec _ _ H2).
    change ([1;1;0;0;0] *> 0 >> Rs w3) with ([1;1;0;0;0;0] *> Rs w3).
    eapply arr_W; eauto.
Qed.

Lemma Inc_det w a b : Inc w a -> Inc w b -> a = b.
Proof.
  intros H; revert b; induction H; intros b Hb; inversion Hb; subst; auto.
  - f_equal; auto.
  - f_equal; auto.
  - assert (w1 = w5) by auto; subst.
    assert (w2 = w6) by auto; subst.
    assert (w3 = w7) by auto; subst.
    congruence.
Qed.

(* three carries, then the first unit is P and is removed (a pop) *)
Definition Inc3Pop (U U' : list unt) : Prop :=
  exists a b, Inc U a /\ Inc a b /\ Inc b (uP :: U').

Fixpoint Pops (k : nat) (U U' : list unt) : Prop :=
  match k with
  | O => U = U'
  | S k' => exists U1, Inc3Pop U U1 /\ Pops k' U1 U'
  end.

(* ===================================================================== *)
(* 3. Window runs: the machine on a finite window, with the rest of the  *)
(*    tape an opaque unit word touched only by the W rule (Inc3Pop).     *)
(* ===================================================================== *)

(* (left cells nearest first, head symbol, right cells, state); the left
   cells are followed by 0^inf, the right cells by the opaque side X. *)
Definition lcfg : Type := (list Sym * Sym * list Sym * Q)%type.

Definition lc (X : side) (c : lcfg) : Q * tape :=
  match c with (l, m, r, q) => (q, (l *> const 0, m, r *> X)) end.

(* one step; the flag is true when the head leaves the window to the left *)
Definition lstep (c : lcfg) : option (lcfg * bool) :=
  match c with
  | (l, m, r, q) =>
      match tm (q, m) with
      | None => None
      | Some (s, L, q') =>
          match l with
          | [] => Some (([], 0, s :: r, q'), true)
          | x :: l' => Some ((l', x, s :: r, q'), false)
          end
      | Some (s, R, q') =>
          match r with
          | [] => None
          | x :: r' => Some ((s :: l, x, r', q'), false)
          end
      end
  end.

Lemma lstep_spec X c c' b : lstep c = Some (c', b) -> lc X c --> lc X c'.
Proof.
  destruct c as [[[l m] r] q]. unfold lstep.
  destruct (tm (q, m)) as [[[s d] q']|] eqn:E; [|discriminate].
  destruct d.
  - destruct l as [|x l']; intros H; inversion H; subst.
    + apply (step_left (l := const 0) (r := r *> X) E).
    + apply (step_left (l := x >> l' *> const 0) (r := r *> X) E).
  - destruct r as [|x r']; intros H; inversion H; subst.
    apply (step_right (l := l *> const 0) (r := x >> r' *> X) E).
Qed.

(* the W rule applies: state B on 1, the window ends with 1 1 0 0 0 *)
Definition wready (c : lcfg) : bool :=
  match c with
  | (_, S1, S1 :: S1 :: S0 :: S0 :: S0 :: [], B) => true
  | _ => false
  end.

Definition wpop (c : lcfg) : lcfg :=
  match c with
  | (l, _, _, _) =>
      match l with
      | [] => ([], 0, [1;1;0;0;0;0;1;1;0;0;0], C)
      | x :: l' => (l', x, [1;1;0;0;0;0;1;1;0;0;0], C)
      end
  end.

Lemma wpop_spec c U U' : wready c = true -> Inc3Pop U U' ->
  lc (Rs U) c -->* lc (Rs U') (wpop c).
Proof.
  intros Hw [a [b [H1 [H2 H3]]]].
  destruct c as [[[l m] r] q].
  assert (HW := arr_W _ _ _ _ (inc_arr _ _ H1) (inc_arr _ _ H2) (inc_arr _ _ H3) (l *> const 0)).
  unfold wready in Hw.
  destruct m; [discriminate|].
  destruct r as [|[|] [|[|] [|[|] [|[|] [|[|] [|]]]]]]; try discriminate.
  destruct q; try discriminate.
  rewrite Rs_cons in HW.
  destruct l as [|x l']; exact HW.
Qed.

Fixpoint wrun (fuel : nat) (c : lcfg) : option (lcfg * nat) :=
  match fuel with
  | O => None
  | S f =>
      if wready c then
        match wrun f (wpop c) with
        | Some (c', k) => Some (c', S k)
        | None => None
        end
      else
        match lstep c with
        | None => None
        | Some (c', true) => Some (c', O)
        | Some (c', false) => wrun f c'
        end
  end.

Lemma wrun_spec f c c' k : wrun f c = Some (c', k) ->
  forall U U', Pops k U U' -> lc (Rs U) c -->+ lc (Rs U') c'.
Proof.
  revert c c' k; induction f as [|f IH]; intros c c' k H U U' HP; [discriminate|].
  cbn in H.
  destruct (wready c) eqn:Ew.
  - destruct (wrun f (wpop c)) as [[c1 k1]|] eqn:E1; [|discriminate].
    inversion H; subst. destruct HP as [U1 [HU1 HP1]].
    eapply evstep_progress_trans.
    + apply (wpop_spec c U U1 Ew HU1).
    + eapply IH; eauto.
  - destruct (lstep c) as [[c1 [|]]|] eqn:E1; [| |discriminate].
    + inversion H; subst. cbn in HP; subst.
      apply progress_base. eapply lstep_spec; eauto.
    + eapply progress_step.
      * eapply lstep_spec; eauto.
      * eapply IH; eauto.
Qed.

(* ===================================================================== *)
(* 4. The nursery: 8 record types and their window runs (Lemma N).       *)
(* ===================================================================== *)

Inductive rt := XC | XD | XE | YC | YD | YE | ZD | ZE.

Definition rq (t : rt) : Q :=
  match t with
  | XC | YC => C
  | XD | YD | ZD => D
  | XE | YE | ZE => E
  end.

(* the gadget: the first three 1-runs after the head cell and 3 cells *)
Definition rg (t : rt) : list Sym :=
  match t with
  | XC => [1;1;1;1;1;1; 0;0;0;0; 1;1; 0;0;0;0; 1;1; 0;0;0]
  | XD => [1;1;1;1;1;1;1; 0;0;0;0; 1;1; 0;0;0;0; 1;1; 0;0;0]
  | XE => [1;1;1;1;1;1;1;1; 0;0;0;0; 1;1; 0;0;0;0; 1;1; 0;0;0]
  | YC => [1;1;0;1;1;1;1; 0;0;0;0; 1;1; 0;0;0]
  | YD => [1;1;1;0;1;1;1;1; 0;0;0;0; 1;1; 0;0;0]
  | YE => [1;1;1;1;0;1;1;1;1; 0;0;0;0; 1;1; 0;0;0]
  | ZD => [1;1;1;1;1; 0;0;0;0; 1;1; 0;0;0; 1;1;1; 0;0;0]
  | ZE => [1;1;1;1;1;1; 0;0;0;0; 1;1; 0;0;0; 1;1;1; 0;0;0]
  end.

Definition rnext (t : rt) : rt :=
  match t with
  | XC => XD | XD => XE | XE => YC | YC => YD
  | YD => YE | YE => ZD | ZD => ZE | ZE => XC
  end.

(* W-rule uses (pops) of each window run *)
Definition rk (t : rt) : nat :=
  match t with XE => 3 | YE => 12 | ZE => 2 | _ => 0 end.

(* the new walls put in front of the unit word *)
Definition rF (t : rt) : list unt :=
  match t with
  | XE => [uW; uW; uP; uSP]
  | YE => [uW; uP; uW; uP; uP; uSP; uP; uP; uP; uP; uSP]
  | ZE => [uP; uSP]
  | _ => []
  end.

(* the configuration at a left record: 0^inf <q G U 0^inf *)
Definition rcfg (t : rt) (U : list unt) : Q * tape :=
  const 0 <{{rq t}} rg t *> Rs U.

Lemma window_gen t U U' :
  wrun 4000 ([], 0, rg t, rq t) = Some (([], 0, rg (rnext t) ++ enc (rF t), rq (rnext t)), rk t) ->
  Pops (rk t) U U' -> rcfg t U -->+ rcfg (rnext t) (rF t ++ U').
Proof.
  intros H HP.
  pose proof (wrun_spec _ _ _ _ H U U' HP) as G.
  unfold rcfg. rewrite Rs_app, <- Str_app_assoc.
  exact G.
Qed.

Lemma window t U U' : Pops (rk t) U U' -> rcfg t U -->+ rcfg (rnext t) (rF t ++ U').
Proof.
  apply window_gen. destruct t; vm_compute; reflexivity.
Qed.

(* ===================================================================== *)
(* 5. The initial segment: 203,465 steps to the first X record.          *)
(* ===================================================================== *)

Definition U0 : list unt :=
  [uP; uSP; uP; uW; uP; uP; uP; uSP; uP; uP; uP; uP; uW;
   uP; uP; uP; uP; uP; uP; uP; uW;
   uP; uP; uP; uP; uP; uP; uP; uP; uP; uP; uP; uW;
   uP; uP; uP; uP; uP; uP; uP; uP; uP; uP;
   uD0; uD0; uD1; uD1; uD1; uD1].

Lemma init : c0 -->* rcfg XC U0.
Proof.
  change (rcfg XC U0) with (cconfig_to_config ([], rg XC ++ enc U0, 0, C)).
  rewrite c0_to_cconfig.
  apply cconfig_evstep_dec_spec with (n := 1000000).
  vm_compute. reflexivity.
Qed.

(* ===================================================================== *)
(* 6. Reduction to the unit-word dynamics.                               *)
(* ===================================================================== *)

Inductive Reach : rt -> list unt -> Prop :=
| Reach0 : Reach XC U0
| ReachS t U U' : Reach t U -> Pops (rk t) U U' -> Reach (rnext t) (rF t ++ U').

Definition AbsDefined : Prop := forall t U, Reach t U -> exists U', Pops (rk t) U U'.

Lemma nonhalt_of_abs : AbsDefined -> ~ halts tm c0.
Proof.
  intros H.
  eapply multistep_nonhalt; [apply init|].
  apply (progress_nonhalt_cond tm (rt * list unt) (XC, U0)
           (fun p => rcfg (fst p) (snd p)) (fun p => Reach (fst p) (snd p))).
  - intros [t U] HR. cbn in HR. destruct (H t U HR) as [U' HP].
    exists (rnext t, rF t ++ U'). split.
    + apply window; auto.
    + econstructor; eauto.
  - constructor.
Qed.

(* ===================================================================== *)
(* 7. Carry library: n carries (IncN), P transparency, digit counters,   *)
(*    Lemma C1.                                                          *)
(* ===================================================================== *)

Inductive IncN : nat -> list unt -> list unt -> Prop :=
| IncN_0 w : IncN 0 w w
| IncN_S n w w1 w2 : Inc w w1 -> IncN n w1 w2 -> IncN (S n) w w2.

Lemma IncN_1 w w' : Inc w w' -> IncN 1 w w'.
Proof. intros H. econstructor; eauto. constructor. Qed.

Lemma IncN_1_inv w w' : IncN 1 w w' -> Inc w w'.
Proof. intros H. inversion H as [|n w0 w1 w2 Hi Hn]; subst. inversion Hn; subst. auto. Qed.

Lemma IncN_add a b w w1 w2 : IncN a w w1 -> IncN b w1 w2 -> IncN (a + b) w w2.
Proof. induction 1; intros; cbn; auto. econstructor; eauto. Qed.

Lemma IncN_split a b w w2 : IncN (a + b) w w2 -> exists w1, IncN a w w1 /\ IncN b w1 w2.
Proof.
  revert w; induction a as [|a IH]; intros w H; cbn in H.
  - exists w. split; [constructor|auto].
  - inversion H as [|n' w' wa wb Hi Hn]; subst. destruct (IH _ Hn) as [w3 [H5 H6]].
    exists w3. split; auto. econstructor; eauto.
Qed.

Lemma IncN_det n w a b : IncN n w a -> IncN n w b -> a = b.
Proof.
  intros H; revert b; induction H as [|n w w1 w2 Hi Hn IH]; intros b Hb;
    inversion Hb as [|n' w' wa wb Hi' Hn']; subst; auto.
  assert (w1 = wa) by (eapply Inc_det; eauto). subst. auto.
Qed.

Lemma IncN_snoc n w w1 w2 : IncN n w w1 -> Inc w1 w2 -> IncN (S n) w w2.
Proof.
  intros H1 H2. replace (S n) with (n + 1) by lia.
  eapply IncN_add; eauto. apply IncN_1; auto.
Qed.

(* P is transparent *)
Lemma IncN_P n w w' : IncN n w w' -> IncN n (uP :: w) (uP :: w').
Proof. induction 1; econstructor; eauto. constructor; auto. Qed.

Lemma IncN_P_inv n w x : IncN n (uP :: w) x -> exists w', x = uP :: w' /\ IncN n w w'.
Proof.
  revert w; induction n as [|n IH]; intros w H; inversion H; subst.
  - exists w; split; [auto|constructor].
  - match goal with Hi : Inc (uP :: w) ?y, Hn : IncN n ?y x |- _ =>
      inversion Hi; subst; destruct (IH _ Hn) as [w'' [E H']]; subst end.
    eexists. split; [reflexivity|]. econstructor; eauto.
Qed.

Fixpoint Ps (a : nat) : list unt := match a with O => [] | S a' => uP :: Ps a' end.

Lemma IncN_Ps a n w w' : IncN n w w' -> IncN n (Ps a ++ w) (Ps a ++ w').
Proof. induction a; cbn; auto. intros H. apply IncN_P; auto. Qed.

(* one digit: t carries on a digit b pass (b + t) / 2 carries up *)
Definition dig (b : nat) : unt := if Nat.eqb (Nat.modulo b 2) O then uD0 else uD1.
Definition dval (u : unt) : nat := match u with uD1 => 1 | _ => 0 end.
Definition isdig (u : unt) : bool := match u with uD0 | uD1 => true | _ => false end.

Lemma IncN_digit t u w w' : isdig u = true -> IncN ((dval u + t) / 2) w w' ->
  IncN t (u :: w) (dig (dval u + t) :: w').
Proof.
  revert u w w'. induction t as [t IH] using lt_wf_ind. intros u w w' Hu H.
  destruct t as [|[|t]].
  - destruct u; try discriminate; cbn in *; inversion H; subst; constructor.
  - destruct u; try discriminate; cbn in *.
    + inversion H; subst. apply IncN_1. constructor.
    + apply IncN_1. apply IncN_1_inv in H. constructor; auto.
  - (* two carries first *)
    destruct u; try discriminate.
    + (* D0: D0 -> D1 -> D0 + one carry *)
      replace ((dval uD0 + S (S t)) / 2) with (1 + (dval uD0 + t) / 2) in H.
      2:{ cbn [dval]. rewrite !Nat.add_0_l. replace (S (S t)) with (t + 1 * 2)%nat by lia.
          rewrite Nat.div_add by lia. lia. }
      destruct (IncN_split _ _ _ _ H) as [w1 [H1 H2]].
      apply IncN_1_inv in H1.
      replace (S (S t)) with (2 + t) by lia.
      eapply IncN_add.
      * econstructor; [constructor|]. econstructor; [constructor; eauto|]. constructor.
      * replace (dig (dval uD0 + (2 + t))) with (dig (dval uD0 + t)).
        { apply IH; try lia; auto. }
        unfold dig. cbn [dval]. f_equal.
        replace (O + (2 + t))%nat with (t + 1 * 2)%nat by lia. rewrite Nat.Div0.mod_add. reflexivity.
    + (* D1: D1 -> D0 + carry -> D1 *)
      replace ((dval uD1 + S (S t)) / 2) with (1 + (dval uD1 + t) / 2) in H.
      2:{ cbn [dval]. replace (1 + S (S t))%nat with ((1 + t) + 1 * 2)%nat by lia.
          rewrite Nat.div_add by lia. lia. }
      destruct (IncN_split _ _ _ _ H) as [w1 [H1 H2]].
      apply IncN_1_inv in H1.
      replace (S (S t)) with (2 + t) by lia.
      eapply IncN_add.
      * econstructor; [constructor; eauto|]. econstructor; [constructor|]. constructor.
      * replace (dig (dval uD1 + (2 + t))) with (dig (dval uD1 + t)).
        { apply IH; try lia; auto. }
        unfold dig. cbn [dval]. f_equal.
        replace (1 + (2 + t))%nat with ((1 + t) + 1 * 2)%nat by lia. rewrite Nat.Div0.mod_add. reflexivity.
Qed.

(* walls: SP (state 0, absorbs the next carry) and W (state 1, fires) *)
Definition wallu (b : bool) : unt := if b then uW else uSP.

Lemma Inc_SP_W r : Inc (uSP :: r) (uW :: r).
Proof. constructor. Qed.

(* a firing: three carries on the rest, then the shift lands on its first unit, a P *)
Lemma Inc_W_fire r r' : Inc3Pop r r' -> Inc (uW :: r) (uP :: uSP :: r').
Proof.
  intros [a [b [H1 [H2 H3]]]]. eapply Inc_W; eauto.
Qed.

Lemma Pops_add a b U U1 U2 : Pops a U U1 -> Pops b U1 U2 -> Pops (a + b) U U2.
Proof.
  revert U; induction a as [|a IH]; intros U H1 H2; cbn in *.
  - subst; auto.
  - destruct H1 as [V [HV H1]]. exists V. split; [auto|eapply IH; eauto].
Qed.

Lemma Pops_split a b U U2 : Pops (a + b) U U2 -> exists U1, Pops a U U1 /\ Pops b U1 U2.
Proof.
  revert U; induction a as [|a IH]; intros U H; cbn in *.
  - exists U. split; auto.
  - destruct H as [V [HV H]]. destruct (IH _ H) as [U1 [H1 H2]].
    exists U1. split; auto. exists V. auto.
Qed.

(* the rotor: t carries on a wall in state b fire it (t + b) / 2 times *)
Lemma wall_feed t (b : bool) r r' :
  Pops ((t + Nat.b2n b) / 2) r r' ->
  IncN t (wallu b :: r) (Ps ((t + Nat.b2n b) / 2) ++ wallu (Nat.odd (t + Nat.b2n b)) :: r').
Proof.
  revert b r r'. induction t as [t IH] using lt_wf_ind. intros b r r' H.
  destruct b.
  - (* W *)
    destruct t as [|t].
    + cbn in *. subst. constructor.
    + replace ((S t + Nat.b2n true) / 2) with (1 + (t + Nat.b2n false) / 2) in *.
      2:{ cbn [Nat.b2n]. replace (S t + 1) with (t + 0 + 1 * 2) by lia.
          rewrite Nat.div_add by lia. lia. }
      destruct (Pops_split _ _ _ _ H) as [r1 [H1 H2]].
      cbn in H1. destruct H1 as [V [HV E]]. subst V.
      econstructor.
      * apply Inc_W_fire. eauto.
      * assert (E : forall x y, Ps (1 + x) ++ y = uP :: (Ps x ++ y)) by reflexivity.
        rewrite E. apply IncN_P.
        replace (Nat.odd (S t + Nat.b2n true)) with (Nat.odd (t + Nat.b2n false)).
        { exact (IH t ltac:(lia) false r1 r' H2). }
        cbn [Nat.b2n]. replace (S t + 1) with (S (S (t + 0))) by lia.
        rewrite Nat.odd_succ_succ. reflexivity.
  - (* SP *)
    destruct t as [|t].
    + cbn in *. subst. constructor.
    + replace ((S t + Nat.b2n false) / 2) with ((t + Nat.b2n true) / 2) in *.
      2:{ cbn [Nat.b2n]. f_equal. lia. }
      econstructor.
      * apply Inc_SP_W.
      * replace (Nat.odd (S t + Nat.b2n false)) with (Nat.odd (t + Nat.b2n true)).
        { apply (IH t ltac:(lia) true). auto. }
        cbn [Nat.b2n]. f_equal. lia.
Qed.

(* Lemma C1: three carries turn a first unit P, S1, SP or W into P *)
Lemma C1 u r x : In u [uP; uS1; uSP; uW] -> IncN 3 (u :: r) x -> exists x', x = uP :: x'.
Proof.
  intros Hu H.
  destruct Hu as [<-|[<-|[<-|[<-|[]]]]].
  - apply IncN_P_inv in H. destruct H as [w' [E _]]. eauto.
  - inversion H as [|n w w1 w2 Hi Hn]; subst. inversion Hi; subst.
    apply IncN_P_inv in Hn. destruct Hn as [w' [E _]]. eauto.
  - inversion H as [|n w w1 w2 Hi Hn]; subst. inversion Hi; subst.
    inversion Hn as [|n' w' wa wb Hi' Hn']; subst. inversion Hi'; subst.
    apply IncN_P_inv in Hn'. destruct Hn' as [w'' [E _]]. eauto.
  - inversion H as [|n w w1 w2 Hi Hn]; subst. inversion Hi; subst.
    apply IncN_P_inv in Hn. destruct Hn as [w' [E _]]. eauto.
Qed.

(* r binary digits of v, least significant first *)
Fixpoint digits (r v : nat) : list unt :=
  match r with
  | O => []
  | S r' => dig v :: digits r' (v / 2)
  end.

Lemma dval_dig v : dval (dig v) = v mod 2.
Proof.
  unfold dig. destruct (Nat.eqb_spec (v mod 2) 0) as [E|E]; cbn [dval]; [lia|].
  pose proof (Nat.mod_upper_bound v 2). lia.
Qed.

Lemma isdig_dig v : isdig (dig v) = true.
Proof. unfold dig. destruct (Nat.eqb (v mod 2) 0); reflexivity. Qed.

Lemma dig_mod v : dig (v mod 2) = dig v.
Proof. unfold dig. rewrite Nat.Div0.mod_mod. reflexivity. Qed.

(* t carries on an r-digit counter pass ((v mod 2^r) + t) / 2^r carries up *)
Lemma IncN_digits r v t rest rest' :
  IncN ((v mod 2 ^ r + t) / 2 ^ r) rest rest' ->
  IncN t (digits r v ++ rest) (digits r (v + t) ++ rest').
Proof.
  revert v t. induction r as [|r IH]; intros v t H.
  - cbn [digits app]. replace ((v mod 2 ^ 0 + t) / 2 ^ 0) with t in H; [auto|].
    rewrite Nat.pow_0_r, Nat.mod_1_r, Nat.div_1_r. lia.
  - cbn [digits app].
    assert (Ev : v = 2 * (v / 2) + v mod 2) by (apply Nat.div_mod; lia).
    assert (E1 : (v + t) / 2 = v / 2 + (v mod 2 + t) / 2).
    { rewrite Ev at 1. replace (2 * (v / 2) + v mod 2 + t) with ((v mod 2 + t) + (v / 2) * 2) by lia.
      rewrite Nat.div_add by lia. lia. }
    replace (dig (v + t)) with (dig (dval (dig v) + t)).
    2:{ rewrite dval_dig. rewrite <- dig_mod, <- (dig_mod (v + t)). f_equal.
        rewrite Nat.Div0.add_mod_idemp_l. reflexivity. }
    apply IncN_digit; [apply isdig_dig|].
    rewrite E1, dval_dig. apply IH.
    replace ((v / 2) mod 2 ^ r + (v mod 2 + t) / 2) with ((v mod 2 ^ S r + t) / 2).
    + rewrite Nat.Div0.div_div. rewrite Nat.pow_succ_r'. exact H.
    + rewrite Nat.pow_succ_r'. rewrite Nat.Div0.mod_mul_r.
      replace (v mod 2 + 2 * ((v / 2) mod 2 ^ r) + t) with ((v mod 2 + t) + ((v / 2) mod 2 ^ r) * 2) by lia.
      rewrite Nat.div_add by lia. lia.
Qed.

(* ===================================================================== *)
(* 8. The closed zone system (proof.md section 5).                       *)
(* ===================================================================== *)

Definition notP (w : list unt) : Prop := match w with uP :: _ => False | _ => True end.

Definition pj (j : nat) : nat := nth (j mod 8) [47; 48; 48; 47; 48; 47; 48; 47] 47.

(* one step: feed c = D + p(j) carries, every leading P is dropped and adds
   3 carries, stop at the least fixed point m = c + 3 A(m), then the
   absorption shift *)
Definition cs_step (Z : list unt) (D j : nat) (Z' : list unt) (D' j' : nat) : Prop :=
  exists m A Y,
    IncN m Z (Ps A ++ Y) /\ notP Y /\ m = D + pj j + 3 * A /\
    (forall m' A' Y', m' < m -> IncN m' Z (Ps A' ++ Y') -> notP Y' -> m' <> D + pj j + 3 * A') /\
    shift Y = Some Z' /\ D' = D + A /\ j' = S j.

Inductive CSreach : list unt -> nat -> nat -> Prop :=
| CS1 : CSreach [uS1; uD0; uD1; uD1; uD1; uD0; uD1] 0 1
| CSS Z D j Z' D' j' : CSreach Z D j -> cs_step Z D j Z' D' j' -> CSreach Z' D' j'.

(* executable carries *)
Fixpoint incf (n : nat) (w : list unt) : option (list unt) :=
  match n with
  | O => None
  | S n' =>
      match w with
      | [] => Some [uD1]
      | uD0 :: w' => Some (uD1 :: w')
      | uS1 :: w' => Some (uP :: w')
      | uSP :: w' => Some (uW :: w')
      | uD1 :: w' => match incf n' w' with Some x => Some (uD0 :: x) | None => None end
      | uP :: w' => match incf n' w' with Some x => Some (uP :: x) | None => None end
      | uW :: w' =>
          match incf n' w' with
          | None => None
          | Some x1 =>
              match incf n' x1 with
              | None => None
              | Some x2 =>
                  match incf n' x2 with
                  | None => None
                  | Some x3 => match shift x3 with Some x4 => Some (uP :: x4) | None => None end
                  end
              end
          end
      end
  end.

Lemma incf_sound n w w' : incf n w = Some w' -> Inc w w'.
Proof.
  revert w w'; induction n as [|n IH]; intros w w' H; [discriminate|].
  destruct w as [|u w]; cbn in H.
  - inversion H; constructor.
  - destruct u.
    + inversion H; constructor.
    + destruct (incf n w) eqn:E; inversion H; subst. constructor; auto.
    + destruct (incf n w) eqn:E; inversion H; subst. constructor; auto.
    + inversion H; constructor.
    + inversion H; constructor.
    + destruct (incf n w) as [x1|] eqn:E1; [|discriminate].
      destruct (incf n x1) as [x2|] eqn:E2; [|discriminate].
      destruct (incf n x2) as [x3|] eqn:E3; [|discriminate].
      destruct (shift x3) as [x4|] eqn:E4; inversion H; subst.
      eapply Inc_W; eauto.
Qed.

Fixpoint incNf (fuel k : nat) (w : list unt) : option (list unt) :=
  match k with
  | O => Some w
  | S k' => match incf fuel w with Some x => incNf fuel k' x | None => None end
  end.

Lemma incNf_sound fuel k w w' : incNf fuel k w = Some w' -> IncN k w w'.
Proof.
  revert w; induction k as [|k IH]; intros w H; cbn in H.
  - inversion H; constructor.
  - destruct (incf fuel w) eqn:E; [|discriminate].
    econstructor; [eapply incf_sound; eauto|]. auto.
Qed.

Fixpoint splitP (w : list unt) : nat * list unt :=
  match w with
  | uP :: w' => let (a, y) := splitP w' in (S a, y)
  | _ => (O, w)
  end.

Lemma splitP_spec w : let (a, y) := splitP w in w = Ps a ++ y /\ notP y.
Proof.
  induction w as [|u w IH]; cbn; [split; [reflexivity|exact I]|].
  destruct u; try (split; [reflexivity|exact I]).
  destruct (splitP w) as [a y]. destruct IH as [E N]. subst. split; auto.
Qed.

Lemma Ps_notP_inj a b x y : Ps a ++ x = Ps b ++ y -> notP x -> notP y -> a = b /\ x = y.
Proof.
  revert b; induction a as [|a IH]; intros [|b] E Nx Ny; cbn in *.
  - auto.
  - subst. contradiction.
  - subst. contradiction.
  - inversion E. destruct (IH b H0 Nx Ny). auto.
Qed.

(* leading P units are never lost *)
Lemma IncN_Ps_inv k a y x : IncN k (Ps a ++ y) x -> exists y', x = Ps a ++ y' /\ IncN k y y'.
Proof.
  revert x; induction a as [|a IH]; intros x H; cbn in *.
  - eauto.
  - apply IncN_P_inv in H. destruct H as [w' [E H]]. subst.
    destruct (IH _ H) as [y' [E2 H2]]. subst. eauto.
Qed.

Lemma Ps_prefix_le a b y Y : Ps a ++ y = Ps b ++ Y -> notP Y -> a <= b.
Proof.
  revert b; induction a as [|a IH]; intros [|b] E N; cbn in *; try lia.
  - subst. contradiction.
  - inversion E. specialize (IH b H0 N). lia.
Qed.

(* no fixed point at m' *)
Definition NF (Z : list unt) (c m' : nat) : Prop :=
  forall A' Y', IncN m' Z (Ps A' ++ Y') -> notP Y' -> m' <> c + 3 * A'.

Fixpoint cs_loop (fuel cf c m : nat) (Zm : list unt) : option (nat * nat * list unt) :=
  match fuel with
  | O => None
  | S f =>
      let (a, y) := splitP Zm in
      if Nat.eqb m (c + 3 * a) then Some (m, a, y)
      else
        match incNf cf (c + 3 * a - m) Zm with
        | Some Zm' => cs_loop f cf c (c + 3 * a) Zm'
        | None => None
        end
  end.

Lemma cs_loop_sound fuel cf c Z m Zm m2 A2 Y2 :
  cs_loop fuel cf c m Zm = Some (m2, A2, Y2) ->
  IncN m Z Zm -> (forall m', m' < m -> NF Z c m') ->
  (forall A Y, Zm = Ps A ++ Y -> notP Y -> m <= c + 3 * A) ->
  IncN m2 Z (Ps A2 ++ Y2) /\ notP Y2 /\ m2 = c + 3 * A2 /\ (forall m', m' < m2 -> NF Z c m').
Proof.
  revert m Zm; induction fuel as [|f IH]; intros m Zm H HZ HNF Hle; [discriminate|].
  cbn [cs_loop] in H. pose proof (splitP_spec Zm) as HS.
  destruct (splitP Zm) as [A Y]. destruct HS as [EZ NY].
  specialize (Hle A Y EZ NY).
  destruct (Nat.eqb m (c + 3 * A)) eqn:Em; [apply Nat.eqb_eq in Em | apply Nat.eqb_neq in Em].
  - inversion H; subst. repeat split; auto.
  - destruct (incNf cf (c + 3 * A - m) Zm) as [Zm'|] eqn:E; [|discriminate].
    apply incNf_sound in E.
    assert (HZ' : IncN (c + 3 * A) Z Zm').
    { replace (c + 3 * A) with (m + (c + 3 * A - m)) by lia. eapply IncN_add; eauto. }
    eapply IH; eauto.
    + intros m' Hm' A' Y' H' NY'.
      destruct (Nat.lt_ge_cases m' m) as [Hlt|Hge].
      * apply (HNF m' Hlt A' Y' H' NY').
      * (* between m and c + 3A: at least A leading P *)
        replace m' with (m + (m' - m)) in H' by lia.
        destruct (IncN_split _ _ _ _ H') as [w1 [Hw1 Hw2]].
        assert (w1 = Zm) by (eapply IncN_det; eauto). subst w1.
        rewrite EZ in Hw2. destruct (IncN_Ps_inv _ _ _ _ Hw2) as [y' [Ey' _]].
        pose proof (Ps_prefix_le _ _ _ _ (eq_sym Ey') NY'). lia.
    + intros A' Y' EZ' NY'. subst Zm'.
      replace (c + 3 * A) with (m + (c + 3 * A - m)) in HZ' by lia.
      destruct (IncN_split _ _ _ _ HZ') as [w1 [Hw1 Hw2]].
      assert (w1 = Zm) by (eapply IncN_det; eauto). subst w1.
      rewrite EZ in Hw2. destruct (IncN_Ps_inv _ _ _ _ Hw2) as [y' [Ey' _]].
      pose proof (Ps_prefix_le _ _ _ _ (eq_sym Ey') NY'). lia.
Qed.

Definition csf (fuel cf : nat) (s : list unt * nat * nat) : option (list unt * nat * nat) :=
  let '(z, d, j) := s in
  match incNf cf (d + pj j) z with
  | None => None
  | Some zc =>
      match cs_loop fuel cf (d + pj j) (d + pj j) zc with
      | None => None
      | Some (m, a, y) =>
          match shift y with
          | Some z' => Some (z', d + a, S j)
          | None => None
          end
      end
  end.

Lemma csf_sound fuel cf Z D j Z' D' j' :
  csf fuel cf (Z, D, j) = Some (Z', D', j') -> cs_step Z D j Z' D' j'.
Proof.
  unfold csf. intros H.
  destruct (incNf cf (D + pj j) Z) as [Zc|] eqn:E1; [|discriminate].
  destruct (cs_loop fuel cf (D + pj j) (D + pj j) Zc) as [[[m A] Y]|] eqn:E2; [|discriminate].
  destruct (shift Y) as [Z''|] eqn:E3; inversion H; subst.
  apply incNf_sound in E1.
  destruct (cs_loop_sound _ _ _ Z _ _ _ _ _ E2 E1) as [H1 [H2 [H3 H4]]].
  - intros m' Hm' A' Y' _ _. lia.
  - intros. lia.
  - exists m, A, Y. repeat split; auto.
    intros m' A' Y' Hm' HI HN. apply (H4 m' Hm' A' Y' HI HN).
Qed.

Fixpoint csiter (n : nat) (s : list unt * nat * nat) : option (list unt * nat * nat) :=
  match n with
  | O => Some s
  | S n' => match csf 200 200 s with Some s' => csiter n' s' | None => None end
  end.

Lemma csiter_reach n Z D j Z' D' j' :
  CSreach Z D j -> csiter n (Z, D, j) = Some (Z', D', j') -> CSreach Z' D' j'.
Proof.
  revert Z D j; induction n as [|n IH]; intros Z D j HR H; cbn [csiter] in H.
  - inversion H; subst; auto.
  - destruct (csf 200 200 (Z, D, j)) as [[[Z1 D1] j1]|] eqn:E; [|discriminate].
    eapply IH; [|exact H]. econstructor; [exact HR|]. eapply csf_sound; eauto.
Qed.

(* the closed system reaches the canonical state C(0) at j = 17 *)
Lemma C0_reach : CSreach [uS1; uD0; uD1; uD1; uD1; uD1; uD1] 16 17.
Proof.
  eapply (csiter_reach 16); [constructor|].
  vm_compute. reflexivity.
Qed.

(* ===================================================================== *)
(* 9. Pops on conveyor words (used by the record invariant).             *)
(* ===================================================================== *)

Lemma IncN_3_inv w x : IncN 3 w x -> exists a b, Inc w a /\ Inc a b /\ Inc b x.
Proof.
  intros H.
  inversion H as [|n1 w1 a1 x1 H1 Hn1]; subst.
  inversion Hn1 as [|n2 w2 a2 x2 H2 Hn2]; subst.
  inversion Hn2 as [|n3 w3 a3 x3 H3 Hn3]; subst.
  inversion Hn3; subst. eauto.
Qed.

Lemma Inc3Pop_of w x : IncN 3 w (uP :: x) -> Inc3Pop w x.
Proof. intros H. destruct (IncN_3_inv _ _ H) as [a [b [H1 [H2 H3]]]]. exists a, b. auto. Qed.

Lemma IncN_of_Inc3Pop w x : Inc3Pop w x -> IncN 3 w (uP :: x).
Proof.
  intros [a [b [H1 [H2 H3]]]].
  econstructor; [eauto|]. econstructor; [eauto|]. econstructor; [eauto|]. constructor.
Qed.

(* a firing over a wire: three carries pass the first P, which is popped *)
Lemma Inc3Pop_P y y3 : IncN 3 y y3 -> Inc3Pop (uP :: y) y3.
Proof. intros H. apply Inc3Pop_of. apply IncN_P. auto. Qed.

Lemma Pops_Ps k a y y' : IncN (3 * k) y y' -> Pops k (Ps (k + a) ++ y) (Ps a ++ y').
Proof.
  revert y; induction k as [|k IH]; intros y H; cbn [Pops].
  - cbn in *. inversion H; subst. reflexivity.
  - replace (3 * S k) with (3 + 3 * k) in H by lia.
    destruct (IncN_split _ _ _ _ H) as [y3 [H3 Hk]].
    exists (Ps (k + a) ++ y3). split.
    + cbn [Ps app]. apply Inc3Pop_P. apply IncN_Ps. auto.
    + apply IH. auto.
Qed.

(* a firing directly below a wall: the wall above has moved (Lemma C1) *)
Lemma Inc3Pop_wall (b : bool) r r' :
  Pops ((3 + Nat.b2n b) / 2) r r' ->
  Inc3Pop (wallu b :: r) (Ps ((3 + Nat.b2n b) / 2 - 1) ++ wallu (Nat.odd (3 + Nat.b2n b)) :: r').
Proof.
  intros H. apply Inc3Pop_of.
  pose proof (wall_feed 3 b r r' H) as G.
  destruct b; cbn in *; exact G.
Qed.

(* ===================================================================== *)
(* 10. Upward flow (Lemma L, item 1): a prefix X that passes e carries   *)
(*     up, with every shift landing inside X, acts on X ++ Y as          *)
(*     X' ++ inc^e(Y).                                                   *)
(* ===================================================================== *)

(* a shift that must land inside X *)
Fixpoint shiftX (X : list unt) : option (list unt) :=
  match X with
  | [] => None
  | uD0 :: X' =>
      match shiftX X' with
      | Some X'' => Some (uD0 :: X'')
      | None => None
      end
  | uD1 :: X' => Some (uS1 :: X')
  | uP :: X' => Some (uSP :: X')
  | _ => None
  end.

Lemma shiftX_app X X' Y : shiftX X = Some X' -> shift (X ++ Y) = Some (X' ++ Y).
Proof.
  revert X'; induction X as [|u X IH]; intros X' H; cbn in H; [discriminate|].
  destruct u; try discriminate.
  - destruct (shiftX X) as [X''|] eqn:E; [|discriminate]. inversion H; subst.
    cbn [app shift]. rewrite (IH X'' eq_refl). reflexivity.
  - inversion H; subst. reflexivity.
  - inversion H; subst. reflexivity.
Qed.

Inductive IncX : list unt -> nat -> list unt -> Prop :=
| IncX_nil : IncX [] 1 []
| IncX_D0 X : IncX (uD0 :: X) 0 (uD1 :: X)
| IncX_S1 X : IncX (uS1 :: X) 0 (uP :: X)
| IncX_SP X : IncX (uSP :: X) 0 (uW :: X)
| IncX_D1 X e X' : IncX X e X' -> IncX (uD1 :: X) e (uD0 :: X')
| IncX_P X e X' : IncX X e X' -> IncX (uP :: X) e (uP :: X')
| IncX_W X e1 e2 e3 X1 X2 X3 X4 :
    IncX X e1 X1 -> IncX X1 e2 X2 -> IncX X2 e3 X3 -> shiftX X3 = Some X4 ->
    IncX (uW :: X) (e1 + e2 + e3) (uP :: X4).

Lemma IncX_flow X e X' : IncX X e X' ->
  forall Y Y', IncN e Y Y' -> Inc (X ++ Y) (X' ++ Y').
Proof.
  induction 1; intros Y Y' HY; cbn [app].
  - apply IncN_1_inv. exact HY.
  - inversion HY; subst. constructor.
  - inversion HY; subst. constructor.
  - inversion HY; subst. constructor.
  - constructor. auto.
  - constructor. auto.
  - rewrite <- Nat.add_assoc in HY.
    destruct (IncN_split _ _ _ _ HY) as [Y1 [Ha Hbc]].
    destruct (IncN_split _ _ _ _ Hbc) as [Y2 [Hb Hc]].
    eapply Inc_W.
    + apply IHIncX1. exact Ha.
    + apply IHIncX2. exact Hb.
    + apply IHIncX3. exact Hc.
    + apply shiftX_app. assumption.
Qed.

(* n carries on X *)
Inductive IncXN : nat -> list unt -> nat -> list unt -> Prop :=
| IncXN_0 X : IncXN 0 X 0 X
| IncXN_S n X e X1 e' X2 : IncX X e X1 -> IncXN n X1 e' X2 -> IncXN (S n) X (e + e') X2.

Lemma IncXN_flow n X e X' : IncXN n X e X' ->
  forall Y Y', IncN e Y Y' -> IncN n (X ++ Y) (X' ++ Y').
Proof.
  induction 1; intros Y Y' HY.
  - inversion HY; subst. constructor.
  - destruct (IncN_split _ _ _ _ HY) as [Y1 [H1 H2]].
    econstructor.
    + eapply IncX_flow; eauto.
    + apply IHIncXN. exact H2.
Qed.

(* executable version *)
Fixpoint incXf (n : nat) (X : list unt) : option (nat * list unt) :=
  match n with
  | O => None
  | S n' =>
      match X with
      | [] => Some (1%nat, [])
      | uD0 :: X' => Some (O, uD1 :: X')
      | uS1 :: X' => Some (O, uP :: X')
      | uSP :: X' => Some (O, uW :: X')
      | uD1 :: X' => match incXf n' X' with Some (e, x) => Some (e, uD0 :: x) | None => None end
      | uP :: X' => match incXf n' X' with Some (e, x) => Some (e, uP :: x) | None => None end
      | uW :: X' =>
          match incXf n' X' with
          | None => None
          | Some (e1, x1) =>
              match incXf n' x1 with
              | None => None
              | Some (e2, x2) =>
                  match incXf n' x2 with
                  | None => None
                  | Some (e3, x3) =>
                      match shiftX x3 with
                      | Some x4 => Some (e1 + e2 + e3, uP :: x4)
                      | None => None
                      end
                  end
              end
          end
      end
  end.

Lemma incXf_sound n X e X' : incXf n X = Some (e, X') -> IncX X e X'.
Proof.
  revert X e X'; induction n as [|n IH]; intros X e X' H; [discriminate|].
  destruct X as [|u X]; cbn [incXf] in H.
  - inversion H; constructor.
  - destruct u.
    + inversion H; constructor.
    + destruct (incXf n X) as [[e0 x]|] eqn:E; inversion H; subst. constructor; auto.
    + destruct (incXf n X) as [[e0 x]|] eqn:E; inversion H; subst. constructor; auto.
    + inversion H; constructor.
    + inversion H; constructor.
    + destruct (incXf n X) as [[e1 x1]|] eqn:E1; [|discriminate].
      destruct (incXf n x1) as [[e2 x2]|] eqn:E2; [|discriminate].
      destruct (incXf n x2) as [[e3 x3]|] eqn:E3; [|discriminate].
      destruct (shiftX x3) as [x4|] eqn:E4; inversion H; subst.
      eapply IncX_W; eauto.
Qed.