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

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

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

(* ===================================================================== *)
(* A symbolic run-length simulator.                                      *)
(* The tape is cut into alternating runs.  A run is a first symbol and a *)
(* length; a length is a linear form c + sum v_i x_i over N.  A side is  *)
(* a list of runs (nearest the head first) followed by either the blank  *)
(* stream or an abstract side.  The simulator crosses a whole run in one *)
(* step when the head state is in one of the two sweep cycles.           *)
(* ===================================================================== *)

Definition sneg (s : Sym) : Sym := match s with S0 => S1 | S1 => S0 end.
Definition seqb (a b : Sym) : bool :=
  match a, b with S0, S0 | S1, S1 => true | _, _ => false end.

Record lf := LF { lc : N; lv : list N }.

Fixpoint dot (vs nu : list N) : N :=
  match vs, nu with
  | v :: vs', x :: nu' => (v * x + dot vs' nu')%N
  | _, _ => 0%N
  end.

Definition ev (nu : list N) (a : lf) : nat := N.to_nat (lc a + dot (lv a) nu).

Fixpoint zadd (a b : list N) : list N :=
  match a, b with
  | x :: a', y :: b' => (x + y)%N :: zadd a' b'
  | [], _ => b
  | _, [] => a
  end.

Definition lf_add (a b : lf) : lf := LF (lc a + lc b) (zadd (lv a) (lv b)).
Definition lf_S (a : lf) : lf := LF (N.succ (lc a)) (lv a).
Definition lf_one : lf := LF 1 [].
Definition allz (vs : list N) : bool := forallb (fun v => N.eqb v 0) vs.
Definition all4 (vs : list N) : bool := forallb (fun v => N.eqb (N.modulo v 4) 0) vs.
Definition is_zero (a : lf) : bool := andb (N.eqb (lc a) 0) (allz (lv a)).
Definition is_one (a : lf) : bool := andb (N.eqb (lc a) 1) (allz (lv a)).
Definition posb (a : lf) : bool := negb (N.eqb (lc a) 0).

Inductive tl_ := T0 | TV (k : nat).
Definition run : Type := (Sym * lf)%type.
Definition sd : Type := (list run * tl_)%type.

Fixpoint alt (b : Sym) (n : nat) : list Sym :=
  match n with O => [] | S n' => b :: alt (sneg b) n' end.

Definition ev_tl (sg : nat -> side) (t : tl_) : side :=
  match t with T0 => const S0 | TV k => sg k end.

Fixpoint ev_runs (nu : list N) (rs : list run) (s : side) : side :=
  match rs with
  | [] => s
  | (b, n) :: rs' => alt b (ev nu n) *> ev_runs nu rs' s
  end.

Definition ev_sd nu sg (s : sd) : side := ev_runs nu (fst s) (ev_tl sg (snd s)).

Fixpoint pop_runs (rs : list run) (t : tl_) : option (Sym * sd) :=
  match rs with
  | (b, n) :: rs' =>
      if is_zero n then pop_runs rs' t
      else if posb n then
        Some (b, ((if is_one n then rs' else (sneg b, LF (N.pred (lc n)) (lv n)) :: rs'), t))
      else None
  | [] => match t with T0 => Some (S0, ([], T0)) | TV _ => None end
  end.

Definition pop (s : sd) : option (Sym * sd) := pop_runs (fst s) (snd s).

Definition push (w : Sym) (s : sd) : sd :=
  match s with
  | ((b0, n0) :: rs, t) =>
      if seqb w b0 then ((w, lf_one) :: (b0, n0) :: rs, t)
      else ((w, lf_S n0) :: rs, t)
  | ([], t) => ([(w, lf_one)], t)
  end.

(* the symbol that would continue the alternation after a run (c, n) *)
Definition afterb (c : Sym) (n : lf) : Sym := if N.eqb (N.modulo (lc n) 2) 0 then c else sneg c.

Definition push_run (c : Sym) (n : lf) (s : sd) : sd :=
  match s with
  | ((b0, n0) :: rs, t) =>
      if seqb (afterb c n) b0 then ((c, lf_add n n0) :: rs, t)
      else ((c, n) :: (b0, n0) :: rs, t)
  | ([], t) => ([(c, n)], t)
  end.

(* the two sweep cycles *)
Definition cR_st (i : nat) : Q :=
  match i mod 4 with 0 => B | 1 => C | 2 => A | _ => B end.
Definition cR_bt (i : nat) : Sym :=
  match i mod 4 with 0 => S0 | 1 => S1 | 2 => S0 | _ => S1 end.
