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

Open Scope list.

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

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

Definition R n m := [1] *> [1;0]^^(1+n) *> [0] *> [1;0]^^(m) *> const 0.

(** ** Words W(e,o): bit d of e on cell 2d, bit d of o on cell 2d+1 (cell 0 is read by A) *)

Definition bt (x:nat) : Sym := if Nat.odd x then 1 else 0.

Fixpoint wd (n e o : nat) : list Sym :=
  match n with
  | O => []
  | S n' => bt e :: bt o :: wd n' (Nat.div2 e) (Nat.div2 o)
  end.

Definition WS e o : side := wd (e+o) e o *> const 0.

Lemma bt_even e: bt (2*e) = 0.
Proof. unfold bt. rewrite Nat.odd_even. reflexivity. Qed.

Lemma bt_odd e: bt (2*e+1) = 1.
Proof. unfold bt. rewrite Nat.odd_odd. reflexivity. Qed.

Lemma div2_even e: Nat.div2 (2*e) = e.
Proof. apply Nat.div2_double. Qed.

Lemma div2_odd e: Nat.div2 (2*e+1) = e.
Proof. rewrite Nat.add_1_r. apply Nat.div2_succ_double. Qed.

Lemma wd_pad n: forall e o k,
  e < 2^n -> o < 2^n ->
  wd (n+k) e o *> const 0 = wd n e o *> const 0.
Proof.
  induction n; intros e o k He Ho.
  - cbn in He,Ho. assert (e=0)%nat by lia. assert (o=0)%nat by lia. subst.
    cbn. induction k.
    + reflexivity.
    + change (wd (S k) 0 0) with (0 :: 0 :: wd k 0 0). cbn [Str_app]. rewrite IHk. rewrite <-!const_unfold. reflexivity.
  - cbn [wd Nat.add Str_app]. f_equal. f_equal.
    apply IHn.
    + rewrite Nat.div2_div. cbn in He. apply Nat.Div0.div_lt_upper_bound; lia.
    + rewrite Nat.div2_div. cbn in Ho. apply Nat.Div0.div_lt_upper_bound; lia.
Qed.

Lemma lt_pow2_self x: x < 2^x.
Proof. apply Nat.pow_gt_lin_r. lia. Qed.

Lemma wd_WS n e o:
  e < 2^n -> o < 2^n ->
  wd n e o *> const 0 = WS e o.
Proof.
  intros He Ho. unfold WS.
  assert (e < 2^(e+o)). { pose proof (lt_pow2_self (e+o)). pose proof (Nat.pow_le_mono_r 2 e (e+o)). lia. }
  assert (o < 2^(e+o)). { pose proof (lt_pow2_self (e+o)). lia. }
  destruct (Nat.le_ge_cases n (e+o)) as [H1|H1].
  - replace (e+o) with (n+(e+o-n)) by lia. rewrite wd_pad; auto.
  - replace n with ((e+o)+(n-(e+o))) by lia. rewrite wd_pad; auto.
Qed.

Lemma WS_split e o:
  WS e o = [bt e; bt o] *> WS (Nat.div2 e) (Nat.div2 o).
Proof.
  rewrite <-(wd_WS (S (e+o)) e o).
  2,3: pose proof (lt_pow2_self (e+o)); pose proof (Nat.pow_le_mono_r 2 (e+o) (S (e+o))); lia.
  cbn [wd Str_app].
  rewrite (wd_WS (e+o)). 1: reflexivity.
  - rewrite Nat.div2_div. apply Nat.Div0.div_lt_upper_bound.
    pose proof (lt_pow2_self (e+o)). rewrite <-Nat.pow_succ_r'. pose proof (Nat.pow_le_mono_r 2 (e+o) (S (e+o))). lia.
  - rewrite Nat.div2_div. apply Nat.Div0.div_lt_upper_bound.
    pose proof (lt_pow2_self (e+o)). rewrite <-Nat.pow_succ_r'. pose proof (Nat.pow_le_mono_r 2 (e+o) (S (e+o))). lia.
Qed.

