Hilbert's tenth problem is undecidable


From Undecidability.ILL Require Import Definitions UNDEC.
From Undecidability.PCP Require Import singleTM.
From Undecidability.Shared.Libs.DLW.Vec Require Import pos vec.
From Undecidability.Shared.Libs.DLW.Utils Require Import utils_tac.
From Undecidability.ILL.Mm Require Import mm_defs.
From Undecidability.H10 Require Import FRACTRAN_DIO HALT_MM MM_FRACTRAN Fractran.fractran_defs.
From Undecidability.H10.Dio Require Import dio_logic dio_elem dio_single.

Set Implicit Arguments.

Hilbert's Tenth problem: given a diophantine equation with n variable and no parameters, does it have a solution

Definition H10_PROBLEM := { n : nat & dio_polynomial (pos n) Empty_set
                                    * dio_polynomial (pos n) Empty_set }%type.

Definition H10 : H10_PROBLEM -> Prop.
Proof.
  intros (n & p & q).
  apply (dio_single_pred (p,q)), (fun _ => 0).
Defined.

Section DIO_SINGLE_SAT_H10.

  Let f : DIO_SINGLE_PROBLEM -> H10_PROBLEM.
  Proof.
    intros (E,v).
    destruct (dio_poly_eq_pos E) as (n & p & q & H2).
    exists n.
    exact (dp_inst_par v p, dp_inst_par v q).
  Defined.

  Theorem DIO_SINGLE_SAT_H10 : DIO_SINGLE_SAT H10.
  Proof.
    exists f; intros (E,v).
    unfold DIO_SINGLE_SAT, H10, f.
    destruct (dio_poly_eq_pos E) as (n & p & q & H2).
    rewrite H2; unfold dio_single_pred.
    simpl.
    split; intros (phi & H); exists phi; revert H;
      repeat rewrite dp_inst_par_eval; auto.
  Qed.

End DIO_SINGLE_SAT_H10.

Theorem Fractran_UNDEC : Halt FRACTRAN_HALTING.
Proof.
  eapply reduces_transitive. exact MM_HALTING_undec.
  exact MM_FRACTRAN_HALTING.
Qed.

Theorem Hilberts_Tenth : Halt PCP
                      /\ PCP MM_HALTING
                      /\ MM_HALTING FRACTRAN_HALTING
                      /\ FRACTRAN_HALTING DIO_LOGIC_SAT
                      /\ DIO_LOGIC_SAT DIO_ELEM_SAT
                      /\ DIO_ELEM_SAT DIO_SINGLE_SAT
                      /\ DIO_SINGLE_SAT H10.
Proof.
  msplit 6.
  + apply Halt_PCP.
  + apply PCP_MM_HALTING.
  + apply MM_FRACTRAN_HALTING.
  + apply FRACTRAN_HALTING_DIO_LOGIC_SAT.
  + apply DIO_LOGIC_ELEM_SAT.
  + apply DIO_ELEM_SINGLE_SAT.
  + apply DIO_SINGLE_SAT_H10.
Qed.

Theorem H10_undec : Halt H10.
Proof.
  repeat (eapply reduces_transitive; [ apply Hilberts_Tenth | ]).
  apply reduces_reflexive.
Qed.

Check H10_undec.
Print Assumptions H10_undec.