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 := rfl

theorem List.elem_nat_cons (n m : Nat) (ms : List Nat) :
    (m :: ms).elemNat n = bif n == m then true else elemNat n ms := rfl

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 := rfl

theorem List.elemPoly_cons {α : Type} [BEq α] (x y : α) (ys : List α) :
    (y :: ys).elemPoly x = bif x == y then true else elemPoly x ys := rfl

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 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.

Note to developers (xhalo32)

This is technically incorrect, the instance BEq Nat, which comes from DecidableEq, does not contain Nat.beq. You can see in proofs of List.elem_nat versus List.elem_poly_eq versus List.elem_poly and how Nat.beq and == play different roles.

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

end DefaultValueScratch

Now for the marking: we need to tell Lean that DefaultValue is the sort of structure it should search for automatically, the way it needs to for List.headOrEx's defaultValue argument. 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α:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ 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α:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ DefaultValue.value = 0 rflAll goals completed! 🐙
example : DefaultValue.value = (-1 : Int) := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ DefaultValue.value = -1 rflAll goals completed! 🐙
example : DefaultValue.value = (none : Option Bool) := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ DefaultValue.value = none rflAll goals completed! 🐙
example : DefaultValue.value = (none : Option (List Nat)) := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ DefaultValue.value = none rflAll goals completed! 🐙
example : ([] : List Nat).headOr = 0 := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ [].headOr = 0 rflAll goals completed! 🐙
example : ([] : List Int).headOr = -1 := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ [].headOr = -1 rflAll goals completed! 🐙
example : ([] : List (Option Bool)).headOr = none := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ [].headOr = none rflAll goals completed! 🐙
example : ([] : List (Option Bool)).headOr = none := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ [].headOr = none rflAll goals completed! 🐙

Synthesis infers instances we could have specified explicitly:

example : instDefaultValueNat.value = (0 : Nat) := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ DefaultValue.value = 0 rflAll goals completed! 🐙
example : instDefaultValueInt.value = (-1 : Int) := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ DefaultValue.value = -1 rflAll goals completed! 🐙
example : instDefaultValueOption.value = (none : Option Nat) := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ 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 1 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. For Nat, that instance is:

Note to developers (@ionathanch)

What is (priority := low)? Do the students need to know why that's there?

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

This is the instance Lean supplies for [BEq α] when List.elemPoly is called on a List Nat — no different from Lean choosing instDefaultValueNat for DefaultValue.value earlier when it was equated with (1 : Nat).

Exercise★(List.elem_poly_eq_elem_nat)

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

theorem 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
  solution!(
  induction ms with
  | nil =>niln:Nat⊢ elemPoly n [] = elemNat n []
    rewrite [List.elemPoly_nil,niln:Nat⊢ false = elemNat n [] List.elem_nat_nilniln:Nat⊢ false = false]niln:Nat⊢ false = false
    rflAll goals completed! 🐙
  | cons hd tl ih =>consn:Nathd:Nattl:List Natih:elemPoly n tl = elemNat n tl⊢ elemPoly n (hd :: tl) = elemNat n (hd :: tl)
    rewrite [List.elemPoly_cons,consn:Nathd:Nattl:List Natih:elemPoly n tl = elemNat n tl⊢ (bif n == hd then true else elemPoly n tl) = elemNat n (hd :: tl) List.elem_nat_cons,consn:Nathd:Nattl:List Natih:elemPoly n tl = elemNat n tl⊢ (bif n == hd then true else elemPoly n tl) = bif n == hd then true else elemNat n tl ihconsn:Nathd:Nattl:List Natih:elemPoly n tl = elemNat n tl⊢ (bif n == hd then true else elemNat n tl) = bif n == hd then true else elemNat n tl]consn:Nathd:Nattl:List Natih:elemPoly n tl = elemNat n tl⊢ (bif n == hd then true else elemNat n tl) = bif n == hd then true else elemNat n tl
    rflAll 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α:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ 1 ≠ 2 intro contraα:Typeβ:TypedefaultValue:αn:Natm:Natcontra:1 = 2⊢ False; contradictionAll 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.

Note to developers (Niklas Halonen @xhalo32)

HasThree needs either grading attributes or manual grading

Exercise★(HasThree)

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
  one_neq_three : one ≠ three
  two_neq_three : two ≠ three

instance : HasThree Nat where
  one := 1
  two := 2
  three := 3
  one_neq_two := solution!(byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ 1 ≠ 2 intro contraα:Typeβ:TypedefaultValue:αn:Natm:Natcontra:1 = 2⊢ False; contradictionAll goals completed! 🐙)
  one_neq_three := solution!(byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ 1 ≠ 3 intro contraα:Typeβ:TypedefaultValue:αn:Natm:Natcontra:1 = 3⊢ False; contradictionAll goals completed! 🐙)
  two_neq_three := solution!(byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ 2 ≠ 3 intro contraα:Typeβ:TypedefaultValue:αn:Natm:Natcontra:2 = 3⊢ False; contradictionAll goals completed! 🐙)

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α:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ ∀ (x : Nat), Nat.add 0 x = x liaAll goals completed! 🐙
  right_id := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ ∀ (x : Nat), x.add 0 = x liaAll goals completed! 🐙
  assoc := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ ∀ (x y z : Nat), x.add (y.add z) = (x.add y).add z liaAll goals completed! 🐙

Note to developers (Niklas Halonen @xhalo32)

Need to come up with a way to grade the data-carrying instances. What makes this more complicated is that the op is fixed but the id is not.

Exercise★(NatMonoidMul)

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

instance : Monoid Nat where
  op := Nat.mul
  id := solution!(1)
  left_id := solution!(byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ ∀ (x : Nat), Nat.mul 1 x = x liaAll goals completed! 🐙)
  right_id := solution!(byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ ∀ (x : Nat), x.mul 1 = x liaAll goals completed! 🐙)
  assoc := solution!(byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ ∀ (x y z : Nat), x.mul (y.mul z) = (x.mul y).mul z liaAll goals completed! 🐙)

Exercise★(ListMonoidAppend)

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:

instance {α : Type} : Monoid (List α) where
  op := List.append
  id := solution!([])
  left_id := solution!(byα✝:Typeβ:TypedefaultValue:α✝n:Natm:Natα:Type⊢ ∀ (x : List α), [].append x = x simpAll goals completed! 🐙)
  right_id := solution!(byα✝:Typeβ:TypedefaultValue:α✝n:Natm:Natα:Type⊢ ∀ (x : List α), x.append [] = x simpAll goals completed! 🐙)
  assoc := solution!(byα✝:Typeβ:TypedefaultValue:α✝n:Natm:Natα:Type⊢ ∀ (x y z : List α), x.append (y.append z) = (x.append y).append z simpAll goals completed! 🐙)

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 however, because these are class instances instead of normal structures, we prepend our tuple by the @ symbol. 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)

