Require Import List Arith Lia Permutation.

Import ListNotations.

From Undecidability.Shared.Libs.DLW
  Require Import utils utils_tac utils_list utils_nat gcd rel_iter prime
                 pos vec subcode sss.

From Undecidability.MinskyMachines.MM Require Import mm_defs mm_no_self.
From Undecidability.FRACTRAN Require Import FRACTRAN fractran_utils prime_seq.

Set Implicit Arguments.

Tactic Notation "rew" "length" := autorewrite with length_db.

Local Notation "e #> x" := (vec_pos e x).
Local Notation "e [ v / x ]" := (vec_change e x v).

Local Notation "I // s -1> t" := (mm_sss I s t).
Local Notation "P /MM/ s → t" := (sss_step (@mm_sss _) P s t) (at level 70, no associativity).
Local Notation "P /MM/ s -[ k ] t" := (sss_steps (@mm_sss _) P k s t) (at level 70, no associativity).
Local Notation "P /MM/ s ↓" := (sss_terminates (@mm_sss _) P s) (at level 70, no associativity).

Local Notation "l /F/ x → y" := (fractran_step l x y) (at level 70, no associativity).
Local Notation "l /F/ x -[ k ] y" := (fractran_steps l k x y) (at level 70, no associativity).

Set Implicit Arguments.





Definition encode_state {n} (c : * vec n) := ps (fst c) * @exp n 0 (snd c).

Definition encode_inc n i (u : pos n) := (ps (i + 1) * qs u, ps i).
Definition encode_dec n i (u : pos n) (_ : ) := (ps (i + 1), ps i * qs u).
Definition encode_dec2 n i (u : pos n) j := (ps j, ps i).

Definition encode_one_instr m i (rho : mm_instr (pos m)) :=
  match with
    | INC u encode_inc i u :: nil
    | DEC u j encode_dec i u j :: encode_dec2 i u j :: nil
  end.

Fixpoint encode_mm_instr m i (l : list (mm_instr (pos m))) : list ( * ) :=
  match l with
    | nil nil
    | :: l encode_one_instr i encode_mm_instr (S i) l
  end.

Fact encode_mm_instr_app m i l r : @encode_mm_instr m i (lr) = encode_mm_instr i lencode_mm_instr (length l+i) r.
Proof.
  revert i; induction l as [ | l IHl ]; intros i; simpl; auto; rewrite IHl, app_ass.
  do 3 f_equal; .
Qed.


Fact encode_mm_instr_regular n i l : Forall ( c fst c 0 snd c 0) (@encode_mm_instr n i l).
Proof.
  revert i; induction l as [ | [ u | u j ] l IHl ]; intros i; simpl.
  + constructor.
  + constructor; auto; unfold encode_inc; simpl; split;
      [ apply Nat.neq_mul_0; split | ]; apply prime_neq_0; apply nthprime_prime.
  + constructor; [ | constructor ]; auto; split; unfold encode_dec, encode_dec2; simpl.
    2: apply Nat.neq_mul_0; split.
    all: apply prime_neq_0; apply nthprime_prime.
Qed.


Fact encode_mm_instr_regular' n i l : fractran_regular (@encode_mm_instr n i l).
Proof.
  generalize (@encode_mm_instr_regular n i l); apply Forall_impl; tauto.
Qed.


Fact encode_mm_instr_in_inv n i P el c er :
          @encode_mm_instr n i P = c::er
        l rho r, P = l::r In c (encode_one_instr (length l+i) ).
Proof.
  revert i c er; induction P as [ | P IHP ]; simpl; intros i c er H.
  + destruct ; discriminate.
  + destruct list_app_cons_eq_inv with (1 := H)
      as [ (m & & ) | (m & & ) ].
    * destruct IHP with (1 := ) as (l & & r & & ).
      exists (::l), , r; subst; split; auto.
      eq goal ; do 2 f_equal; simpl; .
    * exists nil, , P; split; simpl; auto.
      rewrite ; apply in_or_app; simpl; auto.
Qed.


Local Notation divides_mult_inv := prime_div_mult.

Local Ltac inv H := inversion H; subst; clear H.

Opaque ps qs.

Lemma divides_encode_state i k n v : divides (ps i) (@encode_state n (k,v)) i = k.
Proof.
  unfold encode_state. intros. induction v.
  - cbn in H. replace (ps k * 1) with (ps k) in H by .
    now eapply primestream_divides in H.
  - cbn in H. eapply divides_mult_inv in H as [ | [ | ] % divides_mult_inv ]; eauto.
    + now eapply primestream_divides in H.
    + eapply divides_pow in H; eauto.
      now eapply ps_qs_div in H.
    + now eapply ps_exp in H.
Qed.


Lemma skip_steps m k l r k' (v v' : vec _ m) :
      @mm_no_self_loops m (k, l r)
    encode_mm_instr (k + length l) r /F/ encode_state (k + length l,v) encode_state (k',v')
    encode_mm_instr k (l r) /F/ encode_state (k + length l,v) encode_state (k',v').
Proof with eauto; try .
  revert k. induction l; cbn - [subcode] in *; intros.
  - revert . ring_simplify (k + 0). eauto.
  - revert . ring_simplify (k + S (length l)). intros . destruct a.
    + econstructor 2. intros [[|] % divides_mult_inv | ] % divides_mult_inv; eauto.
      * eapply primestream_divides in ; .
      * now eapply ps_qs_div in .
      * eapply divides_encode_state in ; .
      * specialize IHl with (k := S k). revert IHl.
        cbn - [subcode]. ring_simplify (S (k + length l)).
        intros IHl. eapply IHl. 2:exact .
        intros ? ? ?. eapply H. eapply subcode_cons. eassumption.
    + repeat econstructor 2. 2:unfold encode_dec2.
      2,3: cbn- [subcode]. 1: intros [] % divides_mult_inv_l.
      2: intros [ | ] % divides_mult_inv...
      * eapply divides_mult_inv in as [? | ?]...
        eapply primestream_divides in ...
        eapply divides_encode_state in ...
      * eapply primestream_divides in ... subst.
        eapply (H n t). eauto.
      * eapply divides_encode_state in ...
      * specialize (IHl (S k)). revert IHl.
        cbn - [subcode]. ring_simplify (S (k + length l)).
        intros IHl. eapply IHl. 2:exact .
        intros ? ? ?. eapply H. eapply subcode_cons. eassumption.
Qed.


Lemma qs_exp i n u (v : vec n) :
  divides (qs u) (encode_state (i,v)) divides (qs u) (exp 0 v).
Proof.
  split.
  - intros [ | ] % divides_mult_inv; eauto.
    now eapply qs_ps_div in H.
  - intros. unfold encode_state. now eapply divides_mult.
Qed.


Lemma qs_encode_state i n (u : pos n) (v : vec n) :
  divides (qs u) (encode_state (i,v)) v #> u > 0.
