Type of the empty type?

Stream: new members

[Michael Alan Thompson]

Beginner here. As I understand it everything in lean has a type. If this is the case then what is the type of the empty type in lean (or type theories more generally)?

[Rob Lewis]

There are infinitely many empty types. Lean has a hierarchy of type universes Sort 0, Sort 1, Sort 2, .... You can define an empty inductive type inside any universe. In fact, you can define multiple empty inductive types in the same universe, and you can't prove in Lean that they're equal. The type of an empty type will be Sort i for some i.

[Michael Alan Thompson]

Alright, so as an example, what is the type of the empty type which is used when defining the negation of a proposition? When we say ¬A is A -> E what is the type of that E?

[Rob Lewis]

That empty type is named false in Lean. Its type is Sort 0, which also goes by the name Prop.

[Michael Alan Thompson]

Ahh okay thanks. Also when trying to prove something and you end up with false as a hypothesis then you're done right? How does lean know that false proves everything?

[Rob Lewis]

Yep. The theorem false.elim is what you need. In tactic mode, if you have h : false you can use cases h.

[Rob Lewis]

This is the recursion principle for an empty inductive type, btw, which is how Lean "knows" it.

[Patrick Massot]

A variation which is easier to read in tactic mode is: exfalso, exact h

[Johan Commelin]

Or contradiction

[Rob Lewis]

Or the contradiction tactic is even easier to read.

[Michael Alan Thompson]

Can you elaborate on how its "the recursion principle for an empty inductive type" at all? What does that mena?

[Rob Lewis]

When you define an inductive type T, you give a list of the ways to construct a term of type T. The recursion principle says how to define a function with domain T. For each constructor, you say what the function should do given a term created with that constructor. This is enough to define a function, since the constructors are the only way to create a term of type T.

[Rob Lewis]

For an empty type like false, there are no constructors, so there are no inputs to the recursor. It's a function from false to any type.

[Rob Lewis]

Recursors are generated automatically when you define an inductive type. For a simple non-degenerate example:

inductive two
| a
| b

#check @two.rec_on

You define a function out of the finite type two by saying what the values should be on a and b. Equivalently, you prove a theorem about all terms of type two by proving it for a and proving it for b.

[Michael Alan Thompson]

Okay, so thats saying youre making a new type called two and that a and b are the only things of type two?

[Michael Alan Thompson]

And if you added a function as well as the a and b then that would be another way of making a thing of type two?

[Michael Alan Thompson]

So with the empty type you simply give no constructors and so to prove anything about terms of the empty type you dont need to do anything at all?

[Michael Alan Thompson]

If thats right then I feel like im getting it, but I dont quite get how that lets you create a function from false to anything at all

[Patrick Massot]

In order to create a function from A to B, you need to explain where each element of A should go. If there is no element in A then you're done.

[Rob Lewis]

Okay, so thats saying youre making a new type called two and that a and b are the only things of type two?

Yep, exactly. a and b are both constructors of the new type two. The constructors or an inductive type are surjective, meaning any term t : two must be either a or b. They're also injective, meaning a ≠ b (unless two is a Prop, but that's another rabbit hole).

[Michael Alan Thompson]

In order to create a function from A to B, you need to explain where each element of A should go. If there is no element in A then you're done.

That makes sence - when doing the false.elim itll create a function from false to whatever im tryin to prove by going through all the possible things which could be false, then realise there are none becasue theres no constructors and so create the function without a problem

[Michael Alan Thompson]

Yep, exactly. a and b are both constructors of the new type two. The constructors or an inductive type are surjective, meaning any term t : two must be either a or b. They're also injective, meaning a ≠ b (unless two is a Prop, but that's another rabbit hole).

How is = even defined for a and b? is it just part of an inductive type that it defines what = means for terms of the type?

[Michael Alan Thompson]

Also are they any other ways to define types other than by using inductive types?

[Rob Lewis]

Heh, that's another rabbit hole. Have you read any of Theorem Proving in Lean? (https://leanprover.github.io/theorem_proving_in_lean/) Short answer, = is a family of inductive propositions, but that might not mean much to you. It's discussed there in chapter 7.

[Michael Alan Thompson]

Haha youre right about it not meaning much. I have had a breif look at it, ill be sure to look at chapter 7 for that explanation