mathlib3 documentation

number_theory.dioph

Diophantine functions and Matiyasevic's theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Hilbert's tenth problem asked whether there exists an algorithm which for a given integer polynomial determines whether this polynomial has integer solutions. It was answered in the negative in 1970, the final step being completed by Matiyasevic who showed that the power function is Diophantine.

Here a function is called Diophantine if its graph is Diophantine as a set. A subset S ⊆ ℕ ^ α in turn is called Diophantine if there exists an integer polynomial on α ⊕ β such that v ∈ S iff there exists t : ℕ^β with p (v, t) = 0.

Main definitions #

is_poly: a predicate stating that a function is a multivariate integer polynomial.
poly: the type of multivariate integer polynomial functions.
dioph: a predicate stating that a set is Diophantine, i.e. a set S ⊆ ℕ^α is Diophantine if there exists a polynomial on α ⊕ β such that v ∈ S iff there exists t : ℕ^β with p (v, t) = 0.
dioph_fn: a predicate on a function stating that it is Diophantine in the sense that its graph is Diophantine as a set.

Main statements #

pell_dioph states that solutions to Pell's equation form a Diophantine set.
pow_dioph states that the power function is Diophantine, a version of Matiyasevic's theorem.

References #

Tags #

Matiyasevic's theorem, Hilbert's tenth problem

TODO #

Finish the solution of Hilbert's tenth problem.
Connect poly to mv_polynomial

Multivariate integer polynomials #

Note that this duplicates mv_polynomial.

inductive is_poly {α : Type u_1} :

((α → ℕ) → ℤ) → Prop

proj : ∀ {α : Type u_1} (i : α), is_poly (λ (x : α → ℕ), ↑(x i))
const : ∀ {α : Type u_1} (n : ℤ), is_poly (λ (x : α → ℕ), n)
sub : ∀ {α : Type u_1} {f g : (α → ℕ) → ℤ}, is_poly f → is_poly g → is_poly (λ (x : α → ℕ), f x - g x)
mul : ∀ {α : Type u_1} {f g : (α → ℕ) → ℤ}, is_poly f → is_poly g → is_poly (λ (x : α → ℕ), f x * g x)

A predicate asserting that a function is a multivariate integer polynomial. (We are being a bit lazy here by allowing many representations for multiplication, rather than only allowing monomials and addition, but the definition is equivalent and this is easier to use.)

theorem is_poly.neg {α : Type u_1} {f : (α → ℕ) → ℤ} :

is_poly f → is_poly (-f)

theorem is_poly.add {α : Type u_1} {f g : (α → ℕ) → ℤ} (hf : is_poly f) (hg : is_poly g) :

is_poly (f + g)

def poly (α : Type u) :

The type of multivariate integer polynomials

Equations

