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.

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.