Lemma WS_00 e o: WS (2*e) (2*o) = [0;0] *> WS e o.
Proof. rewrite WS_split, bt_even, bt_even, div2_even, div2_even. reflexivity. Qed.
Lemma WS_10 e o: WS (2*e+1) (2*o) = [1;0] *> WS e o.
Proof. rewrite WS_split, bt_even, bt_odd, div2_even, div2_odd. reflexivity. Qed.
Lemma WS_01 e o: WS (2*e) (2*o+1) = [0;1] *> WS e o.
Proof. rewrite WS_split, bt_even, bt_odd, div2_even, div2_odd. reflexivity. Qed.
Lemma WS_11 e o: WS (2*e+1) (2*o+1) = [1;1] *> WS e o.
Proof. rewrite WS_split, bt_odd, bt_odd, div2_odd, div2_odd. reflexivity. Qed.

Lemma WS_0x e o: WS (2*e) o = [0; bt o] *> WS e (Nat.div2 o).
Proof. rewrite WS_split, bt_even, div2_even. reflexivity. Qed.
Lemma WS_1x e o: WS (2*e+1) o = [1; bt o] *> WS e (Nat.div2 o).
Proof. rewrite WS_split, bt_odd, div2_odd. reflexivity. Qed.

(** ** The left step phi, as a relation (A scanning an E-cell / F scanning an E-cell) *)

Inductive PA : nat -> nat -> nat -> nat -> Prop :=
| PA0 e o : PA (2*e) o (2*e+1) o
| PA1 e o e' o' : PA e o e' o' -> PA (2*e+1) (2*o) (2*e') (2*o')
| PA2 e o e' o' : PF e o e' o' -> PA (2*e+1) (2*o+1) (2*e') (2*o')
with PF : nat -> nat -> nat -> nat -> Prop :=
| PF0 e o : PF (2*e) (2*o) (2*e) (2*o+1)
| PF1 e o e' o' : PF e o e' o' -> PF (2*e) (2*o+1) (2*e') (2*o')
| PF2 e o e' o' : PA e o e' o' -> PF (2*e+1) (2*o) (2*e') (2*o')
| PF3 e o e' o' : PF e o e' o' -> PF (2*e+1) (2*o+1) (2*e') (2*o').

Scheme PA_mind := Induction for PA Sort Prop
with PF_mind := Induction for PF Sort Prop.
Combined Scheme PAF_mind from PA_mind, PF_mind.

Lemma TA0 l a r: [0;a] *> l <{{A}} r -->+ [1;a] *> l {{B}}> r.
Proof. es. Qed.
Lemma TA1 l r: [1;0] *> l <{{A}} r -->+ l <{{A}} [1;1] *> r.
Proof. es. Qed.
Lemma TA2 l r: [1;1] *> l <{{A}} r -->+ l <{{F}} [1;1] *> r.
Proof. es. Qed.
Lemma TF0 l r: [0;0] *> l <{{F}} r -->+ [0;1] *> l {{B}}> r.
Proof. es. Qed.
Lemma TF1 l r: [0;1] *> l <{{F}} r -->+ l <{{F}} [1;1] *> r.
Proof. es. Qed.
Lemma TF2 l r: [1;0] *> l <{{F}} r -->+ l <{{A}} [1;1] *> r.
Proof. es. Qed.
Lemma TF3 l r: [1;1] *> l <{{F}} r -->+ l <{{F}} [1;1] *> r.
Proof. es. Qed.
Lemma TB l r: l {{B}}> [1;1] *> r -->+ [0;0] *> l {{B}}> r.
Proof. es. Qed.

Lemma phi_spec:
  (forall e o e' o', PA e o e' o' -> forall r, WS e o <{{A}} r -->+ WS e' o' {{B}}> r) /\
  (forall e o e' o', PF e o e' o' -> forall r, WS e o <{{F}} r -->+ WS e' o' {{B}}> r).
Proof.
  apply PAF_mind.
  all: intros.
  all: try (rewrite WS_0x, WS_1x; apply TA0).
  all: try (rewrite WS_10, WS_00; eapply progress_trans; [apply TA1|]; eapply progress_trans; [apply H|]; apply TB).
  all: try (rewrite WS_11, WS_00; eapply progress_trans; [apply TA2|]; eapply progress_trans; [apply H|]; apply TB).
  all: try (rewrite WS_00, WS_01; apply TF0).
  all: try (rewrite WS_01, WS_00; eapply progress_trans; [apply TF1|]; eapply progress_trans; [apply H|]; apply TB).
  all: try (rewrite WS_10, WS_00; eapply progress_trans; [apply TF2|]; eapply progress_trans; [apply H|]; apply TB).
  all: try (rewrite WS_11, WS_00; eapply progress_trans; [apply TF3|]; eapply progress_trans; [apply H|]; apply TB).
Qed.

Definition PA_spec := proj1 phi_spec.

(** ** Iterates, shape lemmas *)

Inductive PAs : nat -> nat -> nat -> nat -> nat -> Prop :=
| PAs0 e o : PAs 0 e o e o
| PAsS j e o e1 o1 e2 o2 : PA e o e1 o1 -> PAs j e1 o1 e2 o2 -> PAs (S j) e o e2 o2.

Lemma PA_eq e o e' o' e2 o2 e2' o2':
  PA e o e' o' -> e = e2 -> o = o2 -> e' = e2' -> o' = o2' -> PA e2 o2 e2' o2'.
Proof. intros; subst; auto. Qed.

Lemma PF_eq e o e' o' e2 o2 e2' o2':
  PF e o e' o' -> e = e2 -> o = o2 -> e' = e2' -> o' = o2' -> PF e2 o2 e2' o2'.
Proof. intros; subst; auto. Qed.

Lemma PAs_eq j e o e' o' j2 e2 o2 e2' o2':
  PAs j e o e' o' -> j = j2 -> e = e2 -> o = o2 -> e' = e2' -> o' = o2' -> PAs j2 e2 o2 e2' o2'.
Proof. intros; subst; auto. Qed.

Lemma PAs_1 e o e' o': PA e o e' o' -> PAs 1 e o e' o'.
Proof. intros. econstructor; eauto. constructor. Qed.

Lemma PAs_trans j1 j2 e o e1 o1 e2 o2:
  PAs j1 e o e1 o1 -> PAs j2 e1 o1 e2 o2 -> PAs (j1+j2) e o e2 o2.
Proof.
  induction 1; intros; cbn; auto.
  econstructor; eauto.
Qed.

Lemma PAs_split j1 j2 e o e2 o2:
  PAs (j1+j2) e o e2 o2 -> exists e1 o1, PAs j1 e o e1 o1 /\ PAs j2 e1 o1 e2 o2.
Proof.
  gen e o. induction j1; intros e o H.
  - exists e, o. split; [constructor|auto].
  - cbn in H. inversion H; subst.
    destruct (IHj1 _ _ H2) as [e3 [o3 [H3 H4]]].
    exists e3, o3. split; auto. econstructor; eauto.
Qed.

Lemma PAs_dbl j e o e' o':
  PAs j e o e' o' -> PAs (2*j) (2*e) (2*o) (2*e') (2*o').
Proof.
  induction 1.
  - constructor.
  - replace (2 * S j) with (S (S (2*j))) by lia.
    econstructor. 1: apply PA0.
    econstructor. 1: apply PA1; eassumption.
    assumption.
Qed.

Lemma PAs_dbl1 j e o e' o':
  PAs (S j) e o e' o' -> PAs (2*j+1) (2*e+1) (2*o) (2*e') (2*o').
Proof.
  intros H. inversion H; subst.
  replace (2*j+1) with (S (2*j)) by lia.
  econstructor. 1: apply PA1; eassumption.
  apply PAs_dbl; assumption.
Qed.

(** ** Increments *)

Lemma INC_std N: PA N 0 (N+1) 0.
Proof.
  induction N as [N IH] using lt_wf_ind.
  destruct (Nat.Even_or_Odd N) as [[N' HN]|[N' HN]]; subst N.
  - eapply PA_eq. 1: apply (PA0 N' 0). all: lia.
  - eapply PA_eq. 1: apply (PA1 N' 0 (N'+1) 0), IH. all: lia.
Qed.

Lemma INC_stds j N: PAs j N 0 (N+j) 0.
Proof.
  gen N. induction j; intros N.
  - eapply PAs_eq. 1: apply (PAs0 N 0). all: lia.
  - econstructor. 1: apply INC_std.
    eapply PAs_eq. 1: apply (IHj (N+1)). all: lia.
Qed.

Lemma PF_inc0 o: PF 0 o 0 (o+1).
Proof.
  induction o as [o IH] using lt_wf_ind.
  destruct (Nat.Even_or_Odd o) as [[o' Ho]|[o' Ho]]; subst o.
  - eapply PF_eq. 1: apply (PF0 0 o'). all: lia.
  - eapply PF_eq. 1: apply (PF1 0 o' 0 (o'+1)), IH. all: lia.
Qed.

Lemma Gap P: forall c E o1,
  c+1 < 2^(S P) ->
  PA (c + 2^(S P)*E) (2^P*(2*o1+1)) (c + 1 + 2^(S P)*E) (2^P*(2*o1+1)).
Proof.
  induction P; intros c E o1 Hc.
  - cbn in *. eapply PA_eq. 1: apply (PA0 E (2*o1+1)). all: lia.
  - rewrite !Nat.pow_succ_r' in *.
    destruct (Nat.Even_or_Odd c) as [[c' Hc']|[c' Hc']]; subst c.
    + eapply PA_eq. 1: apply (PA0 (c' + 2*2^P*E) (2*2^P*(2*o1+1))). all: lia.
    + eapply PA_eq. 1: apply (PA1 (c' + 2*2^P*E) (2^P*(2*o1+1)) (c'+1+2*2^P*E) (2^P*(2*o1+1))), IHP.
      all: lia.
Qed.

Lemma Gaps P j: forall c E o1,
  c+j < 2^(S P) ->
  PAs j (c + 2^(S P)*E) (2^P*(2*o1+1)) (c + j + 2^(S P)*E) (2^P*(2*o1+1)).
Proof.
  induction j; intros c E o1 Hc.
  - eapply PAs_eq. 1: apply (PAs0 (c + 2^(S P)*E) (2^P*(2*o1+1))). all: lia.
  - econstructor. 1: apply Gap; lia.
    eapply PAs_eq. 1: apply (IHj (c+1) E o1). all: lia.
Qed.

Lemma F_inc h: forall E o O,
  o + 1 < 2^h ->
  PF (2^h*E) (o + 2^h*O) (2^h*E) (o + 1 + 2^h*O).
Proof.
  induction h; intros E o O Ho.
  - cbn in Ho. lia.
  - rewrite !Nat.pow_succ_r' in *.
    destruct (Nat.Even_or_Odd o) as [[o' Ho']|[o' Ho']]; subst o.
    + eapply PF_eq. 1: apply (PF0 (2^h*E) (o' + 2^h*O)). all: lia.
    + eapply PF_eq. 1: apply (PF1 (2^h*E) (o' + 2^h*O) (2^h*E) (o'+1+2^h*O)), IHh.
      all: lia.
Qed.

Lemma F_carry h: forall E O E' O',
  PF E O E' O' ->
  PF (2^h*E) (2^h - 1 + 2^h*O) (2^h*E') (2^h*O').
Proof.
  induction h; intros E O E' O' H.
  - cbn. eapply PF_eq. 1: apply H. all: lia.
  - rewrite !Nat.pow_succ_r' in *.
    pose proof (Nat.pow_nonzero 2 h).
    eapply PF_eq. 1: apply (PF1 (2^h*E) (2^h - 1 + 2^h*O) (2^h*E') (2^h*O')), IHh, H.
    all: lia.
Qed.

(** ** The right step and the overflows *)

Lemma RS l n m:
  l {{B}}> R (S n) m -->+ l <{{A}} R n (S m).
Proof.
  unfold R. es.
Qed.

Lemma shift01 u (r:side): [0;1]^^u *> [0] *> r = [0] *> [1;0]^^u *> r.
Proof.
  induction u.
  - reflexivity.
  - cbn [lpow]. rewrite !Str_app_assoc. rewrite IHu. reflexivity.
Qed.

Lemma OVe l u m:
  ([0;0]^^u *> [1] *> l) {{B}}> R 0 m -->+ l <{{A}} R (1+u+m) 0.
Proof.
  unfold R. es.
Qed.

Lemma OVo l u m:
  ([0;0]^^u *> [0;1;0;0] *> l) {{B}}> R 0 m -->+ l <{{A}} R 0 (u+2+m).
Proof.
  unfold R. es.
Qed.

Definition K e o n m := WS e o <{{A}} R n m.

Lemma init0: c0 -->* K 1 0 0 1.
Proof.
  unfold K. replace (WS 1 0) with ([1] *> const 0).
  2: { unfold WS. cbn. rewrite <-const_unfold. reflexivity. }
  unfold R. esx.
Qed.