Zulip Chat Archive

Stream: new members

Topic: Type of the empty type?


view this post on Zulip Michael Alan Thompson (Oct 01 2019 at 19:17):

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

view this post on Zulip Rob Lewis (Oct 01 2019 at 19:26):

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.

view this post on Zulip Michael Alan Thompson (Oct 01 2019 at 19:32):

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?

view this post on Zulip Rob Lewis (Oct 01 2019 at 19:33):

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

view this post on Zulip Michael Alan Thompson (Oct 01 2019 at 19:40):

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?

view this post on Zulip Rob Lewis (Oct 01 2019 at 19:41):

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

view this post on Zulip Rob Lewis (Oct 01 2019 at 19:44):

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

view this post on Zulip Patrick Massot (Oct 01 2019 at 19:44):

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

view this post on Zulip Johan Commelin (Oct 01 2019 at 19:45):

Or contradiction

view this post on Zulip Rob Lewis (Oct 01 2019 at 19:45):

Or the contradiction tactic is even easier to read.

view this post on Zulip Michael Alan Thompson (Oct 01 2019 at 19:47):

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

view this post on Zulip Rob Lewis (Oct 01 2019 at 19:53):

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.

view this post on Zulip Rob Lewis (Oct 01 2019 at 19:54):

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.

view this post on Zulip Rob Lewis (Oct 01 2019 at 19:58):

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.

view this post on Zulip Michael Alan Thompson (Oct 01 2019 at 20:01):

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

view this post on Zulip Michael Alan Thompson (Oct 01 2019 at 20:02):

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?

view this post on Zulip Michael Alan Thompson (Oct 01 2019 at 20:03):

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?

view this post on Zulip Michael Alan Thompson (Oct 01 2019 at 20:04):

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

view this post on Zulip Patrick Massot (Oct 01 2019 at 20:05):

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.

view this post on Zulip Rob Lewis (Oct 01 2019 at 20:05):

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

view this post on Zulip Michael Alan Thompson (Oct 01 2019 at 20:09):

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

view this post on Zulip Michael Alan Thompson (Oct 01 2019 at 20:11):

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?

view this post on Zulip Michael Alan Thompson (Oct 01 2019 at 20:16):

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

view this post on Zulip Rob Lewis (Oct 01 2019 at 20:17):

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.

view this post on Zulip Michael Alan Thompson (Oct 01 2019 at 20:20):

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


Last updated: May 11 2021 at 13:22 UTC