instance : Group Int where
  op := Int.add
  id := solution!(0)
  inv := solution!(Int.neg)
  left_id := solution!(byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ ∀ (x : Int), Int.add 0 x = x liaAll goals completed! 🐙)
  right_id := solution!(byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ ∀ (x : Int), x.add 0 = x liaAll goals completed! 🐙)
  assoc := solution!(byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ ∀ (x y z : Int), x.add (y.add z) = (x.add y).add z liaAll goals completed! 🐙)
  left_inv := solution!(byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ ∀ (x : Int), x.neg.add x = 0 liaAll goals completed! 🐙)
  right_inv := solution!(byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ ∀ (x : Int), x.add x.neg = 0 liaAll goals completed! 🐙)

The study of groups is called group theory and is a rich area of mathematics. Here, we will only prove a handful of its simplest results:

Note to developers (Daniel Sainati @dsainati1)

This also prints weird.

Exercise★(InverseUnique)

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

theorem 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
  solution!
    ext xα:Typeg₁:Group αg₂:Group αh:OpSet.op = OpSet.opx:α⊢ Group.inv x = Group.inv x
    rw [← g₁.right_id (Group.inv x),α:Typeg₁:Group αg₂:Group αh:OpSet.op = OpSet.opx:α⊢ Group.inv x = Group.inv x ⊗ Monoid.id ← g₁.right_inv xα:Typeg₁:Group αg₂:Group αh:OpSet.op = OpSet.opx:α⊢ Group.inv x = Group.inv x ⊗ x ⊗ Group.inv x]α:Typeg₁:Group αg₂:Group αh:OpSet.op = OpSet.opx:α⊢ Group.inv x = Group.inv x ⊗ x ⊗ Group.inv x
    rw [g₁.assoc,α:Typeg₁:Group αg₂:Group αh:OpSet.op = OpSet.opx:α⊢ Group.inv x = (Group.inv x ⊗ x) ⊗ Group.inv x h,α:Typeg₁:Group αg₂:Group αh:OpSet.op = OpSet.opx:α⊢ Group.inv x = (Group.inv x ⊗ x) ⊗ Group.inv x g₂.left_inv,α:Typeg₁:Group αg₂:Group αh:OpSet.op = OpSet.opx:α⊢ Group.inv x = Monoid.id ⊗ Group.inv x g₂.left_idα:Typeg₁:Group αg₂:Group αh:OpSet.op = OpSet.opx:α⊢ Group.inv x = Group.inv x]All goals completed! 🐙

Note to developers (Daniel Sainati @dsainati1)

Taking suggestions for additional simple group theory theorems to prove here.

Exercise★(IdentityUnique)

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

theorem 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
  solution!
    rw [← right_id xα:Typeinst✝:Monoid αx:αhₗ:∀ (y : α), x ⊗ y = y⊢ x ⊗ id = id]α:Typeinst✝:Monoid αx:αhₗ:∀ (y : α), x ⊗ y = y⊢ x ⊗ id = id
    exact hₗ idAll goals completed! 🐙

Exercise★★(InverseInverse)

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

theorem 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
  solution!
    calc x
      _ = g.id ⊗ x          := byα:Typeg:Group αx:αy:αz:αh₁:Group.inv x = yh₂:Group.inv y = z⊢ x = Monoid.id ⊗ x rw [g.left_id xα:Typeg:Group αx:αy:αz:αh₁:Group.inv x = yh₂:Group.inv y = z⊢ x = x]All goals completed! 🐙
      _ = (g.inv y ⊗ y) ⊗ x := byα:Typeg:Group αx:αy:αz:αh₁:Group.inv x = yh₂:Group.inv y = z⊢ Monoid.id ⊗ x = (Group.inv y ⊗ y) ⊗ x rw [g.left_inv yα:Typeg:Group αx:αy:αz:αh₁:Group.inv x = yh₂:Group.inv y = z⊢ Monoid.id ⊗ x = Monoid.id ⊗ x]All goals completed! 🐙
      _ = g.inv y ⊗ (y ⊗ x) := byα:Typeg:Group αx:αy:αz:αh₁:Group.inv x = yh₂:Group.inv y = z⊢ (Group.inv y ⊗ y) ⊗ x = Group.inv y ⊗ y ⊗ x rw [g.assocα:Typeg:Group αx:αy:αz:αh₁:Group.inv x = yh₂:Group.inv y = z⊢ (Group.inv y ⊗ y) ⊗ x = (Group.inv y ⊗ y) ⊗ x]All goals completed! 🐙
      _ = z ⊗ (y ⊗ x)       := byα:Typeg:Group αx:αy:αz:αh₁:Group.inv x = yh₂:Group.inv y = z⊢ Group.inv y ⊗ y ⊗ x = z ⊗ y ⊗ x rw [h₂α:Typeg:Group αx:αy:αz:αh₁:Group.inv x = yh₂:Group.inv y = z⊢ z ⊗ y ⊗ x = z ⊗ y ⊗ x]All goals completed! 🐙
      _ = z ⊗ (g.inv x ⊗ x) := byα:Typeg:Group αx:αy:αz:αh₁:Group.inv x = yh₂:Group.inv y = z⊢ z ⊗ y ⊗ x = z ⊗ Group.inv x ⊗ x rw [h₁α:Typeg:Group αx:αy:αz:αh₁:Group.inv x = yh₂:Group.inv y = z⊢ z ⊗ y ⊗ x = z ⊗ y ⊗ x]All goals completed! 🐙
      _ = z ⊗ g.id          := byα:Typeg:Group αx:αy:αz:αh₁:Group.inv x = yh₂:Group.inv y = z⊢ z ⊗ Group.inv x ⊗ x = z ⊗ Monoid.id rw [g.left_invα:Typeg:Group αx:αy:αz:αh₁:Group.inv x = yh₂:Group.inv y = z⊢ z ⊗ Monoid.id = z ⊗ Monoid.id]All goals completed! 🐙
      _ = z                 := byα:Typeg:Group αx:αy:αz:αh₁:Group.inv x = yh₂:Group.inv y = z⊢ z ⊗ Monoid.id = z rw [g.right_idα:Typeg:Group αx:αy:αz:αh₁:Group.inv x = yh₂:Group.inv y = z⊢ z = z]All goals completed! 🐙

theorem inv_inv {α : Type} {g : Group α} (x : α) : g.inv (g.inv x) = x := byα:Typeg:Group αx:α⊢ Group.inv (Group.inv x) = x
  solution!
    symmα:Typeg:Group αx:α⊢ x = Group.inv (Group.inv x); apply inv_inv' (y := g.inv x)h₁α:Typeg:Group αx:α⊢ Group.inv x = Group.inv xh₂α:Typeg:Group αx:α⊢ Group.inv (Group.inv x) = Group.inv (Group.inv x)α:Typeg:Group αx:α⊢ Group α <;>h₁α:Typeg:Group αx:α⊢ Group.inv x = Group.inv xh₂α:Typeg:Group αx:α⊢ Group.inv (Group.inv x) = Group.inv (Group.inv x)α:Typeg:Group αx:α⊢ Group α rflAll goals completed! 🐙

end Algebra

11.5. API and Encapsulation🔗

Note to developers (Niklas Halonen @xhalo32)

Here, we should tie back the story from early chapters about characterizing lemmas and definition unfolding. When unfolding a definition directly without characterizing lemmas, the implementation details are exposed. When downstream code can depend on implementation details of upstream library code, it makes it more difficult for the upstream library to evolve.

Explain the following items:

