Require Import List Lia Cantor.
Import ListNotations.
Require Import ssreflect ssrbool ssrfun.
Require Import Undecidability.DiophantineConstraints.H10C.
Set Default Proof Using "Type".
Set Default Goal Selector "!".
Module Argument.
Definition c2_full (x: nat) : { y:nat | y + y = x * S x}.
Proof.
elim: x; first by exists 0.
move=> x [y Hy]. exists (y+x+1). nia.
Qed.
#[local] Notation c2 x := (sval (c2_full x)).
#[local] Notation c2_spec x := (svalP (c2_full x)).
Notation var x t := (Cantor.to_nat (x, t)).
Opaque Cantor.to_nat Cantor.of_nat.
Section Reduction.
Context (ucs: list h10uc).
Definition h10uc_to_h10upcs (c : h10uc) : list h10upc :=
let '(x, y, z) := c in
let '(a, b, c, t1, t2) := (var y 1, var y 2, var y 3, var y 4, var x 1) in
let '(x, y, z) := (var x 0, var y 0, var z 0) in
[((a, a), (b, t1)); ((c, y), (b, a)); ((c, x), (z, t2))].
Definition upcs := flat_map h10uc_to_h10upcs ucs.
Section Transport.
Context (φ: nat -> nat).
Context (Hφ : forall c, In c ucs -> h10uc_sem φ c).
Definition φ' (xn: nat) : nat :=
match Cantor.of_nat xn with
| (x, 0) => φ x
| (x, 1) => c2 (φ x)
| (x, 2) => φ x * φ x + φ x + 1
| (x, 3) => φ x * φ x
| (x, 4) => c2 (c2 (φ x))
| _ => 0
end.
Lemma transport : forall c, In c upcs -> h10upc_sem φ' c.
Proof using Hφ.
apply /Forall_forall /Forall_flat_map.
move: Hφ => /Forall_forall.
apply: Forall_impl => - [[x y] z] /= ?.
constructor; [|constructor; [|constructor]]; last done.
all: rewrite /φ' /= ?Cantor.cancel_of_to ?(c2_spec _); lia.
Qed.
End Transport.
Section InverseTransport.
Context (φ': nat -> nat).
Context (Hφ' : forall c, In c upcs -> h10upc_sem φ' c).
Definition φ (n:nat) : nat := φ' (var n 0).
Lemma inverse_transport : forall c, In c ucs -> h10uc_sem φ c.
Proof using Hφ'.
apply /Forall_forall.
move: Hφ' => /Forall_forall /Forall_flat_map.
apply: Forall_impl => - [[x y] z] /=.
move=> /Forall_cons_iff [+] /Forall_cons_iff [+] /Forall_cons_iff [+ _].
rewrite /φ /=. nia.
Qed.
End InverseTransport.
End Reduction.
End Argument.
Require Import Undecidability.Synthetic.Definitions.
Square Diophantine Constraint Solvability many-one reduces to Uniform Diophantine Constraint Solvability
Theorem reduction : H10UC_SAT ⪯ H10UPC_SAT.
Proof.
exists Argument.upcs. split.
- intros [φ Hφ]. exists (Argument.φ' φ). now apply Argument.transport.
- intros [φ' Hφ']. exists (Argument.φ φ'). now apply Argument.inverse_transport.
Qed.
Proof.
exists Argument.upcs. split.
- intros [φ Hφ]. exists (Argument.φ' φ). now apply Argument.transport.
- intros [φ' Hφ']. exists (Argument.φ φ'). now apply Argument.inverse_transport.
Qed.