11. Typeclasses🔗

Chapter Poly introduced parametric polymorphism, declaring a type variable with no constraint on it.

This lets us work with a type like List α, writing functions like List.reverse and List.length and proofs like List.length_reverse, which use only the list's structure and never inspect any particular a : α.

Sometimes, though, we want less freedom: rather than leaving α completely generic, we want to partially specify its behavior. In Lean, this is done through a form of "ad hoc polymorphism" called typeclasses. The concept originated in Haskell and is analogous to features you may know from other languages, such as traits in Rust.

11.1. Why We Need Typeclasses🔗

Consider the following function, which checks whether a natural number occurs in a list:

def List.elemNat (n : Nat) (ms : List Nat) : Bool :=
  match ms with
  | [] => false
  | m :: ms' => bif n == m then true else elemNat n ms'

theorem List.elem_nat_nil (n : Nat) : [].elemNat n = false := byn:Nat⊢ elemNat n [] = false rflAll goals completed! 🐙

theorem List.elem_nat_cons (n m : Nat) (ms : List Nat) :
    (m :: ms).elemNat n = bif n == m then true else elemNat n ms := byn:Natm:Natms:List Nat⊢ elemNat n (m :: ms) = bif n == m then true else elemNat n ms rflAll goals completed! 🐙

true#eval [0, 1].elemNat 0
true#eval [0, 1].elemNat 1
false#eval [0, 1].elemNat 2

What if we want this to work for lists of any element type, not just Nat? Parametric polymorphism suggests simply replacing Nat with a type variable α, but that produces a puzzling error:

def List.elemPoly {α : Type} (x : α) (ys : List α) : Bool :=
  match ys with
  | [] => false
  | y :: ys' => bif failed to synthesize instance of type class
  BEq α

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.x == y then true else elemPoly x ys'

failed to synthesize instance of type class
  BEq α

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

Lean is trying to use typeclasses to work out how == should behave on a value of type α. We'll see exactly why shortly; for now, here's one way to sidestep the problem: have the caller supply the equality test to use.

def List.elemPolyEq {α : Type} (eq : α → α → Bool) (x : α) (ys : List α) : Bool :=
  match ys with
  | [] => false
  | y :: ys' => bif eq x y then true else elemPolyEq eq x ys'

true#eval [0, 1].elemPolyEq Nat.beq 0

This works, but it's tedious: every caller has to know, and remember to supply, the right equality function.

Typeclasses automate this — instead of the programmer passing the function explicitly, Lean searches for one and provides it on its own. We specify something we want Lean to search for by declaring a class with the needed function as a field; a class is like an interface in Java or a trait in Rust. Particular implementations of that class are called instances; each type can have its own instance of a class. For functions that would use such instances, we specify the name of the class in an instance implicit on the polymorphic variable that the instance's function applies to. This directs Lean to rely on the class inside the function, and to find and fill in the appropriate instance when the function is called.

Here is what this looks like for List.elemPoly:

def List.elemPoly {α : Type} [BEq α] (x : α) (ys : List α) : Bool :=
  match ys with
  | [] => false
  | y :: ys' => bif x == y then true else elemPoly x ys'

theorem List.elemPoly_nil {α : Type} [BEq α] (x : α) : [].elemPoly x = false := byα:Typeinst✝:BEq αx:α⊢ elemPoly x [] = false rflAll goals completed! 🐙

theorem List.elemPoly_cons {α : Type} [BEq α] (x y : α) (ys : List α) :
    (y :: ys).elemPoly x = bif x == y then true else elemPoly x ys := byα:Typeinst✝:BEq αx:αy:αys:List α⊢ elemPoly x (y :: ys) = bif x == y then true else elemPoly x ys rflAll goals completed! 🐙

true#eval [0, 1].elemPoly 0