Proof.
  rewrite qs_exp.
  enough ( i, divides (qs (i + u)) (exp i v) v #> u > 0). eapply H. intros j.
  induction v.
  - inversion u.
  - revert u. eapply pos.pos_S_invert.
    + cbn; rewrite pos2nat_fst, Nat.add_0_r.
      split.
      * intros [ | ] % divides_mult_inv; eauto.
        -- destruct h; try . cbn in H.
           apply divides_1_inv in H.
           generalize (str_prime qs j); rewrite H.
           intros [ [] _ ]; auto.
        -- eapply qs_exp_div in H; now eauto.
      * intros. destruct h. inv H.
        exists (qs j ^ h * exp (S j) v). cbn. ring.
    + cbn. intros. rewrite IHv, pos2nat_nxt.
      rewrite qs_shift with (m := 1).
      simpl.
      replace (j+S (pos2nat p)) with (S (j+p)); try tauto.
      2: rewrite (plus_comm _ (S _)); simpl; rewrite plus_comm; auto.
      split; intros H.
      * eapply divides_mult_inv in H as [ | ]; eauto.
        eapply divides_pow in H; auto.
        eapply primestream_divides in H.
        .
      * eapply divides_mult.
        revert H; cbn; rewrite plus_n_Sm; eauto.
Qed.


Lemma one_step_forward m i P i1 v1 i2 v2 :
     @mm_no_self_loops m (i,P)
   (i, P) /MM/ (, ) (,)
   encode_mm_instr i P /F/ encode_state (,) encode_state (,).
Proof with eauto; try .
  intros HP (k & l & [ u | u j ] & r & v & ? & ? & ?); inversion H; subst; clear H.
  - inversion ; inversion ; subst; clear .
    eapply skip_steps...
    econstructor. cbn. ring_simplify.
    replace (1 + (k + length l)) with (k + length l + 1) by . unfold encode_state, fst, snd.
    rewrite vec_prod_mult.
    rewrite Nat.add_0_r; ring.
  - inversion ; inversion ; subst; clear .
    all:eapply skip_steps...
    + cbn. econstructor 2.
      intros [] % divides_mult_inv_l...
      eapply divides_mult_inv in as [ | ]...
      * now eapply qs_ps_div in .
      * eapply qs_encode_state in . .
      * unfold encode_dec2. econstructor. unfold encode_state, fst, snd. ring.
    + econstructor. cbn. unfold encode_state, fst, snd. ring_simplify.
      replace (1 + (k + length l)) with (k + length l + 1) by .
      erewrite (vec_prod_div _ _ _ ).
      rewrite Nat.add_0_r; ring.
Qed.


Lemma steps_forward m i P i1 v1 i2 v2 k :
    @mm_no_self_loops m (i, P)
  (i, P) /MM/ (, ) -[k]-> (,)
  encode_mm_instr i P /F/ encode_state (,) -[k]-> encode_state (,).
Proof.
  intros HP H. revert H. induction k; intros H; inversion H; subst; clear H; cbn.
  - reflexivity.
  - destruct . eapply one_step_forward in ; eauto.
Qed.



Local Fact divides_from_eq x y t : x*y = t divides x t.
Proof. exists y; subst; ring. Qed.

Local Fact prime_div_mult3 p x y z : prime p divides p (x*y*z) divides p x divides p y divides p z.
Proof.
  intros .
  apply prime_div_mult in ; auto.
  destruct as [ | ]; auto.
  apply prime_div_mult in ; tauto.
Qed.


Local Fact prime_div_mult4 p w x y z : prime p divides p (w*x*y*z) divides p w divides p x divides p y divides p z.
Proof.
  intros .
  apply prime_div_mult3 in ; auto.
  destruct as [ | ]; try tauto.
  apply prime_div_mult in ; tauto.
Qed.


Local Hint Resolve encode_mm_instr_regular' : core.

Lemma one_step_backward m i P i1 v1 st :
     @mm_no_self_loops m (i, P)
   encode_mm_instr i P /F/ @encode_state m (,) st
   i2 v2, st = @encode_state m (,)
                 (i, P) /MM/ (, ) (,).
Proof.
  intros .
  destruct fractran_step_inv with (1 := )
    as ( & p & q & er & & & ).
  unfold encode_state in ; simpl in .
  destruct encode_mm_instr_in_inv with (1 := )
    as (l & & r & & ).
  assert ( = length l+i) as E.
  { unfold encode_one_instr in .
    destruct as [ u | u j ]; unfold encode_inc, encode_dec, encode_dec2 in ;
      [ destruct as [ | [] ] | destruct as [ | [ | [] ] ] ];
      inversion ; subst p q; clear ;
      repeat rewrite mult_assoc in .
    * apply divides_from_eq, prime_div_mult4 in ; auto.
      destruct as [ | [ | [ | ] ] ].
      + apply primestream_divides in ; .
      + apply ps_qs_div in ; tauto.
      + apply primestream_divides in ; .
      + apply ps_exp in ; tauto.
    * rewrite mult_assoc in .
      apply divides_from_eq, prime_div_mult3 in ; auto.
      destruct as [ | [ | ] ].
      + apply primestream_divides in ; .
      + apply primestream_divides in ; .
      + apply ps_exp in ; tauto.
    * apply divides_from_eq, prime_div_mult3 in ; auto.
      destruct as [ | [ | ] ].
      + apply primestream_divides in .
        exfalso; apply ( j u); auto.
      + apply primestream_divides in ; .
      + apply ps_exp in ; tauto. }
  destruct mm_sss_total with (ii := ) (s := (,))
    as (( & ) & ).
  exists , .
  assert ((i, l::r) /MM/ (,) (,)) as .
  { apply in_sss_step; auto; simpl; . }
  split; auto.
  apply one_step_forward in ; auto.
  revert ; apply fractran_step_fun; auto.
Qed.


Lemma steps_backward m i P i1 v1 k st :
     @mm_no_self_loops m (i, P)
   encode_mm_instr i P /F/ encode_state (,) -[k]-> st
   i2 v2, (i, P) /MM/ (, ) -[k]-> (,)
                 st = encode_state (,).
Proof.
  intros .
  revert st; induction k as [ | k IHk ]; intros st H; simpl in H.
  - subst; exists , ; split; auto; constructor.
  - destruct H as ( & & ).
    destruct one_step_backward with (2 := )
      as ( & & & ); auto.
    destruct IHk with (1 := ) as ( & & ? & ).
    exists , ; split; auto.
    constructor 2 with (,); auto.
Qed.


Theorem mm_fractran_simulation n P v :
     @mm_no_self_loops n (1, P)
   (1,P) /MM/ (1,v) encode_mm_instr 1 P /F/ ps 1 * exp 0 v .
Proof.
  intros HP.
  change (ps 1* exp 0 v) with (encode_state (1,v)).
  split.
  + intros ((j,w) & (k & ) & ); simpl fst in *.
    exists (encode_state (j,w)); split.
    * exists k; apply steps_forward in ; auto.
    * intros x Hx.
      destruct one_step_backward with (2 := Hx)
        as ( & & & ?); auto.
      revert H; apply sss_out_step_stall; auto.
  + intros (st & (k & ) & ).
    destruct steps_backward with (2 := )
      as ( & & & ); auto.
    exists (,); split.
    * exists k; auto.
    * simpl fst.
      destruct (in_out_code_dec (1,P)) as [ | ]; auto; exfalso.
      destruct in_code_subcode with (1 := ) as ( & l & r & & ).
      destruct (mm_sss_total (,)) as ((,) & ).
      apply with (encode_state (,)).
      apply one_step_forward; auto.
      subst P; apply in_sss_step; auto.
Qed.


Theorem mm_fractran_not_zero n (P : list (mm_instr (pos n))) :
        { l | Forall ( c fst c 0 snd c 0) l
             v, (1,P) /MM/ (1,v) l /F/ ps 1 * exp 1 v }.
Proof.
   destruct mm_remove_self_loops with (P := P) as (Q & & _ & ).
   exists (encode_mm_instr 1 Q); split.
   + apply encode_mm_instr_regular.
   + intros x.
     rewrite , mm_fractran_simulation; auto.
     simpl exp; rewrite Nat.add_0_r; tauto.
Qed.


Theorem mm_fractran_n n (P : list (mm_instr (pos n))) :
        { l | Forall ( c snd c 0) l
             v, (1,P) /MM/ (1,v) l /F/ ps 1 * exp 1 v }.
Proof.
   destruct (mm_fractran_not_zero P) as (l & & ).
   exists l; split; auto.
   revert ; apply Forall_impl; intros; tauto.
Qed.


Theorem mm_fractran n (P : list (mm_instr (pos (S n)))) :
     { l | x, (1,P) /MM/ (1,x##vec_zero) l /F/ ps 1 * qs 1^x }.
Proof.
   destruct mm_fractran_n with (P := P) as (l & _ & Hl).
   exists l; intros x; rewrite Hl; simpl.
   rewrite exp_zero, Nat.mul_1_r; tauto.
Qed.