An alternate definition of fin n defined as an inductive type instead of a subtype of nat. This is useful for its induction principle and different definitional equalities.
convert a fin2 into a nat
convert a nat into a fin2 if it is in range
i + k : fin2 (n + k) when i : fin2 n and k : ℕ
left k is the embedding fin2 n → fin2 (k + n)
insert_perm a is a permutation of fin2 n with the following properties:
remap_left f k : fin2 (m + k) → fin2 (n + k) applies the function f : fin2 m → fin2 n to inputs less than m, and leaves the right part on the right (that is, remap_left f k (m + i) = n + i).
This is a simple type class inference prover for proof obligations of the form m < n where m n : ℕ.
Use type class inference to infer the boundedness proof, so that we can directly convert a nat into a fin2 n. This supports notation like &1 : fin 3.
Alternate definition of vector based on fin2.
The empty vector
The vector cons operation
Get the ith element of a vector
Construct a vector from a function on fin2.
Get the head of a nonempty vector.
Get the tail of a nonempty vector.
Append two vectors
Insert a into v at index i.
"Curried" exists, i.e. ∃ x1 ... xn, f [x1, ..., xn]
"Curried" forall, i.e. ∀ x1 ... xn, f [x1, ..., xn]
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.
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.
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.)
The type of multivariate integer polynomials
The underlying function of a poly is a polynomial
Extensionality for poly α
Construct a poly given an extensionally equivalent poly.
The ith projection function, x_i.
The constant function with value n : ℤ.
The zero polynomial
The zero polynomial
Subtraction of polynomials
Negation of a polynomial
Addition of polynomials
Multiplication of polynomials
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.
Map the index set of variables, replacing x_i with x_(f i).
combine two functions into a function on the disjoint union
Functions from option can be combined similarly to vector.cons
A set S ⊆ ℕ^α is diophantine if there exists a polynomial on α ⊕ β such that v ∈ S iff there exists t : ℕ^β with p (v, t) = 0.
A partial function is Diophantine if its graph is Diophantine.
A function is Diophantine if its graph is Diophantine.