H10C

Elementary Diophantine constraints solvability

Preliminaries

The definitions below are mechanized in Problems/H10C.v.

A elementary Diophantine constraint has one of the shapes x ≐ 1, x ≐ y+z or x ≐ y⋅z where x, y, z ∈ 𝕍 range over variables. 𝕍 is implemented as nat and constraints as 𝕍+𝕍³+𝕍³.

A valuation φ : 𝕍 → ℕ satisfies the constraints c, denoted ⟦c⟧ φ, and defined by

• ⟦x ≐ 1⟧ φ when φ(x) = 1;
• ⟦x ≐ y+z⟧ φ when φ(x) = φ(y)+φ(z);
• ⟦x ≐ y⋅z⟧ φ when φ(x) = φ(y)*φ(z).

mechanized as ⟦c⟧ φ := h10c_sem c φ.

Problem instance (mechanized as H10C_PROBLEM)

An instance is a list of elementary Diophantine constraints.

Decision problem (mechanized as H10C_SAT)

Given a list lc of elementary Diophantine constraints, is it solvable, ie is there a valuation φ : 𝕍 → ℕ that satisfies all the constraints in lc simultaneously, ie ∃φ ∀c∈lc, ⟦c⟧ φ ?

Reduction

From the more general elementary Diophantine constraints with parameters. TODO: describe better here.