Comparing List.elemPolyEq with List.elemPoly, we see three differences. First, List.elemPolyEq takes an explicit parameter eq, whereas List.elemPoly specifies an instance implicit [BEq α]. The instance implicit indicates that an instance of BEq must be provided at call sites for the particular type α that is used. Second, whereas List.elemPolyEq invokes the parameter eq to test equality, List.elemPoly uses == instead. As Lists noted when we first used it, == on Nat comes from the BEq typeclass. Finally, whereas [0, 1].elemPolyEq Nat.beq 0 passes the equality function Nat.beq explicitly, in [0, 1].elemPoly 0 Lean fills it in automatically based on the type Nat of the List. (It's tempting to assume Lean fills in Nat.beq itself here — it doesn't; we'll see exactly which BEq instance it finds, and why, in "Deciding Propositions" later in this chapter.)

Going back to the earlier version of List.elemPoly, without the instance implicit, we can now understand the error message: α was fully generic, so the == in its body would have needed to work for every type α, and no single BEq instance can do that. So Lean's search failed.

Now it is time to dig into the details of what we have seen so far. We'll see exactly how [BEq α] gets filled in below, starting with how to define a typeclass in the first place.

11.2. Defining Your Own Typeclasses🔗

BEq comes from Lean's standard library. Let's define a typeclass of our own, to see the mechanism — classes, instances, and synthesis — that made == resolve automatically above.

Suppose we want a function that returns the first element of a list, defaulting to a given value if the list is empty. As with List.elemPolyEq above, here is a version that makes the default value an explicit parameter:

def List.headOrEx {α : Type} (defaultValue : α) (xs : List α) : α :=
  match xs with
  | [] => defaultValue
  | x :: _ => x

1#eval [1, 2, 3].headOrEx 0
0#eval ([] : List Nat).headOrEx 0

This works, but again it's tedious: every caller has to supply an element of α to default to, even when there's an obvious choice based on the type of the things in the list, like 0 for Nat.

Getting Lean to fill in defaultValue automatically takes two things. One is marking the parameter as "searchable," rather than something the caller always supplies explicitly. The other is giving Lean some information about what it should search for.

Considering the second problem first: the way to provide this information is to name the data we're after — the default value of a type. In particular, a structure (chapter Lists) is a good way to give this information a name; structures can also bundle together more than one piece of data, which will come in handy later, though we only need a single field here.

To address the first problem, we need to mark this particular structure as one Lean should search for automatically — not every structure-typed argument should be.

Let's build up to what we want in two steps: first the naming, as a plain structure; then the marking, by upgrading it to a class. Here's the structure — we'll put it in its own namespace so we can reuse the name DefaultValue for the class version below:

namespace DefaultValueScratch

structure DefaultValue (α : Type) where
  value : α

A value of type DefaultValue Nat picks out a particular Nat to serve as the type's default: it's built the same way any structure is, by supplying a Nat for the value field:

def natDefault : DefaultValue Nat where
  value := 0

Naming the data this way already lets us take a step toward what we want: a version of List.headOrEx can take a DefaultValue α argument instead of a raw α, with callers supplying a value like natDefault instead of a bare Nat:

def List.headOrEx {α : Type} (defaultValue : DefaultValue α) (xs : List α) : α :=
  match xs with
  | [] => defaultValue.value
  | x :: _ => x

end DefaultValueScratch

This is more verbose than before — callers must build a DefaultValue value first — but it has the right shape: all that's left is marking DefaultValue as searchable, so Lean can supply this argument itself. How do we do that? We need to tell Lean that DefaultValue is the sort of structure it should search for automatically. We do this by writing class in place of structure:

class DefaultValue (α : Type) where
  value : α

We then provide values of this type a bit differently. Instead of def, we use instance:

instance instDefaultValueNat : DefaultValue Nat where
  value := 0

Lean can now find this instance on its own, via typeclass synthesis (or typeclass inference) — the same process that found BEq Nat earlier. That means we can rewrite List.headOrEx the same way we rewrote List.elemPolyEq into List.elemPoly above, replacing the explicit defaultValue parameter with an instance implicit:

def List.headOr {α : Type} [DefaultValue α] (xs : List α) : α :=
  match xs with
  | [] => DefaultValue.value
  | x :: _ => x

1#eval [1, 2, 3].headOr
0#eval ([] : List Nat).headOr

example : DefaultValue.value = (0 : Nat) := by⊢ DefaultValue.value = 0 rflAll goals completed! 🐙

Notice that we refer to DefaultValue.value alone, with no instance named. Because the expression equates DefaultValue.value with the Nat 0, Lean selects instDefaultValueNat, the instance for DefaultValue Nat. We know this because we are able to prove that DefaultValue.value is equal to 0.

Let's declare a second instance, for Int, the type of integers ... -2, -1, 0, 1, 2, ...:

instance instDefaultValueInt : DefaultValue Int where
  value := -1

We can also create instances for polymorphic types, like Option α, whose default is none, by giving the instance declaration a parameter:

instance instDefaultValueOption {α : Type} : DefaultValue (Option α) where
  value := none

Now, Lean can infer instances for all these types, including inside List.headOr:

example : DefaultValue.value = (0 : Nat) := by⊢ DefaultValue.value = 0 rflAll goals completed! 🐙
example : DefaultValue.value = (-1 : Int) := by⊢ DefaultValue.value = -1 rflAll goals completed! 🐙
example : DefaultValue.value = (none : Option Bool) := by⊢ DefaultValue.value = none rflAll goals completed! 🐙
example : DefaultValue.value = (none : Option (List Nat)) := by⊢ DefaultValue.value = none rflAll goals completed! 🐙
example : ([] : List Nat).headOr = 0 := by⊢ [].headOr = 0 rflAll goals completed! 🐙
example : ([] : List Int).headOr = -1 := by⊢ [].headOr = -1 rflAll goals completed! 🐙
example : ([] : List (Option Bool)).headOr = none := by⊢ [].headOr = none rflAll goals completed! 🐙
example : ([] : List (Option Bool)).headOr = none := by⊢ [].headOr = none rflAll goals completed! 🐙

Synthesis infers instances we could have specified explicitly:

example : instDefaultValueNat.value = (0 : Nat) := by⊢ DefaultValue.value = 0 rflAll goals completed! 🐙
example : instDefaultValueInt.value = (-1 : Int) := by⊢ DefaultValue.value = -1 rflAll goals completed! 🐙
example : instDefaultValueOption.value = (none : Option Nat) := by⊢ DefaultValue.value = none rflAll goals completed! 🐙

The option pp.all shows which instance Lean picked:

set_option pp.all true in
@DefaultValue.value Nat instDefaultValueNat : Nat#check (DefaultValue.value : Nat)

@DefaultValue.value Nat instDefaultValueNat : Nat

set_option pp.all true in
@DefaultValue.value Int instDefaultValueInt : Int#check (DefaultValue.value : Int)

@DefaultValue.value Int instDefaultValueInt : Int

This reveals instDefaultValueNat and instDefaultValueInt as the instances Lean picked. The #synth command runs the same search directly:

instDefaultValueNat#synth DefaultValue Nat

instDefaultValueNat

For a typeclass like DefaultValue that carries data — a term, such as the 0 above, rather than only proofs (which we will see below) — we expect at most one instance per type, so this search has a unique answer.

We'll put DefaultValue's standard-library equivalent, Inhabited, to work later in this chapter, when we define maps that need a default value for a generic type. First, though, let's go back to List.elemPoly and see how its [BEq α] argument actually gets resolved.

11.3. Using Typeclasses🔗

Let's check what == meant for List.elemNat, with notation display turned off:

set_option pp.notation false in
BEq.beq 1 2 : Bool#check 1 == 2

BEq.beq 1 2 : Bool

Rather than Nat.beq, == turns out to be notation for BEq.beq, a field of exactly the kind of typeclass we just learned to define:

class BEq (α : Type) where
    beq : α → α → Bool

Writing x == y makes Lean search for an instance of BEq for the type of x and y, the same way it searched for a DefaultValue instance above. Here is one way to define such an instance for Nat:

instance (priority := low) instNatbeq : BEq Nat where
  beq := Nat.beq

This instance is given low priority so that it doesn't override the standard library's own BEq Nat instance — which, as we'll see later in this chapter, is actually derived from Nat's decidable equality rather than from Nat.beq directly. Declaring it here just illustrates what a hand-written BEq instance looks like, the same way instDefaultValueNat illustrated a hand-written DefaultValue instance earlier.

If you prefer a specific instance you can provide it explicitly, by using @ to make the instance argument explicit. Here we provide our instNatbeq instance specifically.

true#eval @List.elemPoly Nat instNatbeq 1 [1,2,3]

Exercise★(List.elem_poly_eq_elem_nat)

Prove that List.elemPoly agrees with List.elemNat when specialized to natural numbers.

theorem declaration uses `sorry`List.elemPoly_eq_elemNat (ms : List Nat) (n : Nat) : ms.elemPoly n = ms.elemNat n := byms:List Natn:Nat⊢ elemPoly n ms = elemNat n ms
  sorryAll goals completed! 🐙

11.4. Proof-Carrying Typeclasses🔗

The above examples enforce no conditions on the data an instance may carry — any value of the right type will do. But sometimes enforcing constraints on data is useful. For example, suppose we want to specify that a type has not just a single element, but two. Here is a first attempt:

class HasTwoIncomplete (α : Type) where
  one : α
  two : α

Unfortunately, this specification isn't precise because it allows one and two to refer to the same term. Fortunately, Lean's typeclasses can carry proofs along with data, so we can write the following to enforce that one and two are distinct.

class HasTwo (α : Type) where
  one : α
  two : α
  one_neq_two : one ≠ two

Declaring instances works in much the same way as before, except that now the HasTwo.one_neq_two field requires a proof:

instance : HasTwo Nat where
  one := 1
  two := 2
  one_neq_two := by⊢ 1 ≠ 2 liaAll goals completed! 🐙

In most languages that support typeclasses (or traits), it is not possible to formally enforce laws such as one_neq_two. Thus it falls to the author to check, informally, that any required invariants are satisfied, which can lead to bugs.

Exercise★(HasThree) (Manually graded)

Following the pattern of DefaultValue and HasTwo, define a class HasThree that specifies a type with at least three distinct elements, and give an instance of it for Nat.

class HasThree (α : Type) where
  one : α
  two : α
  three : α
  one_neq_two : one ≠ two
  --  FILL IN HERE

declaration uses `sorry`instance : HasThree Nat where
  one := 1
  two := 2
  three := 3
  one_neq_two := sorry
  --  FILL IN HERE

namespace Algebra

This facility is very powerful, and is used extensively in Lean to define mathematical structures that carry both operators and laws about how those operators interact. As a simple example, let's use a typeclass to define a monoid, a simple algebraic structure that includes four things:

an underlying set of data, represented by a type α,
an operator (which we'll write ⊗, typed \otimes) that combines two elements of type α into one,
a particular element id of type α, which we call the "identity element," and
some laws about the interaction of ⊗ and id, namely that:
- ∀ x, id ⊗ x = x = x ⊗ id, and
- ∀ x y z, x ⊗ (y ⊗ z) = (x ⊗ y) ⊗ z (i.e., that ⊗ is associative)

We can express these requirements in the form of a typeclass:

-- first we define a notation typeclass for our operator ⊗
class OpSet (α : Type) where
  op : α → α → α

infixr:70 " ⊗ " => OpSet.op

class Monoid (α : Type) extends (OpSet α) where
  id : α
  left_id  (x : α)  : id ⊗ x = x
  right_id (x : α)  : x ⊗ id = x
  assoc (x y z : α) : x ⊗ (y ⊗ z) = (x ⊗ y) ⊗ z

The extends keyword indicates that the Monoid typeclass extends the OpSet typeclass, which just defines a set with an operator and some notation for it. The Monoid typeclass "inherits" the fields of OpSet, similar to how a class would in an object-oriented language.

As one might expect, the + operator over Nats forms a monoid, where 0 is the identity element. Note that we don't have to define Nat's OpSet instance separately; we can define a single instance that implements both classes.

instance : Monoid Nat where
  op := Nat.add
  id := 0
  left_id := by⊢ ∀ (x : Nat), Nat.add 0 x = x liaAll goals completed! 🐙
  right_id := by⊢ ∀ (x : Nat), x.add 0 = x liaAll goals completed! 🐙
  assoc := by⊢ ∀ (x y z : Nat), x.add (y.add z) = (x.add y).add z liaAll goals completed! 🐙

Exercise★(NatMonoidMul) (Manually graded)

However, multiplication on Nats also forms a monoid. What is its identity element?

declaration uses `sorry`instance : Monoid Nat where
  op := Nat.mul
  id := sorry
  left_id := sorry
  right_id := sorry
  assoc := sorry

Exercise★(ListMonoidAppend) (Manually graded)

There are also many monoids over other types. Most usefully in computer science, lists of any type also form a monoid, with List.append as the operator in question:

declaration uses `sorry`instance {α : Type} : Monoid (List α) where
  op := List.append
  id := sorry
  left_id := sorry
  right_id := sorry
  assoc := sorry

In addition to defining instances of Monoid, we can also prove some properties about monoids in general, just based on the laws defined on the typeclass. One simple theorem about monoids is that the identity element of a monoid is unique. That is, if we have two monoids over the same set with the same operator, their identity elements must also be the same:

theorem id_unique {α : Type} {m₁ m₂ : Monoid α} (h : m₁.op = m₂.op) :
  m₁.id = m₂.id := byα:Typem₁:Monoid αm₂:Monoid αh:OpSet.op = OpSet.op⊢ Monoid.id = Monoid.id
    obtain @⟨op₁, id₁, left_id₁, right_id₁, assoc₁⟩ := m₁α:Typem₂:Monoid αop₁:OpSet αid₁:αleft_id₁:∀ (x : α), id₁ ⊗ x = xright_id₁:∀ (x : α), x ⊗ id₁ = xassoc₁:∀ (x y z : α), x ⊗ y ⊗ z = (x ⊗ y) ⊗ zh:OpSet.op = OpSet.op⊢ Monoid.id = Monoid.id
    obtain @⟨op₂, id₂, left_id₂, right_id₂, assoc₂⟩ := m₂α:Typeop₁:OpSet αid₁:αleft_id₁:∀ (x : α), id₁ ⊗ x = xright_id₁:∀ (x : α), x ⊗ id₁ = xassoc₁:∀ (x y z : α), x ⊗ y ⊗ z = (x ⊗ y) ⊗ zop₂:OpSet αid₂:αleft_id₂:∀ (x : α), id₂ ⊗ x = xright_id₂:∀ (x : α), x ⊗ id₂ = xassoc₂:∀ (x y z : α), x ⊗ y ⊗ z = (x ⊗ y) ⊗ zh:OpSet.op = OpSet.op⊢ Monoid.id = Monoid.id
    have h' : id₁ = id₂ := by
      -- this introduces a use of m₁'s operator
      rw [← left_id₁ id₂α:Typeop₁:OpSet αid₁:αleft_id₁:∀ (x : α), id₁ ⊗ x = xright_id₁:∀ (x : α), x ⊗ id₁ = xassoc₁:∀ (x y z : α), x ⊗ y ⊗ z = (x ⊗ y) ⊗ zop₂:OpSet αid₂:αleft_id₂:∀ (x : α), id₂ ⊗ x = xright_id₂:∀ (x : α), x ⊗ id₂ = xassoc₂:∀ (x y z : α), x ⊗ y ⊗ z = (x ⊗ y) ⊗ zh:OpSet.op = OpSet.op⊢ id₁ = id₁ ⊗ id₂]α:Typeop₁:OpSet αid₁:αleft_id₁:∀ (x : α), id₁ ⊗ x = xright_id₁:∀ (x : α), x ⊗ id₁ = xassoc₁:∀ (x y z : α), x ⊗ y ⊗ z = (x ⊗ y) ⊗ zop₂:OpSet αid₂:αleft_id₂:∀ (x : α), id₂ ⊗ x = xright_id₂:∀ (x : α), x ⊗ id₂ = xassoc₂:∀ (x y z : α), x ⊗ y ⊗ z = (x ⊗ y) ⊗ zh:OpSet.op = OpSet.op⊢ id₁ = id₁ ⊗ id₂
      -- we use our hypothesis to rewrite m₁'s operator into m₂'s
      rw [hα:Typeop₁:OpSet αid₁:αleft_id₁:∀ (x : α), id₁ ⊗ x = xright_id₁:∀ (x : α), x ⊗ id₁ = xassoc₁:∀ (x y z : α), x ⊗ y ⊗ z = (x ⊗ y) ⊗ zop₂:OpSet αid₂:αleft_id₂:∀ (x : α), id₂ ⊗ x = xright_id₂:∀ (x : α), x ⊗ id₂ = xassoc₂:∀ (x y z : α), x ⊗ y ⊗ z = (x ⊗ y) ⊗ zh:OpSet.op = OpSet.op⊢ id₁ = id₁ ⊗ id₂]α:Typeop₁:OpSet αid₁:αleft_id₁:∀ (x : α), id₁ ⊗ x = xright_id₁:∀ (x : α), x ⊗ id₁ = xassoc₁:∀ (x y z : α), x ⊗ y ⊗ z = (x ⊗ y) ⊗ zop₂:OpSet αid₂:αleft_id₂:∀ (x : α), id₂ ⊗ x = xright_id₂:∀ (x : α), x ⊗ id₂ = xassoc₂:∀ (x y z : α), x ⊗ y ⊗ z = (x ⊗ y) ⊗ zh:OpSet.op = OpSet.op⊢ id₁ = id₁ ⊗ id₂
      -- then, we can use m₂'s right id
      rw [right_id₂α:Typeop₁:OpSet αid₁:αleft_id₁:∀ (x : α), id₁ ⊗ x = xright_id₁:∀ (x : α), x ⊗ id₁ = xassoc₁:∀ (x y z : α), x ⊗ y ⊗ z = (x ⊗ y) ⊗ zop₂:OpSet αid₂:αleft_id₂:∀ (x : α), id₂ ⊗ x = xright_id₂:∀ (x : α), x ⊗ id₂ = xassoc₂:∀ (x y z : α), x ⊗ y ⊗ z = (x ⊗ y) ⊗ zh:OpSet.op = OpSet.op⊢ id₁ = id₁]α:Typeop₁:OpSet αid₁:αleft_id₁:∀ (x : α), id₁ ⊗ x = xright_id₁:∀ (x : α), x ⊗ id₁ = xassoc₁:∀ (x y z : α), x ⊗ y ⊗ z = (x ⊗ y) ⊗ zop₂:OpSet αid₂:αleft_id₂:∀ (x : α), id₂ ⊗ x = xright_id₂:∀ (x : α), x ⊗ id₂ = xassoc₂:∀ (x y z : α), x ⊗ y ⊗ z = (x ⊗ y) ⊗ zh:OpSet.op = OpSet.oph':id₁ = id₂⊢ Monoid.id = Monoid.id
    -- the goal `m₁.id = m₂.id` is equivalent with `id₁ = id₂`
    -- even though it displays `Monoid.id = Monoid.id`
    exact h'All goals completed! 🐙

In the above proof, we can destructure the monoid instances m₁ and m₂ with the obtain tactic we saw in the Logic chapter. When we do so, we prepend the @ symbol to our tuple so that we can "flatten" the Monoid to reveal both its OpSet field op and its Monoid (only) fields id, left_id, etc., together. When stepping through the above proof, if the notation is confusing to you, remember that you can set set_option pp.all true or set_option pp.explicit true to make Lean show you more clearly what is going on. For example, the goal is displayed as Monoid.id = Monoid.id since the instances m₁ and m₂ are implicit arguments to Monoid.id. Setting pp.explicit true displays the goal as @Eq α (@Monoid.id α m₁) (@Monoid.id α m₂).

A group is a special kind of monoid with an inverse operation inv, which has the property that ∀ x, inv x ⊗ x = id = x ⊗ inv x. We can extend the definition of a Monoid to capture this new feature:

class Group (α : Type) extends (Monoid α) where
  inv : α → α
  left_inv  (x : α) : inv x ⊗ x = id
  right_inv (x : α) : x ⊗ inv x = id

Now, the monoids we described earlier are not groups: there is no inverse operation on the natural numbers such that ∀ x, x + inv x = 0 = inv x + x, for example. However, addition does form a group over the integers:

Exercise★(IntGroupAdd) (Manually graded)

declaration uses `sorry`instance : Group Int where
  op := Int.add
  id := sorry
  inv := sorry
  left_id := sorry
  right_id := sorry
  assoc := sorry
  left_inv := sorry
  right_inv := sorry

In mathematics, the study of groups is called group theory. Let's prove a handful of its simplest results:

Exercise★(InverseUnique)

Two groups defined with the same operation over the same set must have the same inverse as well.

theorem declaration uses `sorry`inv_unique {α : Type} {g₁ g₂ : Group α} (h : g₁.op = g₂.op) :
  g₁.inv = g₂.inv := byα:Typeg₁:Group αg₂:Group αh:OpSet.op = OpSet.op⊢ Group.inv = Group.inv
    sorryAll goals completed! 🐙

Exercise★(IdentityUnique)

If an element of a monoid satisfies just one of the identity laws (here, we take the left), then it must be equal to the monoid's identity element.

theorem declaration uses `sorry`Monoid.id_unique_left {α : Type} [Monoid α] (x : α)
    (hₗ : ∀ y, x ⊗ y = y) : x = id := byα:Typeinst✝:Monoid αx:αhₗ:∀ (y : α), x ⊗ y = y⊢ x = id
  sorryAll goals completed! 🐙

Exercise★★(InverseInverse)

The inverse of the inverse of an element is itself; we prove this using an intermediate lemma.

theorem declaration uses `sorry`inv_inv' {α : Type} {g : Group α} (x y z : α)
    (h₁ : g.inv x = y) (h₂ : g.inv y = z) : x = z := byα:Typeg:Group αx:αy:αz:αh₁:Group.inv x = yh₂:Group.inv y = z⊢ x = z
  sorryAll goals completed! 🐙

theorem declaration uses `sorry`inv_inv {α : Type} {g : Group α} (x : α) :
  g.inv (g.inv x) = x := byα:Typeg:Group αx:α⊢ Group.inv (Group.inv x) = x
    sorryAll goals completed! 🐙

end Algebra

11.5. Maps🔗

Maps (or "dictionaries") are ubiquitous data structures both in ordinary programming and in the theory of programming languages; we're going to need them in many places in later volumes.

Maps are also where the ideas in this chapter come together in a single, realistic example: overloaded notation, typeclass-supplied defaults, and proof-carrying instances that guarantee a data structure behaves the way we expect.

We'll define two flavors of maps: total maps, which include a "default" element to be returned when a key being looked up doesn't exist, and partial maps, which instead return an option to indicate success or failure. Partial maps are defined in terms of total maps, using none as the default element.

11.5.1. Total Maps🔗

The Lists chapter introduced a partial map abstraction, PartialMap, with a find function for lookup, based on lists of key-value pairs. Here, we offer a map abstraction using functions instead. The advantage of this representation is that it offers a more extensional view of maps, as we saw with functions in the Logic chapter: two maps that respond to every query in the same way will be represented as exactly the same function. This simplifies proofs that use maps — we'll see exactly how once we start relating different updates to each other, below. We encapsulate them inside a structure which we call TotalMap. Intuitively, a total map just contains a function inner from a key of type α to a value of type β.

structure TotalMap (α : Type) (β : Type) where
  inner : α → β

An "empty" TotalMap is one that maps every α to the same (default) β. We capture this idea using the Inhabited typeclass, which is the standard library's version of the DefaultValue class we developed above. The function TotalMap.empty yields an empty total map with the given default element.

namespace TotalMap

def empty {α β : Type} [Inhabited β] : TotalMap α β where
  inner := fun _ => default

Just as declaring BEq/DefaultValue instances above hooked == and DefaultValue.value up to our types, we can declare an instance of the standard library's EmptyCollection typeclass to associate ∅ with this empty map.

instance {α β : Type} [Inhabited β] : EmptyCollection (TotalMap α β) where
  emptyCollection := TotalMap.empty

theorem empty_def {α β : Type} [Inhabited β] :
    (∅ : TotalMap α β) = { inner := fun _ => default } := byα:Typeβ:Typeinst✝:Inhabited β⊢ ∅ = { inner := fun x => default } rflAll goals completed! 🐙

Here, for example, is an empty map that takes Nat keys to Nat values:

def emptyNatMap : TotalMap Nat Nat := ∅

11.5.1.1. Getting Elements🔗

While TotalMaps happen to be implemented as functions under the hood, we would prefer not to expose this fact in their public interface. Accordingly, we define a specific function for querying a map, rather than expecting clients to call a TotalMap's inner function directly. This function get, for getting the value associated with a key, plays the role that find played for the Lists chapter's list-based maps.

def get {α β : Type} (m : TotalMap α β) (a : α) := m.inner a

theorem get_def {α β : Type} {m : TotalMap α β} {a : α} :
  m.get a = m.inner a := byα:Typeβ:Typem:TotalMap α βa:α⊢ m.get a = m.inner a rflAll goals completed! 🐙

example : emptyNatMap.get 2 = 0 := by⊢ emptyNatMap.get 2 = 0 rflAll goals completed! 🐙

Function get is the public API counterpart to inner, which is an implementation-specific detail of TotalMap. Because get_def "peeks" through the abstraction, it should be used sparingly, and only inside the TotalMap namespace.

Here is an example that uses the API lemmas empty_def and get_def:

example {n : Nat} : emptyNatMap.get n = 0 := byn:Nat⊢ emptyNatMap.get n = 0
  rewrite [get_def,n:Nat⊢ emptyNatMap.inner n = 0 emptyNatMap,n:Nat⊢ ∅.inner n = 0 empty_def,n:Nat⊢ { inner := fun x => default }.inner n = 0 Nat.default_eq_zeron:Nat⊢ { inner := fun x => 0 }.inner n = 0]n:Nat⊢ { inner := fun x => 0 }.inner n = 0
  rflAll goals completed! 🐙

In the above example, we use rewrite and rfl instead of the usual rw to highlight something interesting. After the rewrites in this proof, we end up with a goal that looks like { inner := fun x => 0 }.inner n = 0, which we can solve with rfl. This is because the projection .inner on a structure of the form { inner := x } is definitionally equal to x.

To make element-getting more convenient, let's define notation so we can write emptyNatMap[2] rather than emptyNatMap.get 2. We could notate get directly — we'll do exactly that for update below — but here we'll instead make "getting an element" its own typeclass, MyGetElem, and notate it. Doing so means m[a] resolves to MyGetElem.getElem m a for any type with a MyGetElem instance, not just TotalMap.

Using typeclasses to define notation is typical in Lean when the same notation is useful for many different types. We have seen the approach already with ==: writing x == y is notation for BEq.beq, resolved by instance search for whatever type x and y have. We also just saw overloaded notation for EmptyCollection above, where ∅ is notation for EmptyCollection.emptyCollection. Our typeclass MyGetElem is a simpler version of the standard library's GetElem typeclass, which has many instances such as Array, List, and Vector. We develop it to illustrate the notation-as-typeclass approach.

end TotalMap

The MyGetElem typeclass takes three type parameters: the collection implementation, its keys, and its values.

class MyGetElem (coll : Type) (idx : Type) (elem : outParam Type) where
  getElem (xs : coll) (i : idx) : elem

(Don't worry about the outParam qualifier; it is a hint to Lean that helps typeclass inference.)

The appropriate instance of MyGetElem for our TotalMap is:

instance {α β : Type} : MyGetElem (TotalMap α β) α β where
  getElem m a := m.get a

Now we can associate the bracket syntax with MyGetElem.getElem. We'll do so with the more general notation/macro_rules forms, rather than the infixl/infixr/scoped macro forms we've used for custom notation so far.

Notation encoding: `MyGetElem` brackets

We've defined custom notation before — :: and [...] for lists (chapter Lists, including an app_unexpander for printing [...]-notation lists back out), or +/*/== for arithmetic — but always with infixl/infixr or scoped macro; this is the first time we reach for the more general notation/macro_rules forms for getting the m[a] syntax to work. Chapters 5 and 6 of Metaprogramming in Lean 4 contain more detail on this mechanism.

namespace MyGetElem

scoped macro_rules | `($xs[$i]) => ``(getElem $xs $i)

@[app_unexpander getElem]
def unexpandGetElem : Lean.PrettyPrinter.Unexpander
  | `($_ $xs $i) => `($xs[$i])
  | _ => throw ()
end MyGetElem

open scoped MyGetElem

Since the standard library already declares the x[i] syntax for GetElem, we only need to define the macro_rules, not the notation as we have done previously. It's scoped since we don't want to override the default GetElem everywhere, but only when open scoped MyGetElem is in force.

Since we provided a MyGetElem instance for TotalMap, we can now use the notation m[a] to access elements of a map m.

namespace TotalMap

theorem getElem_def {α β : Type} (m : TotalMap α β) (a : α) :
  m[a] = m.get a := byα:Typeβ:Typem:TotalMap α βa:α⊢ m[a] = m.get a rflAll goals completed! 🐙

example : emptyNatMap[1] = default := by⊢ emptyNatMap[1] = default rflAll goals completed! 🐙

example {n : Nat} : emptyNatMap[n] = 0 := byn:Nat⊢ emptyNatMap[n] = 0
  rw [getElem_def,n:Nat⊢ emptyNatMap.get n = 0 get_def,n:Nat⊢ emptyNatMap.inner n = 0 emptyNatMapn:Nat⊢ ∅.inner n = 0]n:Nat⊢ ∅.inner n = 0
  rw [empty_def,n:Nat⊢ { inner := fun x => default }.inner n = 0 Nat.default_eq_zeron:Nat⊢ { inner := fun x => 0 }.inner n = 0]All goals completed! 🐙

We want the public API of TotalMap to use the m[a] notation instead of m.get a, so we provide the reverse direction of getElem_def as a simp lemma; the m[a] notation is the TotalMap API's simp normal form.

@[simp]
theorem get_eq_getElem {α β : Type} (m : TotalMap α β) (a : α) :
  m.get a = m[a] := byα:Typeβ:Typem:TotalMap α βa:α⊢ m.get a = m[a] rflAll goals completed! 🐙

example {n : Nat} : emptyNatMap.get n = emptyNatMap[n] := byn:Nat⊢ emptyNatMap.get n = emptyNatMap[n]
  simpAll goals completed! 🐙

This design minimizes the need to use getElem_def outside concrete examples (which are typically solvable with rfl anyway).

11.5.1.2. Updating Elements🔗

Now we turn to the update function, which takes a map m, a key a, and a value b, and returns a new map that takes a to b and takes every other key to whatever m does. We do this by wrapping a new map function around the old one.

def update {α β : Type} (m : TotalMap α β) [BEq α] (a : α) (b : β) :
  TotalMap α β where
    inner := fun a' => bif a == a' then b else m[a']

For example, we can build a map taking String to Bool, where "foo" and "bar" are mapped to true and every other key is mapped to false, like this:

def exampleMap :=
  (∅ : TotalMap String Bool)
    |>.update "foo" true
    |>.update "bar" true

Here |> is Lean's pipe notation: x |>.f y means x.f y, letting us chain a sequence of function or method calls left to right without nested parentheses.

We also introduce a notation for updating maps — this time, rather than going through a typeclass and its own notation/macro_rules machinery as we did for MyGetElem, we write a notation that references TotalMap.update directly. Unlike indexing, update doesn't need to work generically across container types (there's no standard-library operation like GetElem that we're mirroring here), so the simpler, direct route suffices.

notation a:55 " →ₜ " b:55 " ; " m:55 => TotalMap.update m a b

theorem update_apply {α β : Type} [BEq α] (m : TotalMap α β)
  (a a' : α) (b : β) : (a →ₜ b ; m)[a'] =
  bif a == a' then b else m[a'] := byα:Typeβ:Typeinst✝:BEq αm:TotalMap α βa:αa':αb:β⊢ (a →ₜ b ; m)[a'] = bif a == a' then b else m[a'] rflAll goals completed! 🐙

We can omit the map from the notation when we want it to be empty:

notation a:55 " →ₜ " b:55 => TotalMap.update ∅ a b

The exampleMap above can now be defined as follows:

def exampleMap' : TotalMap String Bool := "bar" →ₜ true ; "foo" →ₜ true ; ∅
def exampleMap'' : TotalMap String Bool := "bar" →ₜ true ; "foo" →ₜ true

example : exampleMap = exampleMap' := by⊢ exampleMap = exampleMap' rflAll goals completed! 🐙
example : exampleMap' = exampleMap'' := by⊢ exampleMap' = exampleMap'' rflAll goals completed! 🐙

example : exampleMap'["bar"] = true := by⊢ exampleMap'["bar"] = true rflAll goals completed! 🐙
example : exampleMap'["foo"] = true := by⊢ exampleMap'["foo"] = true rflAll goals completed! 🐙
example : exampleMap'["quux"] = false := by⊢ exampleMap'["quux"] = false rflAll goals completed! 🐙

Let's also see a couple of examples of working with updated maps using rewrites:

example : exampleMap'["bar"] = true := by⊢ exampleMap'["bar"] = true
  rw [exampleMap',⊢ ("bar" →ₜ true ; "foo" →ₜ true)["bar"] = true update_apply,⊢ (bif "bar" == "bar" then true else ("foo" →ₜ true)["bar"]) = true BEq.rfl,⊢ (bif true then true else ("foo" →ₜ true)["bar"]) = true Bool.cond_true⊢ true = true]All goals completed! 🐙

example : exampleMap'["foo"] = true := by⊢ exampleMap'["foo"] = true
  have h : ("bar" == "foo") = false := by simph:("bar" == "foo") = false⊢ exampleMap'["foo"] = true
  rw [exampleMap',h:("bar" == "foo") = false⊢ ("bar" →ₜ true ; "foo" →ₜ true)["foo"] = true update_apply,h:("bar" == "foo") = false⊢ (bif "bar" == "foo" then true else ("foo" →ₜ true)["foo"]) = true h,h:("bar" == "foo") = false⊢ (bif false then true else ("foo" →ₜ true)["foo"]) = true Bool.cond_falseh:("bar" == "foo") = false⊢ ("foo" →ₜ true)["foo"] = true]h:("bar" == "foo") = false⊢ ("foo" →ₜ true)["foo"] = true
  rw [update_apply,h:("bar" == "foo") = false⊢ (bif "foo" == "foo" then true else ∅["foo"]) = true BEq.rfl,h:("bar" == "foo") = false⊢ (bif true then true else ∅["foo"]) = true Bool.cond_trueh:("bar" == "foo") = false⊢ true = true]All goals completed! 🐙

example : exampleMap'["quux"] = false := by⊢ exampleMap'["quux"] = false
  have h₁ : ("bar" == "quux") = false := by simph₁:("bar" == "quux") = false⊢ exampleMap'["quux"] = false
  have h₂ : ("foo" == "quux") = false := by rflh₁:("bar" == "quux") = falseh₂:("foo" == "quux") = false⊢ exampleMap'["quux"] = false
  rw [exampleMap',h₁:("bar" == "quux") = falseh₂:("foo" == "quux") = false⊢ ("bar" →ₜ true ; "foo" →ₜ true)["quux"] = false update_apply,h₁:("bar" == "quux") = falseh₂:("foo" == "quux") = false⊢ (bif "bar" == "quux" then true else ("foo" →ₜ true)["quux"]) = false h₁,h₁:("bar" == "quux") = falseh₂:("foo" == "quux") = false⊢ (bif false then true else ("foo" →ₜ true)["quux"]) = false Bool.cond_falseh₁:("bar" == "quux") = falseh₂:("foo" == "quux") = false⊢ ("foo" →ₜ true)["quux"] = false]h₁:("bar" == "quux") = falseh₂:("foo" == "quux") = false⊢ ("foo" →ₜ true)["quux"] = false
  rw [update_apply,h₁:("bar" == "quux") = falseh₂:("foo" == "quux") = false⊢ (bif "foo" == "quux" then true else ∅["quux"]) = false h₂,h₁:("bar" == "quux") = falseh₂:("foo" == "quux") = false⊢ (bif false then true else ∅["quux"]) = false Bool.cond_falseh₁:("bar" == "quux") = falseh₂:("foo" == "quux") = false⊢ ∅["quux"] = false]h₁:("bar" == "quux") = falseh₂:("foo" == "quux") = false⊢ ∅["quux"] = false
  rw [empty_def,h₁:("bar" == "quux") = falseh₂:("foo" == "quux") = false⊢ { inner := fun x => default }["quux"] = false getElem_def,h₁:("bar" == "quux") = falseh₂:("foo" == "quux") = false⊢ { inner := fun x => default }.get "quux" = false get_def,h₁:("bar" == "quux") = falseh₂:("foo" == "quux") = false⊢ { inner := fun x => default }.inner "quux" = false Bool.default_boolh₁:("bar" == "quux") = falseh₂:("foo" == "quux") = false⊢ { inner := fun x => false }.inner "quux" = false]All goals completed! 🐙

Each have ... = false by simp/by rfl above goes through because String's BEq instance is ultimately derived from its DecidableEq instance — "Deciding Propositions" below explains this mechanism in full (worked out there for Nat, but the connection is general).

11.5.2. Reasoning About Total Maps🔗

When we use maps in later volumes, we'll need several fundamental properties about how they behave. Several of these properties depend on BEq, which our maps use to compare keys of type α.

class ReflBEq (α : Type) [BEq α] : Prop where
    rfl {a : α} : (a == a) = true

class LawfulBEq (α : Type) [BEq α] : Prop extends ReflBEq α where
    eq_of_beq : {a b : α} → (a == b) = true → a = b

These classes refine BEq, specifying that == is reflexive and coincides with propositional equality =. Neither property is automatic: BEq's only obligation is to return some Bool, with no proof attached, so an arbitrary BEq instance could compute anything at all, whether or not it agrees with =. We'll need both facts below: reflexivity to show that looking up the key you just updated returns the new value, and agreement with = to show that updating one key leaves lookups at every other key unchanged. We'll return to this distinction between BEq and provable equality in "Deciding Propositions" below.

Even if you don't work the following exercises, make sure you thoroughly understand the statements of the lemmas! Some of the proofs require the extensionality tactic ext, discussed in the Logic chapter.

Here is our first property, that the empty map returns its default element for all keys:

@[simp]
theorem getElem_empty {α β : Type} [BEq α] [Inhabited β] (a : α) :
  (∅ : TotalMap α β)[a] = default := byα:Typeβ:Typeinst✝¹:BEq αinst✝:Inhabited βa:α⊢ ∅[a] = default
    rw [empty_def,α:Typeβ:Typeinst✝¹:BEq αinst✝:Inhabited βa:α⊢ { inner := fun x => default }[a] = default getElem_def,α:Typeβ:Typeinst✝¹:BEq αinst✝:Inhabited βa:α⊢ { inner := fun x => default }.get a = default get_defα:Typeβ:Typeinst✝¹:BEq αinst✝:Inhabited βa:α⊢ { inner := fun x => default }.inner a = default]All goals completed! 🐙

Next, if we update a map m at a key a with a new value b and then look up a in the map resulting from the update, we get back b:

@[simp]
theorem update_eq {α β : Type} [BEq α] [ReflBEq α] (m : TotalMap α β)
  (a : α) (b : β) : (a →ₜ b ; m)[a] = b := byα:Typeβ:Typeinst✝¹:BEq αinst✝:ReflBEq αm:TotalMap α βa:αb:β⊢ (a →ₜ b ; m)[a] = b
    rw [update_apply,α:Typeβ:Typeinst✝¹:BEq αinst✝:ReflBEq αm:TotalMap α βa:αb:β⊢ (bif a == a then b else m[a]) = b BEq.rfl,α:Typeβ:Typeinst✝¹:BEq αinst✝:ReflBEq αm:TotalMap α βa:αb:β⊢ (bif true then b else m[a]) = b Bool.cond_trueα:Typeβ:Typeinst✝¹:BEq αinst✝:ReflBEq αm:TotalMap α βa:αb:β⊢ b = b]All goals completed! 🐙

On the other hand, if we update a map m at a key a₁ and then look up a different key a₂ in the resulting map, we get the same result that m would have given:

Exercise★★(update_neq) (Optional)

@[simp]
theorem declaration uses `sorry`update_neq {α β : Type} [BEq α] [LawfulBEq α]
  {m : TotalMap α β} {a₁ a₂ : α} (h : a₁ ≠ a₂) (b : β) :
  (a₁ →ₜ b ; m)[a₂] = m[a₂] := byα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa₁:αa₂:αh:a₁ ≠ a₂b:β⊢ (a₁ →ₜ b ; m)[a₂] = m[a₂]
  sorryAll goals completed! 🐙

The two remaining facts are equalities between maps, so we first need to say when two maps are equal. Since a total map is implemented as a function, this is effectively the functional extensionality principle (funext) from the Logic chapter: two maps are equal when they agree at every key. Recording it once, for maps, and tagging it @[ext] lets the ext tactic reduce a goal m₁ = m₂ to the pointwise one in the proofs below.

The fact that TotalMap is a structure complicates things slightly. We need to use injectivity of its constructor mk, which Lean automatically provides for us as mk.injEq. It lets us prove m₁ = m₂ from m₁.inner = m₂.inner or vice versa.

@[ext]
theorem ext {α β : Type} {m₁ m₂ : TotalMap α β}
  (h : ∀ a : α, m₁[a] = m₂[a]) : m₁ = m₂ := byα:Typeβ:Typem₁:TotalMap α βm₂:TotalMap α βh:∀ (a : α), m₁[a] = m₂[a]⊢ m₁ = m₂
    rw [TotalMap.mk.injEqα:Typeβ:Typem₁:TotalMap α βm₂:TotalMap α βh:∀ (a : α), m₁[a] = m₂[a]⊢ m₁.inner = m₂.inner]α:Typeβ:Typem₁:TotalMap α βm₂:TotalMap α βh:∀ (a : α), m₁[a] = m₂[a]⊢ m₁.inner = m₂.inner
    ext aα:Typeβ:Typem₁:TotalMap α βm₂:TotalMap α βh:∀ (a : α), m₁[a] = m₂[a]a:α⊢ m₁.inner a = m₂.inner a; specialize h aα:Typeβ:Typem₁:TotalMap α βm₂:TotalMap α βa:αh:m₁[a] = m₂[a]⊢ m₁.inner a = m₂.inner a
    rw [getElem_def,α:Typeβ:Typem₁:TotalMap α βm₂:TotalMap α βa:αh:m₁.get a = m₂[a]⊢ m₁.inner a = m₂.inner a get_def,α:Typeβ:Typem₁:TotalMap α βm₂:TotalMap α βa:αh:m₁.inner a = m₂[a]⊢ m₁.inner a = m₂.inner a getElem_def,α:Typeβ:Typem₁:TotalMap α βm₂:TotalMap α βa:αh:m₁.inner a = m₂.get a⊢ m₁.inner a = m₂.inner a get_defα:Typeβ:Typem₁:TotalMap α βm₂:TotalMap α βa:αh:m₁.inner a = m₂.inner a⊢ m₁.inner a = m₂.inner a] at hα:Typeβ:Typem₁:TotalMap α βm₂:TotalMap α βa:αh:m₁.inner a = m₂.inner a⊢ m₁.inner a = m₂.inner a
    exact hAll goals completed! 🐙

This proof amounts to peeling off the TotalMap wrapper via mk.injEq, making the goal an equality between the underlying .inner functions. Then the inner ext call finishes it by invoking funext — the standard library's extensionality principle for every function type, already proved once and for all, with nothing TotalMap-specific left to establish. This is the proof-simplifying payoff of representing maps as functions.

To demonstrate this extensionality principle, let's look at an example:

example : "bar" →ₜ true ; "foo" →ₜ true = "foo" →ₜ true ; "bar" →ₜ true := by⊢ "bar" →ₜ true ; "foo" →ₜ true = "foo" →ₜ true ; "bar" →ₜ true
  ext aa:String⊢ ("bar" →ₜ true ; "foo" →ₜ true)[a] = ("foo" →ₜ true ; "bar" →ₜ true)[a]
  by_cases h : "bar" = aposa:Stringh:"bar" = a⊢ ("bar" →ₜ true ; "foo" →ₜ true)[a] = ("foo" →ₜ true ; "bar" →ₜ true)[a]nega:Stringh:¬"bar" = a⊢ ("bar" →ₜ true ; "foo" →ₜ true)[a] = ("foo" →ₜ true ; "bar" →ₜ true)[a]
  ·posa:Stringh:"bar" = a⊢ ("bar" →ₜ true ; "foo" →ₜ true)[a] = ("foo" →ₜ true ; "bar" →ₜ true)[a] subst hpos⊢ ("bar" →ₜ true ; "foo" →ₜ true)["bar"] = ("foo" →ₜ true ; "bar" →ₜ true)["bar"]
    have h' : "foo" ≠ "bar" := by⊢ "bar" →ₜ true ; "foo" →ₜ true = "foo" →ₜ true ; "bar" →ₜ true simpposh':"foo" ≠ "bar"⊢ ("bar" →ₜ true ; "foo" →ₜ true)["bar"] = ("foo" →ₜ true ; "bar" →ₜ true)["bar"]
    rw [update_eq,posh':"foo" ≠ "bar"⊢ true = ("foo" →ₜ true ; "bar" →ₜ true)["bar"] update_neq h',posh':"foo" ≠ "bar"⊢ true = ("bar" →ₜ true)["bar"] update_eqposh':"foo" ≠ "bar"⊢ true = true]All goals completed! 🐙
  ·nega:Stringh:¬"bar" = a⊢ ("bar" →ₜ true ; "foo" →ₜ true)[a] = ("foo" →ₜ true ; "bar" →ₜ true)[a] simp only [update_apply]nega:Stringh:¬"bar" = a⊢ (bif "bar" == a then true else bif "foo" == a then true else ∅[a]) =
  bif "foo" == a then true else bif "bar" == a then true else ∅[a]
    rw [beq_false_of_ne hnega:Stringh:¬"bar" = a⊢ (bif false then true else bif "foo" == a then true else ∅[a]) =
  bif "foo" == a then true else bif false then true else ∅[a]]nega:Stringh:¬"bar" = a⊢ (bif false then true else bif "foo" == a then true else ∅[a]) =
  bif "foo" == a then true else bif false then true else ∅[a]
    simpAll goals completed! 🐙

Given keys a₁ and a₂, the tactic by_cases h : a₁ = a₂ splits the proof into the case where they are equal — where subst h then replaces one by the other — and the case where they are not, which is what update_neq wants. Use it to prove the following theorem, which states that if we update a map to assign key a the same value as it already has in m, then the result is equal to m:

Exercise★★(update_same)

@[simp]
theorem declaration uses `sorry`update_same {α β : Type} [BEq α] [LawfulBEq α] (m : TotalMap α β)
  (a : α) : (a →ₜ m[a] ; m) = m := byα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa:α⊢ a →ₜ m[a] ; m = m
    sorryAll goals completed! 🐙

Similarly, if we update a map m at a key a with a value b₁ and then update again with the same key a and another value b₂, the resulting map behaves the same (gives the same result when applied to any key) as the simpler map obtained by performing just the second update on m:

Exercise★★(update_shadow) (Optional)

@[simp]
theorem declaration uses `sorry`update_shadow {α β : Type} [BEq α] [LawfulBEq α] (m : TotalMap α β)
  (a : α) (b₁ b₂ : β) : (a →ₜ b₂ ; a →ₜ b₁ ; m) = (a →ₜ b₂ ; m) := byα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa:αb₁:βb₂:β⊢ a →ₜ b₂ ; a →ₜ b₁ ; m = a →ₜ b₂ ; m
  sorryAll goals completed! 🐙

Now prove one final property of the update function: if we update a map m at two distinct keys, it doesn't matter in which order we do the updates.

Exercise★★★(update_permute)

theorem declaration uses `sorry`update_permute {α β : Type} [BEq α] [LawfulBEq α]
  {m : TotalMap α β} {a₁ a₂ : α} {b₁ b₂ : β} (h : a₁ ≠ a₂) :
  (a₁ →ₜ b₁ ; a₂ →ₜ b₂ ; m) = (a₂ →ₜ b₂ ; a₁ →ₜ b₁ ; m) := byα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa₁:αa₂:αb₁:βb₂:βh:a₁ ≠ a₂⊢ a₁ →ₜ b₁ ; a₂ →ₜ b₂ ; m = a₂ →ₜ b₂ ; a₁ →ₜ b₁ ; m
  sorryAll goals completed! 🐙

end TotalMap

11.5.3. Notation for Concrete Maps🔗

Wouldn't it be nice if we could use a more natural notation for concrete maps like { "bar" ↦ true, "foo" ↦ true }? To accomplish this, we define a simple structure that consists of a key and a value, along with ↦ notation for it.

@[ext]
structure KVPair (K : Type) (V : Type) where
  key : K
  value : V

namespace KVPair
scoped notation k " ↦ " v => KVPair.mk k v
end KVPair

open scoped KVPair

Next, we declare Insert and Singleton instances — the standard-library typeclasses behind the {x, y, ...} and {x} collection-literal notation that List, Finset, and other stdlib containers already support — so that TotalMap can use it too.

namespace TotalMap

instance {α β : Type} [BEq α] : Insert (KVPair α β) (TotalMap α β) where
  insert kv m := kv.key →ₜ kv.value ; m

instance {α β : Type} [BEq α] [Inhabited β] : Singleton (KVPair α β) (TotalMap α β) where
  singleton kv := insert kv ∅

instance {α β : Type} [BEq α] [Inhabited β] : LawfulSingleton (KVPair α β) (TotalMap α β) where
  insert_empty_eq _ := byα:Typeβ:Typeinst✝¹:BEq αinst✝:Inhabited βx✝:KVPair α β⊢ insert x✝ ∅ = {x✝} rflAll goals completed! 🐙

end TotalMap

Here are a couple of examples using the new notation:

example : ({ "bar" ↦ true, "foo" ↦ true }) = "bar" →ₜ true ; "foo" →ₜ true := by⊢ {"bar" ↦ true, "foo" ↦ true} = "bar" →ₜ true ; "foo" →ₜ true rflAll goals completed! 🐙

example : ({ "foo" ↦ true } : TotalMap String Bool)["foo"] = true := by⊢ {"foo" ↦ true}["foo"] = true rflAll goals completed! 🐙

example : ({ 1 ↦ 2, 1 ↦ 3 } : TotalMap Nat Nat)[1] = 2 := by⊢ {1 ↦ 2, 1 ↦ 3}[1] = 2 rflAll goals completed! 🐙

The reason we need to explicitly specify the type of the map is that Lean doesn't know what type of collection { "foo" ↦ true } is without type hints, as we can see with #check:

{"foo" ↦ true} : ?m.2#check { "foo" ↦ true }

{"foo" ↦ true} : ?m.2

The type shows a ?m.4, which indicates that Lean can't infer the type. A type which can't be inferred doesn't have any type classes like MyGetElem, so typeclass resolution gets stuck in the following example:

example : (typeclass instance problem is stuck
  Singleton (KVPair String Bool) ?m.6

Note: Lean will not try to resolve this typeclass instance problem because the second type argument to `Singleton` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass.

Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.{ "foo" ↦ true })["foo"] = true := by rfl

11.5.4. Partial Maps🔗

Lastly, we define partial maps on top of total maps. A partial map with elements of type β is simply a total map with elements of type Option β, whose default element is none.

structure PartialMap (α : Type) (β : Type) where
  inner : TotalMap α (Option β)

instance {α β : Type} : EmptyCollection (PartialMap α β) where
  emptyCollection := { inner := ∅ }

Note that the definition of EmptyCollection doesn't need β to have an Inhabited instance like TotalMap did. This is because Option β has its own Inhabited instance: none is a value of every Option type.

Now let's define a PartialMap's operations. We will do so using those of TotalMap via PartialMap.toTotal.

namespace PartialMap

def toTotal {α β : Type} (m : PartialMap α β) : TotalMap α (Option β) := m.inner

theorem toTotal_def {α β : Type} (m : PartialMap α β) : m.toTotal = m.inner := byα:Typeβ:Typem:PartialMap α β⊢ m.toTotal = m.inner rflAll goals completed! 🐙

Note that toTotal_def exposes implementation-specific details of PartialMap. So we should aovid using this outside the PartialMap namespace. Now we can define the getElem operation.

instance {α β : Type} : MyGetElem (PartialMap α β) α (Option β) where
  getElem m a := m.toTotal[a]

theorem getElem_def {α β : Type} (m : PartialMap α β) (a : α) : m[a] = m.toTotal[a] := byα:Typeβ:Typem:PartialMap α βa:α⊢ m[a] = m.toTotal[a] rflAll goals completed! 🐙

Here are some examples.

def emptyNatMap : PartialMap Nat Nat where
  inner := ∅

example : emptyNatMap[1] = default := by⊢ emptyNatMap[1] = default rflAll goals completed! 🐙

example {n : Nat} : emptyNatMap[n] = none := byn:Nat⊢ emptyNatMap[n] = none
  rw [getElem_def,n:Nat⊢ emptyNatMap.toTotal[n] = none toTotal_def,n:Nat⊢ emptyNatMap.inner[n] = none emptyNatMapn:Nat⊢ { inner := ∅ }.inner[n] = none]n:Nat⊢ { inner := ∅ }.inner[n] = none
  dsimp onlyn:Nat⊢ ∅[n] = none
  rw [TotalMap.getElem_def,n:Nat⊢ ∅.get n = none TotalMap.get_defn:Nat⊢ ∅.inner n = none]n:Nat⊢ ∅.inner n = none
  rw [TotalMap.empty_def,n:Nat⊢ { inner := fun x => default }.inner n = none Option.default_eq_nonen:Nat⊢ { inner := fun x => none }.inner n = none]All goals completed! 🐙

We again want the public API to use the m[a] notation (instead of m.toTotal[a]), so we provide the reverse direction of getElem_def as a simp lemma to specify that the simp normal form is m[a].

@[simp]
theorem toTotal_eq_getElem {α β : Type} (m : PartialMap α β) (a : α) :
    m.toTotal[a] = m[a] := byα:Typeβ:Typem:PartialMap α βa:α⊢ m.toTotal[a] = m[a] rflAll goals completed! 🐙

Now let's turn to the update operation. Updating a partial map at a key means storing a some value there. So we create a new partial map from a →ₜ some b ; m.toTotal by wrapping it in angle brackets, i.e., using the anonymous constructor syntax. This is equivalent to writing { inner := a →ₜ some b ; m.toTotal }. We also introduce a similar notation for it as for total maps.

def update {α β : Type} [BEq α] (m : PartialMap α β) (a : α) (b : β) : PartialMap α β :=
  ⟨a →ₜ some b ; m.toTotal⟩

notation a:55 " →ₚ " b:55 " ; " m:55 => PartialMap.update m a b

notation a:55 " →ₚ " b:55 => PartialMap.update ∅ a b

def examplePmap : PartialMap String Bool := "Church" →ₚ true ; "Turing" →ₚ false

Now we can provide some fundamental properties about toTotal:

@[simp]
theorem toTotal_empty {α β : Type} : (∅ : PartialMap α β).toTotal =
  (∅ : TotalMap α (Option β)) := byα:Typeβ:Type⊢ ∅.toTotal = ∅ rflAll goals completed! 🐙

@[simp]
theorem toTotal_update {α β : Type} [BEq α] (m : PartialMap α β)
  (a : α) (b : β) : (a →ₚ b ; m).toTotal = a →ₜ some b ; m.toTotal := byα:Typeβ:Typeinst✝:BEq αm:PartialMap α βa:αb:β⊢ (a →ₚ b ; m).toTotal = a →ₜ some b ; m.toTotal rflAll goals completed! 🐙

As an example, here's how we can use these on some concrete maps:

example : (2 →ₚ 3)[2] = some 3 := by⊢ (2 →ₚ 3)[2] = some 3
  rw [getElem_def,⊢ (2 →ₚ 3).toTotal[2] = some 3 toTotal_update,⊢ (2 →ₜ some 3 ; ∅.toTotal)[2] = some 3 toTotal_empty,⊢ (2 →ₜ some 3)[2] = some 3 TotalMap.update_eq⊢ some 3 = some 3]All goals completed! 🐙

This also holds by definition (rfl), since all the rewrites in the above proof do the computation step-by-step.

example : (2 →ₚ 3)[2] = some 3 := by⊢ (2 →ₚ 3)[2] = some 3 rflAll goals completed! 🐙

Next, we lift all of the basic lemmas about total maps to partial maps. To do this, we should first prove an extensionality lemma about partial maps. To prove extensionality, we employ injectivity of PartialMap's constructor mk using mk.injEq.

theorem toTotal_eq_iff {α β : Type} (m₁ m₂ : PartialMap α β) :
  m₁.toTotal = m₂.toTotal ↔ m₁ = m₂ := byα:Typeβ:Typem₁:PartialMap α βm₂:PartialMap α β⊢ m₁.toTotal = m₂.toTotal ↔ m₁ = m₂
    rw [mk.injEqα:Typeβ:Typem₁:PartialMap α βm₂:PartialMap α β⊢ m₁.toTotal = m₂.toTotal ↔ m₁.inner = m₂.inner]α:Typeβ:Typem₁:PartialMap α βm₂:PartialMap α β⊢ m₁.toTotal = m₂.toTotal ↔ m₁.inner = m₂.inner
    rflAll goals completed! 🐙

@[ext]
theorem ext {α β : Type} {m₁ m₂ : PartialMap α β}
  (h : ∀ a : α, m₁[a] = m₂[a]) : m₁ = m₂ := byα:Typeβ:Typem₁:PartialMap α βm₂:PartialMap α βh:∀ (a : α), m₁[a] = m₂[a]⊢ m₁ = m₂
    rw [← toTotal_eq_iffα:Typeβ:Typem₁:PartialMap α βm₂:PartialMap α βh:∀ (a : α), m₁[a] = m₂[a]⊢ m₁.toTotal = m₂.toTotal]α:Typeβ:Typem₁:PartialMap α βm₂:PartialMap α βh:∀ (a : α), m₁[a] = m₂[a]⊢ m₁.toTotal = m₂.toTotal
    exact TotalMap.ext hAll goals completed! 🐙

Now, let's lift the TotalMap lemmas:

@[simp]
theorem getElem_empty {α β : Type} [BEq α] (a : α) :
  (∅ : PartialMap α β)[a] = none := byα:Typeβ:Typeinst✝:BEq αa:α⊢ ∅[a] = none
    rw [getElem_def,α:Typeβ:Typeinst✝:BEq αa:α⊢ ∅.toTotal[a] = none toTotal_empty,α:Typeβ:Typeinst✝:BEq αa:α⊢ ∅[a] = none TotalMap.getElem_empty,α:Typeβ:Typeinst✝:BEq αa:α⊢ default = none Option.default_eq_noneα:Typeβ:Typeinst✝:BEq αa:α⊢ none = none]All goals completed! 🐙

@[simp]
theorem update_eq {α β : Type} [BEq α] [ReflBEq α]
  (m : PartialMap α β) (a : α) (b : β) : (a →ₚ b ; m)[a] = some b := byα:Typeβ:Typeinst✝¹:BEq αinst✝:ReflBEq αm:PartialMap α βa:αb:β⊢ (a →ₚ b ; m)[a] = some b
    rw [getElem_def,α:Typeβ:Typeinst✝¹:BEq αinst✝:ReflBEq αm:PartialMap α βa:αb:β⊢ (a →ₚ b ; m).toTotal[a] = some b toTotal_update,α:Typeβ:Typeinst✝¹:BEq αinst✝:ReflBEq αm:PartialMap α βa:αb:β⊢ (a →ₜ some b ; m.toTotal)[a] = some b TotalMap.update_eqα:Typeβ:Typeinst✝¹:BEq αinst✝:ReflBEq αm:PartialMap α βa:αb:β⊢ some b = some b]All goals completed! 🐙

@[simp]
theorem update_neq {α β : Type} [BEq α] [LawfulBEq α]
  {m : PartialMap α β} {a₁ a₂ : α} (h : a₁ ≠ a₂) (b : β) :
  (a₁ →ₚ b ; m)[a₂] = m[a₂] := byα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:PartialMap α βa₁:αa₂:αh:a₁ ≠ a₂b:β⊢ (a₁ →ₚ b ; m)[a₂] = m[a₂]
    simp only [getElem_def, toTotal_update]α:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:PartialMap α βa₁:αa₂:αh:a₁ ≠ a₂b:β⊢ (a₁ →ₜ some b ; m.toTotal)[a₂] = m.toTotal[a₂]
    rw [TotalMap.update_neq hα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:PartialMap α βa₁:αa₂:αh:a₁ ≠ a₂b:β⊢ m.toTotal[a₂] = m.toTotal[a₂]]All goals completed! 🐙

theorem update_shadow {α β : Type} [BEq α] [LawfulBEq α]
  (m : PartialMap α β) (a : α) (b₁ b₂ : β) :
  (a →ₚ b₂ ; a →ₚ b₁ ; m) = (a →ₚ b₂ ; m) := byα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:PartialMap α βa:αb₁:βb₂:β⊢ a →ₚ b₂ ; a →ₚ b₁ ; m = a →ₚ b₂ ; m
    apply extα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:PartialMap α βa:αb₁:βb₂:β⊢ ∀ (a_1 : α), (a →ₚ b₂ ; a →ₚ b₁ ; m)[a_1] = (a →ₚ b₂ ; m)[a_1]
    intro xα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:PartialMap α βa:αb₁:βb₂:βx:α⊢ (a →ₚ b₂ ; a →ₚ b₁ ; m)[x] = (a →ₚ b₂ ; m)[x]
    simp only [getElem_def, toTotal_update]α:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:PartialMap α βa:αb₁:βb₂:βx:α⊢ (a →ₜ some b₂ ; a →ₜ some b₁ ; m.toTotal)[x] = (a →ₜ some b₂ ; m.toTotal)[x]
    rw [TotalMap.update_shadowα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:PartialMap α βa:αb₁:βb₂:βx:α⊢ (a →ₜ some b₂ ; m.toTotal)[x] = (a →ₜ some b₂ ; m.toTotal)[x]]All goals completed! 🐙

theorem update_same {α β : Type} [BEq α] [LawfulBEq α] {m : PartialMap α β}
  {a : α} {b : β} (h : m[a] = some b) : (a →ₚ b ; m) = m := byα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:PartialMap α βa:αb:βh:m[a] = some b⊢ a →ₚ b ; m = m
    apply extα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:PartialMap α βa:αb:βh:m[a] = some b⊢ ∀ (a_1 : α), (a →ₚ b ; m)[a_1] = m[a_1]
    intro xα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:PartialMap α βa:αb:βh:m[a] = some bx:α⊢ (a →ₚ b ; m)[x] = m[x]
    simp only [getElem_def, toTotal_update]α:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:PartialMap α βa:αb:βh:m[a] = some bx:α⊢ (a →ₜ some b ; m.toTotal)[x] = m.toTotal[x]
    rw [← h,α:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:PartialMap α βa:αb:βh:m[a] = some bx:α⊢ (a →ₜ m[a] ; m.toTotal)[x] = m.toTotal[x] getElem_def,α:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:PartialMap α βa:αb:βh:m[a] = some bx:α⊢ (a →ₜ m.toTotal[a] ; m.toTotal)[x] = m.toTotal[x] TotalMap.update_sameα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:PartialMap α βa:αb:βh:m[a] = some bx:α⊢ m.toTotal[x] = m.toTotal[x]]All goals completed! 🐙

theorem update_permute {α β : Type} [BEq α] [LawfulBEq α]
  {m : PartialMap α β} {a₁ a₂ : α} {b₁ b₂ : β} (h : a₁ ≠ a₂) :
  (a₁ →ₚ b₁ ; a₂ →ₚ b₂ ; m) = (a₂ →ₚ b₂ ; a₁ →ₚ b₁ ; m) := byα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:PartialMap α βa₁:αa₂:αb₁:βb₂:βh:a₁ ≠ a₂⊢ a₁ →ₚ b₁ ; a₂ →ₚ b₂ ; m = a₂ →ₚ b₂ ; a₁ →ₚ b₁ ; m
    apply extα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:PartialMap α βa₁:αa₂:αb₁:βb₂:βh:a₁ ≠ a₂⊢ ∀ (a : α), (a₁ →ₚ b₁ ; a₂ →ₚ b₂ ; m)[a] = (a₂ →ₚ b₂ ; a₁ →ₚ b₁ ; m)[a]
    intro xα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:PartialMap α βa₁:αa₂:αb₁:βb₂:βh:a₁ ≠ a₂x:α⊢ (a₁ →ₚ b₁ ; a₂ →ₚ b₂ ; m)[x] = (a₂ →ₚ b₂ ; a₁ →ₚ b₁ ; m)[x]
    simp only [getElem_def, toTotal_update]α:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:PartialMap α βa₁:αa₂:αb₁:βb₂:βh:a₁ ≠ a₂x:α⊢ (a₁ →ₜ some b₁ ; a₂ →ₜ some b₂ ; m.toTotal)[x] = (a₂ →ₜ some b₂ ; a₁ →ₜ some b₁ ; m.toTotal)[x]
    rw [TotalMap.update_permute hα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:PartialMap α βa₁:αa₂:αb₁:βb₂:βh:a₁ ≠ a₂x:α⊢ (a₂ →ₜ some b₂ ; a₁ →ₜ some b₁ ; m.toTotal)[x] = (a₂ →ₜ some b₂ ; a₁ →ₜ some b₁ ; m.toTotal)[x]]All goals completed! 🐙

example : (2 →ₚ 3)[2] = some 3 := by⊢ (2 →ₚ 3)[2] = some 3
  simpAll goals completed! 🐙

example : examplePmap["Post"] = none := by⊢ examplePmap["Post"] = none
  rw [examplePmap⊢ ("Church" →ₚ true ; "Turing" →ₚ false)["Post"] = none]⊢ ("Church" →ₚ true ; "Turing" →ₚ false)["Post"] = none
  simpAll goals completed! 🐙

And let's add {}-notation for partial maps as well.

instance {α β : Type} [BEq α] : Insert (KVPair α β) (PartialMap α β) where
  insert kv m := kv.key →ₚ kv.value ; m

instance {α β : Type} [BEq α] : Singleton (KVPair α β) (PartialMap α β) where
  singleton kv := insert kv ∅

instance {α β : Type} [BEq α] : LawfulSingleton (KVPair α β) (PartialMap α β) where
  insert_empty_eq _ := byα:Typeβ:Typeinst✝:BEq αx✝:KVPair α β⊢ insert x✝ ∅ = {x✝} rflAll goals completed! 🐙

example : { 1 ↦ 2, 2 ↦ 3 } = 1 →ₚ 2 ; 2 →ₚ 3 := by⊢ {1 ↦ 2, 2 ↦ 3} = 1 →ₚ 2 ; 2 →ₚ 3 rflAll goals completed! 🐙

One last thing: for partial maps, it's convenient to introduce a notion of map inclusion, stating that all the entries in one map are also present in another. Lean already has notation for this — m₁ ⊆ m₂ — which we get by supplying a HasSubset instance.

def Subset {α β : Type} (m₁ m₂ : PartialMap α β) : Prop :=
  ∀ {a : α} {b : β}, m₁[a] = some b → m₂[a] = some b

instance {α β : Type} : HasSubset (PartialMap α β) where
  Subset := PartialMap.Subset

theorem subset_def {α β : Type} (m₁ m₂ : PartialMap α β) :
    m₁ ⊆ m₂ ↔ (∀ {a : α} {b : β}, m₁[a] = some b → m₂[a] = some b) := byα:Typeβ:Typem₁:PartialMap α βm₂:PartialMap α β⊢ m₁ ⊆ m₂ ↔ ∀ {a : α} {b : β}, m₁[a] = some b → m₂[a] = some b rflAll goals completed! 🐙

We can then show that map update preserves map inclusion, that is:

theorem update_subset {α β : Type} [BEq α] [LawfulBEq α] (m₁ m₂ : PartialMap α β) (a : α) (b : β)
    (h : m₁ ⊆ m₂) : (a →ₚ b ; m₁) ⊆ (a →ₚ b ; m₂) := byα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm₁:PartialMap α βm₂:PartialMap α βa:αb:βh:m₁ ⊆ m₂⊢ a →ₚ b ; m₁ ⊆ a →ₚ b ; m₂
  rw [subset_defα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm₁:PartialMap α βm₂:PartialMap α βa:αb:βh:∀ {a : α} {b : β}, m₁[a] = some b → m₂[a] = some b⊢ ∀ {a_1 : α} {b_1 : β}, (a →ₚ b ; m₁)[a_1] = some b_1 → (a →ₚ b ; m₂)[a_1] = some b_1] at h ⊢α:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm₁:PartialMap α βm₂:PartialMap α βa:αb:βh:∀ {a : α} {b : β}, m₁[a] = some b → m₂[a] = some b⊢ ∀ {a_1 : α} {b_1 : β}, (a →ₚ b ; m₁)[a_1] = some b_1 → (a →ₚ b ; m₂)[a_1] = some b_1
  intro a' b' hbα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm₁:PartialMap α βm₂:PartialMap α βa:αb:βh:∀ {a : α} {b : β}, m₁[a] = some b → m₂[a] = some ba':αb':βhb:(a →ₚ b ; m₁)[a'] = some b'⊢ (a →ₚ b ; m₂)[a'] = some b'
  by_cases ha : a = a'posα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm₁:PartialMap α βm₂:PartialMap α βa:αb:βh:∀ {a : α} {b : β}, m₁[a] = some b → m₂[a] = some ba':αb':βhb:(a →ₚ b ; m₁)[a'] = some b'ha:a = a'⊢ (a →ₚ b ; m₂)[a'] = some b'negα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm₁:PartialMap α βm₂:PartialMap α βa:αb:βh:∀ {a : α} {b : β}, m₁[a] = some b → m₂[a] = some ba':αb':βhb:(a →ₚ b ; m₁)[a'] = some b'ha:¬a = a'⊢ (a →ₚ b ; m₂)[a'] = some b'
  ·posα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm₁:PartialMap α βm₂:PartialMap α βa:αb:βh:∀ {a : α} {b : β}, m₁[a] = some b → m₂[a] = some ba':αb':βhb:(a →ₚ b ; m₁)[a'] = some b'ha:a = a'⊢ (a →ₚ b ; m₂)[a'] = some b' subst haposα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm₁:PartialMap α βm₂:PartialMap α βa:αb:βh:∀ {a : α} {b : β}, m₁[a] = some b → m₂[a] = some bb':βhb:(a →ₚ b ; m₁)[a] = some b'⊢ (a →ₚ b ; m₂)[a] = some b'
    rw [update_eqposα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm₁:PartialMap α βm₂:PartialMap α βa:αb:βh:∀ {a : α} {b : β}, m₁[a] = some b → m₂[a] = some bb':βhb:some b = some b'⊢ some b = some b'] at hb ⊢posα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm₁:PartialMap α βm₂:PartialMap α βa:αb:βh:∀ {a : α} {b : β}, m₁[a] = some b → m₂[a] = some bb':βhb:some b = some b'⊢ some b = some b'
    exact hbAll goals completed! 🐙
  ·negα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm₁:PartialMap α βm₂:PartialMap α βa:αb:βh:∀ {a : α} {b : β}, m₁[a] = some b → m₂[a] = some ba':αb':βhb:(a →ₚ b ; m₁)[a'] = some b'ha:¬a = a'⊢ (a →ₚ b ; m₂)[a'] = some b' rw [update_neq hanegα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm₁:PartialMap α βm₂:PartialMap α βa:αb:βh:∀ {a : α} {b : β}, m₁[a] = some b → m₂[a] = some ba':αb':βhb:m₁[a'] = some b'ha:¬a = a'⊢ m₂[a'] = some b'] at hb ⊢negα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm₁:PartialMap α βm₂:PartialMap α βa:αb:βh:∀ {a : α} {b : β}, m₁[a] = some b → m₂[a] = some ba':αb':βhb:m₁[a'] = some b'ha:¬a = a'⊢ m₂[a'] = some b'
    exact h hbAll goals completed! 🐙

end PartialMap

This property is quite useful for reasoning about languages with variable binding — e.g., the Simply Typed Lambda Calculus, which we will see in Type Systems, where maps are used to keep track of which program variables are defined in a given scope.

11.6. Deciding Propositions🔗

The Logic chapter's "Working with Decidable Properties" section explored the trade-offs between stating a claim as a boolean (of type Bool) and as a proposition (of type Prop). Here, we tie up a loose end from the start of this chapter, and along the way formalize decidability itself as a typeclass.

11.6.1. `Decidable` and Equality🔗

Recall from "Why We Need Typeclasses" that [0, 1].elemPoly 0's == is filled in automatically by Lean, in contrast to [0, 1].elemPolyEq Nat.beq 0, which is handed Nat.beq explicitly. It's tempting to assume Lean fills in that very Nat.beq function as the required BEq instance — but it doesn't. We can see this by asking Lean to synthesize the instance directly:

instBEqOfDecidableEq#synth BEq Nat

instBEqOfDecidableEq

What is this? Recall that BEq's only field is beq : α → α → Bool. instBEqOfDecidableEq builds a BEq α instance by setting beq a b := decide (a = b). What is decide? Let's see:

decide : (p : Prop) → [h : Decidable p] → Bool#check @decide

decide : (p : Prop) → [h : Decidable p] → Bool

We can see that decide takes a proposition (like a = b) and a proof that that proposition is decidable (i.e., Decidable (a = b)), and returns a Bool corresponding to the truth or falsehood of that proposition. What does it mean for a proposition to be Decidable? Here is its definition:

class inductive Decidable (p : Prop) where
  /-- Proves that `p` is decidable by supplying a proof of `¬ p` -/
  | isFalse (h : Not p) : Decidable p
  /-- Proves that `p` is decidable by supplying a proof of `p` -/
  | isTrue (h : p) : Decidable p

In other words, Decidable p expresses that a single proposition p can be settled one way or the other, computationally. (But "computationally" is caveated: later we'll see that classical axioms can manufacture a Decidable p instance that doesn't compute, and explain what that means.) Like HasTwo's one_neq_two field earlier in this chapter, Decidable.isTrue/Decidable.isFalse are proof-carrying: each one packages a proof — of p or of ¬p — alongside which case holds. instBEqOfDecidableEq references DecidableEq α, which means ∀ a b : α, Decidable (a = b), i.e., it's a shorthand for having one of these proof-carrying values for every equality proposition a = b in α.

Because decide (a = b) genuinely computes whether a = b holds, deriving BEq from DecidableEq this way also guarantees the result is LawfulBEq: the beq it produces is certain to agree with =. That guarantee is a fact about this instance, though, not something BEq demands of every instance — as the Maps section noted, beq's only obligation is to return some Bool, with no proof attached, unlike Decidable's constructors, whose whole point is to carry one. List.elemPoly's [BEq α] constraint is therefore the weakest assumption sufficient for a purely computational membership test: it doesn't require the caller to have decidable equality, or even a comparison that agrees with =, at all.

This is also why the chapter's earlier hand-written BEq Nat instance — the low-priority one built directly from Nat.beq — is a worse choice, not just a redundant one. Nat.beq does happen to agree with =, but nothing tells Lean that automatically: proving that hand-written instance is LawfulBEq would take its own separate induction on Nat.beq's recursive definition. Deriving BEq Nat from DecidableEq Nat sidesteps that work entirely — the proof of agreement is already carried by the Decidable instance, as we saw above — which is exactly why the standard library prefers it.

A Decidable instance also allows computation — branching — on the truth/falsehood of a proposition. You can write if p then a else b where p is a Prop and a and b are expressions of some type α. For example, we can write

"ok"#eval if 2 = 3 then "wrong" else "ok"

"ok"

Here, Lean synthesizes a Decidable instance for the proposition 2 = 3 which if (under the covers: ite) case-splits on, returning the then branch's result on matching the isTrue case and the else branch's result on the isFalse case. Asking Lean to synthesize the instance for this branched-on proposition shows which one gets used:

instDecidableEqNat 2 3#synth Decidable (2 = 3)

instDecidableEqNat 2 3

What is this? Let's see.

@[instance_reducible] def instDecidableEqNat : DecidableEq Nat :=
Nat.decEq#print instDecidableEqNat

@[instance_reducible] def instDecidableEqNat : DecidableEq Nat :=
Nat.decEq

Going one layer deeper ...

@[reducible] protected def Nat.decEq : (n m : Nat) → Decidable (n = m) :=
fun n m =>
  match h : n.beq m with
  | true => isTrue ⋯
  | false => isFalse ⋯#print Nat.decEq

@[reducible] protected def Nat.decEq : (n m : Nat) → Decidable (n = m) :=
fun n m =>
  match h : n.beq m with
  | true => isTrue ⋯
  | false => isFalse ⋯

So we have landed back at Nat.beq! It computes the result as a Bool and then Nat.decEq returns a proof of that computation's result in a Decidable instance. Above, our synthesized Decidable instance was for a particular equality, but it was just an application of instDecidableEqNat to a particular pair of Nats, so instDecidableEqNat will get used in the general case, too.

def nat_eq (m n : Nat) : Bool := if m = n then true else false

But if we slightly generalize this function, it will fail.

def eq {α : Type} (x y : α) : Bool := failed to synthesize instance of type class
  Decidable (x = y)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.if x = y then true else false

failed to synthesize instance of type class
  Decidable (x = y)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

Lean cannot synthesize a decidable equality instance for arbitrary types, and gives the same sort of error we saw at the beginning of this chapter when defining List.elemPoly. And the solution is the same too: Add an instance implicit.

def eq_dec {α : Type} [DecidableEq α] (x y : α) : Bool :=
  if x = y then true else false

Lean provides some automation for proofs of propositions that are Decidable, in the form of the decide tactic — not to be confused with the decide function from earlier. The function merely computes a Bool from a Decidable instance; the tactic instead closes a goal p outright, by computing that decide p reduces to true and invoking the connection between the two (made precise below):

example : 3 = 3 := by⊢ 3 = 3 decideAll goals completed! 🐙
example : 2 ≠ 3 := by⊢ 2 ≠ 3 decideAll goals completed! 🐙

The decide tactic rests on two lemmas relating a Decidable instance's underlying boolean to the proposition it decides: decide_eq_true_iff says decide p = true ↔ p, and decide_eq_false_iff_not says decide p = false ↔ ¬p. decide reduces the goal p to computing whether decide p evaluates to true, then invokes the first of these.

11.6.2. `Decidable` Beyond Equality🔗

instDecidableEqNat works automatically because Lean's core library derives it for us — but not every proposition we might want to decide comes with a ready-made instance. Sometimes we have to build one ourselves. Let's revisit the Logic chapter's "even" example to see what that looks like: it stated the property as both Nat.even (a Bool computation) and Nat.Even (a Prop), connected by reflection via Nat.even_bool_prop. We restate the relevant pieces here, in their own namespace (dropping the Nat. prefix), so they don't require that chapter's import:

namespace Reflection

def even (n : Nat) :=
  match n with
  | 0     => true
  | 1     => false
  | n + 2 => even n

theorem even_zero : even 0 = true := by⊢ even 0 = true rflAll goals completed! 🐙

theorem even_succ (n : Nat) :
    even (n + 1) = !(even n) := byn:Nat⊢ even (n + 1) = !even n
  induction n with
  | zero =>zero⊢ even (0 + 1) = !even 0
    rflAll goals completed! 🐙
  | succ n' ih =>succn':Natih:even (n' + 1) = !even n'⊢ even (n' + 1 + 1) = !even (n' + 1)
    rw [even,succn':Natih:even (n' + 1) = !even n'⊢ even n' = !even (n' + 1) ih,succn':Natih:even (n' + 1) = !even n'⊢ even n' = !!even n' Bool.not_notsuccn':Natih:even (n' + 1) = !even n'⊢ even n' = even n']All goals completed! 🐙

def double (n : Nat) : Nat :=
  match n with
  | 0    => 0
  | n' + 1 => double n' + 2

theorem double_zero : double 0 = 0 := by⊢ double 0 = 0 rflAll goals completed! 🐙

theorem double_succ (n : Nat) : double (n + 1) = double n + 2 := byn:Nat⊢ double (n + 1) = double n + 2 rflAll goals completed! 🐙

def Even x := ∃ n : Nat, x = double n

theorem even_double (k : Nat) : even (double k) = true := byk:Nat⊢ even (double k) = true
  induction k with
  | zero =>zero⊢ even (double 0) = true
    rw [double_zero,zero⊢ even 0 = true even_zerozero⊢ true = true]All goals completed! 🐙
  | succ n ih =>succn:Natih:even (double n) = true⊢ even (double (n + 1)) = true
    rw [double_succ,succn:Natih:even (double n) = true⊢ even (double n + 2) = true even_succ,succn:Natih:even (double n) = true⊢ (!even (double n + 1)) = true even_succ,succn:Natih:even (double n) = true⊢ (!!even (double n)) = true Bool.not_notsuccn:Natih:even (double n) = true⊢ even (double n) = true]succn:Natih:even (double n) = true⊢ even (double n) = true
    exact ihAll goals completed! 🐙

theorem even_double_exists (n : Nat) :
    ∃ (k : Nat), n = bif even n then double k else double k + 1 := byn:Nat⊢ ∃ k, n = bif even n then double k else double k + 1
  induction n with
  | zero =>zero⊢ ∃ k, 0 = bif even 0 then double k else double k + 1
    exists 0All goals completed! 🐙
  | succ n ih =>succn:Natih:∃ k, n = bif even n then double k else double k + 1⊢ ∃ k, n + 1 = bif even (n + 1) then double k else double k + 1
    obtain ⟨k, ih⟩ := ihsuccn:Natk:Natih:n = bif even n then double k else double k + 1⊢ ∃ k, n + 1 = bif even (n + 1) then double k else double k + 1
    rewrite [even_succsuccn:Natk:Natih:n = bif even n then double k else double k + 1⊢ ∃ k, n + 1 = bif !even n then double k else double k + 1]succn:Natk:Natih:n = bif even n then double k else double k + 1⊢ ∃ k, n + 1 = bif !even n then double k else double k + 1
    by_cases h : even nposn:Natk:Natih:n = bif even n then double k else double k + 1h:even n = true⊢ ∃ k, n + 1 = bif !even n then double k else double k + 1negn:Natk:Natih:n = bif even n then double k else double k + 1h:¬even n = true⊢ ∃ k, n + 1 = bif !even n then double k else double k + 1
    ·posn:Natk:Natih:n = bif even n then double k else double k + 1h:even n = true⊢ ∃ k, n + 1 = bif !even n then double k else double k + 1 exists kposn:Natk:Natih:n = bif even n then double k else double k + 1h:even n = true⊢ n + 1 = bif !even n then double k else double k + 1
      rw [hposn:Natk:Natih:n = bif true then double k else double k + 1h:even n = true⊢ n + 1 = bif !true then double k else double k + 1] at ih ⊢posn:Natk:Natih:n = bif true then double k else double k + 1h:even n = true⊢ n + 1 = bif !true then double k else double k + 1
      subst ihposk:Nath:even (bif true then double k else double k + 1) = true⊢ (bif true then double k else double k + 1) + 1 = bif !true then double k else double k + 1
      rflAll goals completed! 🐙
    ·negn:Natk:Natih:n = bif even n then double k else double k + 1h:¬even n = true⊢ ∃ k, n + 1 = bif !even n then double k else double k + 1 exists k + 1negn:Natk:Natih:n = bif even n then double k else double k + 1h:¬even n = true⊢ n + 1 = bif !even n then double (k + 1) else double (k + 1) + 1
      rw [Bool.not_eq_truenegn:Natk:Natih:n = bif even n then double k else double k + 1h:even n = false⊢ n + 1 = bif !even n then double (k + 1) else double (k + 1) + 1] at hnegn:Natk:Natih:n = bif even n then double k else double k + 1h:even n = false⊢ n + 1 = bif !even n then double (k + 1) else double (k + 1) + 1
      rw [hnegn:Natk:Natih:n = bif false then double k else double k + 1h:even n = false⊢ n + 1 = bif !false then double (k + 1) else double (k + 1) + 1] at ih ⊢negn:Natk:Natih:n = bif false then double k else double k + 1h:even n = false⊢ n + 1 = bif !false then double (k + 1) else double (k + 1) + 1
      subst ihnegk:Nath:even (bif false then double k else double k + 1) = false⊢ (bif false then double k else double k + 1) + 1 = bif !false then double (k + 1) else double (k + 1) + 1
      rw [Bool.cond_false,negk:Nath:even (bif false then double k else double k + 1) = false⊢ double k + 1 + 1 = bif !false then double (k + 1) else double (k + 1) + 1 Bool.not_false,negk:Nath:even (bif false then double k else double k + 1) = false⊢ double k + 1 + 1 = bif true then double (k + 1) else double (k + 1) + 1 Bool.cond_truenegk:Nath:even (bif false then double k else double k + 1) = false⊢ double k + 1 + 1 = double (k + 1)]negk:Nath:even (bif false then double k else double k + 1) = false⊢ double k + 1 + 1 = double (k + 1)
      rflAll goals completed! 🐙

theorem even_iff_Even {n : Nat} : even n = true ↔ Even n where
  mp h := byn:Nath:even n = true⊢ Even n
    have ⟨k, hk⟩ := even_double_exists nn:Nath:even n = truek:Nathk:n = bif even n then double k else double k + 1⊢ Even n
    rw [h,n:Nath:even n = truek:Nathk:n = bif true then double k else double k + 1⊢ Even n Bool.cond_truen:Nath:even n = truek:Nathk:n = double k⊢ Even n] at hkn:Nath:even n = truek:Nathk:n = double k⊢ Even n
    subst hkk:Nath:even (double k) = true⊢ Even (double k)
    exists kAll goals completed! 🐙
  mpr h := byn:Nath:Even n⊢ even n = true
    obtain ⟨k, hk⟩ := hn:Natk:Nathk:n = double k⊢ even n = true
    subst hkk:Nat⊢ even (double k) = true
    exact even_double kAll goals completed! 🐙

even_iff_Even (our copied-in version of Nat.even_bool_prop from Logic) is the kind of iff-shaped reflection lemma we need: the standard library's decidable_of_decidable_of_iff carries a Decidable instance across any p ↔ q — from Decidable p to Decidable q. Applying it here is all it takes to build a custom Decidable (Even n) instance:

instance (n : Nat) : Decidable (Even n) :=
  decidable_of_decidable_of_iff even_iff_Even

Its type shows exactly what it needs and produces:

@decidable_of_decidable_of_iff : {p q : Prop} → [Decidable p] → (p ↔ q) → Decidable q#check @decidable_of_decidable_of_iff

@decidable_of_decidable_of_iff : {p q : Prop} → [Decidable p] → (p ↔ q) → Decidable q

Given a Decidable p instance and a proof p ↔ q, it produces a Decidable q. Here, p is even n = true — already decidable, since equality of Bools always is — and q is Even n; even_iff_Even supplies the connecting p ↔ q. Under the hood, it checks whether p holds (using the Decidable p instance it was given) and uses the iff to turn that proof of p or ¬p into one of q or ¬q, which it then packages with Decidable.isTrue/Decidable.isFalse.

Now we can complete such proofs by computation, using the decide tactic, and use Even in if expressions.

if Even 2 then "is even" else "is odd" : String#check if Even 2 then "is even" else "is odd"
def odd (n : Nat) : Bool :=
  if Even n then false else true
example : Even 2 := by⊢ Even 2 decideAll goals completed! 🐙
example : Even 4 := by⊢ Even 4 decideAll goals completed! 🐙
example : Even 6 := by⊢ Even 6 decideAll goals completed! 🐙
example : Even 100 := by⊢ Even 100 decideAll goals completed! 🐙
example : ¬ Even 101 := by⊢ ¬Even 101 decideAll goals completed! 🐙
example : ∀ n < 10, Even (2 * n) := by⊢ ∀ (n : Nat), n < 10 → Even (2 * n) decideAll goals completed! 🐙
example : ∀ n < 10, Even (2 * n) ∧ ¬ Even (2 * n + 1) := by⊢ ∀ (n : Nat), n < 10 → Even (2 * n) ∧ ¬Even (2 * n + 1) decideAll goals completed! 🐙

11.6.3. `Decidable` and Classical Logic🔗

Computable instances like instDecidableEqNat and the one we built for Even are only half the story. Lean is also often used in applications where we don't care about computability, such as pure mathematics. The Logic chapter's "Classical vs. Constructive Logic" section already showed how Classical.choice lets Lean prove p ∨ ¬ p for an arbitrary proposition p via Classical.em, something no computable procedure could do in general. The same axiom lets Lean manufacture a Decidable p instance for arbitrary p, letting us write a function for arbitrary equality that no decision procedure could actually compute:

open scoped Classical in
noncomputable def eq {α : Type} (x y : α) := if x = y then true else false

set_option pp.all true in
def Reflection.eq : {α : Type} → (x y : α) → Bool :=
fun {α : Type} (x y : α) => @ite.{1} Bool (@Eq.{1} α x y) (Classical.propDecidable (@Eq.{1} α x y)) Bool.true Bool.false#print eq

def Reflection.eq : {α : Type} → (x y : α) → Bool :=
fun {α : Type} (x y : α) => @ite.{1} Bool (@Eq.{1} α x y) (Classical.propDecidable (@Eq.{1} α x y)) Bool.true Bool.false

But we have indicated to Lean, using the noncomputable keyword and Classical namespace, that we are not interested in computation. What is happening in the background is that this allows typeclass synthesis to find the scoped instance Classical.propDecidable, which makes use of the axiom of choice to provide a proof that all propositions are classically decidable. This sort of definition is suitable for use with proofs, but is not allowed to be used in conjunction with computational features of Lean such as the decide tactic or the #eval command.

To see this concretely, consider Maps section's TotalMap.update_same exercise, proves that updating a map with the value already stored there changes nothing, for a fully generic α constrained only by [BEq α] [LawfulBEq α]. If you use by_cases h : a = a' in your proof and then do #print axioms update_same you will see Classical.choice in the list. If you additionally require [DecidableEq α] along with [BEq α] and [LawfulBEq α], though, then you bring a genuine decision procedure for equality in scope, and by_cases splits on it directly rather than falling back to the excluded middle. Try it out!

end Reflection

Source revision: e85fe77, committed 2026-10-06 21:16 UTC