Linear Algebra in Lean 4
Spring 2023
What is it?
This project is my final project for Professor Kurtz's Type Theory class.
For this project, we were tasked with forming groups and researching a proof-checking programming language. Then, with the language, we needed to write some proofs and present the language and our proofs to the class.
My group of 3 students chose to learn the language Lean 4, which is currently a Microsoft research project. We chose this language because it is very new and contains many modern features that give it a much better user experience than other older, more well-established proof assistants.
For a quick introduction to Lean 4, check out the file LinearAlgebra/Demo.lean in the GitHub repository linked below. For more comprehensive information, check out Microsoft's official website.
What did we implement?
Vector Spaces
We implemented Vector Spaces using type classes in LinearAlgebra/VectorSpace.lean.
Type classes are perfect for this purpose, as Vector Spaces are, by definition, a set of axioms that can be satisfied by any number of mathematical structures. Type classes allow you to define these axioms in a way that makes it easy to show that any given structure satisfies them.
Vectors
We implemented Vectors in 2 different ways: as nested pairs and as a list along with a proof of length. I worked on the nested pairs implementation and the other implementation is largely based on Microsoft's official math library's implementation, so I will only discuss the nested pairs implementation here.
Here is our implementation of Vectors as nested pairs, which is found in LinearAlgebra/Vec.lean:
def Vec (α : Type u) (n : ℕ₁) :=
match n with
| 1 => α
| k + 1 => α × (Vec α k)
By this definition, given a type a, a Vec a 1 is identical to the type a and a Vec a (k + 1) for a natural number k is a pair of a and a Vec a k.
This recursive definition ensures that a Vec a n is a nested pair type representing a grouping of exactly n elements of type a.
Functional Programming Vec Reductions
To make proofs with Vecs easier, we implemented many functional programming methods that, when used effectively, can drastically simplify proofs regarding Vecs. These simplifications are so impactful that they can reduce most proofs involving entrywise Vec operations to proofs that the operation works on a single term. For example, these functions can reduce a proof that entrywise Vec F n addition is commutative (F is a field and n is a natural number) to a proof that addition in the field F is commutative.
The functional programming methods we implemented include map, apply (based on <*> from the applicative type class from Haskell), zip_with, foldr, foldl, and replicate for creating Vecs. All of these function definitions are in the file LinearAlgebra/Vec.lean.
The most important of these functional programming methods are map, apply, and zip_with. This is because entrywise operations can be defined very naturally with zip_with, and zip_with is implemented in the backend by nested apply and map calls. Because of this, every proof involving entrywise operations can be reduced to simplifying a series of nested apply and map calls.
To help reduce nested apply and map calls, we created a bunch of theorems that allow you to simplify these calls into a simplest form we designed. The rules for this simplest form are as follows:
- Nested apply calls must be on the left input of the parent apply
- Map calls must always happen before apply calls (Ex: apply (map v) u)
- Map calls nested under apply calls must be on the left input of the apply
- Nested map calls should simplify to a single map call
- Each nested apply call should have a different Vec as its rightmost input
These reductions are so powerful that they can reduce many complex proofs into a single line! For example, consider this tactics-proof that Vec addition is associative:
theorem add_assoc {α : Type} [AddCommGroup α] {n : ℕ₁} (u v w : Vec α n) :
add_Vec u (add_Vec v w) = add_Vec (add_Vec u v) w := by
simp[entrywise_eq, AddSemigroup.add_assoc]
As you can see, a single simp tactic is sufficient to prove that Vec addition is associative! For more information on this proof and for a full series of absurdly short proofs that a Vec of fields is a Vector Space, check out the file LinearAlgebra/VecOperations.lean.
Also, for another example of how ridiculously broken these simplifications are and how broken the simp tactic can be, check out the #print command on the 3rd to last line of LinearAlgebra/Vec.lean (try it in VSCode, as you can only see the results there). This command showcases how a simple proof consisting of 5 simp tactics is internally represented by a crazily long proof that no one could possibly think of on their own!
Basis Vectors
The last things we proved are the fundamental theorems regarding the basis of a Vector Space.
The Basis of a Vector Space is mathematically defined as a set of elements of the Vector Space that satisfy the property that any element in the Vector Space can be represented via a unique linear combination of the elements in that set.
However, in most instances, Bases are defined through their Spanning and Linear Independent properties.
A Spanning Set is a set of elements of a Vector Space that satisfy the property that any element in the Vector Space can be represented by a (not necessarily unique) linear combination of the elements in that set.
A Linear Independent Set is a set of elements of a Vector Space that satisfies the property that the only way to represent the element 0 in the Vector Space through a linear combination of the elements of this set is by multiplying each element in the set by 0 in the field of the Vector Space and summing them together (the field coefficients of the linear combination are all 0)
In order to use these properties to define a Basis, it is necessary to prove that a set is a Basis of a Vector Space if and only if the set is a Linearly Independent Spanning Set of the Vector Space.
In the file LinearAlgebra/Basis.lean, we implemented all of these properties and proved the relationship between a Basis and Linear Independent Spanning sets. Here are our definitions of Basis, LinearIndependent, and Spanning:
namespace Basis
variable (𝔽 : Type) [Field 𝔽] (V : Type u) [AddCommGroup V] [VectorSpace 𝔽 V] {n : ℕ₁} (vs : Vec V n)
class Spanning where
span : ∀ (v : V), ∃ (factors : Vec 𝔽 n), accum vs factors = v
class Unique where
unique : ∀ (v : V), ∀ (factors₁ factors₂ : Vec 𝔽 n),
accum vs factors₁ = v ∧ accum vs factors₂ = v
→ factors₁ = factors₂
class LinearIndependent where
linear_independent : ∀ (factors : Vec 𝔽 n),
accum vs factors = 0 → factors = 0
end Basis
class Basis (𝔽 : Type) [Field 𝔽] (V : Type u) [AddCommGroup V] [VectorSpace 𝔽 V] {n : ℕ₁} (vs : Vec V n) extends Basis.Spanning 𝔽 V vs, Basis.Unique 𝔽 V vs
Resources
GitHub Repository: github.com/JSerf02/Lean_Linear_Algebra