Zulip Chat Archive
Stream: new members
Topic: Type of the empty type?
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)?
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
.
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?
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
.
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?
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
.
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.
Patrick Massot (Oct 01 2019 at 19:44):
A variation which is easier to read in tactic mode is: exfalso, exact h
Johan Commelin (Oct 01 2019 at 19:45):
Or contradiction
Rob Lewis (Oct 01 2019 at 19:45):
Or the contradiction
tactic is even easier to read.
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?
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
.
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.
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
.
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?
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?
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?
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
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.
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).
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
Michael Alan Thompson (Oct 01 2019 at 20:11):
Yep, exactly.
a
andb
are both constructors of the new typetwo
. The constructors or an inductive type are surjective, meaning any termt : two
must be eithera
orb
. They're also injective, meaninga ≠ b
(unlesstwo
is aProp
, 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 (Oct 01 2019 at 20:16):
Also are they any other ways to define types other than by using inductive types?
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.
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: Dec 20 2023 at 11:08 UTC