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
def vector3 (α : Type u) (n : ) :
Type u

Alternate definition of vector based on fin2.

Equations
def vector3.nil {α : Type u_1} :
vector3 α 0

The empty vector

def vector3.cons {α : Type u_1} {n : } (a : α) (v : vector3 α n) :

The vector cons operation

Equations
@[simp]
theorem vector3.cons_fz {α : Type u_1} {n : } (a : α) (v : vector3 α n) :
(a :: v) fin2.fz = a
@[simp]
theorem vector3.cons_fs {α : Type u_1} {n : } (a : α) (v : vector3 α n) (i : fin2 n) :
(a :: v) i.fs = v i
def vector3.nth {α : Type u_1} {n : } (i : fin2 n) (v : vector3 α n) :
α

Get the ith element of a vector

Equations
def vector3.of_fn {α : Type u_1} {n : } (f : fin2 n → α) :
vector3 α n

Construct a vector from a function on fin2.

Equations
def vector3.head {α : Type u_1} {n : } (v : vector3 α n.succ) :
α

Get the head of a nonempty vector.

Equations
def vector3.tail {α : Type u_1} {n : } (v : vector3 α n.succ) :
vector3 α n

Get the tail of a nonempty vector.

Equations
theorem vector3.eq_nil {α : Type u_1} (v : vector3 α 0) :
theorem vector3.cons_head_tail {α : Type u_1} {n : } (v : vector3 α n.succ) :
v.head :: v.tail = v
def vector3.nil_elim {α : Type u_1} {C : vector3 α 0Sort u} (H : C vector3.nil) (v : vector3 α 0) :
C v
Equations
def vector3.cons_elim {α : Type u_1} {n : } {C : vector3 α n.succSort u} (H : Π (a : α) (t : vector3 α n), C (a :: t)) (v : vector3 α n.succ) :
C v
Equations
@[simp]
theorem vector3.cons_elim_cons {α : Type u_1} {n : } {C : vector3 α n.succSort u_2} {H : Π (a : α) (t : vector3 α n), C (a :: t)} {a : α} {t : vector3 α n} :
vector3.cons_elim H (a :: t) = H a t
def vector3.rec_on {α : Type u_1} {C : Π {n : }, vector3 α nSort u} {n : } (v : vector3 α n) (H0 : C vector3.nil) (Hs : Π {n : } (a : α) (w : vector3 α n), C wC (a :: w)) :
C v
Equations
@[simp]
theorem vector3.rec_on_nil {α : Type u_1} {C : Π {n : }, vector3 α nSort u_2} {H0 : C vector3.nil} {Hs : Π {n : } (a : α) (w : vector3 α n), C wC (a :: w)} :
@[simp]
theorem vector3.rec_on_cons {α : Type u_1} {C : Π {n : }, vector3 α nSort u_2} {H0 : C vector3.nil} {Hs : Π {n : } (a : α) (w : vector3 α n), C wC (a :: w)} {n : } {a : α} {v : vector3 α n} :
(a :: v).rec_on H0 Hs = Hs a v (v.rec_on H0 Hs)
def vector3.append {α : Type u_1} {m : } (v : vector3 α m) {n : } (w : vector3 α n) :
vector3 α (n + m)

Append two vectors

Equations
@[simp]
theorem vector3.append_nil {α : Type u_1} {n : } (w : vector3 α n) :
@[simp]
theorem vector3.append_cons {α : Type u_1} (a : α) {m : } (v : vector3 α m) {n : } (w : vector3 α n) :
(a :: v).append w = a :: v.append w
@[simp]
theorem vector3.append_left {α : Type u_1} {m : } (i : fin2 m) (v : vector3 α m) {n : } (w : vector3 α n) :
v.append w (fin2.left n i) = v i
@[simp]
theorem vector3.append_add {α : Type u_1} {m : } (v : vector3 α m) {n : } (w : vector3 α n) (i : fin2 n) :
v.append w (i.add m) = w i
def vector3.insert {α : Type u_1} (a : α) {n : } (v : vector3 α n) (i : fin2 n.succ) :

Insert a into v at index i.

Equations
@[simp]
theorem vector3.insert_fz {α : Type u_1} (a : α) {n : } (v : vector3 α n) :
@[simp]
theorem vector3.insert_fs {α : Type u_1} (a : α) {n : } (b : α) (v : vector3 α n) (i : fin2 n.succ) :
theorem vector3.append_insert {α : Type u_1} (a : α) {k : } (t : vector3 α k) {n : } (v : vector3 α n) (i : fin2 n.succ) (e : n.succ + k = (n + k).succ) :
vector3.insert a (t.append v) (e.rec_on (i.add k)) = e.rec_on (t.append (vector3.insert a v i))
def vector_ex {α : Type u_1} (k : ) :
(vector3 α k → Prop) → Prop

"Curried" exists, i.e. ∃ x1 ... xn, f [x1, ..., xn]

Equations
def vector_all {α : Type u_1} (k : ) :
(vector3 α k → Prop) → Prop

"Curried" forall, i.e. ∀ x1 ... xn, f [x1, ..., xn]

Equations
theorem exists_vector_zero {α : Type u_1} (f : vector3 α 0 → Prop) :
theorem exists_vector_succ {α : Type u_1} {n : } (f : vector3 α n.succ → Prop) :
Exists f ∃ (x : α) (v : vector3 α n), f (x :: v)
theorem vector_ex_iff_exists {α : Type u_1} {n : } (f : vector3 α n → Prop) :
theorem vector_all_iff_forall {α : Type u_1} {n : } (f : vector3 α n → Prop) :
vector_all n f ∀ (v : vector3 α n), f v
def vector_allp {α : Type u_1} (p : α → Prop) {n : } (v : vector3 α n) :
Prop

vector_allp p v is equivalent to ∀ i, p (v i), but unfolds directly to a conjunction, i.e. vector_allp p [0, 1, 2] = p 0 ∧ p 1 ∧ p 2.

Equations
@[simp]
theorem vector_allp_nil {α : Type u_1} (p : α → Prop) :
@[simp]
theorem vector_allp_singleton {α : Type u_1} (p : α → Prop) (x : α) :
@[simp]
theorem vector_allp_cons {α : Type u_1} (p : α → Prop) {n : } (x : α) (v : vector3 α n) :
vector_allp p (x :: v) p x vector_allp p v
theorem vector_allp_iff_forall {α : Type u_1} (p : α → Prop) {n : } (v : vector3 α n) :
vector_allp p v ∀ (i : fin2 n), p (v i)
theorem vector_allp.imp {α : Type u_1} {p q : α → Prop} (h : ∀ (x : α), p xq x) {n : } {v : vector3 α n} (al : vector_allp p v) :
@[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} :
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 α → β) :
v none :: v some = v
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