(** ** Packed counter *)

Definition pkE N := N - 2^(Nat.log2 N).
Definition pkO N := 2^(Nat.log2 N - 1).

Lemma pk_eq P N: 2^(S P) <= N < 2^(S (S P)) -> pkE N = N - 2^(S P) /\ pkO N = 2^P.
Proof.
  intros H. unfold pkE, pkO.
  rewrite (Nat.log2_unique N (S P)); [|lia|lia].
  split; [reflexivity|]. f_equal. lia.
Qed.

Lemma PAs_last j e o e2 o2:
  PAs (S j) e o e2 o2 -> exists e1 o1, PAs j e o e1 o1 /\ PA e1 o1 e2 o2.
Proof.
  intros H. replace (S j) with (j+1) in H by lia.
  destruct (PAs_split _ _ _ _ _ _ H) as [e1 [o1 [H1 H2]]].
  exists e1, o1. split; auto.
  inversion H2; subst. inversion H7; subst. assumption.
Qed.

Lemma INC_pk N: 2 <= N -> PA (pkE N) (pkO N) (pkE (S N)) (pkO (S N)).
Proof.
  intros HN.
  pose proof (Nat.log2_spec N ltac:(lia)) as HL.
  assert (1 <= Nat.log2 N). { pose proof (Nat.log2_le_mono 2 N HN). cbn in H. lia. }
  remember (Nat.log2 N - 1) as P.
  replace (Nat.log2 N) with (S P) in HL by lia.
  destruct (pk_eq P N HL) as [E1 E2]. rewrite E1, E2.
  rewrite (Nat.pow_succ_r' 2 (S P)) in HL.
  destruct (Nat.eq_dec (S N) (2^(S (S P)))) as [Ec|Ec].
  - destruct (pk_eq (S P) (S N)) as [E3 E4].
    { rewrite !(Nat.pow_succ_r' 2 (S _)). rewrite !Nat.pow_succ_r' in Ec. lia. }
    rewrite E3, E4.
    pose proof (Sweep (S P) P 0 (2^(S P) - 1) 0 0 0 1) as H.
    specialize (H ltac:(rewrite Nat.pow_succ_r'; lia) ltac:(lia) (PF0 0 0)).
    rewrite !Nat.mul_0_r, Nat.mul_1_r in H.
    replace (2 ^ S (S P) - 2 ^ S P * (2 * 0 + 1) - (2 ^ S P - 1)) with 1 in H.
    2: { rewrite !(Nat.pow_succ_r' 2 (S _)). lia. }
    inversion H; subst. inversion H7; subst.
    eapply PA_eq. 1: apply H6. all: rewrite ?Nat.pow_succ_r' in *; lia.
  - destruct (pk_eq P (S N)) as [E3 E4].
    { rewrite (Nat.pow_succ_r' 2 (S P)). lia. }
    rewrite E3, E4.
    pose proof (Gap P (N - 2^(S P)) 0 0) as H.
    specialize (H ltac:(rewrite ?(Nat.pow_succ_r' 2 (S P)) in *; lia)).
    eapply PA_eq. 1: apply H. all: lia.
Qed.

Lemma INC_pks j N: 2 <= N -> PAs j (pkE N) (pkO N) (pkE (N+j)) (pkO (N+j)).
Proof.
  gen N. induction j; intros N HN.
  - eapply PAs_eq. 1: apply (PAs0 (pkE N) (pkO N)). all: f_equal; lia.
  - econstructor. 1: apply INC_pk; lia.
    eapply PAs_eq. 1: apply (IHj (S N)); lia. all: f_equal; lia.
Qed.

(** ** Macro rules (proof.md 3.4).  l is bitlen(k)-1, b = 1+i+m. *)

Lemma bounces0 j e o e' o' m:
  PAs j e o e' o' -> K e o j m -->* K e' o' 0 (j+m).
Proof.
  intros H. pose proof (bounces j e o e' o' 0 m H) as H1.
  rewrite Nat.add_0_r in H1. exact H1.
Qed.

Lemma OVB e o a c u m e' o':
  PA e o ((2*a+1)*2^u) (c*2^u) ->
  PAs (1+u+m) c a e' o' ->
  K e o 0 m -->+ K e' o' 0 (1+u+m).
Proof.
  intros H1 H2. eapply progress_evstep_trans. 1: apply OV_even, H1.
  eapply evstep_trans. 1: apply bounces0, H2.
  finish.
Qed.

Lemma std_ov k i: PA ((2*k+1)*2^i-1) 0 ((2*k+1)*2^i) (0*2^i).
Proof.
  pose proof (pow_pos i).
  eapply PA_eq. 1: apply INC_std. all: nia.
Qed.

Lemma BS_S0 i m: K (2^i-1) 0 0 m -->+ K (1+i+m) 0 0 (1+i+m).
Proof.
  apply OVB with (a:=0) (c:=0).
  - pose proof (std_ov 0 i). eapply PA_eq. 1: apply H. all: lia.
  - eapply PAs_eq. 1: apply INC_stds. all: lia.
Qed.

Lemma OVoS0 e o u m: PA e o 0 (2^u) -> K e o 0 m -->+ K (u+3+m) 0 0 (u+3+m).
Proof.
  intros H.
  eapply progress_trans. 1: apply (OV_odd e o 0 0 u m).
  - eapply PA_eq. 1: apply H. all: lia.
  - pose proof (BS_S0 0 (u+2+m)) as H1. cbn in H1.
    eapply progress_trans. 1: apply H1. finish.
Qed.

Lemma BS_S1a l k i m:
  k = 2^l ->
  K ((2*k+1)*2^i-1) 0 0 m -->+ K (pkE (2*k+(1+i+m))) (pkO (2*k+(1+i+m))) 0 (1+i+m).
Proof.
  intros Hk.
  apply OVB with (a:=k) (c:=0).
  1: apply std_ov.
  destruct (pk_eq l (2^(S l))) as [E1 E2].
  { rewrite !Nat.pow_succ_r'. pose proof (pow_pos l). lia. }
  eapply PAs_eq. 1: apply (INC_pks (1+i+m) (2^(S l))).
  - rewrite Nat.pow_succ_r'. pose proof (pow_pos l). lia.
  - reflexivity.
  - rewrite E1. lia.
  - rewrite E2. lia.
  - f_equal. rewrite Nat.pow_succ_r'. lia.
  - f_equal. rewrite Nat.pow_succ_r'. lia.
Qed.

(** sweep of W(0,k), k < 2^(l+1), into pk(2^(l+2)) *)
Lemma O3_merge l k:
  1 <= k < 2^(S l) ->
  PAs (2^(S (S l)) - 2*k) 0 k (pkE (2^(S (S l)))) (pkO (2^(S (S l)))).
Proof.
  intros Hk.
  destruct (lowbit k) as [P [o1 Ho]]; [lia|].
  pose proof (Sweep (S l) P o1 0 0 0 0 1) as H.
  specialize (H ltac:(lia) ltac:(pose proof (pow_pos (S P)); lia) (PF0 0 0)).
  destruct (pk_eq (S l) (2^(S (S l)))) as [E1 E2].
  { rewrite !(Nat.pow_succ_r' 2 (S _)). pose proof (pow_pos (S l)). lia. }
  rewrite E1, E2.
  eapply PAs_eq. 1: apply H. all: rewrite ?Nat.pow_succ_r' in *; lia.
Qed.

Lemma BS_S1b l k i m:
  2^l <= k < 2^(S l) ->
  2^(S (S l)) <= 2*k+(1+i+m) ->
  K ((2*k+1)*2^i-1) 0 0 m -->+ K (pkE (2*k+(1+i+m))) (pkO (2*k+(1+i+m))) 0 (1+i+m).
Proof.
  intros Hk Hb.
  pose proof (pow_pos l).
  apply OVB with (a:=k) (c:=0).
  1: apply std_ov.
  pose proof (O3_merge l k ltac:(lia)) as H1.
  pose proof (INC_pks (2*k+(1+i+m)-2^(S (S l))) (2^(S (S l)))) as H2.
  specialize (H2 ltac:(rewrite !Nat.pow_succ_r'; lia)).
  pose proof (PAs_trans _ _ _ _ _ _ _ _ H1 H2) as H3.
  eapply PAs_eq. 1: apply H3. all: try reflexivity.
  - rewrite !(Nat.pow_succ_r' 2 (S _)) in *. rewrite !Nat.pow_succ_r' in *. lia.
  - f_equal. lia.
  - f_equal. lia.
Qed.

Lemma BS_S2 l k i m:
  2^l <= k < 2^(S l) ->
  2*k+(1+i+m)+1 = 2^(S (S l)) ->
  K ((2*k+1)*2^i-1) 0 0 m -->+ K (l+4+(1+i+m)) 0 0 (l+4+(1+i+m)).
Proof.
  intros Hk Hb.
  pose proof (pow_pos l).
  pose proof (O3_merge l k ltac:(lia)) as H1.
  destruct (pk_eq (S l) (2^(S (S l)))) as [E1 E2].
  { rewrite !(Nat.pow_succ_r' 2 (S _)). pose proof (pow_pos (S l)). lia. }
  rewrite E1, E2 in H1.
  replace (2 ^ S (S l) - 2 * k) with (S (1+i+m)) in H1 by lia.
  destruct (PAs_last _ _ _ _ _ H1) as [e1 [o1 [H2 H3]]].
  eapply progress_trans. 1: apply OV_even with (a:=k) (c:=0) (u:=i), std_ov.
  eapply evstep_progress_trans. 1: apply bounces0, H2.
  eapply progress_trans. 1: apply (OVoS0 _ _ (S l)).
  - eapply PA_eq. 1: apply H3. all: lia.
  - finish.
Qed.

Lemma pk_ov_full i: 2 <= i ->
  PA (pkE (2^i-1)) (pkO (2^i-1)) 0 (2^(i-1)).
Proof.
  intros Hi.
  pose proof (INC_pk (2^i-1)) as H.
  assert (4 <= 2^i). { pose proof (Nat.pow_le_mono_r 2 2 i ltac:(lia) Hi). cbn in H0. lia. }
  specialize (H ltac:(lia)).
  replace (S (2^i-1)) with (2^i) in H by lia.
  destruct (pk_eq (i-2) (2^i)) as [E1 E2].
  { replace (S (S (i-2))) with i by lia. split. 2: pose proof (Nat.pow_lt_mono_r 2 i (S i)); lia.
    replace i with (S (i-1)) at 2 by lia. rewrite Nat.pow_succ_r'. pose proof (Nat.pow_le_mono_r 2 (S (i-2)) i). lia. }
  rewrite E1, E2 in H.
  eapply PA_eq. 1: apply H. all: try reflexivity.
  - replace (S (i-2)) with i by lia. lia.
  - f_equal. lia.
Qed.

Lemma BS_P0 i m: 2 <= i ->
  K (pkE (2^i-1)) (pkO (2^i-1)) 0 m -->+ K (2+i+m) 0 0 (2+i+m).
Proof.
  intros Hi.
  eapply progress_trans. 1: apply (OVoS0 _ _ (i-1)), pk_ov_full, Hi.
  finish.
Qed.

(** pk(N) with N+1 = (2k+1) 2^i, 2^l <= k < 2^(l+1), k = 2^l + r: overflow gives W(2^l, r) *)
Lemma pk_ov l r i:
  r < 2^l ->
  PA (pkE ((2*(2^l+r)+1)*2^i-1)) (pkO ((2*(2^l+r)+1)*2^i-1)) ((2*r+1)*2^i) (2^l*2^i).
Proof.
  intros Hr.
  pose proof (pow_pos l). pose proof (pow_pos i).
  destruct (pk_eq (l+i) ((2*(2^l+r)+1)*2^i-1)) as [E1 E2].
  { rewrite !Nat.pow_succ_r', Nat.pow_add_r. nia. }
  rewrite E1, E2.
  pose proof (Gap (l+i) ((2*r+1)*2^i-1) 0 0) as H.
  specialize (H ltac:(rewrite !Nat.pow_succ_r', Nat.pow_add_r; nia)).
  eapply PA_eq. 1: apply H.
  all: rewrite ?Nat.pow_succ_r', ?Nat.pow_add_r; nia.
Qed.

Lemma BS_P1 l i m:
  K (pkE ((2*(2^l+0)+1)*2^i-1)) (pkO ((2*(2^l+0)+1)*2^i-1)) 0 m -->+ K (2^l+(1+i+m)) 0 0 (1+i+m).
Proof.
  apply OVB with (a:=0) (c:=2^l).
  1: apply pk_ov; apply pow_pos.
  eapply PAs_eq. 1: apply INC_stds. all: lia.
Qed.

Lemma BS_P2 l r i m:
  1 <= r < 2^l ->
  2^(S l) <= 2*r+(1+i+m) ->
  K (pkE ((2*(2^l+r)+1)*2^i-1)) (pkO ((2*(2^l+r)+1)*2^i-1)) 0 m -->+ K (2*r+(1+i+m)) 0 0 (1+i+m).
Proof.
  intros Hr Hb.
  apply OVB with (a:=r) (c:=2^l).
  1: apply pk_ov; lia.
  destruct (lowbit r) as [P [o1 Ho]]; [lia|].
  pose proof (Sweep l P o1 0 1 0 2 0) as H.
  specialize (H ltac:(lia) ltac:(pose proof (pow_pos (S P)); lia)).
  specialize (H (PF2 0 0 1 0 (PA0 0 0))).
  pose proof (INC_stds (2*r+(1+i+m)-2^(S l)) (2^l*2)) as H2.
  pose proof (PAs_trans _ _ _ _ _ _ _ _ H H2) as H3.
  eapply PAs_eq. 1: apply H3. all: rewrite ?Nat.pow_succ_r' in *; lia.
Qed.

Lemma BS_P3 l r i m:
  1 <= r < 2^l ->
  2*r+(1+i+m)+1 = 2^(S l) ->
  K (pkE ((2*(2^l+r)+1)*2^i-1)) (pkO ((2*(2^l+r)+1)*2^i-1)) 0 m -->+ K (l+2+(1+i+m)) 0 0 (l+2+(1+i+m)).
Proof.
  intros Hr Hb.
  destruct (lowbit r) as [P [o1 Ho]]; [lia|].
  pose proof (Sweep l P o1 0 1 0 2 0) as H.
  specialize (H ltac:(lia) ltac:(pose proof (pow_pos (S P)); lia)).
  specialize (H (PF2 0 0 1 0 (PA0 0 0))).
  replace (2 ^ S l - 2 ^ S P * (2 * o1 + 1) - 0) with (S (1+i+m)) in H by (rewrite ?Nat.pow_succ_r' in *; lia).
  destruct (PAs_last _ _ _ _ _ H) as [e1 [o1' [H2 H3]]].
  eapply progress_trans. 1: apply OV_even with (a:=r) (c:=2^l) (u:=i), pk_ov; lia.
  eapply evstep_progress_trans. 1: eapply bounces0; eapply PAs_eq; [apply H2|..]; rewrite ?Nat.pow_succ_r' in *; lia.
  eapply progress_evstep_trans. 1: apply OV_even with (a:=0) (c:=0) (u:=S l).
  - eapply PA_eq. 1: apply H3. all: rewrite ?Nat.pow_succ_r' in *; lia.
  - eapply evstep_trans. 1: apply bounces0, INC_stds.
    finish.
Qed.