FRACTRAN reduces to Diophantine logic


Require Import List Arith Omega.

From Undecidability Require Import ILL.Definitions.

From Undecidability.Shared.Libs.DLW.Utils Require Import utils_tac.
From Undecidability.Shared.Libs.DLW.Vec Require Import pos vec.
From Undecidability.H10.Fractran Require Import fractran_defs fractran_dio.
From Undecidability.H10.Dio Require Import dio_elem dio_single dio_logic.
From Undecidability.H10 Require Import MM_FRACTRAN.

Set Implicit Arguments.

A diophantine logic satisfiability question is given a diophantine logic formula f and a valuation for the parameters. Is the formula valid ?

Definition DIO_LOGIC_PROBLEM := (dio_formula * (nat -> nat))%type.

Definition DIO_LOGIC_SAT : DIO_LOGIC_PROBLEM -> Prop.
Proof.
  intros (A,v).
  exact (df_pred A v).
Defined.

Section FRACTRAN_HALTING_DIO_LOGIC_SAT.

  Let f : FRACTRAN_PROBLEM -> DIO_LOGIC_PROBLEM.
  Proof.
    intros (l & x).
    destruct FRACTRAN_HALTING_on_diophantine with (ll := l) (x := fun _ : nat -> nat => x)
      as (A & HA).
    + auto.
    + exact (A, fun _ => 0).
  Defined.

  Opaque FRACTRAN_HALTING_on_diophantine.

  Theorem FRACTRAN_HALTING_DIO_LOGIC_SAT : FRACTRAN_HALTING DIO_LOGIC_SAT.
  Proof.
    exists f.
    intros (l & x); simpl.
    destruct FRACTRAN_HALTING_on_diophantine with (ll := l) as (A & HA); simpl.
    unfold DIO_LOGIC_SAT; rewrite HA; tauto.
  Qed.

End FRACTRAN_HALTING_DIO_LOGIC_SAT.

An elementary diophantine problem is a list of elementary diophantine constraints and a valuation for the parameters. The question is whether there exists a valuation for the variables that satisfies all the constraints simultaneously

Definition DIO_ELEM_PROBLEM := (list dio_constraint * (nat -> nat))%type.

Definition DIO_ELEM_SAT : DIO_ELEM_PROBLEM -> Prop.
Proof.
  intros (l,v).
  exact (exists φ, Forall (dc_eval φ v) l).
Defined.

Section DIO_LOGIC_ELEM_SAT.

  Let f : DIO_LOGIC_PROBLEM -> DIO_ELEM_PROBLEM.
  Proof.
    intros (A,v).
    destruct (dio_formula_elem A) as (l & _ & _ & H3).
    exact (l,v).
  Defined.

  Theorem DIO_LOGIC_ELEM_SAT : DIO_LOGIC_SAT DIO_ELEM_SAT.
  Proof.
    exists f; intros (A,v); unfold DIO_LOGIC_SAT, DIO_ELEM_SAT, f.
    destruct (dio_formula_elem A) as (l & _ & _ & H3); simpl; auto.
  Qed.

End DIO_LOGIC_ELEM_SAT.

Definition DIO_SINGLE_PROBLEM := (dio_single nat nat * (nat -> nat))%type.

Definition DIO_SINGLE_SAT : DIO_SINGLE_PROBLEM -> Prop.
Proof.
  intros (e,v).
  apply (dio_single_pred e v).
Defined.

Section DIO_ELEM_SINGLE_SAT.

  Let f : DIO_ELEM_PROBLEM -> DIO_SINGLE_PROBLEM.
  Proof.
    intros (l,v).
    destruct (dio_elem_equation l) as (e & _ & H1).
    exact (e,v).
  Defined.

  Theorem DIO_ELEM_SINGLE_SAT : DIO_ELEM_SAT DIO_SINGLE_SAT.
  Proof.
    exists f; intros (l,v).
    unfold DIO_ELEM_SAT, DIO_SINGLE_SAT, f.
    destruct (dio_elem_equation l) as (e & _ & H1).
    rewrite H1; tauto.
  Qed.

End DIO_ELEM_SINGLE_SAT.