mathlib documentation

number_theory.dioph

Diophantine functions and Matiyasevic's theorem #

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 #

Main statements #

References #

Tags #

Matiyasevic's theorem, Hilbert's tenth problem

TODO #

theorem int.eq_nat_abs_iff_mul (x : ) (n : ) :
x.nat_abs = n (x - n) * (x + n) = 0
@[simp]
def list_all {α : Type u_1} (p : α → Prop) :
list α → Prop

list_all p l is equivalent to ∀ a ∈ l, p a, but unfolds directly to a conjunction, i.e. list_all p [0, 1, 2] = p 0 ∧ p 1 ∧ p 2.

Equations
@[simp]
theorem list_all_cons {α : Type u_1} (p : α → Prop) (x : α) (l : list α) :
list_all p (x :: l) p x list_all p l
theorem list_all_iff_forall {α : Type u_1} (p : α → Prop) (l : list α) :
list_all p l ∀ (x : α), x lp x
theorem list_all.imp {α : Type u_1} {p q : α → Prop} (h : ∀ (x : α), p xq x) {l : list α} :
list_all p llist_all q l
@[simp]
theorem list_all_map {α : Type u_1} {β : Type u_2} {p : β → Prop} (f : α → β) {l : list α} :
list_all p (list.map f l) list_all (p f) l
theorem list_all_congr {α : Type u_1} {p q : α → Prop} (h : ∀ (x : α), p x q x) {l : list α} :
@[instance]
def decidable_list_all {α : Type u_1} (p : α → Prop) [decidable_pred p] (l : list α) :
Equations
inductive is_poly {α : Sort u_1} :
((α → )) → Prop

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.)

def poly (α : Type u) :
Type u

The type of multivariate integer polynomials

Equations
@[instance]
def poly.has_coe_to_fun {α : Type u} :
has_coe_to_fun (poly α) (λ (_x : poly α), (α → ))
Equations
theorem poly.isp {α : Type u} (f : poly α) :

The underlying function of a poly is a polynomial

theorem poly.ext {α : Type u} {f g : poly α} (e : ∀ (x : α → ), f x = g x) :
f = g

Extensionality for poly α

def poly.subst {α : Type u} (f : poly α) (g : (α → )) (e : ∀ (x : α → ), f x = g x) :
poly α

Construct a poly given an extensionally equivalent poly.

Equations
@[simp]
theorem poly.subst_eval {α : Type u} (f : poly α) (g : (α → )) (e : ∀ (x : α → ), f x = g x) (x : α → ) :
(f.subst g e) x = g x
def poly.proj {α : Type u} (i : α) :
poly α

The ith projection function, x_i.

Equations
@[simp]
theorem poly.proj_eval {α : Type u} (i : α) (x : α → ) :
(poly.proj i) x = (x i)
def poly.const {α : Type u} (n : ) :
poly α

The constant function with value n : ℤ.

Equations
@[simp]
theorem poly.const_eval {α : Type u} (n : ) (x : α → ) :
def poly.zero {α : Type u} :
poly α

The zero polynomial

Equations
@[instance]
def poly.has_zero {α : Type u} :
Equations
@[simp]
theorem poly.zero_eval {α : Type u} (x : α → ) :
0 x = 0
def poly.one {α : Type u} :
poly α

The zero polynomial

Equations
@[instance]
def poly.has_one {α : Type u} :
Equations
@[simp]
theorem poly.one_eval {α : Type u} (x : α → ) :
1 x = 1
def poly.sub {α : Type u} :
poly αpoly αpoly α

Subtraction of polynomials

Equations
@[instance]
def poly.has_sub {α : Type u} :
Equations
@[simp]
theorem poly.sub_eval {α : Type u} (f g : poly α) (x : α → ) :
(f - g) x = f x - g x
def poly.neg {α : Type u} (f : poly α) :
poly α

Negation of a polynomial

Equations
@[instance]
def poly.has_neg {α : Type u} :
Equations
@[simp]
theorem poly.neg_eval {α : Type u} (f : poly α) (x : α → ) :
(-f) x = -f x
def poly.add {α : Type u} :
poly αpoly αpoly α

Addition of polynomials

Equations
@[instance]
def poly.has_add {α : Type u} :
Equations
@[simp]
theorem poly.add_eval {α : Type u} (f g : poly α) (x : α → ) :
(f + g) x = f x + g x
def poly.mul {α : Type u} :
poly αpoly αpoly α

Multiplication of polynomials

