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 : nat * vec nat 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) (_ : nat) := (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 rho 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 (nat * nat) :=
match l with
| nil => nil
| rho :: l => encode_one_instr i rho ++ encode_mm_instr (S i) l
end.
Fact encode_mm_instr_app m i l r : @encode_mm_instr m i (l++r) = encode_mm_instr i l++encode_mm_instr (length l+i) r.
Proof.
revert i; induction l as [ | rho l IHl ]; intros i; simpl; auto; rewrite IHl, app_ass.
do 3 f_equal; lia.
Qed.
Fact encode_mm_instr_regular n i l : Forall (fun 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 = el++c::er
-> exists l rho r, P = l++rho::r /\ In c (encode_one_instr (length l+i) rho).
Proof.
revert i el c er; induction P as [ | rho P IHP ]; simpl; intros i el c er H.
+ destruct el; discriminate.
+ destruct list_app_cons_eq_inv with (1 := H)
as [ (m & H1 & H2) | (m & H1 & H2) ].
* destruct IHP with (1 := H2) as (l & rho' & r & G1 & G2).
exists (rho::l), rho', r; subst; split; auto.
eq goal G2; do 2 f_equal; simpl; lia.
* exists nil, rho, P; split; simpl; auto.
rewrite <- H1; 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 lia.
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 lia.
revert k. induction l; cbn - [subcode] in *; intros.
- revert H0. ring_simplify (k + 0). eauto.
- revert H0. ring_simplify (k + S (length l)). intros H1. destruct a.
+ econstructor 2. intros [[|] % divides_mult_inv | ] % divides_mult_inv; eauto.
* eapply primestream_divides in H0; lia.
* now eapply ps_qs_div in H0.
* eapply divides_encode_state in H0; lia.
* specialize IHl with (k := S k). revert IHl.
cbn - [subcode]. ring_simplify (S (k + length l)).
intros IHl. eapply IHl. 2:exact H1.
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 H0 as [? | ?]...
eapply primestream_divides in H0...
eapply divides_encode_state in H0...
* eapply primestream_divides in H0... subst.
eapply (H n t). eauto.
* eapply divides_encode_state in H0...
* specialize (IHl (S k)). revert IHl.
cbn - [subcode]. ring_simplify (S (k + length l)).
intros IHl. eapply IHl. 2:exact H1.
intros ? ? ?. eapply H. eapply subcode_cons. eassumption.
Qed.
Lemma qs_exp i n u (v : vec nat 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 nat n) :
divides (qs u) (encode_state (i,v)) <-> v #> u > 0.
Proof.
rewrite qs_exp.
enough (forall 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 lia. 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.
lia.
* 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/ (i1, v1) → (i2,v2)
-> encode_mm_instr i P /F/ encode_state (i1,v1) → encode_state (i2,v2).
Proof with eauto; try lia.
intros HP (k & l & [ u | u j ] & r & v & ? & ? & ?); inversion H; subst; clear H.
- inversion H0; inversion H1; subst; clear H0 H1.
eapply skip_steps...
econstructor. cbn. ring_simplify.
replace (1 + (k + length l)) with (k + length l + 1) by lia. unfold encode_state, fst, snd.
rewrite vec_prod_mult.
rewrite Nat.add_0_r; ring.
- inversion H0; inversion H1; subst; clear H0 H1.
all:eapply skip_steps...
+ cbn. econstructor 2.
intros [] % divides_mult_inv_l...
eapply divides_mult_inv in H0 as [ | ]...
* now eapply qs_ps_div in H0.
* eapply qs_encode_state in H0. lia.
* 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 lia.
erewrite <- (vec_prod_div _ _ _ H4).
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/ (i1, v1) -[k]-> (i2,v2)
-> encode_mm_instr i P /F/ encode_state (i1,v1) -[k]-> encode_state (i2,v2).
Proof.
intros HP H. revert v1 i1 i2 H. induction k; intros v1 i1 i2 H; inversion H; subst; clear H; cbn.
- reflexivity.
- destruct st2. eapply one_step_forward in H1; 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 H1 H2.
apply prime_div_mult in H2; auto.
destruct H2 as [ H2 | ]; auto.
apply prime_div_mult in H2; 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 H1 H2.
apply prime_div_mult3 in H2; auto.
destruct H2 as [ H2 | H2 ]; try tauto.
apply prime_div_mult in H2; 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 (i1,v1) → st
-> exists i2 v2, st = @encode_state m (i2,v2)
/\ (i, P) /MM/ (i1, v1) → (i2,v2).
Proof.
intros H1 H2.
destruct fractran_step_inv with (1 := H2)
as (el & p & q & er & H3 & H4 & H5).
unfold encode_state in H5; simpl in H5.
destruct encode_mm_instr_in_inv with (1 := H3)
as (l & rho & r & -> & G2).
assert (i1 = length l+i) as E.
{ unfold encode_one_instr in G2.
destruct rho as [ u | u j ]; unfold encode_inc, encode_dec, encode_dec2 in G2;
[ destruct G2 as [ G2 | [] ] | destruct G2 as [ G2 | [ G2 | [] ] ] ];
inversion G2; subst p q; clear G2;
repeat rewrite mult_assoc in H5.
* apply divides_from_eq, prime_div_mult4 in H5; auto.
destruct H5 as [ H5 | [ H5 | [ H5 | H5 ] ] ].
+ apply primestream_divides in H5; lia.
+ apply ps_qs_div in H5; tauto.
+ apply primestream_divides in H5; lia.
+ apply ps_exp in H5; tauto.
* rewrite <- mult_assoc in H5.
apply divides_from_eq, prime_div_mult3 in H5; auto.
destruct H5 as [ H5 | [ H5 | H5 ] ].
+ apply primestream_divides in H5; lia.
+ apply primestream_divides in H5; lia.
+ apply ps_exp in H5; tauto.
* apply divides_from_eq, prime_div_mult3 in H5; auto.
destruct H5 as [ H5 | [ H5 | H5 ] ].
+ apply primestream_divides in H5.
exfalso; apply (H1 j u); auto.
+ apply primestream_divides in H5; lia.
+ apply ps_exp in H5; tauto. }
destruct mm_sss_total with (ii := rho) (s := (i1,v1))
as ((i2 & v2) & H7).
exists i2, v2.
assert ((i, l++rho::r) /MM/ (i1,v1) → (i2,v2)) as H8.
{ apply in_sss_step; auto; simpl; lia. }
split; auto.
apply one_step_forward in H8; auto.
revert H2 H8; 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 (i1,v1) -[k]-> st
-> exists i2 v2, (i, P) /MM/ (i1, v1) -[k]-> (i2,v2)
/\ st = encode_state (i2,v2).
Proof.
intros H1.
revert i1 v1 st; induction k as [ | k IHk ]; intros i1 v1 st H; simpl in H.
- subst; exists i1, v1; split; auto; constructor.
- destruct H as (st1 & H2 & H3).
destruct one_step_backward with (2 := H2)
as (i2 & v2 & -> & H5); auto.
destruct IHk with (1 := H3) as (i3 & v3 & ? & ->).
exists i3, v3; split; auto.
constructor 2 with (i2,v2); 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 & H1) & H2); simpl fst in *.
exists (encode_state (j,w)); split.
* exists k; apply steps_forward in H1; auto.
* intros x Hx.
destruct one_step_backward with (2 := Hx)
as (i2 & v2 & -> & ?); auto.
revert H; apply sss_out_step_stall; auto.
+ intros (st & (k & H1) & H2).
destruct steps_backward with (2 := H1)
as (i2 & v2 & H3 & ->); auto.
exists (i2,v2); split.
* exists k; auto.
* simpl fst.
destruct (in_out_code_dec i2 (1,P)) as [ H4 | H4 ]; auto; exfalso.
destruct in_code_subcode with (1 := H4) as (rho & l & r & G1 & G2).
destruct (mm_sss_total rho (i2,v2)) as ((i3,v3) & G3).
apply H2 with (encode_state (i3,v3)).
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 (fun c => fst c <> 0 /\ snd c <> 0) l
/\ forall v, (1,P) /MM/ (1,v) ↓ <-> l /F/ ps 1 * exp 1 v ↓ }.
Proof.
destruct mm_remove_self_loops with (P := P) as (Q & H1 & _ & H2).
exists (encode_mm_instr 1 Q); split.
+ apply encode_mm_instr_regular.
+ intros x.
rewrite H2, 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 (fun c => snd c <> 0) l
/\ forall v, (1,P) /MM/ (1,v) ↓ <-> l /F/ ps 1 * exp 1 v ↓ }.
Proof.
destruct (mm_fractran_not_zero P) as (l & H1 & H2).
exists l; split; auto.
revert H1; apply Forall_impl; intros; tauto.
Qed.
Theorem mm_fractran n (P : list (mm_instr (pos (S n)))) :
{ l | forall 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.