Enumerated Types

The simplest kind of inductive type is simply a type with a finite, enumerated list of elements. The following command declares the enumerated type Weekday.

inductive Weekday where
  | sunday    : Weekday
  | monday    : Weekday
  | tuesday   : Weekday
  | wednesday : Weekday
  | thursday  : Weekday
  | friday    : Weekday
  | saturday  : Weekday

The Weekday type has 7 constructors/elements. The constructors live in the Weekday namespace Think of sunday, monday, …, saturday as being distinct elements of Weekday, with no other distinguishing properties.

# inductive Weekday where
#  | sunday    : Weekday
#  | monday    : Weekday
#  | tuesday   : Weekday
#  | wednesday : Weekday
#  | thursday  : Weekday
#  | friday    : Weekday
#  | saturday  : Weekday
#check Weekday.sunday   -- Weekday
#check Weekday.monday   -- Weekday

You can define functions by pattern matching. The following function converts a Weekday into a natural number.

# inductive Weekday where
#  | sunday    : Weekday
#  | monday    : Weekday
#  | tuesday   : Weekday
#  | wednesday : Weekday
#  | thursday  : Weekday
#  | friday    : Weekday
#  | saturday  : Weekday
def natOfWeekday (d : Weekday) : Nat :=
  match d with
  | Weekday.sunday    => 1
  | Weekday.monday    => 2
  | Weekday.tuesday   => 3
  | Weekday.wednesday => 4
  | Weekday.thursday  => 5
  | Weekday.friday    => 6
  | Weekday.saturday  => 7

#eval natOfWeekday Weekday.tuesday -- 3

It is often useful to group definitions related to a type in a namespace with the same name. For example, we can put the function above into the Weekday namespace. We are then allowed to use the shorter name when we open the namespace.

In the following example, we define functions from Weekday to Weekday in the namespace Weekday.

# inductive Weekday where
#  | sunday    : Weekday
#  | monday    : Weekday
#  | tuesday   : Weekday
#  | wednesday : Weekday
#  | thursday  : Weekday
#  | friday    : Weekday
#  | saturday  : Weekday
namespace Weekday

def next (d : Weekday) : Weekday :=
  match d with
  | sunday    => monday
  | monday    => tuesday
  | tuesday   => wednesday
  | wednesday => thursday
  | thursday  => friday
  | friday    => saturday
  | saturday  => sunday

end Weekday

It is so common to start a definition with a match in Lean, that Lean provides a syntax sugar for it.

# inductive Weekday where
#  | sunday    : Weekday
#  | monday    : Weekday
#  | tuesday   : Weekday
#  | wednesday : Weekday
#  | thursday  : Weekday
#  | friday    : Weekday
#  | saturday  : Weekday
# namespace Weekday
def previous : Weekday -> Weekday
  | sunday    => saturday
  | monday    => sunday
  | tuesday   => monday
  | wednesday => tuesday
  | thursday  => wednesday
  | friday    => thursday
  | saturday  => friday
# end Weekday

We can use the command #eval to test our definitions.

# inductive Weekday where
#  | sunday    : Weekday
#  | monday    : Weekday
#  | tuesday   : Weekday
#  | wednesday : Weekday
#  | thursday  : Weekday
#  | friday    : Weekday
#  | saturday  : Weekday
# namespace Weekday
# def next (d : Weekday) : Weekday :=
#  match d with
#  | sunday    => monday
#  | monday    => tuesday
#  | tuesday   => wednesday
#  | wednesday => thursday
#  | thursday  => friday
#  | friday    => saturday
#  | saturday  => sunday
# def previous : Weekday -> Weekday
#  | sunday    => saturday
#  | monday    => sunday
#  | tuesday   => monday
#  | wednesday => tuesday
#  | thursday  => wednesday
#  | friday    => thursday
#  | saturday  => friday
def toString : Weekday -> String
  | sunday    => "Sunday"
  | monday    => "Monday"
  | tuesday   => "Tuesday"
  | wednesday => "Wednesday"
  | thursday  => "Thursday"
  | friday    => "Friday"
  | saturday  => "Saturday"

#eval toString (next sunday)             -- "Monday"
#eval toString (next tuesday)            -- "Wednesday"
#eval toString (previous wednesday)      -- "Tuesday"
#eval toString (next (previous sunday))  -- "Sunday"
#eval toString (next (previous monday))  -- "Monday"
-- ..
# end Weekday

We can now prove the general theorem that next (previous d) = d for any weekday d. The idea is to perform a proof by cases using match, and rely on the fact for each constructor both sides of the equality reduce to the same term.

# inductive Weekday where
#  | sunday    : Weekday
#  | monday    : Weekday
#  | tuesday   : Weekday
#  | wednesday : Weekday
#  | thursday  : Weekday
#  | friday    : Weekday
#  | saturday  : Weekday
# namespace Weekday
# def next (d : Weekday) : Weekday :=
#  match d with
#  | sunday    => monday
#  | monday    => tuesday
#  | tuesday   => wednesday
#  | wednesday => thursday
#  | thursday  => friday
#  | friday    => saturday
#  | saturday  => sunday
# def previous : Weekday -> Weekday
#  | sunday    => saturday
#  | monday    => sunday
#  | tuesday   => monday
#  | wednesday => tuesday
#  | thursday  => wednesday
#  | friday    => thursday
#  | saturday  => friday
theorem nextOfPrevious (d : Weekday) : next (previous d) = d :=
  match d with
  | sunday    => rfl
  | monday    => rfl
  | tuesday   => rfl
  | wednesday => rfl
  | thursday  => rfl
  | friday    => rfl
  | saturday  => rfl
# end Weekday