Require Import List Arith Lia.
From Undecidability.Shared.Libs.DLW
Require Import utils gcd pos vec subcode sss.
From Undecidability.MinskyMachines.MMA
Require Import mma_defs mma_utils.
From Undecidability.FRACTRAN
Require Import FRACTRAN fractran_utils.
Set Implicit Arguments.
Set Default Proof Using "Type".
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 "P /MM2/ s -+> t" := (sss_progress (@mma_sss _) P s t) (at level 70, no associativity).
Local Notation "P /MM2/ s ->> t" := (sss_compute (@mma_sss _) P s t) (at level 70, no associativity).
Local Notation "P /MM2/ s ↓" := (sss_terminates (@mma_sss _) P s) (at level 70, no associativity).
Local Notation "l /F/ x → y" := (fractran_step l x y) (at level 70, no associativity).
Section Fractran_with_two_counters.
Hint Resolve subcode_refl : core.
Hint Rewrite mma_null_length mma_transfert_length mma_incs_length mma_decs_copy_length
mma_mult_cst_length mma_decs_length mma_mod_cst_length mma_div_cst_length : length_db.
Let src : pos 2 := pos0.
Let dst : pos 2 := pos1.
Ltac dest x y := destruct (pos_eq_dec x y) as [ | ]; [ subst x | ]; rew vec.
Let Hsrc_dst : src <> dst. Proof. discriminate. Qed.
Let Hdst_src : dst <> src. Proof. discriminate. Qed.
Section mma_loop.
Definition mma_loop := INC src :: DEC src 1 :: nil.
Fact mma_loop_loop v : (1,mma_loop) /MM2/ (1,v) -+> (1,v).
Proof.
unfold mma_loop.
mma sss INC with src.
mma sss DEC S with src 1 (v#>src); rew vec.
mma sss stop.
Qed.
Theorem mma_loop_spec v : ~ (1,mma_loop) /MM2/ (1,v) ↓.
Proof.
intros (w & (k & Hk) & H2); revert w Hk H2.
induction on k as IHk with measure k; intros w Hk Hw.
destruct subcode_sss_progress_inv with (4 := mma_loop_loop v) (5 := Hk)
as (q & H1 & H2); auto.
{ apply mma_sss_fun. }
apply IHk with (1 := H1) (2 := H2); auto.
Qed.
End mma_loop.
Section mma_fractran_one.
Variables (a b : nat) (p i : nat).
Definition mma_fractran_one :=
mma_mult_cst src dst a i
++ mma_mod_cst dst src (11+a+4*b+i) (21+a+7*b+i) b (5+a+i)
++ mma_div_cst src dst b (11+a+4*b+i)
++ mma_transfert dst src (16+a+7*b+i)
++ INC dst :: DEC dst p
:: mma_div_cst src dst a (21+a+7*b+i)
++ mma_transfert dst src (26+4*a+7*b+i).
Fact mma_fractran_one_length : length mma_fractran_one = 29+4*a+7*b.
Proof. unfold mma_fractran_one; rew length; lia. Qed.
Hypothesis (Ha : a <> 0) (Hb : b <> 0).
Fact mma_fractran_one_ok_progress k v :
k*b = a*(v#>src)
-> v#>dst = 0
-> (i,mma_fractran_one) /MM2/ (i,v) -+> (p,v[k/src]).
Proof using Ha Hb.
intros H1 H2; unfold mma_fractran_one.
apply sss_progress_trans with (5+a+i,v[0/src][(k*b)/dst]).
{ apply subcode_sss_progress with (P := (i,mma_mult_cst src dst a i)); auto.
apply mma_mult_cst_progress; auto.
rewrite H2, <- H1; do 2 f_equal; lia. }
apply sss_progress_trans with (11+a+4*b+i,v[(k*b)/src][0/dst]).
{ apply subcode_sss_progress with (P := (5+a+i,mma_mod_cst dst src (11+a+4*b+i) (21+a+7*b+i) b (5+a+i))); auto.
apply mma_mod_cst_divides_progress with k; rew vec; try lia.
f_equal; apply vec_pos_ext; intros y; dest y dst; try lia; dest y src. }
apply sss_progress_trans with (16+a+7*b+i,v[0/src][k/dst]).
{ apply subcode_sss_progress with (P := (11+a+4*b+i,mma_div_cst src dst b (11+a+4*b+i))); auto.
apply mma_div_cst_progress with k; auto; rew vec; try lia.
f_equal; try lia.
apply vec_pos_ext; intros y; dest y dst; try lia; dest y src. }
apply sss_progress_trans with (19+a+7*b+i,v[k/src][0/dst]).
{ apply subcode_sss_progress with (P := (16+a+7*b+i,mma_transfert dst src (16+a+7*b+i))); auto.
apply mma_transfert_progress; auto.
f_equal; try lia.
apply vec_pos_ext; intros y; dest y dst; try lia; dest y src. }
mma sss INC with dst.
mma sss DEC S with dst p 0; rew vec.
mma sss stop; f_equal.
apply vec_pos_ext; intros y; dest y dst; try lia; dest y src.
Qed.
Fact mma_fractran_one_nok_progress v :
~ divides b (a*(v#>src))
-> v#>dst = 0
-> (i,mma_fractran_one) /MM2/ (i,v) -+> (length mma_fractran_one+i,v).
Proof using Ha Hb.
rewrite mma_fractran_one_length.
intros H1 H2; unfold mma_fractran_one.
rewrite divides_rem_eq in H1.
revert H1.
generalize (div_rem_spec1 (a*(v#>src)) b)
(div_rem_spec2 (a*(v#>src)) Hb).
generalize (div (a*(v#>src)) b) (rem (a*(v#>src)) b); intros x y H3 H4 H5.
apply sss_progress_trans with (5+a+i,v[0/src][(x*b+y)/dst]).
{ apply subcode_sss_progress with (P := (i,mma_mult_cst src dst a i)); auto.
apply mma_mult_cst_progress; auto.
rewrite H2, <- H3; do 2 f_equal; lia. }
apply sss_progress_trans with (21+a+7*b+i,v[(a*(v#>src))/src][0/dst]).
{ apply subcode_sss_progress with (P := (5+a+i,mma_mod_cst dst src (11+a+4*b+i) (21+a+7*b+i) b (5+a+i))); auto.
apply mma_mod_cst_not_divides_progress with x y; rew vec; try lia.
f_equal; apply vec_pos_ext; intros c; dest c dst; try lia; dest c src; lia. }
apply sss_progress_trans with (26+4*a+7*b+i,v[0/src][(v#>src)/dst]).
{ apply subcode_sss_progress with (P := (21+a+7*b+i,mma_div_cst src dst a (21+a+7*b+i))); auto.
apply mma_div_cst_progress with (v#>src); auto; rew vec; try lia; try ring.
f_equal; try lia.
apply vec_pos_ext; intros c; dest c dst; try lia; dest c src. }
apply subcode_sss_progress with (P := (26+4*a+7*b+i,mma_transfert dst src (26+4*a+7*b+i))); auto.
apply mma_transfert_progress; auto.
f_equal; try lia.
apply vec_pos_ext; intros c; dest c dst; try lia; dest c src.
Qed.
End mma_fractran_one.
Hint Rewrite mma_fractran_one_length : length_db.
Section mma_fractran_step.
Variable (p : nat).
Fixpoint mma_fractran_step ll i { struct ll } :=
match ll with
| nil => nil
| (a,b)::ll => let P := mma_fractran_one a b p i
in P ++ mma_fractran_step ll (length P+i)
end.
Fact mma_fractran_step_success_progress ll i x y v :
Forall (fun c => fst c <> 0 /\ snd c <> 0) ll
-> ll /F/ x → y
-> v#>src = x
-> v#>dst = 0
-> (i,mma_fractran_step ll i) /MM2/ (i,v) -+> (p,v[y/src]).
Proof.
intros H1 H2; revert H2 i v H1.
induction 1 as [ a b ll x y H1 | a b ll x y H1 H2 IH2 ];
intros i v H3 H6 H7; rewrite Forall_cons_inv in H3; destruct H3 as ((H3 & H4) & H5); simpl in H3, H4;
unfold mma_fractran_step; fold mma_fractran_step.
+ apply subcode_sss_progress with (P := (i,mma_fractran_one a b p i)); auto.
apply mma_fractran_one_ok_progress; auto; rewrite H6, <- H1; ring.
+ apply sss_progress_trans with (length (mma_fractran_one a b p i)+i,v).
{ apply subcode_sss_progress with (P := (i,mma_fractran_one a b p i)); auto.
apply mma_fractran_one_nok_progress; auto; rewrite H6; auto. }
{ apply subcode_sss_progress with (P := (length (mma_fractran_one a b p i)+i,
mma_fractran_step ll (length (mma_fractran_one a b p i)+i))); auto.
apply subcode_right; lia. }
Qed.
Fact mma_fractran_step_failure_compute ll i v :
Forall (fun c => fst c <> 0 /\ snd c <> 0) ll
-> fractran_stop ll (v#>src)
-> v#>dst = 0
-> (i,mma_fractran_step ll i) /MM2/ (i,v) ->> (length (mma_fractran_step ll i)+i,v).
Proof.
intros H1 H2 H3; revert H1 i H2.
induction 1 as [ | (a,b) ll (Ha & Hb) Hll IH ]; intros i H4.
+ mma sss stop.
+ apply fractan_stop_cons_inv in H4; destruct H4 as (H4 & H5).
unfold mma_fractran_step; fold mma_fractran_step.
set (P := mma_fractran_one a b p i); rew length.
apply sss_compute_trans with (length P+i,v).
{ apply subcode_sss_compute with (P := (i,P)); auto.
apply sss_progress_compute, mma_fractran_one_nok_progress; auto. }
{ apply subcode_sss_compute with (P := (length P+i,mma_fractran_step ll (length P + i))); auto.
{ apply subcode_right; lia. }
replace (length P+length (mma_fractran_step ll (length P + i))+i)
with (length (mma_fractran_step ll (length P + i)) + (length P+i)) by lia.
auto. }
Qed.
End mma_fractran_step.
Section fractran_mma.
Variables (ll : list (nat*nat)) (Hll : Forall (fun c => fst c <> 0 /\ snd c <> 0) ll).
Let i := 1.
Definition fractran_mma := mma_fractran_step i ll i.
Lemma fractran_mma_sound v x w :
v#>dst = 0
-> fractran_compute ll (v#>src) x
-> fractran_stop ll x
-> w = v[x/src]
-> (i,fractran_mma) /MM2/ (i,v) ->> (length fractran_mma+i,w).
Proof using Hll.
intros H1 (u & H2) H3 ?; subst w.
revert v x H1 H2 H3.
induction u as [ | u IHu ]; simpl; intros v y H1 H2 H3.
+ rewrite <- H2; rew vec.
apply mma_fractran_step_failure_compute; auto.
rewrite H2; auto.
+ destruct H2 as (z & H2 & H4).
apply mma_fractran_step_success_progress
with (1 := Hll) (p := i) (i := i) (v := v) in H2; auto.
apply IHu with (v := v[z/src]) in H3; auto; rew vec.
revert H3; rew vec; intros H3.
apply sss_compute_trans with (2 := H3).
apply sss_progress_compute; auto.
Qed.
Lemma fractran_mma_complete v :
v#>dst = 0
-> (i,fractran_mma) /MM2/ (i,v) ↓
-> ll /F/ (v#>src) ↓.
Proof using Hll.
intros H1 ((j,w) & (u & H2) & H3); simpl fst in H3.
revert v H1 H2.
induction on u as IHu with measure u; intros v H1 H2.
destruct (fractran_step_dec ll (v#>src)) as [ (y & Hy) | H4 ].
2: { exists (v#>src); split; auto; exists 0; simpl; auto. }
generalize Hy; intros H4.
apply mma_fractran_step_success_progress
with (1 := Hll) (p := i) (i := i) (v := v)
in H4; auto.
fold fractran_mma in H4.
destruct subcode_sss_progress_inv with (4 := H4) (5 := H2)
as (p & H5 & H6); auto.
1: apply mma_sss_fun.
apply IHu in H6; auto; rew vec.
destruct H6 as (z & (k & Hk) & Hz2).
exists z; split; auto; exists (S k), y; split; auto.
revert Hk; rew vec.
Qed.
Theorem fractran_mma_reduction x :
ll /F/ x ↓ <-> (i,fractran_mma) /MM2/ (i,x##0##vec_nil) ↓.
Proof using Hll.
split; auto.
+ intros (y & H2 & H3).
exists (length fractran_mma+i,y##0##vec_nil); split; simpl; auto; try lia.
apply fractran_mma_sound with (x := y); auto.
+ apply fractran_mma_complete; auto.
Qed.
End fractran_mma.
End Fractran_with_two_counters.
Section fractran_mma_reg_reduction.
Variables (ll : list (nat*nat)).
Let reduction : { P | Forall (fun c => snd c <> 0) ll -> forall x, ll /F/ x ↓ <-> (1,P) /MM2/ (1,x##0##vec_nil) ↓ }.
Proof.
destruct (Forall_Exists_dec (fun c : nat * nat => fst c <> 0)) with (l := ll) as [ H | H ].
+ intros (x,?); simpl; destruct (eq_nat_dec x 0); subst; auto.
+ exists (fractran_mma ll); intros Hll x.
apply fractran_mma_reduction.
revert H Hll; repeat rewrite Forall_forall; firstorder.
+ rewrite Exists_exists in H.
exists mma_loop; intros Hll.
destruct H as ((x,y) & H1 & H2); simpl in H2.
replace x with 0 in H1 by lia; clear H2.
intros n; split.
* intros H; exfalso.
revert H; apply FRACTRAN_HALTING_zero_num.
apply Exists_exists; exists (0,y); auto.
* intros H; exfalso; revert H; apply mma_loop_spec.
Qed.
Definition fractran_reg_mma := proj1_sig reduction.
Theorem fractran_reg_mma_reduction :
Forall (fun c => snd c <> 0) ll
-> forall x, ll /F/ x ↓
<-> (1,fractran_reg_mma) /MM2/ (1,x##0##vec_nil) ↓.
Proof. apply (proj2_sig reduction). Qed.
End fractran_mma_reg_reduction.