Define your own choices | Lean foundations

A structure is one shape with several fields. Sometimes a value is one of several choices instead: a lamp is off, warm or bright. An inductive type lists every choice:

inductive Mode where
  | off
  | warm
  | bright

Each choice is a constructor, and the type has no other values. Its full name is Mode.off; where Lean already expects a Mode you can write just .off.

A function on such a type gives one answer per constructor. This is called pattern matching:

def isOn : Mode → Bool
  | .off => false
  | .warm => true
  | .bright => true

Lean checks that every constructor is handled. Leave one out and the definition is rejected with Missing cases, so a forgotten case can never slip through. The pattern _ matches whatever the lines above it did not.

Worked example

inductive Door where
  | opened
  | closed

def toggle : Door → Door
  | .opened => .closed
  | .closed => .opened

example : toggle .opened = .closed := by
  rfl

Step through the proof1 / 2

At the start of the proof on line 9. Everything above ⊢ may be used; the line below it is what must be proved.

⊢toggle Door.opened = Door.closed

Two constructors, two lines. Your type has three constructors, so your function needs three lines.

Takeaway

An inductive type lists every possible choice. Pattern matching gives one answer per choice, and Lean checks that none is missing.

Practise on Problems

48. What comes before red Easy

Exercise 1 of 3

Define an inductive type Mode with constructors off, warm and bright. Define advance : Mode → Mode so that they cycle in that order: off, warm, bright, off.

Suggested steps

Declare all three Mode constructors
Give advance the type Mode → Mode
Write one line for every constructor

These marks only recognize text. Another correct proof may use different steps; Lean checks whether it works.

Exercise.lean

Loading editor…

These lines run underneath whatever you write. They are what decides the exercise, so your names and types have to match them.

example : advance Mode.off = Mode.warm := by rfl
example : advance Mode.warm = Mode.bright := by rfl
example : advance Mode.bright = Mode.off := by rfl

ReadyLn 1, Col 1Lean 4

Draft saved in this browser

Stuck?

Worked example

Knowledge check