poly α = {f // is_poly f}

Instances for poly

@[protected, instance]

def poly.fun_like {α : Type u_1} :

fun_like (poly α) (α → ℕ) (λ (_x : α → ℕ), ℤ)

Equations

poly.fun_like = {coe := subtype.val (λ (f : (α → ℕ) → ℤ), is_poly f), coe_injective' := _}

@[protected, instance]

def poly.has_coe_to_fun {α : Type u_1} :

has_coe_to_fun (poly α) (λ (_x : poly α), (α → ℕ) → ℤ)

Helper instance for when there are too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations

poly.has_coe_to_fun = fun_like.has_coe_to_fun

@[protected]

theorem poly.is_poly {α : Type u_1} (f : poly α) :

The underlying function of a poly is a polynomial

@[ext]

theorem poly.ext {α : Type u_1} {f g : poly α} :

(∀ (x : α → ℕ), ⇑f x = ⇑g x) → f = g

Extensionality for poly α

def poly.proj {α : Type u_1} (i : α) :

The ith projection function, x_i.

Equations

poly.proj i = ⟨λ (x : α → ℕ), ↑(x i), _⟩

@[simp]

theorem poly.proj_apply {α : Type u_1} (i : α) (x : α → ℕ) :

⇑(poly.proj i) x = ↑(x i)

def poly.const {α : Type u_1} (n : ℤ) :

The constant function with value n : ℤ.

Equations

poly.const n = ⟨λ (x : α → ℕ), n, _⟩

@[simp]

theorem poly.const_apply {α : Type u_1} (n : ℤ) (x : α → ℕ) :

⇑(poly.const n) x = n

@[protected, instance]

def poly.has_zero {α : Type u_1} :

has_zero (poly α)

Equations

poly.has_zero = {zero := poly.const 0}

@[protected, instance]

def poly.has_one {α : Type u_1} :

has_one (poly α)

Equations

poly.has_one = {one := poly.const 1}

@[protected, instance]

def poly.has_neg {α : Type u_1} :

has_neg (poly α)

Equations

poly.has_neg = {neg := λ (f : poly α), ⟨-⇑f, _⟩}

@[protected, instance]

def poly.has_add {α : Type u_1} :

has_add (poly α)

Equations

poly.has_add = {add := λ (f g : poly α), ⟨⇑f + ⇑g, _⟩}

@[protected, instance]

def poly.has_sub {α : Type u_1} :

has_sub (poly α)

Equations

poly.has_sub = {sub := λ (f g : poly α), ⟨⇑f - ⇑g, _⟩}

@[protected, instance]

def poly.has_mul {α : Type u_1} :

has_mul (poly α)

Equations

poly.has_mul = {mul := λ (f g : poly α), ⟨⇑f * ⇑g, _⟩}

@[simp]

theorem poly.coe_zero {α : Type u_1} :

⇑0 = ⇑(poly.const 0)

@[simp]

theorem poly.coe_one {α : Type u_1} :

⇑1 = ⇑(poly.const 1)

@[simp]

theorem poly.coe_neg {α : Type u_1} (f : poly α) :

@[simp]

theorem poly.coe_add {α : Type u_1} (f g : poly α) :

⇑(f + g) = ⇑f + ⇑g

@[simp]

theorem poly.coe_sub {α : Type u_1} (f g : poly α) :

⇑(f - g) = ⇑f - ⇑g

@[simp]

theorem poly.coe_mul {α : Type u_1} (f g : poly α) :

⇑(f * g) = ⇑f * ⇑g

@[simp]

theorem poly.zero_apply {α : Type u_1} (x : α → ℕ) :

⇑0 x = 0

@[simp]

theorem poly.one_apply {α : Type u_1} (x : α → ℕ) :

⇑1 x = 1

@[simp]

theorem poly.neg_apply {α : Type u_1} (f : poly α) (x : α → ℕ) :

(⇑-f) x = -⇑f x

@[simp]

theorem poly.add_apply {α : Type u_1} (f g : poly α) (x : α → ℕ) :

⇑(f + g) x = ⇑f x + ⇑g x

@[simp]

theorem poly.sub_apply {α : Type u_1} (f g : poly α) (x : α → ℕ) :

⇑(f - g) x = ⇑f x - ⇑g x

@[simp]

theorem poly.mul_apply {α : Type u_1} (f g : poly α) (x : α → ℕ) :

⇑(f * g) x = ⇑f x * ⇑g x

@[protected, instance]

def poly.inhabited (α : Type u_1) :

inhabited (poly α)

Equations

poly.inhabited α = {default := 0}

@[protected, instance]

def poly.add_comm_group {α : Type u_1} :

add_comm_group (poly α)

Equations

poly.add_comm_group = {add := has_add.add poly.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := nsmul_rec {add := has_add.add poly.has_add}, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg poly.has_neg, sub := has_sub.sub poly.has_sub, sub_eq_add_neg := _, zsmul := zsmul_rec {neg := has_neg.neg poly.has_neg}, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}

@[protected, instance]

def poly.add_group_with_one {α : Type u_1} :

add_group_with_one (poly α)

Equations

poly.add_group_with_one = {int_cast := poly.const α, add := add_comm_group.add poly.add_comm_group, add_assoc := _, zero := add_comm_group.zero poly.add_comm_group, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul poly.add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg poly.add_comm_group, sub := add_comm_group.sub poly.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul poly.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, nat_cast := λ (n : ℕ), poly.const ↑n, one := 1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _}

@[protected, instance]

def poly.comm_ring {α : Type u_1} :

comm_ring (poly α)

Equations

poly.comm_ring = {add := has_add.add poly.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_group_with_one.nsmul poly.add_group_with_one, nsmul_zero' := _, nsmul_succ' := _, neg := add_group_with_one.neg poly.add_group_with_one, sub := add_group_with_one.sub poly.add_group_with_one, sub_eq_add_neg := _, zsmul := add_group_with_one.zsmul poly.add_group_with_one, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := add_group_with_one.int_cast poly.add_group_with_one, nat_cast := add_group_with_one.nat_cast poly.add_group_with_one, one := 1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := has_mul.mul poly.has_mul, mul_assoc := _, one_mul := _, mul_one := _, npow := npow_rec {mul := has_mul.mul poly.has_mul}, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}

theorem poly.induction {α : Type u_1} {C : poly α → Prop} (H1 : ∀ (i : α), C (poly.proj i)) (H2 : ∀ (n : ℤ), C (poly.const n)) (H3 : ∀ (f g : poly α), C f → C g → C (f - g)) (H4 : ∀ (f g : poly α), C f → C g → C (f * g)) (f : poly α) :

C f

def poly.sumsq {α : Type u_1} :

list (poly α) → poly α

The sum of squares of a list of polynomials. This is relevant for Diophantine equations, because it means that a list of equations can be encoded as a single equation: x = 0 ∧ y = 0 ∧ z = 0 is equivalent to x^2 + y^2 + z^2 = 0.

Equations

poly.sumsq (p :: ps) = p * p + poly.sumsq ps
poly.sumsq list.nil = 0

theorem poly.sumsq_nonneg {α : Type u_1} (x : α → ℕ) (l : list (poly α)) :

0 ≤ ⇑(poly.sumsq l) x

theorem poly.sumsq_eq_zero {α : Type u_1} (x : α → ℕ) (l : list (poly α)) :

⇑(poly.sumsq l) x = 0 ↔ list.all₂ (λ (a : poly α), ⇑a x = 0) l

def poly.map {α : Type u_1} {β : Type u_2} (f : α → β) (g : poly α) :

Map the index set of variables, replacing x_i with x_(f i).

Equations

poly.map f g = ⟨λ (v : β → ℕ), ⇑g (v ∘ f), _⟩

@[simp]

theorem poly.map_apply {α : Type u_1} {β : Type u_2} (f : α → β) (g : poly α) (v : β → ℕ) :

⇑(poly.map f g) v = ⇑g (v ∘ f)

Diophantine sets #

def dioph {α : Type u} (S : set (α → ℕ)) :

Prop

A set S ⊆ ℕ^α is Diophantine if there exists a polynomial on α ⊕ β such that v ∈ S iff there exists t : ℕ^β with p (v, t) = 0.

Equations

dioph S = ∃ {β : Type u} (p : poly (α ⊕ β)), ∀ (v : α → ℕ), S v ↔ ∃ (t : β → ℕ), ⇑p (sum.elim v t) = 0

theorem dioph.ext {α : Type u} {S S' : set (α → ℕ)} (d : dioph S) (H : ∀ (v : α → ℕ), v ∈ S ↔ v ∈ S') :

theorem dioph.of_no_dummies {α : Type u} (S : set (α → ℕ)) (p : poly α) (h : ∀ (v : α → ℕ), S v ↔ ⇑p v = 0) :

theorem dioph.inject_dummies_lem {α β γ : Type u} (f : β → γ) (g : γ → option β) (inv : ∀ (x : β), g (f x) = option.some x) (p : poly (α ⊕ β)) (v : α → ℕ) :

(∃ (t : β → ℕ), ⇑p (sum.elim v t) = 0) ↔ ∃ (t : γ → ℕ), ⇑(poly.map (sum.elim sum.inl (sum.inr ∘ f)) p) (sum.elim v t) = 0

theorem dioph.inject_dummies {α β γ : Type u} {S : set (α → ℕ)} (f : β → γ) (g : γ → option β) (inv : ∀ (x : β), g (f x) = option.some x) (p : poly (α ⊕ β)) (h : ∀ (v : α → ℕ), S v ↔ ∃ (t : β → ℕ), ⇑p (sum.elim v t) = 0) :

∃ (q : poly (α ⊕ γ)), ∀ (v : α → ℕ), S v ↔ ∃ (t : γ → ℕ), ⇑q (sum.elim v t) = 0

theorem dioph.reindex_dioph {α : Type u} (β : Type u) {S : set (α → ℕ)} (f : α → β) (d : dioph S) :

dioph {v : β → ℕ | v ∘ f ∈ S}

theorem dioph.dioph_list.all₂ {α : Type u} (l : list (set (α → ℕ))) (d : list.all₂ dioph l) :

dioph {v : α → ℕ | list.all₂ (λ (S : set (α → ℕ)), v ∈ S) l}

theorem dioph.inter {α : Type u} {S S' : set (α → ℕ)} (d : dioph S) (d' : dioph S') :

dioph (S ∩ S')

theorem dioph.union {α : Type u} {S S' : set (α → ℕ)} (d : dioph S) (d' : dioph S') :

dioph (S ∪ S')

def dioph.dioph_pfun {α : Type u} (f : (α → ℕ) →. ℕ) :

Prop

A partial function is Diophantine if its graph is Diophantine.

Equations

dioph.dioph_pfun f = dioph {v : option α → ℕ | f.graph (v ∘ option.some, v option.none)}

def dioph.dioph_fn {α : Type u} (f : (α → ℕ) → ℕ) :

Prop

A function is Diophantine if its graph is Diophantine.

Equations

dioph.dioph_fn f = dioph {v : option α → ℕ | f (v ∘ option.some) = v option.none}

theorem dioph.reindex_dioph_fn {α β : Type u} {f : (α → ℕ) → ℕ} (g : α → β) (d : dioph.dioph_fn f) :

dioph.dioph_fn (λ (v : β → ℕ), f (v ∘ g))

theorem dioph.ex_dioph {α β : Type u} {S : set (α ⊕ β → ℕ)} :

dioph S → dioph {v : α → ℕ | ∃ (x : β → ℕ), sum.elim v x ∈ S}

theorem dioph.ex1_dioph {α : Type u} {S : set (option α → ℕ)} :

dioph S → dioph {v : α → ℕ | ∃ (x : ℕ), option.elim x v ∈ S}

theorem dioph.dom_dioph {α : Type u} {f : (α → ℕ) →. ℕ} (d : dioph.dioph_pfun f) :

theorem dioph.dioph_fn_iff_pfun {α : Type u} (f : (α → ℕ) → ℕ) :

dioph.dioph_fn f = dioph.dioph_pfun ↑f

theorem dioph.abs_poly_dioph {α : Type u} (p : poly α) :

dioph.dioph_fn (λ (v : α → ℕ), (⇑p v).nat_abs)

theorem dioph.proj_dioph {α : Type u} (i : α) :

dioph.dioph_fn (λ (v : α → ℕ), v i)

theorem dioph.dioph_pfun_comp1 {α : Type u} {S : set (option α → ℕ)} (d : dioph S) {f : (α → ℕ) →. ℕ} (df : dioph.dioph_pfun f) :

dioph {v : α → ℕ | ∃ (h : f.dom v), option.elim (f.fn v h) v ∈ S}

theorem dioph.dioph_fn_comp1 {α : Type u} {S : set (option α → ℕ)} (d : dioph S) {f : (α → ℕ) → ℕ} (df : dioph.dioph_fn f) :

dioph {v : α → ℕ | option.elim (f v) v ∈ S}

theorem dioph.dioph_fn_vec_comp1 {n : ℕ} {S : set (vector3 ℕ n.succ)} (d : dioph S) {f : vector3 ℕ n → ℕ} (df : dioph.dioph_fn f) :

dioph {v : vector3 ℕ n | f v::v ∈ S}

theorem dioph.vec_ex1_dioph (n : ℕ) {S : set (vector3 ℕ n.succ)} (d : dioph S) :

dioph {v : fin2 n → ℕ | ∃ (x : ℕ), x::v ∈ S}

theorem dioph.dioph_fn_vec {n : ℕ} (f : vector3 ℕ n → ℕ) :

dioph.dioph_fn f ↔ dioph {v : fin2 n.succ → ℕ | f (v ∘ fin2.fs) = v fin2.fz}

theorem dioph.dioph_pfun_vec {n : ℕ} (f : vector3 ℕ n →. ℕ) :

dioph.dioph_pfun f ↔ dioph {v : fin2 n.succ → ℕ | f.graph (v ∘ fin2.fs, v fin2.fz)}

theorem dioph.dioph_fn_compn {α : Type} {n : ℕ} {S : set (α ⊕ fin2 n → ℕ)} (d : dioph S) {f : vector3 ((α → ℕ) → ℕ) n} (df : vector_allp dioph.dioph_fn f) :

dioph {v : α → ℕ | sum.elim v (λ (i : fin2 n), f i v) ∈ S}

theorem dioph.dioph_comp {α : Type} {n : ℕ} {S : set (vector3 ℕ n)} (d : dioph S) (f : vector3 ((α → ℕ) → ℕ) n) (df : vector_allp dioph.dioph_fn f) :

dioph {v : α → ℕ | (λ (i : fin2 n), f i v) ∈ S}

theorem dioph.dioph_fn_comp {α : Type} {n : ℕ} {f : vector3 ℕ n → ℕ} (df : dioph.dioph_fn f) (g : vector3 ((α → ℕ) → ℕ) n) (dg : vector_allp dioph.dioph_fn g) :

dioph.dioph_fn (λ (v : α → ℕ), f (λ (i : fin2 n), g i v))

theorem dioph.proj_dioph_of_nat {n : ℕ} (m : ℕ) [fin2.is_lt m n] :

dioph.dioph_fn (λ (v : vector3 ℕ n), v (fin2.of_nat' m))

theorem dioph.const_dioph {α : Type} (n : ℕ) :

dioph.dioph_fn (function.const (α → ℕ) n)

theorem dioph.dioph_comp2 {α : Type} {f g : (α → ℕ) → ℕ} (df : dioph.dioph_fn f) (dg : dioph.dioph_fn g) {S : ℕ → ℕ → Prop} (d : dioph (λ (v : vector3 ℕ 2), S (v (fin2.of_nat' 0)) (v (fin2.of_nat' 1)))) :

dioph (λ (v : α → ℕ), S (f v) (g v))

theorem dioph.dioph_fn_comp2 {α : Type} {f g : (α → ℕ) → ℕ} (df : dioph.dioph_fn f) (dg : dioph.dioph_fn g) {h : ℕ → ℕ → ℕ} (d : dioph.dioph_fn (λ (v : vector3 ℕ 2), h (v (fin2.of_nat' 0)) (v (fin2.of_nat' 1)))) :

dioph.dioph_fn (λ (v : α → ℕ), h (f v) (g v))

theorem dioph.eq_dioph {α : Type} {f g : (α → ℕ) → ℕ} (df : dioph.dioph_fn f) (dg : dioph.dioph_fn g) :

dioph (λ (v : α → ℕ), f v = g v)

theorem dioph.add_dioph {α : Type} {f g : (α → ℕ) → ℕ} (df : dioph.dioph_fn f) (dg : dioph.dioph_fn g) :

dioph.dioph_fn (λ (v : α → ℕ), f v + g v)

theorem dioph.mul_dioph {α : Type} {f g : (α → ℕ) → ℕ} (df : dioph.dioph_fn f) (dg : dioph.dioph_fn g) :

dioph.dioph_fn (λ (v : α → ℕ), f v * g v)

theorem dioph.le_dioph {α : Type} {f g : (α → ℕ) → ℕ} (df : dioph.dioph_fn f) (dg : dioph.dioph_fn g) :

dioph {v : α → ℕ | f v ≤ g v}

theorem dioph.lt_dioph {α : Type} {f g : (α → ℕ) → ℕ} (df : dioph.dioph_fn f) (dg : dioph.dioph_fn g) :

dioph {v : α → ℕ | f v < g v}

theorem dioph.ne_dioph {α : Type} {f g : (α → ℕ) → ℕ} (df : dioph.dioph_fn f) (dg : dioph.dioph_fn g) :

dioph {v : α → ℕ | f v ≠ g v}

theorem dioph.sub_dioph {α : Type} {f g : (α → ℕ) → ℕ} (df : dioph.dioph_fn f) (dg : dioph.dioph_fn g) :

dioph.dioph_fn (λ (v : α → ℕ), f v - g v)

theorem dioph.dvd_dioph {α : Type} {f g : (α → ℕ) → ℕ} (df : dioph.dioph_fn f) (dg : dioph.dioph_fn g) :

dioph (λ (v : α → ℕ), f v ∣ g v)

theorem dioph.mod_dioph {α : Type} {f g : (α → ℕ) → ℕ} (df : dioph.dioph_fn f) (dg : dioph.dioph_fn g) :

dioph.dioph_fn (λ (v : α → ℕ), f v % g v)

theorem dioph.modeq_dioph {α : Type} {f g : (α → ℕ) → ℕ} (df : dioph.dioph_fn f) (dg : dioph.dioph_fn g) {h : (α → ℕ) → ℕ} (dh : dioph.dioph_fn h) :

dioph (λ (v : α → ℕ), f v ≡ g v [MOD h v])

theorem dioph.div_dioph {α : Type} {f g : (α → ℕ) → ℕ} (df : dioph.dioph_fn f) (dg : dioph.dioph_fn g) :

dioph.dioph_fn (λ (v : α → ℕ), f v / g v)

theorem dioph.pell_dioph :

dioph (λ (v : vector3 ℕ 4), ∃ (h : 1 < v (fin2.of_nat' 0)), pell.xn h (v (fin2.of_nat' 1)) = v (fin2.of_nat' 2) ∧ pell.yn h (v (fin2.of_nat' 1)) = v (fin2.of_nat' 3))

theorem dioph.xn_dioph :

dioph.dioph_pfun (λ (v : vector3 ℕ 2), {dom := 1 < v (fin2.of_nat' 0), get := λ (h : 1 < v (fin2.of_nat' 0)), pell.xn h (v (fin2.of_nat' 1))})

theorem dioph.pow_dioph {α : Type} {f g : (α → ℕ) → ℕ} (df : dioph.dioph_fn f) (dg : dioph.dioph_fn g) :

dioph.dioph_fn (λ (v : α → ℕ), f v ^ g v)

A version of Matiyasevic's theorem