Require Import List Arith Omega.
From Undecidability.Shared.Libs.DLW.Vec Require Import pos vec.
From Undecidability.Shared.Libs.DLW.Utils Require Import utils_tac utils_list sums.
From Undecidability.ILL.Code Require Import sss.
From Undecidability.ILL.Mm Require Import mm_defs.
From Undecidability.H10.Fractran Require Import fractran_defs fractran_dio mm_fractran prime_seq.
From Undecidability.H10.Dio Require Import dio_logic dio_elem dio_single.
Set Implicit Arguments.
Local Notation "P /MM/ s ↓" := (sss_terminates (@mm_sss _) P s) (at level 70, no associativity).
Local Notation "l '/F/' x ↓" := (fractran_terminates l x) (at level 70, no associativity).
Local Notation "'⟦' p '⟧'" := (fun φ ν => dp_eval φ ν p).
Definitions of n-ary recursive enumerable predicates
Definition mm_recognisable_n n (R : vec nat n -> Prop) :=
{ m & { M : list (mm_instr (n+m)) | forall v, R v <-> (1,M) /MM/ (1,vec_app v vec_zero) ↓ } }.
Definition diophantine_n n (R : vec nat n -> Prop) :=
{ m : nat &
{ p : dio_polynomial (pos m) (pos n) &
{ q : dio_polynomial (pos m) (pos n) |
forall v, R v <-> exists w, ⟦p⟧ (vec_pos w) (vec_pos v)
= ⟦q⟧ (vec_pos w) (vec_pos v) } } }.
Section DPRM_n.
Variable (n : nat) (R : vec nat n -> Prop) (HR : mm_recognisable_n R).
Let FRACTRAN : { l | forall v, R v <-> l /F/ ps 1 * exp 1 v ↓ }.
Proof.
destruct HR as (m & Q & HQ).
destruct mm_fractran_n with (P := Q) as (l & _ & Hl).
exists l.
intros x; rewrite HQ, Hl.
rewrite exp_app, exp_zero, Nat.mul_1_r; tauto.
Qed.
Theorem DPRM_n : diophantine_n R.
Proof.
destruct FRACTRAN as (l & Hl).
clear FRACTRAN HR.
destruct FRACTRAN_HALTING_on_exp_diophantine with n l as (f & Hf); auto.
destruct (dio_formula_elem f) as (ll & _ & _ & G3).
destruct (dio_elem_equation ll) as (c & _ & G4).
destruct (dio_poly_eq_pos c) as (m & p & q & Hpq).
exists m, (dp_proj_par n p), (dp_proj_par n q); intros phi.
rewrite <- (fun2vec_vec2fun phi) with (x := 0) at 1.
rewrite Hl, <- Hf, G3, <- G4, Hpq, dio_poly_eq_pos_equiv.
split; intros (w & Hw); exists w; eq goal Hw; f_equal;
rewrite dp_proj_par_eval; apply dp_eval_ext; auto.
Qed.
End DPRM_n.
Print mm_recognisable_n.
Print diophantine_n.
Check DPRM_n.
Print Assumptions DPRM_n.