A practical difference between Props and Types in Lean

Recently, I've been playing around with Lean, a proof assistant (and technically a programming language) that got a lot of publicity in the past year from a few mathematicians like Kevin Buzzard and Sébastien Gouëzel.

In Lean, there are lots of definitions that treat Props and Types uniformly (that is, the definition takes an argument whose type is Sort l for an arbitrary l), but there are places where something can only be a Prop, and places where something can only be a Type. And in those cases, there are often two parallel definitions which do essentially the same thing, except that one is for Props and one is for Types. So what's different between the cases where we can have a uniform definition for both, and the cases where we need two separate definitions?

In this post, I want to give a small concrete example of a case where Props and Types don't behave the same in Lean. You can follow along using this link to all the code in this post in the Lean playground if you want.

Proof irrelevance

One of the few fundamental differences between Props and Types is that we have proof irrelevance for Props. Concretely, this shows up in Lean as the following theorem, which is available from the core library:

#check @proof_irrel
-- proof_irrel : ∀ {a : Prop} (h₁ h₂ : a), h₁ = h₂

This theorem says that, given a proposition a and two proofs h₁ and h₂ of a, the two proofs are always equal in the eyes of Lean.

This might seem innocuous, but let's combine it with another theorem from the core library:

#check @congr_arg
-- congr_arg : ∀ {α : Sort u_1} {β : Sort u_2} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂

This theorem (which is uniform between Props and Types, because its parameters are Sorts), says that when we apply a function f to equal arguments (a₁ and a₂, in this case), the results are equal. This is a totally reasonable theorem. If it wasn't true, f would not be a well-defined function.

But together, these two theorems say that whenever we have a function from a Prop to a Type, that function has to be a constant function. The result can't depend on the structure of the proof that we feed to the function. It can only depend on the existence of a proof, and it must always be the same result.

The confusing thing is that when we have a function from a Prop to another Prop, we are allowed to pattern-match on the structure of the input proof, so it looks like the function's result can depend on the details of the proof. But as long as we produce a proof of the target Prop in all code branches of the function, the result is always equal, by proof irrelevance! So the function is still a constant function, even though it doesn't look like one.

Example: flowers are pretty

Ok, I said I would give a concrete example, but so far it's been pretty theoretical.

Let's say we want to talk about a world with flowers in it. And in this world, the defining characteristic of a flower is its name, so we might write the following type definition to capture it:

inductive flower : Type
| grow : forall (name : string), flower

There's just one constructor for flowers, flower.grow, which takes an arbitrary string for the name of the flower, and returns the corresponding flower.

We also want to talk about whether this is a pretty world, and let's say it's pretty iff there exists a flower. We can capture this property by having a constructor with the same type signature as the constructor for flowers:

inductive pretty : Prop
| grow : forall (name : string), pretty

Apart from having a different type name (flower vs pretty), the only difference is that flower is a Type, and pretty is a Prop. We could justify this by saying that flower is a noun, a thing that the world can have, whereas pretty is an adjective, a thing that the world can be.

Let's prove that there exist two different flowers:

def rose : flower := flower.grow "rose"
def violet : flower := flower.grow "violet"

theorem not_equal_strings : "rose" ≠ "violet" :=
theorem not_equal_flowers : rose ≠ violet :=
  not_equal_strings ∘ flower.grow.inj

On the other hand, any two proofs that the world is pretty are equal. Lean believes that roses and violets are pretty in exactly the same way:

def pretty_rose : pretty := pretty.grow "rose"
def pretty_violet : pretty := pretty.grow "violet"

theorem equal_proofs : pretty_rose = pretty_violet :=
  proof_irrel _ _

So, we can easily write a function from the Type to the Prop:

def forget_difference : flower → pretty
| (flower.grow name) := pretty.grow name

But Lean will complain if we try to go in the other direction:

def cant_remember_difference : pretty → flower
| (pretty.grow name) := flower.grow name
-- error: recursor 'pretty.dcases_on' can only eliminate into Prop

Does this mean that the world of Props is a black hole and that we can never escape back into the world of Types? No! There are a few allowed ways to write a function which takes a proof of a Prop and returns a value of a Type, such as:

As an example of the first point, we could write the following function, which is totally fine:

def pick_one : pretty → flower :=
  fun _, flower.grow "thistle"

This function just ignores the pretty flower that we give it, and instead gives us back a pretty thistle, always. Another workaround is to turn flower into a Prop, by using nonempty:

#print nonempty
inductive nonempty : Sort u → Prop
nonempty.intro : ∀ {α : Sort u}, α → nonempty α

This turns any Type α into the proposition that "there exists a value of type α". So, we can write the following function, which doesn't completely ignore the pretty flower we give it:

def look_at_this_one : pretty → (nonempty flower)
| (pretty.grow name) := nonempty.intro (flower.grow name)

In effect, wrapping a Type in nonempty gives us a version of the Type where we promise to not actually depend on the value, only on its existence, and the rest of the type system enforces that promise. Once we make that promise, we're allowed to depend on the structure of the input proof.

Under the hood

So, concretely, how does the type system enforce the promise that we can only depend on the structure of a proof when we're producing a proof of a Prop? To answer this, we have to look at the fundamental, low-level building blocks that Lean provides for us when we write an inductive definition. For the example above, we can see that Lean automatically defines a whole bunch of stuff just from the definitions of flower and pretty:

#print prefix flower
flower : Type
flower.cases_on : Π {C : flower → Sort l} (n : flower), (Π (name : string), C (flower.grow name)) → C n
flower.grow : string → flower
flower.grow.inj : ∀ {name name_1 : string}, flower.grow name = flower.grow name_1 → name = name_1
flower.grow.inj_arrow : Π {name name_1 : string}, flower.grow name = flower.grow name_1 → Π ⦃P : Sort l⦄, (name = name_1 → P) → P
flower.grow.inj_eq : ∀ {name name_1 : string}, flower.grow name = flower.grow name_1 = (name = name_1)
flower.grow.sizeof_spec : ∀ (name : string), flower.sizeof (flower.grow name) = 1 + sizeof name
flower.has_sizeof_inst : has_sizeof flower
flower.no_confusion : Π {P : Sort l} {v1 v2 : flower}, v1 = v2 → flower.no_confusion_type P v1 v2
flower.no_confusion_type : Sort l → flower → flower → Sort l
flower.rec : Π {C : flower → Sort l}, (Π (name : string), C (flower.grow name)) → Π (n : flower), C n
flower.rec_on : Π {C : flower → Sort l} (n : flower), (Π (name : string), C (flower.grow name)) → C n
flower.sizeof : flower → ℕ

#print prefix pretty
pretty : Prop
pretty.cases_on : ∀ {C : Prop}, pretty → (string → C) → C
pretty.dcases_on : ∀ {C : pretty → Prop} (n : pretty), (∀ (name : string), C _) → C n
pretty.drec : ∀ {C : pretty → Prop}, (∀ (name : string), C _) → ∀ (n : pretty), C n
pretty.drec_on : ∀ {C : pretty → Prop} (n : pretty), (∀ (name : string), C _) → C n
pretty.grow : string → pretty
pretty.rec : ∀ {C : Prop}, (string → C) → pretty → C
pretty.rec_on : ∀ {C : Prop}, pretty → (string → C) → C

In both cases, Lean generates lots of stuff, but it all boils down to just three things, and everything else is defined from these three things:

The type signatures for the eliminators look a bit weird, so let's break them down, starting with pretty.rec because it's simpler:

pretty.rec : ∀ {C : Prop}, (string → C) → pretty → C

For example, we could use pretty.rec to try (and fail) again to write the "obvious" function pretty → flower:

def cant_remember : pretty → flower :=
    flower  -- The target type
    (fun name, flower.grow name)  -- The callback for `pretty.grow`
-- error: type mismatch

It doesn't look like it, but the eliminator flower.rec follows the same pattern:

flower.rec : Π {C : flower → Sort l}, (Π (name : string), C (flower.grow name)) → Π (n : flower), C n

For example, we can try (and succeed) to use flower.rec to write the obvious function flower → pretty:

def can_forget : flower → pretty :=
    (fun _, pretty)  -- The target type is `pretty` for all flowers
    (fun name, pretty.grow name)  -- The callback for `flower.grow`