2.2.1. Days of the Week (Enumerated Types)🔗

An inductive definition for an enumerated type:

A function on days:

Evaluation:

Day.monday

Day.tuesday

We can also record what we expect the result of calling a function to be in the form of a Lean example:

The rfl tactic is used to observe that both sides of an equal sign evaluate to the same value.

2.2.2. Aside: Using the VS Code Lean Extension🔗

2.2.3. Booleans🔗

Another familiar enumerated type; we'll switch to Lean's built-in Bool later:

This command opens the namespace associated with the MyBool type:

Functions over booleans can be defined in the same way as functions over days of the week.

Note the syntax for defining multi-argument functions (and and or).

Lean also allows us to define symbolic notations for these functions.

Going forward, most exercises will be omitted from the "terse" version of the notes used in lecture. The "full" version (used online and for homeworks) contains both longer explanations and all the exercises.

2.3.1. Aside: Unicode in Lean🔗

2.3.2. Types🔗

We can use #check to check the type of an expression:

Bool.true : Bool

true : Bool

!true : Bool

2.3.3. New Types from Old🔗

A more interesting type definition:

We can define functions on colors using pattern matching, just as we did for Day and MyBool.

We can use a wildcard pattern _ to match something we don't care about:

We can use a constant argument to Color.primary to match a specific primary color:

An alternative way to write the same function would be to explicitly nest match statements:

This isRed' function produces the same result as isRed. It also illustrates the use of a pattern variable in the corresponding branch.

2.3.4. Namespaces🔗

namespace declarations create separate namespaces.

myFoo : Bool

Playground.myFoo : RGB

Playground.myBar : RGB

The names of an inductive type's constructors are prefixed by the type's name.

Top-level definitions can also be prefixed by a namespace, which opens the namespace temporarily for the body of the definition.

RGB.myBlue : RGB

RGB.myOtherBlue : RGB

Unknown identifier `myBlue`

open brings definitions from a namespace into scope.

MyNamespace.myDef : Bool

If we only want to bring some, rather than all, of the definitions of a namespace into the current scope, we can use the open (...) form:

MyOtherNamespace.myVisibleDef : Bool

But myHiddenDef, which we did not include in the open, still needs to be qualified:

Unknown identifier `myHiddenDef`

Lean's prelude exports common names from the Bool namespace.

Bool.true : Bool

Bool.true : Bool

Lean can often use the expected type to resolve a name beginning with .:

Here, Lean can't figure out which version of .true we mean.

Invalid dotted identifier notation: The expected type of `.true` could not be determined

Hint: Using one of these would be unambiguous:
  [apply] `true`
  [apply] `MyBool.true`
  [apply] `Lake.Toml.true`
  [apply] `Lean.LBool.true`
  [apply] `Std.Do.ExceptConds.true`
  [apply] `Lean.Meta.Grind.Filter.true`

But in the following example, because Bool.not takes a Bool argument, Lean knows that .true must here be a Bool:

!true : Bool

2.3.5. Constructors with Multiple Parameters (Tuple Types)🔗

A Nibble is half a byte — four bits.

Nibble.bits Bit.b1 Bit.b0 Bit.b1 Bit.b0 : Nibble

We can deconstruct a Nibble by pattern matching.

{ x0 := Playground.Bit.b0, x1 := Playground.Bit.b0, x2 := Playground.Bit.b0, x3 := Playground.Bit.b0 } : NibbleStruct

2.3.6. Natural Numbers🔗

For simplicity in proofs, we choose a unary representation of natural numbers.

Eventually we'll swap to Lean's definition of natural numbers, which is very similar to this.

We can also write functions on Nat.

Look at the types of succ, pred, and minusTwo:

succ : Nat → Nat

pred : Nat → Nat

minusTwo : Nat → Nat

These are all things that can be applied to a number to yield a number. But there is a difference between succ and the other two.

Here are some recursive functions on natural numbers:

We could define odd by a similar recursive declaration, but here is a simpler way:

This function takes multiple parameters, recursing on the second:

NatPlayground.Nat.succ (NatPlayground.Nat.succ (NatPlayground.Nat.succ (NatPlayground.Nat.zero)))

We can also define infix notation for our add function.

NatPlayground.Nat.succ (NatPlayground.Nat.succ (NatPlayground.Nat.succ (NatPlayground.Nat.zero)))

2.4.1. Proving Properties about Functions in Lean🔗

We can prove properties of recursive functions like add:

NatPlayground.Nat.add_zero (n : Nat) : n + zero = n

Using our simplification rule add_zero, we can carry out a simple proof about natural numbers.

2.4.2. Proof State and Tactics🔗

Here is the previous proof in more detail:

Give this proof a try (it's similar):

2.4.3. The rewrite tactic🔗

2.4.4. The rfl tactic🔗

The rfl closes a goal that looks like a = a, reducing both sides of the equality in the process.

2.4.5. A New add Rule🔗

Here's another rule we can use for add:

Now, let's use add_succ in a proof:

2.4.6. Irreducibility, Rewriting, and Proof Engineering🔗

After proving the theorems that characterize a definition, we mark the definition irreducible to require rewriting by them instead of using rfl.

These simplification rules also follow a particular pattern. Let's look again at the definition of add, without the + notation for maximum clarity:

Each branch of a definition's control flow gets one simplification rule. Here are the two for pred:

Now that we have defined and proved pred's simplification rules, we can mark it irreducible to enforce rewriting by these lemmas.

Similarly, for each of the three branches of the definition of even, we need one simplification rule:

From here on, we pair each definition with its simplification rules and rewrite by those rules rather than rfl-ing through the definition.

2.4.7. Working with Numerals🔗

We know from our definitions above that one is just succ zero, two is succ one, and so on. We can write rules for these equalities too: