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 `Prop`

s and `Type`

s 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 `Prop`

s and one is for `Type`

s. 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 `Prop`

s and `Type`

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

One of the few fundamental differences between `Prop`

s and `Type`

s is that we have *proof irrelevance* for `Prop`

s. 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 `Prop`

s and `Type`

s, because its parameters are `Sort`

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

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 `flower`

s, `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 `flower`

s:

```
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" :=
dec_trivial
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 `Prop`

s is a black hole and that we can never escape back into the world of `Type`

s? 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:

- Not using the proof in the function body. This seems pretty silly, but it's a useful escape hatch. And it can still act as a contract imposed on the function callers: we're only allowed to call the function in contexts where a proof exists.
- Using the proof for control flow. If we have a code branch that's unreachable in our function,
`false.elim`

will let us provide a proof of unreachability instead of writing actual code for that branch, even if the function is supposed to return a value of a`Type`

. - Using the proof for recursion. Lean allows us to write recursive functions, but only when it can prove that the recursion will terminate, instead of entering an infinite loop. Most of the time it can do that automatically, but sometimes we have to provide (part of) the proof.

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
/-
@[class]
inductive nonempty : Sort u → Prop
constructors:
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.

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 name (in this case,
`flower`

and`pretty`

), so that we can write function signatures using the new type. - The type constructors (
`flower.grow`

and`pretty.grow`

), so that we can produce values of the new type. - The eliminator for the type (
`flower.rec`

and`pretty.rec`

), so that we can write functions which consume a value of the new type and whose result depends on the internals of the value. This is where the difference between`Prop`

s and`Type`

s happens.

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

- The return type is
`(pretty → C)`

, that is, a function from proofs of prettiness to values of some target type`C`

. - The second parameter has type
`(string → C)`

, that is, it's a function from*names*of pretty flowers to values of the target type`C`

. The whole information content of a proof of prettiness is the name of a pretty flower (that is, the argument to the constructor`pretty.grow`

), so that's what we have to work with to produce a value of the target type`C`

. If we had more constructors for`pretty`

, the eliminator`pretty.rec`

would have more parameters like this, which take the*arguments*of a constructor and produce a value of the target type`C`

. Each one of these parameters is like a callback that knows how to handle values produced by a particular constructor. And if we have callbacks for all possible constructors, the eliminator just dispatches to the appropriate callback. - The first parameter is
`{C : Prop}`

, a target type for the function that`pretty.rec`

returns. And sure enough, this is forced to be a`Prop`

, not a`Type`

nor an unrestricted`Sort`

.

For example, we could use `pretty.rec`

to try (and fail) again to write the "obvious" function `pretty → flower`

:

```
def cant_remember : pretty → flower :=
@pretty.rec
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
```

- The first parameter is
`{C : flower → Sort l}`

, a*family*of target types for the function that`flower.rec`

returns. That's because Lean uses dependent types, so each`flower`

value can have its own target type. Also, the target types are in`Sort l`

, so they can be`Prop`

s or`Type`

s. - The second parameter has type
`(Π (name : string), C (flower.grow name))`

, so it's a callback that uses the argument`(name : string)`

of the`flower.grow`

constructor, and produces a value of the target type`(C (flower.grow name))`

for that specific`flower`

. - The return type is
`(Π (n : flower), C n)`

, that is, a function that takes a flower`n`

and returns a value of the target type`(C n)`

for that flower.

For example, we can try (and succeed) to use `flower.rec`

to write the obvious function `flower → pretty`

:

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