From Undecidability Require Import ProgrammingTools.
From Undecidability Require Import BinNumbers.EncodeBinNumbers.
From Undecidability Require Import BinNumbers.PosDefinitions.

Local Open Scope positive_scope.

Definition atBit (t : tape sigPos^+) (lp : positive) (mb : bool) (rs : list bool) :=
  exists (ls : list sigPos^+),
    t = midtape (map inr (rev (encode lp)) ++ inl START :: ls) (bitToSigPos' mb) (map bitToSigPos' rs ++ [inl STOP]).

Definition atLSB (t : tape sigPos^+) (lp : positive) (mb : bool) := atBit t lp mb nil.

Lemma atLSB_moveRight_contains_rev (t : tape sigPos^+) (lp : positive) (mb : bool) :
  atLSB t lp mb ->
  tape_move t R ≂ lp ~~ mb.
Proof.
  intros (ls&->); cbn. hnf; destruct mb; cbn; eexists; f_equal.
  - unfold bitToSigPos'; cbn. simpl_list. rewrite <- map_rev; cbn. simpl_list. f_equal. f_equal.
    rewrite !map_rev. f_equal. now rewrite map_id.
  - unfold bitToSigPos'; cbn. simpl_list. rewrite <- map_rev; cbn. simpl_list. f_equal. f_equal.
    rewrite !map_rev. f_equal. now rewrite map_id.
Qed.

Lemma atBit_moveRight_cons (t : tape sigPos^+) (lp : positive) (b b' : bool) (rs : list bool) :
  atBit t lp b (b' :: rs) ->
  atBit (tape_move t R) (lp ~~ b) b' rs.
Proof.
  intros (ls&->). hnf. cbn.
  rewrite Encode_positive_app_xIO. rewrite rev_app_distr. cbn.
  destruct b; cbn.
  - eexists. f_equal.
  - eexists. f_equal.
Qed.

Lemma atBit_moveRight (t : tape sigPos^+) (lp : positive) (b : bool) (rs : list bool) :
  atBit t lp b rs ->
  match rs with
  | nil => tape_move t R ≂ lp ~~ b
  | b' :: rs' => atBit (tape_move t R) (lp ~~ b) b' rs'
  end.
Proof.
  intros H. destruct rs as [ | b' rs'].
  - now apply atLSB_moveRight_contains_rev.
  - now apply atBit_moveRight_cons.
Qed.

Lemma contains_rev_moveLeft_atLSB (t : tape sigPos^+) (lp : positive) (mb : bool) :
  t ≂ (lp ~~ mb) ->
  atLSB (tape_move t L) lp mb.
Proof.
  intros (ls&->); cbn. hnf.
  rewrite Encode_positive_app_xIO.
  rewrite <- !map_rev.
  destruct mb; cbn.
  - rewrite rev_app_distr; cbn. eexists. f_equal. f_equal. f_equal. now rewrite map_id.
  - rewrite rev_app_distr; cbn. eexists. f_equal. f_equal. f_equal. now rewrite map_id.
Qed.

Lemma atBit_moveLeft_cons (t : tape sigPos^+) (lp : positive) (b b' : bool) (rs : list bool) :
  atBit t (lp ~~ b) b' rs ->
  atBit (tape_move t L) lp b (b' :: rs).
Proof.
  intros (ls&->); cbn. hnf.
  rewrite Encode_positive_app_xIO.
  destruct b; cbn.
  - exists ls. simpl_list. cbn. f_equal.
  - exists ls. simpl_list. cbn. f_equal.
Qed.

Definition atHSB (t : tape sigPos^+) (p : positive) :=
  exists (ls : list sigPos^+),
    t = midtape (inl START :: ls) (inr sigPos_xH) (map inr (tl (encode p)) ++ [inl STOP]).

Lemma atHSB_moveLeft_contains (t : tape sigPos^+) (p : positive) :
  atHSB t p ->
  tape_move t L ≃ p.
Proof.
  intros (ls&->). hnf. cbn.
  pose proof Encode_positive_startsWith_xH p as (str'&H); setoid_rewrite H; clear H; cbn.
  eexists. f_equal. f_equal. now rewrite map_id.
Qed.

Lemma contains_moveRight_atHSB (t : tape sigPos^+) (p : positive) :
  t ≃ p ->
  atHSB (tape_move t R) p.
Proof.
  intros (ls&->). hnf. cbn.
  pose proof Encode_positive_startsWith_xH p as (str'&H); setoid_rewrite H; clear H; cbn.
  eexists. f_equal. f_equal. now rewrite map_id.
Qed.

Lemma atBit_moveLeft_atHSB (t : tape sigPos^+) (b : bool) (rs : list bool) :
  atBit t 1 b rs ->
  atHSB (tape_move t L) (bits_to_pos (b :: rs)).
Proof.
  intros (ls&->). cbn -[bits_to_pos]. hnf. exists ls. f_equal. cbn -[bits_to_pos]. rewrite app_comm_cons. f_equal.
  rewrite encode_bits_to_pos. cbn. f_equal. now rewrite map_map.
Qed.

Lemma atBit_ext (t : tape sigPos^+) (p0 : positive) (b0 : bool) (bits0 : list bool) (p1 : positive) (b1 : bool) (bits1 : list bool) :
  atBit t p0 b0 bits0 ->
  p0 = p1 ->
  b0 = b1 ->
  bits0 = bits1 ->
  atBit t p1 b1 bits1.
Proof. now intros H -> -> ->. Qed.

Lemma atLSB_ext (t : tape sigPos^+) (p0 : positive) (b0 : bool) (p1 : positive) (b1 : bool) :
  atLSB t p0 b0 ->
  p0 = p1 ->
  b0 = b1 ->
  atLSB t p1 b1 .
Proof. now intros H -> ->. Qed.

Lemma atHSB_ext (t : tape sigPos^+) (p0 : positive) (p1 : positive) :
  atHSB t p0 ->
  p0 = p1 ->
  atHSB t p1.
Proof. now intros H ->. Qed.

Ltac atBit_ext :=
  lazymatch goal with
  | [ H : atBit ?t ?p0 ?b0 ?bits0 |- atBit ?t ?p1 ?b1 ?bits0 ] => apply (atBit_ext H); auto
  | [ H : atLSB ?t ?p0 ?b0 |- atLSB ?t ?p1 ?b1 ] => apply (atLSB_ext H); auto
  | [ H : atHSB ?t ?p0 |- atHSB ?t ?p1 ] => apply (atHSB_ext H); auto
  end.