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.