Require Import List Arith Omega.
From Undecidability Require Import ILL.Definitions.
From Undecidability.Shared.Libs.DLW.Vec Require Import pos vec.
From Undecidability.ILL.Code Require Import sss subcode.
From Undecidability.ILL.Mm Require Import mm_defs.
From Undecidability.H10.Fractran Require Import fractran_defs mm_fractran prime_seq.
Set Implicit Arguments.
Given a FRACTRAN program and a starting state, does it terminate
Definition FRACTRAN_PROBLEM := (list (nat*nat) * nat)%type.
Definition FRACTRAN_HALTING (P : FRACTRAN_PROBLEM) : Prop.
Proof.
destruct P as (l & x).
exact (l /F/ x ↓).
Defined.
Given a FRACTRAN program and a starting vector v1,...,vn,
does the program terminate starting from p1 * q1^v1 * ... qn^vn
Definition FRACTRAN_ALT_PROBLEM := (list (nat*nat) * { n : nat & vec nat n })%type.
Definition FRACTRAN_ALT_HALTING : FRACTRAN_ALT_PROBLEM -> Prop.
Proof.
intros (l & n & v).
exact (l /F/ ps 1 * exp 1 v ↓).
Defined.
Section MM_HALTING_FRACTRAN_ALT_HALTING.
Let f : MM_PROBLEM -> FRACTRAN_ALT_PROBLEM.
Proof.
intros (n & P & v); red.
destruct (mm_fractran_n P) as (l & H1 & _).
split.
+ exact l.
+ exists n; exact v.
Defined.
Theorem MM_FRACTRAN_ALT_HALTING : MM_HALTING ⪯ FRACTRAN_ALT_HALTING.
Proof.
exists f; intros (n & P & v); simpl.
destruct (mm_fractran_n P) as (l & H1 & H2); simpl; auto.
Qed.
End MM_HALTING_FRACTRAN_ALT_HALTING.
Section FRACTRAN_ALT_HALTING_HALTING.
Let f : FRACTRAN_ALT_PROBLEM -> FRACTRAN_PROBLEM.
Proof.
intros (l & n & v).
exact (l,(ps 1 * exp 1 v)).
Defined.
Theorem FRACTRAN_ALT_HALTING_HALTING : FRACTRAN_ALT_HALTING ⪯ FRACTRAN_HALTING.
Proof.
exists f; intros (n & P & v); simpl; tauto.
Qed.
End FRACTRAN_ALT_HALTING_HALTING.
Corollary MM_FRACTRAN_HALTING : MM_HALTING ⪯ FRACTRAN_HALTING.
Proof.
eapply reduces_transitive. apply MM_FRACTRAN_ALT_HALTING.
exact FRACTRAN_ALT_HALTING_HALTING.
Qed.
Check MM_FRACTRAN_HALTING.
Print Assumptions MM_FRACTRAN_HALTING.