From Undecidability.TM Require Import ProgrammingTools.
From Undecidability.TM Require Import EncodeBinNumbers.
From Undecidability.TM Require Export ArithPrelim. From Coq Require Export BinPos.


Local Open Scope positive_scope.





Definition append_bit (p : positive) (b : bool) := if b then p~1 else p~0.
Notation "p ~~ b" := (append_bit p b) (at level 7, left associativity, format "p '~~' b") : positive_scope.

Definition bitToSigPos (b : bool) : sigPos := if b then sigPos_xI else sigPos_xO.
Definition bitToSigPos' (b : bool) : sigPos^+ := inr (bitToSigPos b).

Lemma Encode_positive_app_xI (p : positive) :
  encode_pos (p ~ 0) = encode_pos p ++ [sigPos_xO].
Proof. cbn. congruence. Qed.

Lemma Encode_positive_app_xO (p : positive) :
  encode_pos (p ~ 1) = encode_pos p ++ [sigPos_xI].
Proof. cbn. congruence. Qed.

Lemma Encode_positive_app_xIO (p : positive) (b : bool) :
  encode_pos (p ~~ b) = encode_pos p ++ [if b then sigPos_xI else sigPos_xO].
Proof. destruct b. apply Encode_positive_app_xO. apply Encode_positive_app_xI. Qed.

Fixpoint append_bits (x : positive) (bits : list bool) : positive :=
  match bits with
  | nil => x
  | b :: bits' => append_bits (x~~b) bits'
  end.


Goal encode_pos (append_bits 1234567890 [false;true;true]) = encode_pos 1234567890 ++ map bitToSigPos [false;true;true]. Proof. reflexivity. Qed.

Lemma append_bits_bit (b : bool) (p : positive) (bits : list bool) :
  append_bits p (b :: bits) = append_bits (p~~b) bits.
Proof. reflexivity. Qed.

Lemma encode_append_bits (p : positive) (bits : list bool) :
  encode_pos (append_bits p bits) = encode_pos p ++ map bitToSigPos bits.
Proof.
  revert p. induction bits; intros; cbn in *; auto.
  - now simpl_list.
  - rewrite IHbits.
    rewrite Encode_positive_app_xIO.
    simpl_list; cbn.
    f_equal.
Qed.

Fixpoint bits_to_pos' (bits : list bool) : positive :=
  match bits with
  | nil => 1
  | b :: bits' => (bits_to_pos' bits') ~~ b
  end.
Definition bits_to_pos (bits : list bool) := bits_to_pos' (rev bits).


Lemma bits_to_pos'_cons (bit : bool) (bits : list bool) :
  bits_to_pos' (bit :: bits) = (bits_to_pos' bits) ~~ bit.
Proof. reflexivity. Qed.

Lemma bits_to_pos_cons (bit : bool) (bits : list bool) :
  bits_to_pos (bits ++ [bit]) = (bits_to_pos bits) ~~ bit.
Proof. unfold bits_to_pos. simpl_list; cbn. apply bits_to_pos'_cons. Qed.

Lemma encode_bits_to_pos' (bits : list bool) :
  encode_pos (bits_to_pos' bits) = sigPos_xH :: map bitToSigPos (rev bits).
Proof.
  induction bits; cbn in *; f_equal; auto.
  rewrite Encode_positive_app_xIO.
  rewrite IHbits. cbn. f_equal. simpl_list. cbn. auto.
Qed.

Lemma encode_bits_to_pos (bits : list bool) :
  encode_pos (bits_to_pos bits) = sigPos_xH :: map bitToSigPos bits.
Proof. unfold bits_to_pos. rewrite encode_bits_to_pos'. now simpl_list. Qed.

Fixpoint pos_to_bits (p : positive) : list bool :=
  match p with
  | 1 => []
  | p ~ 1 => pos_to_bits p ++ [true]
  | p ~ 0 => pos_to_bits p ++ [false]
  end.

Lemma pos_to_bits_to_pos (p : positive) :
  bits_to_pos (pos_to_bits p) = p.
Proof.
  induction p; cbn; f_equal; eauto.
  - simpl_list; cbn. f_equal. eauto.
  - simpl_list; cbn. f_equal. auto.
Qed.

Lemma pos_to_bits_app_bit (b : bool) (p : positive) :
  pos_to_bits (p ~~ b) = pos_to_bits p ++ [b].
Proof. destruct b; reflexivity. Qed.

Lemma bits_to_pos_to_bits' (bits : list bool) :
  pos_to_bits (bits_to_pos' bits) = rev bits.
Proof.
  induction bits; intros; cbn in *.
  - auto.
  - simpl_list; cbn. rewrite pos_to_bits_app_bit. f_equal. auto.
Qed.

Lemma bits_to_pos_to_bits (bits : list bool) :
  pos_to_bits (bits_to_pos bits) = bits.
Proof. unfold bits_to_pos. rewrite bits_to_pos_to_bits'. now simpl_list. Qed.

Lemma pos_to_bits_append_bits : forall bits p, pos_to_bits (append_bits p bits) = pos_to_bits p ++ bits.
Proof.
  induction bits; intros; cbn in *.
  - now simpl_list.
  - destruct a; cbn; rewrite IHbits; cbn; simpl_list; cbn; auto.
Qed.

Lemma pos_to_bits_append_bits' : forall bits1 bits2, pos_to_bits (append_bits (bits_to_pos bits1) bits2) = bits1 ++ bits2.
Proof.
  intros.
  rewrite pos_to_bits_append_bits. now rewrite bits_to_pos_to_bits.
Qed.

Lemma Encode_positive_eq_pos_to_bits (p : positive) :
  encode_pos p = sigPos_xH :: map bitToSigPos (pos_to_bits p).
Proof.
  induction p; cbn; auto.
  - rewrite IHp; simpl_list; cbn; auto.
  - rewrite IHp; simpl_list; cbn; auto.
Qed.

Lemma pos_to_bits_inj : forall (p1 p2 : positive), pos_to_bits p1 = pos_to_bits p2 -> p1 = p2.
Proof.
  intros. apply Encode_positive_injective. cbn.
  rewrite !Encode_positive_eq_pos_to_bits. f_equal. f_equal. auto.
Qed.

Arguments bits_to_pos : simpl never.

Fixpoint pushHSB (p : positive) (b : bool) : positive :=
  match p with
  | p' ~ 1 => (pushHSB p' b) ~ 1
  | p' ~ 0 => (pushHSB p' b) ~ 0
  | 1 => 1 ~~ b
  end.


Lemma encode_pushHSB (p : positive) (b : bool) :
  encode_pos (pushHSB p b) = sigPos_xH :: bitToSigPos b :: tl (encode_pos p).
Proof.
  induction p; cbn.
  - rewrite IHp. simpl_list; cbn. now rewrite tl_app by apply Encode_positive_eq_nil.
  - rewrite IHp. simpl_list; cbn. now rewrite tl_app by apply Encode_positive_eq_nil.
  - rewrite Encode_positive_app_xIO. cbn. reflexivity.
Qed.

Lemma pos_to_bits_pushHSB (p : positive) (b : bool) :
  pos_to_bits (pushHSB p b) = b :: pos_to_bits p.
Proof.
  induction p; cbn.
  - rewrite IHp. simpl_list; cbn. auto.
  - rewrite IHp. simpl_list; cbn. auto.
  - destruct b; auto.
Qed.


Fixpoint shift_left (p : positive) (n : nat) :=
  match n with
  | O => p
  | S n' => shift_left (p~0) n'
  end.

Definition removeLSB (p : positive) : positive :=
  match p with
  | 1 => 1
  | p~0 => p
  | p~1 => p
  end.

Fixpoint shift_right (p : positive) (n : nat) :=
  match n with
  | O => p
  | S n' => shift_right (removeLSB p) n'
  end.

Lemma append_bit_removeLSB (p : positive) (b : bool) :
  removeLSB (p~~b) = p.
Proof. destruct b; reflexivity. Qed.

Lemma shift_left_append_zero (p : positive) (n : nat) :
  shift_left (p~0) n = (shift_left p n) ~ 0.
Proof. revert p. induction n; intros; cbn in *; auto. Qed.

Lemma shift_left_shift_right (p : positive) (n : nat) :
  shift_right (shift_left p n) n = p.
Proof.
  revert p. induction n; intros; cbn in *; auto.
  rewrite shift_left_append_zero. cbn. auto.
Qed.

Fixpoint pos_size (p : positive) : nat :=
  match p with
  | 1 => 0
  | p~1 => S (pos_size p)
  | p~0 => S (pos_size p)
  end.

Lemma pos_size_append_bit (p : positive) (b : bool) :
  pos_size (p~~b) = S (pos_size p).
Proof. now destruct b. Qed.

Lemma pos_size_correct (p : positive) :
  S (pos_size p) = Pos.size_nat p.
Proof. induction p; cbn; auto. Qed.

Lemma pos_size_monotone (x y : positive) :
  x <= y ->
  (pos_size x <= pos_size y) % nat.
Proof.
  revert y. induction x; intros; cbn in *.
  - destruct y; cbn in *.
    + apply le_n_S. apply IHx. nia.
    + apply le_n_S. apply IHx. nia.
    + nia.
  - destruct y; cbn in *.
    + apply le_n_S. apply IHx. nia.
    + apply le_n_S. apply IHx. nia.
    + nia.
  - nia.
Qed.

Lemma pos_size_lt (p1 p2 : positive) :
  (pos_size p1 < pos_size p2) % nat ->
  p1 < p2.
Proof.
  revert p2. induction p1; intros; cbn in *; auto.
  - destruct p2; cbn in *.
    + specialize (IHp1 p2). spec_assert IHp1 by nia. nia.
    + specialize (IHp1 p2). spec_assert IHp1 by nia. nia.
    + nia.
  - destruct p2; cbn in *.
    + specialize (IHp1 p2). spec_assert IHp1 by nia. nia.
    + specialize (IHp1 p2). spec_assert IHp1 by nia. nia.
    + nia.
  - destruct p2; cbn in *; nia.
Qed.