Definition cR_idx (q : Q) (b : Sym) : option nat :=
  match q, b with
  | B, S0 => Some 0 | C, S1 => Some 1 | A, S0 => Some 2 | B, S1 => Some 3
  | _, _ => None
  end.
Definition cL_st (i : nat) : Q :=
  match i mod 4 with 0 => D | 1 => D | 2 => E | _ => C end.
Definition cL_bt (i : nat) : Sym :=
  match i mod 4 with 0 => S1 | 1 => S0 | 2 => S1 | _ => S0 end.
Definition cL_idx (q : Q) (b : Sym) : option nat :=
  match q, b with
  | D, S1 => Some 0 | D, S0 => Some 1 | E, S1 => Some 2 | C, S0 => Some 3
  | _, _ => None
  end.

(* the last symbol of a run (c, n) *)
Definition lastb (c : Sym) (n : lf) : Sym := if N.eqb (N.modulo (lc n) 2) 0 then sneg c else c.

Inductive cfg := Rc (q : Q) (l r : sd) | Lc (q : Q) (l r : sd).

Definition ev_cfg nu sg (c : cfg) : Q * tape :=
  match c with
  | Rc q l r => (ev_sd nu sg l) {{q}}> (ev_sd nu sg r)
  | Lc q l r => (ev_sd nu sg l) <{{q}} (ev_sd nu sg r)
  end.

Definition single (c : cfg) : option cfg :=
  match c with
  | Rc q l r =>
    match pop r with
    | Some (s, r') =>
      match tm (q, s) with
      | Some (w, R, q') => Some (Rc q' (push w l) r')
      | Some (w, L, q') => Some (Lc q' l (push w r'))
      | None => None
      end
    | None => None
    end
  | Lc q l r =>
    match pop l with
    | Some (s, l') =>
      match tm (q, s) with
      | Some (w, R, q') => Some (Rc q' (push w l') r)
      | Some (w, L, q') => Some (Lc q' l' (push w r))
      | None => None
      end
    | None => None
    end
  end.

Definition tag (o : option cfg) : option (cfg * bool) :=
  match o with Some c => Some (c, true) | None => None end.

Definition sstep (c : cfg) : option (cfg * bool) :=
  match c with
  | Rc q l ((b, n) :: rs, t) =>
      if is_zero n then Some (Rc q l (rs, t), false) else
      match cR_idx q b with
      | Some i =>
          if all4 (lv n) then
            Some (Rc (cR_st (i + N.to_nat (N.modulo (lc n) 4))) (push_run (sneg (lastb b n)) n l) (rs, t), posb n)
          else tag (single c)
      | None => tag (single c)
      end
  | Lc q ((b, n) :: ls, t) r =>
      if is_zero n then Some (Lc q (ls, t) r, false) else
      match cL_idx q b with
      | Some i =>
          if all4 (lv n) then
            Some (Lc (cL_st (i + N.to_nat (N.modulo (lc n) 4))) (ls, t) (push_run (sneg (lastb b n)) n r), posb n)
          else tag (single c)
      | None => tag (single c)
      end
  | _ => tag (single c)
  end.

(* run exactly p steps; the flag says whether at least one TM step was made *)
Fixpoint runp (p : positive) (c : cfg) : option (cfg * bool) :=
  match p with
  | xH => sstep c
  | xO p' =>
      match runp p' c with
      | Some (c1, b1) => match runp p' c1 with Some (c2, b2) => Some (c2, orb b1 b2) | None => None end
      | None => None
      end
  | xI p' =>
      match sstep c with
      | Some (c0, b0) =>
          match runp p' c0 with
          | Some (c1, b1) => match runp p' c1 with Some (c2, b2) => Some (c2, orb b0 (orb b1 b2)) | None => None end
          | None => None
          end
      | None => None
      end
  end.

(* ===================================================================== *)
(* Soundness                                                             *)
(* ===================================================================== *)

Lemma sneg_neq a b : seqb a b = false -> b = sneg a.
Proof. destruct a, b; cbn; congruence. Qed.

Lemma seqb_eq a b : seqb a b = true -> a = b.
Proof. destruct a, b; cbn; congruence. Qed.

Lemma sneg_sneg a : sneg (sneg a) = a.
Proof. destruct a; reflexivity. Qed.

Lemma dot_zadd a b nu : dot (zadd a b) nu = (dot a nu + dot b nu)%N.
Proof.
  revert b nu. induction a as [|x a IH]; intros [|y b] [|z nu]; cbn; try lia.
  rewrite IH, N.mul_add_distr_r. lia.
Qed.

Lemma ev_add nu a b : ev nu (lf_add a b) = ev nu a + ev nu b.
Proof. unfold ev, lf_add; cbn. rewrite dot_zadd. lia. Qed.

Lemma ev_S nu a : ev nu (lf_S a) = S (ev nu a).
Proof. unfold ev, lf_S; cbn. lia. Qed.

Lemma allz_dot vs nu : allz vs = true -> dot vs nu = 0%N.
Proof.
  unfold allz in *. revert nu. induction vs as [|v vs IH]; intros [|x nu] H; cbn [dot forallb] in *; try reflexivity.
  apply andb_prop in H as [H1 H2]. apply N.eqb_eq in H1. subst. rewrite IH by exact H2. lia.
Qed.

Lemma all4_dot vs nu : all4 vs = true -> exists k, dot vs nu = (4 * k)%N.
Proof.
  unfold all4 in *. revert nu. induction vs as [|v vs IH]; intros [|x nu] H; cbn [dot forallb] in *; try (exists 0%N; lia).
  apply andb_prop in H as [H1 H2]. apply N.eqb_eq in H1.
  destruct (IH nu H2) as [k Hk].
  apply N.Div0.mod_divides in H1 as [j Hj].
  exists (j * x + k)%N. rewrite Hk, Hj. lia.
Qed.

Lemma ev_zero nu a : is_zero a = true -> ev nu a = 0.
Proof.
  unfold is_zero, ev. intros H. apply andb_prop in H as [H1 H2].
  apply N.eqb_eq in H1. rewrite H1, (allz_dot _ _ H2). reflexivity.
Qed.

Lemma ev_one nu a : is_one a = true -> ev nu a = 1.
Proof.
  unfold is_one, ev. intros H. apply andb_prop in H as [H1 H2].
  apply N.eqb_eq in H1. rewrite H1, (allz_dot _ _ H2). reflexivity.
Qed.

Lemma ev_pos nu a : posb a = true -> ev nu a = S (ev nu (LF (N.pred (lc a)) (lv a))).
Proof.
  unfold posb, ev. cbn. intros H. apply Bool.negb_true_iff, N.eqb_neq in H. lia.
Qed.

Lemma ev_mod4 nu a : all4 (lv a) = true -> exists k, ev nu a = N.to_nat (lc a) + 4 * k.
Proof.
  intros H. destruct (all4_dot _ nu H) as [k Hk]. unfold ev. rewrite Hk.
  exists (N.to_nat k). lia.
Qed.

Lemma ev_runs_app nu rs1 rs2 s : ev_runs nu (rs1 ++ rs2) s = ev_runs nu rs1 (ev_runs nu rs2 s).
Proof. induction rs1 as [|[b n] rs1 IH]; cbn; [reflexivity|]. rewrite IH. reflexivity. Qed.

Lemma pop_runs_spec nu sg rs t b s' :
  pop_runs rs t = Some (b, s') -> ev_runs nu rs (ev_tl sg t) = b >> ev_sd nu sg s'.
Proof.
  revert b s'. induction rs as [|[b0 n] rs IH]; intros b s' H; cbn in H.
  - destruct t; [|discriminate]. inversion H; subst. cbn. apply const_unfold.
  - destruct (is_zero n) eqn:Ez.
    + cbn. rewrite (ev_zero nu n Ez). cbn. apply IH, H.
    + destruct (posb n) eqn:Ep; [|discriminate].
      inversion H; subst; clear H. cbn.
      destruct (is_one n) eqn:Eo.
      * rewrite (ev_one nu n Eo). reflexivity.
      * rewrite (ev_pos nu n Ep). reflexivity.
Qed.

Lemma pop_spec nu sg s b s' : pop s = Some (b, s') -> ev_sd nu sg s = b >> ev_sd nu sg s'.
Proof. destruct s as [rs t]. apply pop_runs_spec. Qed.

Lemma push_spec nu sg w s : ev_sd nu sg (push w s) = w >> ev_sd nu sg s.
Proof.
  destruct s as [[|[b0 n0] rs] t]; cbn; [reflexivity|].
  destruct (seqb w b0) eqn:E; cbn; [reflexivity|].
  rewrite ev_S. cbn. rewrite <-(sneg_neq _ _ E). reflexivity.
Qed.

Definition afterb_nat (c : Sym) (n : nat) : Sym := if Nat.eqb (n mod 2) 0 then c else sneg c.

Lemma afterb_nat_S c m : afterb_nat c (S m) = afterb_nat (sneg c) m.
Proof.
  unfold afterb_nat.
  destruct (Nat.eqb_spec (S m mod 2) 0), (Nat.eqb_spec (m mod 2) 0); try lia;
    [symmetry; apply sneg_sneg | reflexivity].
Qed.

Lemma alt_add c m k : alt c (m + k) = alt c m ++ alt (afterb_nat c m) k.
Proof.
  revert c. induction m as [|m IH]; intros c; [reflexivity|].
  change (S m + k) with (S (m + k)). cbn [alt app].
  rewrite IH, afterb_nat_S. reflexivity.
Qed.

Lemma afterb_ev nu c n : all4 (lv n) = true -> afterb c n = afterb_nat c (ev nu n).
Proof.
  intros H. destruct (ev_mod4 nu n H) as [k Hk]. rewrite Hk. unfold afterb, afterb_nat.
  destruct (N.eqb_spec (lc n mod 2) 0), (Nat.eqb_spec ((N.to_nat (lc n) + 4 * k) mod 2) 0);
    try reflexivity; exfalso; lia.
Qed.

Lemma push_run_spec nu sg c n s :
  all4 (lv n) = true -> ev_sd nu sg (push_run c n s) = alt c (ev nu n) *> ev_sd nu sg s.
Proof.
  intros H4. destruct s as [[|[b0 n0] rs] t]; cbn; [reflexivity|].
  destruct (seqb (afterb c n) b0) eqn:E; cbn.
  - rewrite ev_add, alt_add, Str_app_assoc. apply seqb_eq in E.
    rewrite <-(afterb_ev nu c n H4), E. reflexivity.
  - reflexivity.
Qed.

Definition lastb_nat (c : Sym) (m : nat) : Sym := if Nat.eqb (m mod 2) 0 then sneg c else c.

Lemma lastb_ev nu c n : all4 (lv n) = true -> lastb c n = lastb_nat c (ev nu n).
Proof.
  intros H. destruct (ev_mod4 nu n H) as [k Hk]. rewrite Hk. unfold lastb, lastb_nat.
  destruct (N.eqb_spec (lc n mod 2) 0), (Nat.eqb_spec ((N.to_nat (lc n) + 4 * k) mod 2) 0);
    try reflexivity; exfalso; lia.
Qed.

Lemma rev_alt b m (l : side) :
  alt (sneg (lastb_nat b (S m))) (S m) *> l = alt (sneg (lastb_nat (sneg b) m)) m *> (sneg b >> l).
Proof.
  rewrite <-Nat.add_1_r, alt_add, Str_app_assoc. cbn [alt Str_app].
  unfold lastb_nat, afterb_nat.
  destruct (Nat.eqb_spec ((m + 1) mod 2) 0), (Nat.eqb_spec (m mod 2) 0); try lia;
    destruct b; reflexivity.
Qed.

Lemma cR_cases i : (i mod 4 = 0 /\ S i mod 4 = 1) \/ (i mod 4 = 1 /\ S i mod 4 = 2) \/
                   (i mod 4 = 2 /\ S i mod 4 = 3) \/ (i mod 4 = 3 /\ S i mod 4 = 0).
Proof. lia. Qed.

Lemma cR_tm i : tm (cR_st i, cR_bt i) = Some (sneg (cR_bt i), R, cR_st (S i)).
Proof.
  unfold cR_st, cR_bt. destruct (cR_cases i) as [[H1 H2]|[[H1 H2]|[[H1 H2]|[H1 H2]]]];
    rewrite H1, H2; reflexivity.
Qed.

Lemma cR_bt_S i : cR_bt (S i) = sneg (cR_bt i).
Proof.
  unfold cR_bt. destruct (cR_cases i) as [[H1 H2]|[[H1 H2]|[[H1 H2]|[H1 H2]]]];
    rewrite H1, H2; reflexivity.
Qed.

Lemma cL_tm i : tm (cL_st i, cL_bt i) = Some (sneg (cL_bt i), L, cL_st (S i)).
Proof.
  unfold cL_st, cL_bt. destruct (cR_cases i) as [[H1 H2]|[[H1 H2]|[[H1 H2]|[H1 H2]]]];
    rewrite H1, H2; reflexivity.
Qed.

Lemma cL_bt_S i : cL_bt (S i) = sneg (cL_bt i).
Proof.
  unfold cL_bt. destruct (cR_cases i) as [[H1 H2]|[[H1 H2]|[[H1 H2]|[H1 H2]]]];
    rewrite H1, H2; reflexivity.
Qed.

Lemma accR_step i l X :
  (l {{cR_st i}}> (cR_bt i >> X)) --> ((sneg (cR_bt i) >> l) {{cR_st (S i)}}> X).
Proof. exact (step_right (cR_tm i)). Qed.

Lemma accL_step i r X :
  ((cL_bt i >> X) <{{cL_st i}} r) --> (X <{{cL_st (S i)}} (sneg (cL_bt i) >> r)).
Proof. exact (step_left (cL_tm i)). Qed.

Lemma accR m : forall i l r,
  (l {{cR_st i}}> (alt (cR_bt i) m *> r)) -->*
  ((alt (sneg (lastb_nat (cR_bt i) m)) m *> l) {{cR_st (i + m)}}> r).
Proof.
  induction m as [|m IH]; intros i l r.
  - rewrite Nat.add_0_r. apply evstep_refl.
  - eapply evstep_step; [cbn [alt Str_app]; apply accR_step|].
    pose proof (IH (S i) (sneg (cR_bt i) >> l) r) as H. rewrite cR_bt_S in H.
    rewrite rev_alt, Nat.add_succ_r. exact H.
Qed.

Lemma accR_S m i l r :
  (l {{cR_st i}}> (alt (cR_bt i) (S m) *> r)) -->+
  ((alt (sneg (lastb_nat (cR_bt i) (S m))) (S m) *> l) {{cR_st (i + S m)}}> r).
Proof.
  eapply progress_intro; [cbn [alt Str_app]; apply accR_step|].
  pose proof (accR m (S i) (sneg (cR_bt i) >> l) r) as H. rewrite cR_bt_S in H.
  rewrite rev_alt, Nat.add_succ_r. exact H.
Qed.

Lemma accL m : forall i l r,
  ((alt (cL_bt i) m *> l) <{{cL_st i}} r) -->*
  (l <{{cL_st (i + m)}} (alt (sneg (lastb_nat (cL_bt i) m)) m *> r)).
Proof.
  induction m as [|m IH]; intros i l r.
  - rewrite Nat.add_0_r. apply evstep_refl.
  - eapply evstep_step; [cbn [alt Str_app]; apply accL_step|].
    pose proof (IH (S i) l (sneg (cL_bt i) >> r)) as H. rewrite cL_bt_S in H.
    rewrite rev_alt, Nat.add_succ_r. exact H.
Qed.

Lemma accL_S m i l r :
  ((alt (cL_bt i) (S m) *> l) <{{cL_st i}} r) -->+
  (l <{{cL_st (i + S m)}} (alt (sneg (lastb_nat (cL_bt i) (S m))) (S m) *> r)).
Proof.
  eapply progress_intro; [cbn [alt Str_app]; apply accL_step|].
  pose proof (accL m (S i) l (sneg (cL_bt i) >> r)) as H. rewrite cL_bt_S in H.
  rewrite rev_alt, Nat.add_succ_r. exact H.
Qed.

Lemma single_spec nu sg c c' : single c = Some c' -> ev_cfg nu sg c --> ev_cfg nu sg c'.
Proof.
  destruct c as [q l r|q l r]; cbn [single].
  - destruct (pop r) as [[s r']|] eqn:Ep; [|discriminate].
    pose proof (pop_spec nu sg r s r' Ep) as Hr.
    destruct (tm (q, s)) as [[[w [|]] q']|] eqn:Et; intros H; inversion H; subst; clear H;
      cbn [ev_cfg]; rewrite Hr, ?push_spec.
    + exact (step_left Et).
    + exact (step_right Et).
  - destruct (pop l) as [[s l']|] eqn:Ep; [|discriminate].
    pose proof (pop_spec nu sg l s l' Ep) as Hl.
    destruct (tm (q, s)) as [[[w [|]] q']|] eqn:Et; intros H; inversion H; subst; clear H;
      cbn [ev_cfg]; rewrite Hl, ?push_spec.
    + exact (step_left Et).
    + exact (step_right Et).
Qed.

Definition Rel (b : bool) (c c' : Q * tape) : Prop := if b then c -->+ c' else c -->* c'.

Lemma Rel_trans b1 b2 c c' c'' : Rel b1 c c' -> Rel b2 c' c'' -> Rel (orb b1 b2) c c''.
Proof.
  destruct b1, b2; cbn; intros H1 H2.
  - eapply progress_trans; eauto.
  - eapply progress_evstep_trans; eauto.
  - eapply evstep_progress_trans; eauto.
  - eapply evstep_trans; eauto.
Qed.

Lemma tag_spec nu sg c o c' b : o = single c -> tag o = Some (c', b) -> Rel b (ev_cfg nu sg c) (ev_cfg nu sg c').
Proof.
  intros -> H. unfold tag in H. destruct (single c) eqn:E; [|discriminate].
  inversion H; subst. cbn. apply progress_base. apply single_spec, E.
Qed.

Lemma cR_idx_spec q b i : cR_idx q b = Some i -> q = cR_st i /\ b = cR_bt i.
Proof. destruct q, b; cbn; intros H; inversion H; subst; split; reflexivity. Qed.

Lemma cL_idx_spec q b i : cL_idx q b = Some i -> q = cL_st i /\ b = cL_bt i.
Proof. destruct q, b; cbn; intros H; inversion H; subst; split; reflexivity. Qed.

Lemma cR_st_mod i k : cR_st (i + N.to_nat (N.modulo k 4)) = cR_st (i + N.to_nat k).
Proof.
  unfold cR_st. rewrite N2Nat.inj_mod by discriminate. change (N.to_nat 4) with 4.
  rewrite Nat.Div0.add_mod_idemp_r. reflexivity.
Qed.

Lemma cL_st_mod i k : cL_st (i + N.to_nat (N.modulo k 4)) = cL_st (i + N.to_nat k).
Proof.
  unfold cL_st. rewrite N2Nat.inj_mod by discriminate. change (N.to_nat 4) with 4.
  rewrite Nat.Div0.add_mod_idemp_r. reflexivity.
Qed.

Lemma cR_st_add4 i a k : cR_st (i + (a + 4 * k)) = cR_st (i + a).
Proof. unfold cR_st. replace ((i + (a + 4 * k)) mod 4) with ((i + a) mod 4) by lia. reflexivity. Qed.

Lemma cL_st_add4 i a k : cL_st (i + (a + 4 * k)) = cL_st (i + a).
Proof. unfold cL_st. replace ((i + (a + 4 * k)) mod 4) with ((i + a) mod 4) by lia. reflexivity. Qed.

Lemma sstep_spec nu sg c c' b : sstep c = Some (c', b) -> Rel b (ev_cfg nu sg c) (ev_cfg nu sg c').
Proof.
  intros H.
  destruct c as [q l [[|[b0 n] rs] t]|q [[|[b0 n] ls] t] r];
    try (eapply tag_spec; [reflexivity | exact H]).
  - cbn [sstep] in H.
    destruct (is_zero n) eqn:Ez.
    + inversion H; subst. cbn. unfold ev_sd. cbn [fst snd ev_runs]. rewrite (ev_zero nu n Ez). cbn. apply evstep_refl.
    + destruct (cR_idx q b0) as [i|] eqn:Ei; [|eapply tag_spec; [reflexivity|exact H]].
      destruct (all4 (lv n)) eqn:E4; [|eapply tag_spec; [reflexivity|exact H]].
      inversion H; subst; clear H.
      destruct (cR_idx_spec _ _ _ Ei) as [-> ->].
      cbn [ev_cfg]. rewrite push_run_spec by exact E4. unfold ev_sd at 2. cbn [fst snd ev_runs].
      rewrite (lastb_ev nu _ _ E4), cR_st_mod.
      destruct (ev_mod4 nu n E4) as [k Hk].
      replace (cR_st (i + N.to_nat (lc n))) with (cR_st (i + ev nu n)) by (rewrite Hk; apply cR_st_add4).
      unfold posb. destruct (N.eqb_spec (lc n) 0) as [Hz|Hz]; cbn.
      * apply accR.
      * destruct (ev nu n) as [|m] eqn:Em; [lia|]. apply accR_S.
  - cbn [sstep] in H.
    destruct (is_zero n) eqn:Ez.
    + inversion H; subst. cbn. unfold ev_sd. cbn [fst snd ev_runs]. rewrite (ev_zero nu n Ez). cbn. apply evstep_refl.
    + destruct (cL_idx q b0) as [i|] eqn:Ei; [|eapply tag_spec; [reflexivity|exact H]].
      destruct (all4 (lv n)) eqn:E4; [|eapply tag_spec; [reflexivity|exact H]].
      inversion H; subst; clear H.
      destruct (cL_idx_spec _ _ _ Ei) as [-> ->].
      cbn [ev_cfg]. rewrite push_run_spec by exact E4. unfold ev_sd at 1. cbn [fst snd ev_runs].
      rewrite (lastb_ev nu _ _ E4), cL_st_mod.
      destruct (ev_mod4 nu n E4) as [k Hk].
      replace (cL_st (i + N.to_nat (lc n))) with (cL_st (i + ev nu n)) by (rewrite Hk; apply cL_st_add4).
      unfold posb. destruct (N.eqb_spec (lc n) 0) as [Hz|Hz]; cbn.
      * apply accL.
      * destruct (ev nu n) as [|m] eqn:Em; [lia|]. apply accL_S.
Qed.

Lemma runp_spec nu sg p : forall c c' b, runp p c = Some (c', b) -> Rel b (ev_cfg nu sg c) (ev_cfg nu sg c').
Proof.
  induction p as [p IH|p IH|]; intros c c' b H; cbn [runp] in H.
  - destruct (sstep c) as [[c0 b0]|] eqn:E0; [|discriminate].
    destruct (runp p c0) as [[c1 b1]|] eqn:E1; [|discriminate].
    destruct (runp p c1) as [[c2 b2]|] eqn:E2; [|discriminate].
    inversion H; subst.
    eapply Rel_trans; [apply (sstep_spec nu sg _ _ _ E0)|].
    eapply Rel_trans; [apply (IH _ _ _ E1)|apply (IH _ _ _ E2)].
  - destruct (runp p c) as [[c1 b1]|] eqn:E1; [|discriminate].
    destruct (runp p c1) as [[c2 b2]|] eqn:E2; [|discriminate].
    inversion H; subst.
    eapply Rel_trans; [apply (IH _ _ _ E1)|apply (IH _ _ _ E2)].
  - apply sstep_spec, H.
Qed.

(* ===================================================================== *)
(* Running to a target configuration                                     *)
(* ===================================================================== *)

Fixpoint strip0 (vs : list N) : list N :=
  match vs with
  | [] => []
  | v :: vs' => match strip0 vs' with [] => if N.eqb v 0 then [] else [v] | w => v :: w end
  end.

Fixpoint listN_eqb (a b : list N) : bool :=
  match a, b with
  | [], [] => true
  | x :: a', y :: b' => andb (N.eqb x y) (listN_eqb a' b')
  | _, _ => false
  end.

Definition lf_eqb (a b : lf) : bool := andb (N.eqb (lc a) (lc b)) (listN_eqb (strip0 (lv a)) (strip0 (lv b))).

Definition runs_eqb (a b : list run) : bool :=
  (fix f (a b : list run) := match a, b with
   | [], [] => true
   | (x, n) :: a', (y, m) :: b' => andb (andb (seqb x y) (lf_eqb n m)) (f a' b')
   | _, _ => false end) a b.

Definition tl_eqb (a b : tl_) : bool :=
  match a, b with T0, T0 => true | TV i, TV j => Nat.eqb i j | _, _ => false end.

Definition sd_eqb (a b : sd) : bool := andb (runs_eqb (fst a) (fst b)) (tl_eqb (snd a) (snd b)).

Definition q_eqb (a b : Q) : bool :=
  match a, b with A, A | B, B | C, C | D, D | E, E | F, F => true | _, _ => false end.

Definition cfg_eqb (a b : cfg) : bool :=
  match a, b with
  | Rc q l r, Rc q' l' r' => andb (q_eqb q q') (andb (sd_eqb l l') (sd_eqb r r'))
  | Lc q l r, Lc q' l' r' => andb (q_eqb q q') (andb (sd_eqb l l') (sd_eqb r r'))
  | _, _ => false
  end.

Lemma dot_strip0 vs nu : dot (strip0 vs) nu = dot vs nu.
Proof.
  revert nu. induction vs as [|v vs IH]; intros nu; [reflexivity|].
  cbn [strip0]. destruct (strip0 vs) as [|w ws] eqn:E.
  - destruct (N.eqb_spec v 0) as [->|Hv]; destruct nu as [|x nu]; cbn [dot]; try reflexivity.
    + rewrite <-IH. cbn. lia.
    + rewrite <-IH. cbn. lia.
  - destruct nu as [|x nu]; cbn [dot]; [reflexivity|]. rewrite <-IH. reflexivity.
Qed.

Lemma listN_eqb_eq a b : listN_eqb a b = true -> a = b.
Proof.
  revert b. induction a as [|x a IH]; intros [|y b] H; cbn in H; try discriminate; [reflexivity|].
  apply andb_prop in H as [H1 H2]. apply N.eqb_eq in H1. subst. f_equal. apply IH, H2.
Qed.

Lemma lf_eqb_ev nu a b : lf_eqb a b = true -> ev nu a = ev nu b.
Proof.
  unfold lf_eqb, ev. intros H. apply andb_prop in H as [H1 H2].
  apply N.eqb_eq in H1. apply listN_eqb_eq in H2.
  rewrite H1, <-(dot_strip0 (lv a)), <-(dot_strip0 (lv b)), H2. reflexivity.
Qed.

Lemma runs_eqb_ev nu a b s : runs_eqb a b = true -> ev_runs nu a s = ev_runs nu b s.
Proof.
  revert b. induction a as [|[x n] a IH]; intros [|[y m] b] H; cbn in H; try discriminate; [reflexivity|].
  apply andb_prop in H as [H1 H3]. apply andb_prop in H1 as [H1 H2].
  apply seqb_eq in H1. subst. cbn. rewrite (lf_eqb_ev nu _ _ H2), (IH _ H3). reflexivity.
Qed.

Lemma sd_eqb_ev nu sg a b : sd_eqb a b = true -> ev_sd nu sg a = ev_sd nu sg b.
Proof.
  destruct a as [ra ta], b as [rb tb]. unfold sd_eqb, ev_sd; cbn [fst snd]. intros H.
  apply andb_prop in H as [H1 H2].
  assert (ta = tb) as ->.
  { destruct ta, tb; cbn in H2; try discriminate; [reflexivity|]. apply Nat.eqb_eq in H2. subst. reflexivity. }
  apply runs_eqb_ev, H1.
Qed.

Lemma q_eqb_eq a b : q_eqb a b = true -> a = b.
Proof. destruct a, b; cbn; congruence. Qed.

Lemma cfg_eqb_ev nu sg a b : cfg_eqb a b = true -> ev_cfg nu sg a = ev_cfg nu sg b.
Proof.
  destruct a as [q l r|q l r], b as [q' l' r'|q' l' r']; cbn [cfg_eqb]; intros H; try discriminate;
  apply andb_prop in H as [H1 H]; apply andb_prop in H as [H2 H3];
  apply q_eqb_eq in H1; subst; cbn [ev_cfg];
  rewrite (sd_eqb_ev nu sg _ _ H2), (sd_eqb_ev nu sg _ _ H3); reflexivity.
Qed.

Definition rstep (tgt : cfg) (st : cfg * bool * bool) : cfg * bool * bool :=
  let '(c, pr, dn) := st in
  if dn then st else
  match sstep c with
  | Some (c', b) => (c', orb pr b, cfg_eqb c' tgt)
  | None => st
  end.

(* reach fuel c tgt = true: c reaches tgt in at most fuel simulator steps, at least one machine step *)
Definition reach (fuel : positive) (c tgt : cfg) : bool :=
  let '(c', pr, dn) := Pos.iter (rstep tgt) (c, false, false) fuel in andb pr dn.

Lemma reach_spec fuel c tgt : reach fuel c tgt = true ->
  forall nu sg, ev_cfg nu sg c -->+ ev_cfg nu sg tgt.
Proof.
  intros H nu sg. unfold reach in H.
  pose (Inv := fun st : cfg * bool * bool => let '(c', pr, dn) := st in
    Rel pr (ev_cfg nu sg c) (ev_cfg nu sg c') /\ (dn = true -> cfg_eqb c' tgt = true)).
  assert (HI : Inv (Pos.iter (rstep tgt) (c, false, false) fuel)).
  { apply Pos.iter_invariant.
    - intros [[c1 pr] dn] [HR Hd]. unfold rstep.
      destruct dn; [split; assumption|].
      destruct (sstep c1) as [[c2 b]|] eqn:Es; [|split; assumption].
      split; [|intros E; exact E].
      apply (Rel_trans _ _ _ _ _ HR (sstep_spec nu sg _ _ _ Es)).
    - split; [apply evstep_refl | discriminate]. }
  destruct (Pos.iter (rstep tgt) (c, false, false) fuel) as [[c' pr] dn].
  destruct HI as [HR Hd]. apply andb_prop in H as [-> ->].
  rewrite <-(cfg_eqb_ev nu sg _ _ (Hd eq_refl)). exact HR.
Qed.