Lean Seminar week 2

George McNinch

2026-09-22

This post contains some comments about the week 2 lecture of the Tufts seminar on "Formalization of math and Lean".

Lists (and other things) of a particular type.

Given a type α we pointed out that List α is the type with terms like [a,b,c] where a b c : α.

There were some questions of the form: "how would I get a list containing terms of differing types?". I scribbled an answer on the board, but let me reiterate this and provide another alternative as well.

solution one: use Sum

(In the lecture, I said to use the Haskell name Either, but as it turns out, Lean actually uses the name Sum.)

Given types α β : Type, the new type Sum α β (or you can write α ⊕ β) has two constructors: Sum.inl : α → Sum α β and Sum.inr : β → Sum α β.

So a list with natural numbers and strings might look like this:
example : List (String ⊕ ℕ) := [ Sum.inr 1, Sum.inr 23, Sum.inl "potato" ]
solution two: define your own inductive type.
inductive MyType | N : ℕ → MyType | S : String → MyType | R : ℚ → MyType deriving Repr
This type has constructors N, S, and R. Using it, you can make a list containing natural numbers, strings, and rationals:
open MyType def l : List MyType := [ N 1, S "potato", R (1/2), N 23 ] [MyType.N 1, MyType.S "potato", MyType.R (1 : Rat)/2, MyType.N 23]#eval l
```
[MyType.N 1, MyType.S "potato", MyType.R (1 : Rat)/2, MyType.N 23]
```

Like List, Set depends on a type: Set α is sets of things of type α. So the "one type per collection" constraint applies here too.

Writing the set {1, 2, "potato"} fails for the same reason [1, 2, "potato"] does, and the fixes are the same: use Set (String ⊕ ℕ) or your own inductive type.

Here is one way that Set α differs from List α, though:

example : ¬ ([1,2,3] : List ℕ) = ([1,2,3,3] : List ℕ) := by⊢ ¬[1, 2, 3] = [1, 2, 3, 3] decideAll goals completed! 🐙

-- sets defined by listing elements aren't affected by repetition
example : ({1,2,3} : Set ℕ) = ({1,2,3,3} : Set ℕ) := by⊢ {1, 2, 3} = {1, 2, 3, 3} 
  ext xhx:ℕ⊢ x ∈ {1, 2, 3} ↔ x ∈ {1, 2, 3, 3} -- sets are equal iff they have the same elements
  simpAll goals completed! 🐙

Using names in binders

In the lecture, I had originally written

theorem modus_ponens {p q : Prop} : (f : p → q) → (h : p)  → q := byp:Propq:Prop⊢ (p → q) → p → q
  intro f hp:Propq:Propf:p → qh:p⊢ q
  exact f hAll goals completed! 🐙

The signature of a definition or theorem says what it takes as input and what it produces: it lists the arguments, each with its type, and the type of the result. For a theorem, the arguments are the hypotheses and the result type is the statement being proved.

The type of modus_ponens as stated is

(f : p → q) → (h : p)  → q

But in this case, there is no real reason for introducing names for the terms in the signature. Thus, we could have written

theorem modus_ponens_shorter {p q : Prop} : (p → q) → p  → q := byp:Propq:Prop⊢ (p → q) → p → q
  intro f hp:Propq:Propf:p → qh:p⊢ q
  exact f hAll goals completed! 🐙

Note that sometimes it is useful to give binders in the signature. In the following example, List.Vector α n is the type of vectors of length n with entries of type α:

open List.Vector in
def rept {α : Type} : α  → (n : ℕ) → List.Vector α n := byα:Type⊢ α → (n : ℕ) → List.Vector α n
  intro a nα:Typea:αn:ℕ⊢ List.Vector α n
  match n with 
  | 0 =>α:Typea:αn:ℕ⊢ List.Vector α 0 exact nilAll goals completed! 🐙
  | Nat.succ n =>α:Typea:αn✝:ℕn:ℕ⊢ List.Vector α n.succ exact cons a (rept a n)All goals completed! 🐙

rept "aaa" 4 : List.Vector String 4#check rept "aaa" 4 -- List.Vector String 4
["aaa", "aaa", "aaa", "aaa"]#eval rept "aaa" 4

["aaa", "aaa", "aaa", "aaa"]

rept [1, 2] 3 : List.Vector (List ℕ) 3#check rept [1,2] 3 -- List.Vector (List ℕ) 3
[[1, 2], [1, 2], [1, 2]]#eval rept [1,2] 3

[[1, 2], [1, 2], [1, 2]]

Here in the definition of rept we needed to name the natural number argument (in this case, n : ℕ) in the signature, because it is used later in the signature (List.Vector α n).