What is API and how does it relate to typeclasses
What is encapsulation: public and private API
- Function definitions and one-field structures are encapsulation boundaries
- Definitions and structures are usually private, characterizing lemmas are public
- Constructors of inductives are public
- Mention public, private keywords and that we don't use them on the course?
- One can mostly ignore proof terms due to proof irrelevance

Here is an example where the proof term is blocking a rewrite. The solution is to simplify it away.

-- set_option pp.proofs true in
example {n m : Nat} {a : Fin n} {b : Fin m} (h₁ : n = m) (h₂ : a.val = b.val) :
    a = ⟨b.val, h₁ ▸ b.isLt⟩ := byα:Typeβ:TypedefaultValue:αn✝:Natm✝:Natn:Natm:Nata:Fin nb:Fin mh₁:n = mh₂:↑a = ↑b⊢ a = ⟨↑b, ⋯⟩
  -- ext
  -- dsimp only
  rw [Tactic `rewrite` failed: motive is not type correct:
  fun _a => a = ⟨_a, ⋯⟩
Error: Application type mismatch: The argument
  h✝
has type
  _a < m
but is expected to have type
  ↑b < m
in the application
  Eq.ndrec (motive := fun {m} => ∀ {b : Fin m}, ↑a = ↑b → ↑b < m → ↑b < n) (fun {b} h₂ h => h) h₁ h₂ h✝

Explanation: The rewrite tactic rewrites an expression 'e' using an equality 'a = b' by the following process. First, it looks for all 'a' in 'e'. Second, it tries to abstract these occurrences of 'a' to create a function 'm := fun _a => ...', called the *motive*, with the property that 'm a' is definitionally equal to 'e'. Third, we observe that 'congrArg' implies that 'm a = m b', which can be used with lemmas such as 'Eq.mpr' to change the goal. However, if 'e' depends on specific properties of 'a', then the motive 'm' might not typecheck.

Possible solutions: use rewrite's 'occs' configuration option to limit which occurrences are rewritten, or use 'simp' or 'conv' mode, which have strategies for certain kinds of dependencies (these tactics can handle proofs and 'Decidable' instances whose types depend on the rewritten term, and 'simp' can apply user-defined '@[congr]' theorems as well).

α β:TypedefaultValue:αn✝ m✝ n m:Nata:Fin nb:Fin mh₁:n = mh₂:↑a = ↑b⊢ a = ⟨↑b, ⋯⟩← h₂α:Typeβ:TypedefaultValue:αn✝:Natm✝:Natn:Natm:Nata:Fin nb:Fin mh₁:n = mh₂:↑a = ↑b⊢ a = ⟨↑b, ⋯⟩]α:Typeβ:TypedefaultValue:αn✝:Natm✝:Natn:Natm:Nata:Fin nb:Fin mh₁:n = mh₂:↑a = ↑b⊢ a = ⟨↑b, ⋯⟩

11.6. 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.

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.6.1. Key and Value Types🔗

To define maps, we first need a type for the keys that we will use to index into our maps and a type for the values the maps return. In this section, we'll use the type variable α for the type of keys and β for values. In addition to BEq, which we have already seen, our key type α requires instances of the ReflBEq and LawfulBEq typeclasses:

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

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

These classes refine BEq, specifying that (==) is reflexive and coincides with proposition equality =.

In general, we place no constraints on the value type β.

11.6.2. 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 are going to build 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, rather than just as "equivalent" list structures. This simplifies proofs that use maps.

Instead of using functions directly, 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 : α → β

namespace TotalMap

In order to declare a default value of β we will use the Inhabited typeclass, which is the standard library's implementation of our DefaultValue example from above:

The function TotalMap.empty yields an empty total map, given a default element; this map always returns the default element when applied to any key.

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

These types and implicit instances are now available automatically to all the definitions in this section.

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.6.2.1. Getting Elements🔗

While TotalMaps happen to be implemented as functions under the hood, we would prefer not to expose this fact in its public interface. Accordingly, we define new operations for querying and updating mappings. We define a function get for getting the value associated with a key playing the role that find played for the Lists chapter's list-based maps,

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

/-- This exposes implementation-specific details of `TotalMap`.
  Avoid using this outside the `TotalMap` namespace. -/
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α:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ emptyNatMap.get 2 = 0 rflAll goals completed! 🐙

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

example {n : Nat} : emptyNatMap.get n = 0 := byα:Typeβ:TypedefaultValue:αn✝:Natm:Natn:Nat⊢ emptyNatMap.get n = 0
  rewrite [get_def,α:Typeβ:TypedefaultValue:αn✝:Natm:Natn:Nat⊢ emptyNatMap.inner n = 0 emptyNatMap,α:Typeβ:TypedefaultValue:αn✝:Natm:Natn:Nat⊢ ∅.inner n = 0 empty_def,α:Typeβ:TypedefaultValue:αn✝:Natm:Natn:Nat⊢ { inner := fun x => default }.inner n = 0 Nat.default_eq_zeroα:Typeβ:TypedefaultValue:αn✝:Natm:Natn:Nat⊢ { inner := fun x => 0 }.inner n = 0]α:Typeβ:TypedefaultValue:αn✝:Natm:Natn: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.

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.

To make element-getting more convenient, let's define notation so we can write emptyNatMap[2] rather than emptyNatMap.get. 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.

Note to developers (Niklas Halonen @xhalo32)

A reason I can come up with why we use a notation typeclass (in library code) over a plain notation is that it makes it possible (for a downstream consumer) to write open scoped MyGetElem instead of writing open scoped TotalMap and open scoped PartialMap individually. This wouldn't be a good sell if →ₜ and →ₚ are scoped notations, but they're currently global.

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'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.

Don't worry about following the mechanism in detail — the macro_rules and the app_unexpander below are minor technicalities. However, if you do wish to learn more, Chapter 5 and 6 of Metaprogramming in Lean 4 contain more detail.

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.

Note to developers (Benjamin Pierce @bcpierce00)

Make sure we've really explained open scoped somewhere...

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α:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ emptyNatMap[1] = default rflAll goals completed! 🐙

example {n : Nat} : emptyNatMap[n] = 0 := byα:Typeβ:TypedefaultValue:αn✝:Natm:Natn:Nat⊢ emptyNatMap[n] = 0
  rw [getElem_def,α:Typeβ:TypedefaultValue:αn✝:Natm:Natn:Nat⊢ emptyNatMap.get n = 0 get_def,α:Typeβ:TypedefaultValue:αn✝:Natm:Natn:Nat⊢ emptyNatMap.inner n = 0 emptyNatMap,α:Typeβ:TypedefaultValue:αn✝:Natm:Natn:Nat⊢ ∅.inner n = 0 empty_def,α:Typeβ:TypedefaultValue:αn✝:Natm:Natn:Nat⊢ { inner := fun x => default }.inner n = 0 Nat.default_eq_zeroα:Typeβ:TypedefaultValue:αn✝:Natm:Natn: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] := rfl

example {n : Nat} : emptyNatMap.get n = emptyNatMap[n] := byα:Typeβ:TypedefaultValue:αn✝:Natm:Natn: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 anyways).

11.6.2.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.

Note to developers (Benjamin Pierce @bcpierce00)

Should we introduce this notation earlier? (Are there good places to use it earlier?)

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

/-- This exposes implementation-specific details of `TotalMap`.
  Avoid using this outside the `TotalMap` namespace.
  Prefer `update_apply` if possible. -/
theorem update_def {α β : Type} [BEq α] (m : TotalMap α β) (a : α) (b : β) :
  a →ₜ b ; m = { inner := fun a' => bif a == a' then b else m[a'] } := byα:Typeβ:Typeinst✝:BEq αm:TotalMap α βa:αb:β⊢ a →ₜ b ; m = { inner := fun a' => bif a == a' then b else m[a'] } rflAll goals completed! 🐙

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α:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ exampleMap = exampleMap' rflAll goals completed! 🐙
example : exampleMap' = exampleMap'' := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ exampleMap' = exampleMap'' rflAll goals completed! 🐙

example : exampleMap'["bar"] = true := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ exampleMap'["bar"] = true rflAll goals completed! 🐙
example : exampleMap'["foo"] = true := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ exampleMap'["foo"] = true rflAll goals completed! 🐙
example : exampleMap'["quux"] = false := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ 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α:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ exampleMap'["bar"] = true
  rw [exampleMap',α:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ ("bar" →ₜ true ; "foo" →ₜ true)["bar"] = true update_apply,α:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ (bif "bar" == "bar" then true else ("foo" →ₜ true)["bar"]) = true BEq.rfl,α:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ (bif true then true else ("foo" →ₜ true)["bar"]) = true `cond_true` has been deprecated: Use `Bool.cond_true` instead

Note: The updated constant has a different type:
  ∀ {α : Sort u} {a b : α}, (bif true then a else b) = a
instead of
  ∀ {α : Sort u_1} (a b : α), (bif true then a else b) = acond_trueα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ true = true]All goals completed! 🐙

example : exampleMap'["foo"] = true := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ exampleMap'["foo"] = true
  rw [exampleMap',α:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ ("bar" →ₜ true ; "foo" →ₜ true)["foo"] = true update_apply,α:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ (bif "bar" == "foo" then true else ("foo" →ₜ true)["foo"]) = true show ("bar" == "foo") = false byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ exampleMap'["foo"] = true simpAll goals completed! 🐙, `cond_false` has been deprecated: Use `Bool.cond_false` instead

Note: The updated constant has a different type:
  ∀ {α : Sort u} {a b : α}, (bif false then a else b) = b
instead of
  ∀ {α : Sort u_1} (a b : α), (bif false then a else b) = bcond_falseα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ ("foo" →ₜ true)["foo"] = true]α:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ ("foo" →ₜ true)["foo"] = true
  rw [update_apply,α:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ (bif "foo" == "foo" then true else ∅["foo"]) = true BEq.rfl,α:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ (bif true then true else ∅["foo"]) = true `cond_true` has been deprecated: Use `Bool.cond_true` instead

Note: The updated constant has a different type:
  ∀ {α : Sort u} {a b : α}, (bif true then a else b) = a
instead of
  ∀ {α : Sort u_1} (a b : α), (bif true then a else b) = acond_trueα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ true = true]All goals completed! 🐙

example : exampleMap'["quux"] = false := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ exampleMap'["quux"] = false
  rw [exampleMap',α:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ ("bar" →ₜ true ; "foo" →ₜ true)["quux"] = false update_apply,α:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ (bif "bar" == "quux" then true else ("foo" →ₜ true)["quux"]) = false show ("bar" == "quux") = false byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ exampleMap'["quux"] = false simpAll goals completed! 🐙, `cond_false` has been deprecated: Use `Bool.cond_false` instead

Note: The updated constant has a different type:
  ∀ {α : Sort u} {a b : α}, (bif false then a else b) = b
instead of
  ∀ {α : Sort u_1} (a b : α), (bif false then a else b) = bcond_falseα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ ("foo" →ₜ true)["quux"] = false]α:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ ("foo" →ₜ true)["quux"] = false
  rw [update_apply,α:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ (bif "foo" == "quux" then true else ∅["quux"]) = false show ("foo" == "quux") = false byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ exampleMap'["quux"] = false rflAll goals completed! 🐙, `cond_false` has been deprecated: Use `Bool.cond_false` instead

Note: The updated constant has a different type:
  ∀ {α : Sort u} {a b : α}, (bif false then a else b) = b
instead of
  ∀ {α : Sort u_1} (a b : α), (bif false then a else b) = bcond_falseα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ ∅["quux"] = false]α:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ ∅["quux"] = false
  rw [empty_def,α:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ { inner := fun x => default }["quux"] = false getElem_def,α:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ { inner := fun x => default }.get "quux" = false get_def,α:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ { inner := fun x => default }.inner "quux" = false Bool.default_boolα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ { inner := fun x => false }.inner "quux" = false]All goals completed! 🐙

When we use maps in later volumes, we'll need several fundamental facts about how they behave.

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.)

First, 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! 🐙

Notice that in the example exampleMap'["quux"] = false the last rewrite is effectively just getElem_empty.

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_def,α:Typeβ:Typeinst✝¹:BEq αinst✝:ReflBEq αm:TotalMap α βa:αb:β⊢ { inner := fun a' => bif a == a' then b else m[a'] }[a] = b getElem_def,α:Typeβ:Typeinst✝¹:BEq αinst✝:ReflBEq αm:TotalMap α βa:αb:β⊢ { inner := fun a' => bif a == a' then b else m[a'] }.get a = b get_defα:Typeβ:Typeinst✝¹:BEq αinst✝:ReflBEq αm:TotalMap α βa:αb:β⊢ { inner := fun a' => bif a == a' then b else m[a'] }.inner a = b]α:Typeβ:Typeinst✝¹:BEq αinst✝:ReflBEq αm:TotalMap α βa:αb:β⊢ { inner := fun a' => bif a == a' then b else m[a'] }.inner a = b
  dsimp onlyα:Typeβ:Typeinst✝¹:BEq αinst✝:ReflBEq αm:TotalMap α βa:αb:β⊢ (bif a == a then b else m[a]) = b -- reduces `{ inner := ... }.inner` so that we get a subterm that looks like `a == a`
  rw [BEq.rfl,α:Typeβ:Typeinst✝¹:BEq αinst✝:ReflBEq αm:TotalMap α βa:αb:β⊢ (bif true then b else m[a]) = b `cond_true` has been deprecated: Use `Bool.cond_true` instead

Note: The updated constant has a different type:
  ∀ {α : Sort u} {a b : α}, (bif true then a else b) = a
instead of
  ∀ {α : Sort u_1} (a b : α), (bif true then a else b) = acond_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 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₂]
  solution!
    rw [update_def,α:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa₁:αa₂:αh:a₁ ≠ a₂b:β⊢ { inner := fun a' => bif a₁ == a' then b else m[a'] }[a₂] = m[a₂] getElem_def,α:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa₁:αa₂:αh:a₁ ≠ a₂b:β⊢ { inner := fun a' => bif a₁ == a' then b else m[a'] }.get a₂ = m[a₂] get_defα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa₁:αa₂:αh:a₁ ≠ a₂b:β⊢ { inner := fun a' => bif a₁ == a' then b else m[a'] }.inner a₂ = m[a₂]]α:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa₁:αa₂:αh:a₁ ≠ a₂b:β⊢ { inner := fun a' => bif a₁ == a' then b else m[a'] }.inner a₂ = m[a₂]
    dsimp onlyα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa₁:αa₂:αh:a₁ ≠ a₂b:β⊢ (bif a₁ == a₂ then b else m[a₂]) = m[a₂]
    rw [beq_false_of_ne h,α:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa₁:αa₂:αh:a₁ ≠ a₂b:β⊢ (bif false then b else m[a₂]) = m[a₂] `cond_false` has been deprecated: Use `Bool.cond_false` instead

Note: The updated constant has a different type:
  ∀ {α : Sort u} {a b : α}, (bif false then a else b) = b
instead of
  ∀ {α : Sort u_1} (a b : α), (bif false then a else b) = bcond_falseα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa₁:αa₂:αh:a₁ ≠ a₂b:β⊢ m[a₂] = m[a₂]]All 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! 🐙

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

example : "bar" →ₜ true ; "foo" →ₜ true = "foo" →ₜ true ; "bar" →ₜ true := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ "bar" →ₜ true ; "foo" →ₜ true = "foo" →ₜ true ; "bar" →ₜ true
  ext aα:Typeβ:TypedefaultValue:αn:Natm:Nata:String⊢ ("bar" →ₜ true ; "foo" →ₜ true)[a] = ("foo" →ₜ true ; "bar" →ₜ true)[a]
  by_cases h : "bar" = aposα:Typeβ:TypedefaultValue:αn:Natm:Nata:Stringh:"bar" = a⊢ ("bar" →ₜ true ; "foo" →ₜ true)[a] = ("foo" →ₜ true ; "bar" →ₜ true)[a]negα:Typeβ:TypedefaultValue:αn:Natm:Nata:Stringh:¬"bar" = a⊢ ("bar" →ₜ true ; "foo" →ₜ true)[a] = ("foo" →ₜ true ; "bar" →ₜ true)[a]
  ·posα:Typeβ:TypedefaultValue:αn:Natm:Nata:Stringh:"bar" = a⊢ ("bar" →ₜ true ; "foo" →ₜ true)[a] = ("foo" →ₜ true ; "bar" →ₜ true)[a] subst hposα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ ("bar" →ₜ true ; "foo" →ₜ true)["bar"] = ("foo" →ₜ true ; "bar" →ₜ true)["bar"]
    rw [update_eq,posα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ true = ("foo" →ₜ true ; "bar" →ₜ true)["bar"] update_neq (show "foo" ≠ "bar" byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ "bar" →ₜ true ; "foo" →ₜ true = "foo" →ₜ true ; "bar" →ₜ true simpAll goals completed! 🐙), update_eqposα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ true = true]All goals completed! 🐙
  ·negα:Typeβ:TypedefaultValue:αn:Natm:Nata:Stringh:¬"bar" = a⊢ ("bar" →ₜ true ; "foo" →ₜ true)[a] = ("foo" →ₜ true ; "bar" →ₜ true)[a] simp only [update_apply]negα:Typeβ:TypedefaultValue:αn:Natm:Nata: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 hnegα:Typeβ:TypedefaultValue:αn:Natm:Nata: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]]negα:Typeβ:TypedefaultValue:αn:Natm:Nata: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 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
  solution!
    ext a'α:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa:αa':α⊢ (a →ₜ m[a] ; m)[a'] = m[a']
    by_cases h : a = a'posα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa:αa':αh:a = a'⊢ (a →ₜ m[a] ; m)[a'] = m[a']negα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa:αa':αh:¬a = a'⊢ (a →ₜ m[a] ; m)[a'] = m[a']
    ·posα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa:αa':αh:a = a'⊢ (a →ₜ m[a] ; m)[a'] = m[a'] subst hposα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa:α⊢ (a →ₜ m[a] ; m)[a] = m[a]
      simpAll goals completed! 🐙
    ·negα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa:αa':αh:¬a = a'⊢ (a →ₜ m[a] ; m)[a'] = m[a'] simp [update_neq h]All 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 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
  solution!
    ext a'α:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa:αb₁:βb₂:βa':α⊢ (a →ₜ b₂ ; a →ₜ b₁ ; m)[a'] = (a →ₜ b₂ ; m)[a']
    by_cases h : a = a'posα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa:αb₁:βb₂:βa':αh:a = a'⊢ (a →ₜ b₂ ; a →ₜ b₁ ; m)[a'] = (a →ₜ b₂ ; m)[a']negα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa:αb₁:βb₂:βa':αh:¬a = a'⊢ (a →ₜ b₂ ; a →ₜ b₁ ; m)[a'] = (a →ₜ b₂ ; m)[a']
    ·posα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa:αb₁:βb₂:βa':αh:a = a'⊢ (a →ₜ b₂ ; a →ₜ b₁ ; m)[a'] = (a →ₜ b₂ ; m)[a'] subst hposα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa:αb₁:βb₂:β⊢ (a →ₜ b₂ ; a →ₜ b₁ ; m)[a] = (a →ₜ b₂ ; m)[a]
      simpAll goals completed! 🐙
    ·negα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa:αb₁:βb₂:βa':αh:¬a = a'⊢ (a →ₜ b₂ ; a →ₜ b₁ ; m)[a'] = (a →ₜ b₂ ; m)[a'] simp [update_neq h]All goals completed! 🐙

Note to developers (mwhicks1, NOW)

Two things the Rocq source says here have been dropped.

Rocq frames this case analysis around destruct (eqb_spec x1 x2), which "simultaneously performs case analysis on the result of String.eqb x1 x2 and generates hypotheses about the equality (in the sense of =) of x1 and x2" — the boolean/propositional reflection idiom. The paragraph above replaces that with by_cases/subst, which is what the Lean proof uses. But reflection is what the Reflection section below is about, so the two may want to be connected rather than have one silently displace the other.

Rocq then says "With the example in chapter IndProp as a template, use String.eqb_spec to prove ...". That cross-reference is dropped, since it is unclear what the Lean IndProp chapter will end up containing. Revisit later.

Note to developers (Niklas Halonen @xhalo32)

Regarding reflection: I have used show ("bar" == "foo") = false by simp in some of the above sections which would be good to explain in more detail in the reflection section. The BEq instance is derived from DecidableEq in instBEqOfDecidableEq. All of the following proofs of the fact use decide internally.

-- set_option trace.Meta.synthInstance true in
-- set_option trace.Meta.whnf true in
example : ("bar" == "foo") = false := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ ("bar" == "foo") = false
  simpAll goals completed! 🐙 -- goes through a simproc `String.reduceBEq` which reduces to `decide`
example : ("bar" == "foo") = false := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ ("bar" == "foo") = false
  rflAll goals completed! 🐙 -- ends up calling `decide ("bar" = "foo")`
example : ("bar" == "foo") = false := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ ("bar" == "foo") = false
  decideAll goals completed! 🐙

Similarly, 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.

Note to developers (mwhicks1, NOW)

Rocq says "Similarly, use String.eqb_spec to prove ..."; the instruction to use a specific lemma is dropped here for the same reason as in the note above.

Exercise★★★(update_permute)

theorem 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
  solution!
    ext aα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa₁:αa₂:αb₁:βb₂:βh:a₁ ≠ a₂a:α⊢ (a₁ →ₜ b₁ ; a₂ →ₜ b₂ ; m)[a] = (a₂ →ₜ b₂ ; a₁ →ₜ b₁ ; m)[a]
    by_cases h₁ : a₁ = aposα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa₁:αa₂:αb₁:βb₂:βh:a₁ ≠ a₂a:αh₁:a₁ = a⊢ (a₁ →ₜ b₁ ; a₂ →ₜ b₂ ; m)[a] = (a₂ →ₜ b₂ ; a₁ →ₜ b₁ ; m)[a]negα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa₁:αa₂:αb₁:βb₂:βh:a₁ ≠ a₂a:αh₁:¬a₁ = a⊢ (a₁ →ₜ b₁ ; a₂ →ₜ b₂ ; m)[a] = (a₂ →ₜ b₂ ; a₁ →ₜ b₁ ; m)[a]
    ·posα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa₁:αa₂:αb₁:βb₂:βh:a₁ ≠ a₂a:αh₁:a₁ = a⊢ (a₁ →ₜ b₁ ; a₂ →ₜ b₂ ; m)[a] = (a₂ →ₜ b₂ ; a₁ →ₜ b₁ ; m)[a] subst h₁posα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa₁:αa₂:αb₁:βb₂:βh:a₁ ≠ a₂⊢ (a₁ →ₜ b₁ ; a₂ →ₜ b₂ ; m)[a₁] = (a₂ →ₜ b₂ ; a₁ →ₜ b₁ ; m)[a₁]
      rw [update_eq,posα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa₁:αa₂:αb₁:βb₂:βh:a₁ ≠ a₂⊢ b₁ = (a₂ →ₜ b₂ ; a₁ →ₜ b₁ ; m)[a₁] update_neq h.symm,posα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa₁:αa₂:αb₁:βb₂:βh:a₁ ≠ a₂⊢ b₁ = (a₁ →ₜ b₁ ; m)[a₁] update_eqposα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa₁:αa₂:αb₁:βb₂:βh:a₁ ≠ a₂⊢ b₁ = b₁]All goals completed! 🐙
    ·negα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa₁:αa₂:αb₁:βb₂:βh:a₁ ≠ a₂a:αh₁:¬a₁ = a⊢ (a₁ →ₜ b₁ ; a₂ →ₜ b₂ ; m)[a] = (a₂ →ₜ b₂ ; a₁ →ₜ b₁ ; m)[a] rw [update_neq h₁negα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa₁:αa₂:αb₁:βb₂:βh:a₁ ≠ a₂a:αh₁:¬a₁ = a⊢ (a₂ →ₜ b₂ ; m)[a] = (a₂ →ₜ b₂ ; a₁ →ₜ b₁ ; m)[a]]negα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa₁:αa₂:αb₁:βb₂:βh:a₁ ≠ a₂a:αh₁:¬a₁ = a⊢ (a₂ →ₜ b₂ ; m)[a] = (a₂ →ₜ b₂ ; a₁ →ₜ b₁ ; m)[a]
      by_cases h₂ : a₂ = aposα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa₁:αa₂:αb₁:βb₂:βh:a₁ ≠ a₂a:αh₁:¬a₁ = ah₂:a₂ = a⊢ (a₂ →ₜ b₂ ; m)[a] = (a₂ →ₜ b₂ ; a₁ →ₜ b₁ ; m)[a]negα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa₁:αa₂:αb₁:βb₂:βh:a₁ ≠ a₂a:αh₁:¬a₁ = ah₂:¬a₂ = a⊢ (a₂ →ₜ b₂ ; m)[a] = (a₂ →ₜ b₂ ; a₁ →ₜ b₁ ; m)[a]
      ·posα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa₁:αa₂:αb₁:βb₂:βh:a₁ ≠ a₂a:αh₁:¬a₁ = ah₂:a₂ = a⊢ (a₂ →ₜ b₂ ; m)[a] = (a₂ →ₜ b₂ ; a₁ →ₜ b₁ ; m)[a] subst h₂posα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa₁:αa₂:αb₁:βb₂:βh:a₁ ≠ a₂h₁:¬a₁ = a₂⊢ (a₂ →ₜ b₂ ; m)[a₂] = (a₂ →ₜ b₂ ; a₁ →ₜ b₁ ; m)[a₂]
        rw [update_eq,posα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa₁:αa₂:αb₁:βb₂:βh:a₁ ≠ a₂h₁:¬a₁ = a₂⊢ b₂ = (a₂ →ₜ b₂ ; a₁ →ₜ b₁ ; m)[a₂] update_eqposα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa₁:αa₂:αb₁:βb₂:βh:a₁ ≠ a₂h₁:¬a₁ = a₂⊢ b₂ = b₂]All goals completed! 🐙
      ·negα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa₁:αa₂:αb₁:βb₂:βh:a₁ ≠ a₂a:αh₁:¬a₁ = ah₂:¬a₂ = a⊢ (a₂ →ₜ b₂ ; m)[a] = (a₂ →ₜ b₂ ; a₁ →ₜ b₁ ; m)[a] rw [update_neq h₂,negα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa₁:αa₂:αb₁:βb₂:βh:a₁ ≠ a₂a:αh₁:¬a₁ = ah₂:¬a₂ = a⊢ m[a] = (a₂ →ₜ b₂ ; a₁ →ₜ b₁ ; m)[a] update_neq h₂,negα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa₁:αa₂:αb₁:βb₂:βh:a₁ ≠ a₂a:αh₁:¬a₁ = ah₂:¬a₂ = a⊢ m[a] = (a₁ →ₜ b₁ ; m)[a] update_neq h₁negα:Typeβ:Typeinst✝¹:BEq αinst✝:LawfulBEq αm:TotalMap α βa₁:αa₂:αb₁:βb₂:βh:a₁ ≠ a₂a:αh₁:¬a₁ = ah₂:¬a₂ = a⊢ m[a] = m[a]]All goals completed! 🐙

Note to developers

The Rocq source also has getElem_empty (originally apply_empty) and update_eq as (optional) exercises; here they are worked examples, since update_eq was already presented that way. Reconsider if this section is rebalanced.

end TotalMap

11.6.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.

/--
A key-value pair with `↦` syntax.
-/
@[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 _ := rfl

end TotalMap

Here are a couple of examples using the new notation:

example : ({ "bar" ↦ true, "foo" ↦ true }) = "bar" →ₜ true ; "foo" →ₜ true ; ∅ := rfl

example : ({ "foo" ↦ true } : TotalMap String Bool)["foo"] = true := rfl

example : ({ 1 ↦ 2, 1 ↦ 3 } : TotalMap Nat Nat)[1] = 2 := rfl

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.6.4. Partial Maps🔗

Note to developers (Niklas Halonen @xhalo32)

We should spend some time discussing differences between the inductive approach in Lists.lean and the approach here. The inductive approach could be made polymorphic and proven to be equivalent with partial maps (I believe), so the point is not that the maps are extensionally different. A question (that I don't have an answer to) is then: what makes the new partial map better?

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
  /-- The underlying total map. Lean always generates a public projection for a structure
    field, so `inner` is technically accessible, but it isn't part of the intended interface:
    use `PartialMap.toTotal` instead, so there's exactly one sanctioned way to get at it. -/
  inner : TotalMap α (Option β)

/- Note that this 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. -/
instance {α β : Type} : EmptyCollection (PartialMap α β) where
  emptyCollection := { inner := ∅ }

namespace PartialMap

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

/-- This exposes implementation-specific details of `PartialMap`.
  Avoid using this outside the `PartialMap` namespace. -/
theorem toTotal_def {α β : Type} (m : PartialMap α β) : m.toTotal = m.inner := byα:Typeβ:Typem:PartialMap α β⊢ m.toTotal = m.inner rflAll goals completed! 🐙

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

theorem getElem_def {α β : Type} (m : PartialMap α β) (a : α) : m[a] = m.toTotal[a] := rfl

def emptyNatMap : PartialMap Nat Nat where
  inner := ∅

example : emptyNatMap[1] = default := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ emptyNatMap[1] = default rflAll goals completed! 🐙

example {n : Nat} : emptyNatMap[n] = none := byα:Typeβ:TypedefaultValue:αn✝:Natm:Natn:Nat⊢ emptyNatMap[n] = none
  rw [getElem_def,α:Typeβ:TypedefaultValue:αn✝:Natm:Natn:Nat⊢ emptyNatMap.toTotal[n] = none toTotal_def,α:Typeβ:TypedefaultValue:αn✝:Natm:Natn:Nat⊢ emptyNatMap.inner[n] = none emptyNatMapα:Typeβ:TypedefaultValue:αn✝:Natm:Natn:Nat⊢ { inner := ∅ }.inner[n] = none]α:Typeβ:TypedefaultValue:αn✝:Natm:Natn:Nat⊢ { inner := ∅ }.inner[n] = none
  dsimp onlyα:Typeβ:TypedefaultValue:αn✝:Natm:Natn:Nat⊢ ∅[n] = none
  rw [TotalMap.getElem_def,α:Typeβ:TypedefaultValue:αn✝:Natm:Natn:Nat⊢ ∅.get n = none TotalMap.get_def,α:Typeβ:TypedefaultValue:αn✝:Natm:Natn:Nat⊢ ∅.inner n = none TotalMap.empty_def,α:Typeβ:TypedefaultValue:αn✝:Natm:Natn:Nat⊢ { inner := fun x => default }.inner n = none Option.default_eq_noneα:Typeβ:TypedefaultValue:αn✝:Natm:Natn:Nat⊢ { inner := fun x => none }.inner n = none]All goals completed! 🐙

@[simp]
theorem toTotal_eq_getElem {α β : Type} (m : PartialMap α β) (a : α) :
    m.toTotal[a] = m[a] := rfl

We previously defined TotalMap.get so that users can retrieve elements from a TotalMap in a manner independent of its actual implementation, which is a function stored in TotalMap.inner. We follow a similar principle with PartialMaps, and define PartialMap.toTotal to be the public API counterpart to PartialMap.inner.

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].

Updating a partial map at a key means storing a some value there. To update, 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

Next, we provide some fundamental properties about toTotal:

@[simp]
theorem toTotal_empty {α β : Type} : (∅ : PartialMap α β).toTotal = (∅ : TotalMap α (Option β)) := rfl

@[simp]
theorem toTotal_update {α β : Type} [BEq α] (m : PartialMap α β) (a : α) (b : β) :
    (a →ₚ b ; m).toTotal = a →ₜ some b ; m.toTotal := rfl

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

example : (2 →ₚ 3)[2] = some 3 := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ (2 →ₚ 3)[2] = some 3
  rw [getElem_def,α:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ (2 →ₚ 3).toTotal[2] = some 3 toTotal_update,α:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ (2 →ₜ some 3 ; ∅.toTotal)[2] = some 3 toTotal_empty,α:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ (2 →ₜ some 3)[2] = some 3 TotalMap.update_eqα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ 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α:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ (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α:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ (2 →ₚ 3)[2] = some 3
  simpAll goals completed! 🐙

example : examplePmap["Post"] = none := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ examplePmap["Post"] = none
  rw [examplePmapα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ ("Church" →ₚ true ; "Turing" →ₚ false)["Post"] = none]α:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ ("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 _ := rfl

example : { 1 ↦ 2, 2 ↦ 3 } = 1 →ₚ 2 ; 2 →ₚ 3 := rfl

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) := .rfl

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.7. Reflection🔗

namespace Reflection

In this section, we will make use of some definitions and theorems about natural numbers that we discussed and proved in previous chapters; copy your solutions to those problems here:

namespace Nat

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
  solution!
    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 = Nat.double n

We've seen two different ways of expressing logical claims in Lean: with booleans (of type Bool), and with propositions (of type Prop).

Here are the key differences between Bool and Prop:

⠀	`Bool`	`Prop`
decidable?	yes	no
useable with `match`?	yes	no
works with `rewrite` tactic?	no	yes

The crucial difference between the two worlds is decidability. Every (closed) Lean expression of type Bool can be simplified in a finite number of steps to either true or false — i.e., there is a terminating mechanical procedure for deciding whether or not it is true.

This means that, for example, the type Nat → Bool is inhabited only by functions that, given a Nat, always yield either true or false in finite time; and this, in turn, means (by a standard computability argument) that there is no function in Nat → Bool that checks whether a given number is the code of a terminating Turing machine.

By contrast, the type Prop includes both decidable and undecidable mathematical propositions; in particular, the type Nat → Prop does contain functions representing properties like "the nth Turing machine halts." The second row in the table follows directly from this essential difference. To evaluate a pattern match (or conditional) on a boolean, we need to know whether the scrutinee evaluates to true or false; this only works for Bool, not Prop.

The third row highlights an important practical difference: equality functions like Nat.beq that return a boolean cannot be used directly to justify rewriting with the rewrite tactic; propositional equality is required for this. Since Prop includes both decidable and undecidable properties, we have two options when we want to formalize a property that happens to be decidable: we can express it either as a boolean computation or as a function into Prop.

As an example, we can write

example : even 42 := rfl

or that there exists some k such that 42 = double k.

example : Even 42 := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ Even 42 exists 21All goals completed! 🐙

Of course, it would be deeply strange if these two characterizations of evenness did not describe the same set of natural numbers!

Fortunately, they do! To prove this, we first need two helper lemmas.

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! 🐙

Exercise★★★(even_double_exists)

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
  solution!
    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 : Nat.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 [`cond_false` has been deprecated: Use `Bool.cond_false` instead

Note: The updated constant has a different type:
  ∀ {α : Sort u} {a b : α}, (bif false then a else b) = b
instead of
  ∀ {α : Sort u_1} (a b : α), (bif false then a else b) = bcond_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 `cond_true` has been deprecated: Use `Bool.cond_true` instead

Note: The updated constant has a different type:
  ∀ {α : Sort u} {a b : α}, (bif true then a else b) = a
instead of
  ∀ {α : Sort u_1} (a b : α), (bif true then a else b) = acond_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! 🐙

Now the main theorem:

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 `cond_true` has been deprecated: Use `Bool.cond_true` instead

Note: The updated constant has a different type:
  ∀ {α : Sort u} {a b : α}, (bif true then a else b) = a
instead of
  ∀ {α : Sort u_1} (a b : α), (bif true then a else b) = acond_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! 🐙

end Nat

In view of this theorem, we can say that the boolean computation Nat.even n is reflected in the truth of the proposition ∃ (k : Nat), n = Nat.double k.

Similarly, to state that two numbers n and m are equal, we can say either

that n == m returns true, or
that n = m

Again, these two notions are equivalent:

Note to developers

This proof is from the typeclass version, which makes more sense if maps are included — CGH

example (n₁ n₂ : Nat) : n₁ == n₂ ↔ n₁ = n₂ := beq_iff_eq

So what should we do in situations where some claim could be formalized as either a proposition or a boolean computation? Which should we choose?

In general, both can be useful. Which we choose has to do with the computational nature of Lean's core language, which is designed so that every function it expresses is total, and by default computable unless we explicit indicate otherwise. As an example, consider trying to write a function α → α → Bool checking for equality on an arbitrary type:

Note to developers

dsainati12 days ago We use regular if for the first time here. It is probably necessary to explain at this point what if is and how it differs from bif.

👍 1 berberman1 day ago Should we clarify the difference between = and ==? Observably if and bif can possibly accept both as the condition because of Coe or DecidableEq instances, which IMO could be confusing.

Probably we can talk a bit about the coercion system in this file as well, since Coe could be an example of typeclasses, so long as if we ignore the outParam thing...

chenson20181 day ago I definitely intended for this to cover = versus ==. Maps uses LawfulBEq (which says = and == coincide). If that will now appear here it's a good place to give some more detail?

rogerburtonpatel1 day ago I think right after this part on decidability is good. It's a hefty chunk of information already, so keeping distinct ideas distinct is more likely than not a good call.

Note to developers

@dsainati - commenting this out for the same reason as above

@ionathanch - this needs to be put back in, right? nat_eq continues on referring to this

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

Lean will complain here that it cannot find an instance of Decidable. This typeclass

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

is the way that we express in Lean that a given proposition is decidable. This is the generalization of our observation that Nat.even_iff_Even was reflecting a proof between boolean and propositional equality. In fact, we can use this theorem to directly construct a Decidable instance.

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

Now we are able to complete such proofs by computation using the decide tactic:

example : Nat.Even 2 := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ Nat.Even 2 decideAll goals completed! 🐙
example : Nat.Even 4 := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ Nat.Even 4 decideAll goals completed! 🐙
example : Nat.Even 6 := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ Nat.Even 6 decideAll goals completed! 🐙
example : Nat.Even 100 := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ Nat.Even 100 decideAll goals completed! 🐙
example : ¬ Nat.Even 101 := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ ¬Nat.Even 101 decideAll goals completed! 🐙
example : ∀ n < 10, Nat.Even (2 * n) := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ ∀ (n : Nat), n < 10 → Nat.Even (2 * n) decideAll goals completed! 🐙
example : ∀ n < 10, Nat.Even (2 * n) ∧ ¬ Nat.Even (2 * n + 1) := byα:Typeβ:TypedefaultValue:αn:Natm:Nat⊢ ∀ (n : Nat), n < 10 → Nat.Even (2 * n) ∧ ¬Nat.Even (2 * n + 1) decideAll goals completed! 🐙

In general, Lean will try to use typeclass synthesis with Decidable in order to determine when it is appropriate to use Prop and Bool interchangeably. For instance, while our example eq failed above while trying to use propositional equality = in the condition of an if statement, we are allowed to write

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

Why is this allowed? It is precisely because equality of natural numbers is decidable, and Lean makes use of this fact. If we print this definition with notation unset, we would find that it is using instDecidableEqNat:

set_option pp.all true in
def Reflection.nat_eq : (m n : Nat) → Bool :=
fun (m n : Nat) => @ite.{1} Bool (@Eq.{1} Nat m n) (instDecidableEqNat m n) Bool.true Bool.false#print nat_eq

which proves that this equality is decidable.

This is only half the story however: while Lean's core theory enables this computation, Lean is also often used in applications where we don't care about computability, such as pure mathematics. In particular, it is possible to write a function for arbitrary equality:

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

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.

11.8. TODO🔗

Note to developers (Benjamin Pierce @bcpierce00)

Needs finishing...

Note to developers

Below are some stray examples from IndProp. Decidable only carries the proposition and not the boolean, so one direction of reflect_iff is easily translated, but the other is a bit different. I list some theorems below but you should Loogle and see if that's what you want. Some the the proofs can be a bit advanced if you follow core, or otherwise a bit circular. — CGH

decidable_of_bool {a : Prop} (b : Bool) : (b = true ↔ a) → Decidable a#check decidable_of_bool

example {p : Prop} (b : Bool) (h : b = true ↔ p) : Decidable p := byα:Typeβ:TypedefaultValue:αn:Natm:Natp:Propb:Boolh:b = true ↔ p⊢ Decidable p
  by_cases hb : bposα:Typeβ:TypedefaultValue:αn:Natm:Natp:Propb:Boolh:b = true ↔ phb:b = true⊢ Decidable pnegα:Typeβ:TypedefaultValue:αn:Natm:Natp:Propb:Boolh:b = true ↔ phb:¬b = true⊢ Decidable p
  ·posα:Typeβ:TypedefaultValue:αn:Natm:Natp:Propb:Boolh:b = true ↔ phb:b = true⊢ Decidable p apply isTrueposα:Typeβ:TypedefaultValue:αn:Natm:Natp:Propb:Boolh:b = true ↔ phb:b = true⊢ p
    simp [← h, hb]All goals completed! 🐙
  ·negα:Typeβ:TypedefaultValue:αn:Natm:Natp:Propb:Boolh:b = true ↔ phb:¬b = true⊢ Decidable p apply isFalsenegα:Typeβ:TypedefaultValue:αn:Natm:Natp:Propb:Boolh:b = true ↔ phb:¬b = true⊢ ¬p
    simp [← h, hb]All goals completed! 🐙

decide_eq_false_iff_not {p : Prop} {x✝ : Decidable p} : decide p = false ↔ ¬p#check decide_eq_false_iff_not
decide_eq_true_iff {p : Prop} [Decidable p] : decide p = true ↔ p#check decide_eq_true_iff

Note to developers

I'm not sure what part of the signature here is important to translate. Is the point the Bool/Prop mismatch? — CGH

declaration uses `sorry`example {α : Type} (x : α) [BEq α] [LawfulBEq α] (xs : List α)
    (neq : xs.filter (x == ·) ≠ []) : x ∈ xs := byα✝:Typeβ:TypedefaultValue:α✝n:Natm:Natα:Typex:αinst✝¹:BEq αinst✝:LawfulBEq αxs:List αneq:List.filter (fun x_1 => x == x_1) xs ≠ []⊢ x ∈ xs
  sorryAll goals completed! 🐙

Note to developers

Burtonpatel: Some more examples would be good. It might be good to start with Nat and then move to the Indprop ones. This is a short chapter, so 5-6 well-chosen, informative exercises could easily fit.

end Reflection

Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC