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

Open Scope list.

Definition tm := Eval compute in (TM_from_str "1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC").

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

Definition C n := BinInc [1;1] n.
Definition HF (l r : side) := l <{{E}} [1;0;1;1] *> r.

Lemma RIncG l r n:
  l <* [1;1;0;1] {{A}}> [1;1]^^n *> [0;0] *> r -->+
  l <{{E}} [1;0;1;1] *> [0;0]^^n *> [1;1] *> r.
Proof. es. Qed.

Lemma RInc n l:
  l <* [1;1;0;1] {{A}}> C n -->+ HF l (C (1+n)).
Proof.
  unfold C, HF. apply RBinInc_spec. intros. apply RIncG.
Qed.

Lemma L1 u b r:
  HF (u <* [1] <* [0;1]^^b) r -->+ u <* [0] <* [0;1]^^b <* [1;1;0;1] {{A}}> r.
Proof. unfold HF. es. Qed.

Lemma L0 u b r:
  HF (u <* [0;0;1;0] <* [0;1]^^b) r -->+ u <* [0;1;0;1] <* [0;1]^^b <* [1;1;0;1] {{A}}> r.
Proof. unfold HF. es. Qed.

Lemma L011 u r:
  HF (u <* [0;0;1;1;0;1]) r -->+ u <* [0;1;1;0;1;0] <* [1;1;0;1] {{A}}> r.
Proof. unfold HF. es. Qed.

Lemma LEat b r:
  HF (0inf <* [0;1]^^b) r -->+ 0inf <* [0;1]^^(b+2) <* [0;1;1] {{A}}> r.
Proof. unfold HF. es. Qed.

Lemma Y1C v n:
  v <* [0;1;1] {{A}}> C (n*2+1) -->+ HF (v <* [1]) (C (1+n)).
Proof.
  unfold C. rewrite BinInc_mul2add1. fold (C n).
  eapply progress_trans. 2: apply RInc.
  unfold C. es.
Qed.

Lemma Y2C v n:
  v <* [0;1;1] {{A}}> C (n*4) -->+ HF (v <* [1;1;1]) (C n).
Proof.
  unfold C. replace (n*4) with (n*2*2) by lia. rewrite !BinInc_mul2.
  unfold HF. es.
Qed.

Lemma Y3 v s r:
  v <* [0;1;1] {{A}}> [0;0] *> [1;1] *> [1;1]^^s *> [0;0] *> r -->+
  HF (v <* [1;1]) ([0;0]^^s *> [0] *> [1;1] *> r).
Proof. unfold HF. es. Qed.

Lemma Y4 v m:
  v <* [0;1;1] {{A}}> [1;1;0] *> [1;1] *> C m -->+ HF (v <* [1;0;1;1]) (C (1+m)).
Proof.
  eapply progress_trans. 2: apply RInc.
  es.
Qed.

Lemma Y1Q v r:
  v <* [0;1;1] {{A}}> [1;1] *> [0;0] *> r -->+ HF (v <* [1]) ([1;1] *> r).
Proof. unfold HF. es. Qed.

Lemma ROvf l j m:
  l <* [1;1;0;1] {{A}}> [1;1]^^j *> [0;1;1] *> C m -->+
  HF (l <* [0;1] <* [1;1]^^j <* [1]) (C (1+m)).
Proof.
  eapply progress_trans. 2: apply RInc.
  es.
Qed.

(** ** Generic counting *)

Definition Inc r r' := forall l, l <* [1;1;0;1] {{A}}> r -->+ HF l r'.

Lemma IncC n: Inc (C n) (C (1+n)).
Proof. intros l. apply RInc. Qed.

Lemma Inc00 r: Inc ([0;0] *> r) ([1;1] *> r).
Proof. intros l. apply (RIncG l r 0). Qed.

Lemma pt3 c1 c2 c2' c3: c1 -->+ c2 -> c2 = c2' -> c2' -->+ c3 -> c1 -->+ c3.
Proof. intros H1 -> H2. eapply progress_trans; eauto. Qed.

Lemma pt_pre c1 c1' c2: c1 = c1' -> c1' -->+ c2 -> c1 -->+ c2.
Proof. intros -> H1. exact H1. Qed.

Lemma pt_eq c1 c2 c3: c1 -->+ c2 -> c2 = c3 -> c1 -->+ c3.
Proof. intros H1 ->. exact H1. Qed.

Lemma HF_eq l l' r r': l = l' -> r = r' -> HF l r = HF l' r'.
Proof. intros -> ->. reflexivity. Qed.

Lemma Cnt1 u b r r': Inc r r' ->
  HF (u <* [1] <* [0;1]^^b) r -->+ HF (u <* [0] <* [0;1]^^b) r'.
Proof. intros I. eapply progress_trans. 1: apply L1. apply I. Qed.

Lemma Cnt0 u b r r': Inc r r' ->
  HF (u <* [0;0;1;0] <* [0;1]^^b) r -->+ HF (u <* [0;1;0;1] <* [0;1]^^b) r'.
Proof. intros I. eapply progress_trans. 1: apply L0. apply I. Qed.

Lemma Cnt011 u r r': Inc r r' ->
  HF (u <* [0;0;1;1;0;1]) r -->+ HF (u <* [0;1;1;0;1;0]) r'.
Proof. intros I. eapply progress_trans. 1: apply L011. apply I. Qed.

(** ** The misaligned counter Q_k(x,y) = D_k(x) 0 C(y) *)

Fixpoint Dk (k x : nat) : list Sym :=
  match k with
  | O => []
  | S k' => (if Nat.odd x then [1;1] else [0;0]) ++ Dk k' (Nat.div2 x)
  end.

Definition Q k x y := Dk k x *> [0] *> C y.

Lemma Dk_even k a: Dk (S k) (2*a) = [0;0] ++ Dk k a.
Proof.
  cbn [Dk]. rewrite Nat.div2_double.
  replace (Nat.odd (2*a)) with false. 1: reflexivity.
  rewrite <-Nat.negb_even, Nat.even_mul. reflexivity.
Qed.

Lemma Dk_odd k a: Dk (S k) (2*a+1) = [1;1] ++ Dk k a.
Proof.
  replace (2*a+1) with (S (2*a)) by lia.
  cbn [Dk]. rewrite Nat.div2_succ_double.
  replace (Nat.odd (S (2*a))) with true. 1: reflexivity.
  rewrite Nat.odd_succ, Nat.even_mul. reflexivity.
Qed.

Lemma Dk_0 k: Dk k 0 = [0;0]^^k.
Proof. induction k as [|k IH]. 1: reflexivity. cbn. rewrite IH. reflexivity. Qed.

Lemma Dk_1 k: Dk (S k) 1 = [1;1] ++ [0;0]^^k.
Proof. cbn [Dk]. cbn. rewrite Dk_0. reflexivity. Qed.

Lemma Dk_full k: Dk k (2^k-1) = [1;1]^^k.
Proof.
  induction k as [|k IH]. 1: reflexivity.
  replace (2^(S k)-1) with (2*(2^k-1)+1).
  2: { rewrite Nat.pow_succ_r'. pose proof (Nat.pow_nonzero 2 k). lia. }
  rewrite Dk_odd, IH. reflexivity.
Qed.

Lemma Dk_inc k: forall x, S x < 2^k -> exists t rest,
  Dk k x = [1;1]^^t ++ [0;0] ++ rest /\ Dk k (S x) = [0;0]^^t ++ [1;1] ++ rest.
Proof.
  induction k as [|k IH]; intros x Hx.
  1: cbn in Hx; lia.
  rewrite Nat.pow_succ_r' in Hx.
  destruct (Nat.Even_or_Odd x) as [[a ->]|[a ->]].
  - exists O, (Dk k a). rewrite Dk_even.
    replace (S (2*a)) with (2*a+1) by lia. rewrite Dk_odd. split; reflexivity.
  - destruct (IH a) as [t [rest [E1 E2]]]. 1: lia.
    exists (S t), rest. rewrite Dk_odd.
    replace (S (2*a+1)) with (2*(S a)) by lia. rewrite Dk_even.
    rewrite E1, E2. split; reflexivity.
Qed.

Lemma IncQ k x y: S x < 2^k -> Inc (Q k x y) (Q k (S x) y).
Proof.
  intros Hx l. unfold Q.
  destruct (Dk_inc k x Hx) as [t [rest [E1 E2]]].
  rewrite E1, E2, !Str_app_assoc. apply RIncG.
Qed.

(** ** Walks *)

Lemma lp2 (b:nat) (X:side): [0;1]^^b *> [0;1;0;1] *> X = [0;1]^^(S (S b)) *> X.
Proof.
  change ([0;1;0;1] *> X) with ([0;1] *> [0;1] *> X).
  rewrite !lpow_shift'. reflexivity.
Qed.

Lemma lp1 (b:nat) (X:side): [0;1]^^b *> [0;1] *> X = [0;1]^^(S b) *> X.
Proof. rewrite lpow_shift'. reflexivity. Qed.

(* W2: G(u (10)^2 1 (10)^b, r1) -> G(u 1 (10)^(b+2), r3), counts INC1, INC0 *)
Lemma W2 u b r1 r2 r3: Inc r1 r2 -> Inc r2 r3 ->
  HF (u <* [0;1;0;1] <* [1] <* [0;1]^^b) r1 -->+ HF (u <* [1] <* [0;1]^^(S (S b))) r3.
Proof.
  intros I1 I2.
  eapply progress_trans. 1: apply (Cnt1 (u <* [0;1;0;1]) b r1 r2 I1).
  eapply pt_eq. 1: apply (Cnt0 (u <* [1]) b r2 r3 I2).
  apply HF_eq. 2: reflexivity.
  apply lp2.
Qed.

(* W(a,b) *)
Lemma Wk a: forall b n,
  HF (0inf <* [0;1]^^a <* [1] <* [0;1]^^b) (C n) -->+
  HF (0inf <* [0;1]^^(a+b+a mod 2)) (C (n+a+1)).
Proof.
  induction a as [a IH] using lt_wf_ind. intros b n.
  destruct a as [|[|a]].
  - eapply pt_eq. 1: apply (Cnt1 0inf b (C n) _ (IncC n)).
    apply HF_eq. 2: f_equal; lia.
    cbn [Nat.add Nat.modulo]. rewrite Nat.add_0_r.
    cbn [Str_app]. rewrite <-const_unfold. reflexivity.
  - eapply progress_trans. 1: apply (Cnt1 (0inf <* [0;1]) b (C n) _ (IncC n)).
    eapply pt_pre. 1: { apply HF_eq. 2: reflexivity.
      instantiate (1:= 0inf <* [0;0;1;0] <* [0;1]^^b).
      cbn [Str_app]. rewrite <-const_unfold. reflexivity. }
    eapply pt_eq. 1: apply (Cnt0 0inf b (C (1+n)) _ (IncC (1+n))).
    apply HF_eq. 2: f_equal; lia.
    rewrite lp2. f_equal. f_equal.
    pose proof (Nat.mod_upper_bound (S (S b)) 2).
    cbn. lia.
  - eapply progress_trans.
    1: apply (W2 (0inf <* [0;1]^^a) b (C n) (C (1+n)) (C (1+(1+n))) (IncC n) (IncC (1+n))).
    eapply pt_eq. 1: apply (IH a ltac:(lia) (S (S b)) (1+(1+n))).
    apply HF_eq. 2: f_equal; lia.
    f_equal. f_equal. lia.
Qed.

(* W2 iterated on Q: phase (d) of M5 *)
Lemma W2Q t y i: forall u b x, x + 2*i < 2^t ->
  HF (u <* [0;1;0;1]^^i <* [1] <* [0;1]^^b) (Q t x y) -->*
  HF (u <* [1] <* [0;1]^^(b+2*i)) (Q t (x+2*i) y).
Proof.
  induction i as [|i IH]; intros u b x Hx.
  - apply evstep_refl'. apply HF_eq. 2: f_equal; lia.
    rewrite Nat.add_0_r. reflexivity.
  - apply progress_evstep.
    eapply progress_evstep_trans.
    1: apply (W2 (u <* [0;1;0;1]^^i) b _ _ _ (IncQ t x y ltac:(lia)) (IncQ t (S x) y ltac:(lia))).
    eapply evstep_trans. 1: apply (IH u (S (S b)) (S (S x)) ltac:(lia)).
    apply evstep_refl'. apply HF_eq; lia_refl.
Qed.

(* B(s): G(u 1^(2s+1) (10)^j, C n) -> G(u 0 (10)^(s+j), C(n+s+1)), s+1 counts INC1 *)
Lemma Bk s: forall j u n,
  HF (u <* [1;1]^^s <* [1] <* [0;1]^^j) (C n) -->+
  HF (u <* [0] <* [0;1]^^(s+j)) (C (n+s+1)).
Proof.
  induction s as [|s IH]; intros j u n.
  - eapply pt_eq. 1: apply (Cnt1 u j (C n) _ (IncC n)).
    apply HF_eq. 1: reflexivity. f_equal; lia.
  - eapply progress_trans. 1: apply (Cnt1 (u <* [1;1]^^s <* [1;1]) j (C n) _ (IncC n)).
    eapply pt_pre. 1: { apply HF_eq. 2: reflexivity.
      instantiate (1:= u <* [1;1]^^s <* [1] <* [0;1]^^(S j)).
      apply lp1. }
    eapply pt_eq. 1: apply (IH (S j) u (1+n)).
    apply HF_eq; lia_refl.
Qed.

(* W0(c,d): G(u 0 (10)^(2c+1) 0 (10)^d, C n) -> G(u (10)^(2c+2+d), C(n+2c+1)) *)
Lemma W0k c: forall d u n,
  HF (u <* [0] <* [0;1] <* [0;1;0;1]^^c <* [0] <* [0;1]^^d) (C n) -->+
  HF (u <* [0;1]^^(2*c+2+d)) (C (n+2*c+1)).
Proof.
  induction c as [|c IH]; intros d u n.
  - eapply pt_eq. 1: apply (Cnt0 u d (C n) _ (IncC n)).
    apply HF_eq. 2: f_equal; lia.
    rewrite lp2. reflexivity.
  - eapply progress_trans.
    1: apply (Cnt0 (u <* [0] <* [0;1] <* [0;1;0;1]^^c <* [1]) d (C n) _ (IncC n)).
    eapply pt_pre. 1: { apply HF_eq. 2: reflexivity.
      instantiate (1:= u <* [0] <* [0;1] <* [0;1;0;1]^^c <* [1] <* [0;1]^^(S (S d))).
      apply lp2. }
    eapply progress_trans.
    1: apply (Cnt1 (u <* [0] <* [0;1] <* [0;1;0;1]^^c) (S (S d)) _ _ (IncC (1+n))).
    eapply pt_eq. 1: apply (IH (S (S d)) u (1+(1+n))).
    apply HF_eq; lia_refl.
Qed.


(** ** Eat configurations and the macro rules *)

Definition EC p N := HF (0inf <* [0;1]^^p) (C N).

Lemma C_split m i: C (((m*2+1)*2^i-1)*2) = [0;0] *> [1;1]^^i *> [0;0] *> C m.
Proof. unfold C. rewrite BinInc_mul2, BinInc_mulpow2sub1. reflexivity. Qed.

Lemma C_odd n: C (n*2+1) = [1;1] *> C n.
Proof. unfold C. rewrite BinInc_mul2add1. reflexivity. Qed.

Lemma lp4 i (X:side): [0;1;0;1]^^i *> X = [0;1]^^(2*i) *> X.
Proof.
  induction i as [|i IH]. 1: reflexivity.
  replace (2*S i) with (S (S (2*i))) by lia.
  cbn [lpow]. rewrite Str_app_assoc, IH. reflexivity.
Qed.

(* M1: N odd *)
Lemma BS1 p n: EC p (n*2+1) -->+ EC (p+2+p mod 2) (n+p+4).
Proof.
  unfold EC.
  eapply progress_trans. 1: apply LEat.
  eapply progress_trans. 1: apply Y1C.
  eapply pt_eq. 1: apply (Wk (p+2) 0 (1+n)).
  apply HF_eq. 2: f_equal; lia.
  f_equal. f_equal.
  pose proof (Nat.mod_upper_bound p 2). pose proof (Nat.mod_upper_bound (p+2) 2).
  pose proof (Nat.div_mod p 2). pose proof (Nat.div_mod (p+2) 2). lia.
Qed.

(* M2: N = 0 mod 4 *)
Lemma BS2 p n: EC p (n*4) -->+ EC (p+3+p mod 2) (n+p+4).
Proof.
  unfold EC.
  eapply progress_trans. 1: apply LEat.
  eapply progress_trans. 1: apply Y2C.
  eapply progress_trans. 1: apply (Cnt1 (0inf <* [0;1]^^(p+2) <* [1;1]) 0 (C n) _ (IncC n)).
  eapply pt_eq. 1: apply (Wk (p+2) 1 (1+n)).
  apply HF_eq. 2: f_equal; lia.
  f_equal. f_equal. lia.
Qed.

(* M3: N = 2 mod 8 *)
Lemma BS3 p m: EC p (((m*2+1)*2^1-1)*2) -->+ EC (p+4+p mod 2) (m+p+6).
Proof.
  unfold EC.
  eapply progress_trans. 1: apply LEat.
  rewrite C_split.
  eapply progress_trans. 1: apply (Y3 _ 0 (C m)).
  eapply progress_trans. 1: apply (L1 (0inf <* [0;1]^^(p+2) <* [1]) 0).
  eapply progress_trans. 1: apply (ROvf _ 0 m).
  eapply pt_eq. 1: apply (Wk (S (S (p+2))) 0 (1+m)).
  apply HF_eq. 2: f_equal; lia.
  f_equal. f_equal. lia.
Qed.

(* M4: N = 6 mod 16 *)
Lemma BS4 p m: EC p (((m*2+1)*2^2-1)*2) -->+ EC (p+7) (m+5).
Proof.
  unfold EC.
  eapply progress_trans. 1: apply LEat.
  rewrite C_split.
  eapply progress_trans. 1: apply (Y3 _ 1 (C m)).
  eapply progress_trans. 1: apply (Cnt1 (0inf <* [0;1]^^(p+2) <* [1]) 0 _ _ (Inc00 ([0;1;1] *> C m))).
  eapply progress_trans. 1: apply (LEat (S (p+2))).
  eapply progress_trans. 1: apply Y4.
  eapply progress_trans. 1: apply (Cnt1 (0inf <* [0;1]^^(S (p+2)+2) <* [0;1;1]) 0 _ _ (IncC _)).
  eapply progress_trans. 1: apply (Cnt011 (0inf <* [0;1]^^(p+2+2)) _ _ (IncC _)).
  eapply progress_trans. 1: apply (Cnt1 (0inf <* [0;1]^^(p+2+2) <* [0;1;0]) 1 _ _ (IncC _)).
  eapply pt_eq. 1: apply (Cnt0 (0inf <* [0;1]^^(p+2+2)) 1 _ _ (IncC _)).
  apply HF_eq. 2: f_equal; lia.
  replace (p+7) with (S (S (S (p+2+2)))) by lia. reflexivity.
Qed.

(* M5: N = (2m+1) 2^(t+4) - 2 with t' = t+1 >= 1, precondition 2^t' <= p+7 *)
Lemma BS5 p m t: 2^(S t) <= p+7 ->
  EC p (((m*2+1)*2^(S (S (S t)))-1)*2) -->+ EC (p+8+t) (m+2^(S t)+t+2).
Proof.
  intros Hp.
  pose proof (Nat.pow_nonzero 2 t ltac:(lia)) as HT.
  rewrite Nat.pow_succ_r' in Hp.
  unfold EC.
  (* (a) *)
  eapply progress_trans. 1: apply LEat.
  rewrite C_split.
  eapply progress_trans. 1: apply (Y3 _ (S (S t)) (C m)).
  (* (b) *)
  eapply progress_trans.
  1: apply (Cnt1 (0inf <* [0;1]^^(p+2) <* [1]) 0 _ _ (Inc00 ([0;0]^^(S t) *> [0] *> [1;1] *> C m))).
  (* (c) *)
  eapply progress_trans. 1: apply (LEat (S (p+2))).
  eapply pt3. 1: apply (Y1Q _ ([0;0]^^t *> [0] *> [1;1] *> C m)).
  1: { instantiate (1 := HF (0inf <* [0;1]^^(S (p+2)+2) <* [1]) (Q (S t) 1 (m*2+1))).
    apply HF_eq. 1: reflexivity. unfold Q. rewrite Dk_1, C_odd, !Str_app_assoc. reflexivity. }
  (* (d) *)
  set (i := 2^t-1).
  eapply evstep_progress_trans.
  1: { eapply evstep_trans. 2: apply (W2Q (S t) (m*2+1) i (0inf <* [0;1]^^(p+7-2*2^t)) 0 1).
    2: { rewrite Nat.pow_succ_r'. unfold i. lia. }
    apply evstep_refl'. apply HF_eq. 2: reflexivity.
    rewrite lp4, lpow_add'. cbn [Str_app lpow]. unfold i. lia_refl. }
  (* (e) *)
  eapply progress_trans. 1: apply L1.
  replace (Q (S t) (1+2*i) (m*2+1)) with ([1;1]^^(S t) *> [0;1;1] *> C m).
  2: { unfold Q. replace (1+2*i) with (2^(S t)-1).
    2: { rewrite Nat.pow_succ_r'. unfold i. lia. }
    rewrite Dk_full, C_odd. reflexivity. }
  eapply progress_trans. 1: apply ROvf.
  (* (f) *)
  eapply progress_trans. 1: apply (Bk (S t) 0 _ (1+m)).
  (* (g) *)
  eapply pt_pre. 1: { apply HF_eq. 2: reflexivity.
    instantiate (1 := 0inf <* [0;1]^^(p+7-2*2^t) <* [0] <* [0;1] <* [0;1;0;1]^^i <* [0] <* [0;1]^^(S t+0)).
    rewrite lp4. f_equal. f_equal. cbn [Nat.add]. rewrite lpow_shift'. reflexivity. }
  eapply pt_eq. 1: apply W0k.
  apply HF_eq.
  - rewrite lpow_add'. f_equal. f_equal. unfold i. lia.
  - f_equal. unfold i. rewrite Nat.pow_succ_r'. lia.
Qed.