Equations
@[instance]
def poly.has_mul {α : Type u} :
Equations
@[simp]
theorem poly.mul_eval {α : Type u} (f g : poly α) (x : α → ) :
(f * g) x = (f x) * g x
theorem poly.induction {α : Type u} {C : poly α → Prop} (H1 : ∀ (i : α), C (poly.proj i)) (H2 : ∀ (n : ), C (poly.const n)) (H3 : ∀ (f g : poly α), C fC gC (f - g)) (H4 : ∀ (f g : poly α), C fC gC (f * g)) (f : poly α) :
C f
def poly.sumsq {α : Type u} :
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
theorem poly.sumsq_nonneg {α : Type u} (x : α → ) (l : list (poly α)) :
theorem poly.sumsq_eq_zero {α : Type u} (x : α → ) (l : list (poly α)) :
(poly.sumsq l) x = 0 list_all (λ (a : poly α), a x = 0) l
def poly.remap {α : Type u_1} {β : Type u_2} (f : α → β) (g : poly α) :
poly β

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

Equations
@[simp]
theorem poly.remap_eval {α : Type u_1} {β : Type u_2} (f : α → β) (g : poly α) (v : β → ) :
(poly.remap f g) v = g (v f)
def sum.join {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α → γ) (g : β → γ) :
α β → γ

combine two functions into a function on the disjoint union

Equations
def option.cons {α : Type u_1} {β : Sort u_2} (a : β) (v : α → β) :
option α → β

Functions from option can be combined similarly to vector.cons

Equations
  • a::v = option.rec a v
@[simp]
theorem option.cons_head_tail {α : Type u_1} {β : Sort u_2} (v : option α → β) :
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
theorem dioph.ext {α : Type u} {S S' : set (α → )} (d : dioph S) (H : ∀ (v : α → ), S v S' v) :
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) = some x) (p : poly β)) (v : α → ) :
(∃ (t : β → ), p (sum.join v t) = 0) ∃ (t : γ → ), (poly.remap (sum.join sum.inl (sum.inr f)) p) (sum.join v t) = 0
theorem dioph.inject_dummies {α β γ : Type u} {S : set (α → )} (f : β → γ) (g : γ → option β) (inv : ∀ (x : β), g (f x) = some x) (p : poly β)) (h : ∀ (v : α → ), S v ∃ (t : β → ), p (sum.join v t) = 0) :
∃ (q : poly γ)), ∀ (v : α → ), S v ∃ (t : γ → ), q (sum.join v t) = 0
theorem dioph.reindex_dioph {α β : Type u} {S : set (α → )} (d : dioph S) (f : α → β) :
dioph (λ (v : β → ), S (v f))
theorem dioph.dioph_list_all {α : Type u} (l : list (set (α → ))) (d : list_all dioph l) :
dioph (λ (v : α → ), list_all (λ (S : set (α → )), S v) l)
theorem dioph.and_dioph {α : Type u} {S S' : set (α → )} (d : dioph S) (d' : dioph S') :
dioph (λ (v : α → ), S v S' v)
theorem dioph.or_dioph {α : Type u} {S S' : set (α → )} (d : dioph S) (d' : dioph S') :
dioph (λ (v : α → ), S v S' v)
def dioph.dioph_pfun {α : Type u} (f : (α → ) →. ) :
Prop

A partial function is Diophantine if its graph is Diophantine.

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

A function is Diophantine if its graph is Diophantine.

Equations
theorem dioph.reindex_dioph_fn {α β : Type u} {f : (α → )} (d : dioph.dioph_fn f) (g : α → β) :
dioph.dioph_fn (λ (v : β → ), f (v g))
theorem dioph.ex_dioph {α β : Type u} {S : set β)} :
dioph Sdioph (λ (v : α → ), ∃ (x : β → ), S (sum.join v x))
theorem dioph.ex1_dioph {α : Type u} {S : set (option α)} :
dioph Sdioph (λ (v : α → ), ∃ (x : ), S (x::v))
theorem dioph.dom_dioph {α : Type u} {f : (α → ) →. } (d : dioph.dioph_pfun f) :
theorem dioph.dioph_fn_iff_pfun {α : Type u} (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), S (f.fn v h::v))
theorem dioph.dioph_fn_comp1 {α : Type u} {S : set (option α)} (d : dioph S) {f : (α → )} (df : dioph.dioph_fn f) :
dioph (λ (v : α → ), S (f v::v))
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), S (f v::v))
theorem dioph.vec_ex1_dioph (n : ) {S : set (vector3 n.succ)} (d : dioph S) :
dioph (λ (v : vector3 n), ∃ (x : ), S (x::v))
theorem dioph.dioph_fn_vec {n : } (f : vector3 n) :
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 : α → ), S (sum.join v (λ (i : fin2 n), f i v)))
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 : α → ), S (λ (i : fin2 n), f i v))
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] :
theorem dioph.const_dioph {α : Type} (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