Seminar 10 – Structures

Structures

In Lean, structures can hold a collection of data, just like structures in programming languages like C. Lean structures can also contain proofs. For example, consider the following structure

  structure EvenNumber where
  val : ℕ
  is_even : ∃ k : ℕ, val = 2 * k

To define an instance of this structure, we should give the natural number val and a proof that it is even. For example, with the following code:

def two_even : EvenNumber where
  val := 2
  is_even := by
    use 1

Lean will convert this to a tuple ⟨val, is_even⟩. As the proposition is_even has an existential quantifier, its terms are tuples, too. The first element is the natural number k, and the second term is a proof that val = 2*k. Hence, we can also define two_even with the following code:

def two_even : EvenNumber := ⟨2, ⟨1, rfl⟩⟩

The annotation @[ext] states that two instances are equal if their entries are equal.

Next week

Before starting with a quantum-related Lean project, we still need to cover chapters 8, 9 and 10. Next week, we will finish chapter 7 (structures) and continue with chapter 8 about hierarchies.