What to do with empty?

Stream: general

[provemeifyoucan]

Hi. Why does this code not work?

def wtf : (b:Bool) -> if b then Unit else Empty
| true => ()
| false => by contradiction

[Mitchell Lee]

It would be a contradiction if you could prove False, but it isn't a contradiction to have a boolean value that's equal to false.

[Yaël Dillies]

I think you meant something like

def notWTF : (b:Bool) -> b -> if b then Unit else Empty

[provemeifyoucan]

Yaël Dillies said:

I think you meant something like

def notWTF : (b:Bool) -> b -> if b then Unit else Empty

Why is it necessary to pass b twice? In the original example, the goal becomes Empty too. What should I do in such cases? Passing the argument twice doesn't look like the cleanest solution possible...

[Kim Morrison]

This is not passing b twice. It is passing a boolean and then a proof that the boolean equals true.

[Kim Morrison]

If the boolean is false, there is no way you are going to construct a term of type Empty.

[Eric Wieser]

Perhaps it's more clear if you write it as

def notWTF : (b : Bool) -> (h : b) -> if b then Unit else Empty

which means exactly the same thing as what Yaël Dillies wrote

[provemeifyoucan]

Eric Wieser said:

Perhaps it's more clear if you write it as

def notWTF : (b : Bool) -> (h : b) -> if b then Unit else Empty

which means exactly the same thing as what Yaël Dillies wrote

Now I am even more confused. How is it legal to do h : b? b is already an instance of type Bool, right? Still not clear what I have to do when the goal of some expression evaluates to an empty type.

[Johan Commelin]

provemeifyoucan said:

Still not clear what I have to do when the goal of some expression evaluates to an empty type.

Find a term of the empty type in your local context. If there is none, construct one using stuff from your local context.

[Eric Wieser]

How is it legal to do h : b?

h : b actually elaborates as h : b = true

[provemeifyoucan]

Johan Commelin said:

provemeifyoucan said:

Still not clear what I have to do when the goal of some expression evaluates to an empty type.

Find a term of the empty type in your local context. If there is none, construct one using stuff from your local context.

In my local context, I got just b being pattern-matched to true and false with the goals in arms being respectively Unit and Empty types. I supposed I wouldn't need anything else to state some trivia...

[Eric Wieser]

Johan missed one thing from his list. "If you can't construct one, then you need to backtrack and undo a previous wrong turn". Here, your pattern match was fine, but your original definition is nonsense.

[provemeifyoucan]

Eric Wieser said:

Johan missed one thing from his list. "If you can't construct one, then you need to backtrack and undo a previous wrong turn". Here, your pattern match was fine, but your original definition is nonsense.

Nonesense how?

[Johan Commelin]

If (and only if) you are still trying to make this work

def wtf : (b:Bool) -> if b then Unit else Empty
| true => ()
| false => by contradiction

then I suggest that you first try to understand why

def zero? : (n:Nat) -> if n = 0 then Unit else Empty
| 0 => ()
| n+1 => by contradiction

doesn't work

[Eric Wieser]

Nonsense in this sense:

def wtf : (b:Bool) -> if b then Unit else Empty := sorry

-- if the `sorry` above can be filled, then false is true
example : False := (wtf false).elim

[provemeifyoucan]

Johan Commelin said:

If (and only if) you are still trying to make this work

def wtf : (b:Bool) -> if b then Unit else Empty
| true => ()
| false => by contradiction

then I suggest that you first try to understand why

def zero? : (n:Nat) -> if n = 0 then Unit else Empty
| 0 => ()
| n+1 => by contradiction

doesn't work

In case you didnt notice I asking why it doesnt work, which implies that I would like to have an answer to this.

Anyway, since you just said the case with zero? doesn't work it makes me question usefulness of lean at this point.

[Johan Commelin]

Do you understand why

def oops : Empty := by contradiction

doesn't work?

[Johan Commelin]

It isn't too much of an exaggeration to say that Lean is useful precisely because examples like yours don't work.

[provemeifyoucan]

Eric Wieser said:

Nonsense in this sense:

def wtf : (b:Bool) -> if b then Unit else Empty := sorry

-- if the `sorry` above can be filled, then false is true
example : False := (wtf false).elim

What would make it true? I expected that any attempt to pattern match empty type would just lead to nowhere.

[Eric Wieser]

That's the opposite of the case: pattern matching an empty type leads to everywhere!

def foo (e : Empty) : AProofOfAnyMilleniumProblem := nomatch e

[Johan Commelin]

You are trying to define something of type Empty. I think it shouldn't be surprising that it is not possible.

[provemeifyoucan]

Johan Commelin said:

Do you understand why

def oops : Empty := by contradiction

doesn't work?

I feel like it should. Because an attempt to use it would be never possible.
Like nothing compromises things like this

def f : Empty -> Type
| ...

[Yaël Dillies]

Maybe you're confused by the (b : Bool) → notation? This is exactly the same as your original example, but using ∀:

def wtf : ∀ b : Bool, if b then Unit else Empty
| true => ()
| false => by contradiction

[Eric Wieser]

provemeifyoucan said:

Like nothing compromises things like this

def f : Empty -> Type
| ...

"given a thing that can't exist, produce X", is very different to "produce a thing that can't exist". There is a very fundamental difference between the left and right of ->.

[Yaël Dillies]

So wtf is the collection for every Boolean b of an element of type if b then Unit else Empty. Equivalently, it's the data of an element of Unit and of an element of Empty.

[provemeifyoucan]

Eric Wieser said:

provemeifyoucan said:

Like nothing compromises things like this

def f : Empty -> Type
| ...

"given a thing that can't exist, produce X", is very different to "produce a thing that can't exist". There is a very fundamental difference between the left and right of ->.

I meant that inexistence of such functions woulndt suddenly be allowed

[Johan Commelin]

provemeifyoucan said:

Johan Commelin said:

Do you understand why

def oops : Empty := by contradiction

doesn't work?

I feel like it should.

But that means that oops will be an element of Empty. But Empty is empty! It can't have any elements. That's its nature!

So really, it is a fantastic feature of Lean that you cannot complete the line

def oops : Empty :=

[Johan Commelin]

Btw, there certainly is a function Empty -> Type. Lean is perfectly happy with that. For every element of Empty, you need to tell Lean to which type you want to send it. But because Empty doesn't have any elements, you are done before you even started.

[provemeifyoucan]

Yaël Dillies said:

Maybe you're confused by the (b : Bool) → notation? This is exactly the same as your original example, but using ∀:

def wtf : ∀ b : Bool, if b then Unit else Empty
| true => ()
| false => by contradiction

I think I want confused by notation, as long as (a:T) -> expr a means a dependent function. Only about what I should do when the goal is empty type. Like... what should I write there? How just pattern matching leading to an impossible case is not enough for contradiction to work?

[Kyle Miller]

"you can use emptiness, but you cannot create emptiness"

[Eric Wieser]

Contradiction requires impossible assumptions, not impossible conclusions

[provemeifyoucan]

Johan Commelin said:

provemeifyoucan said:

Johan Commelin said:

Do you understand why

def oops : Empty := by contradiction

doesn't work?

I feel like it should.

But that means that oops will be an element of Empty. But Empty is empty! It can't have any elements. That's its nature!

So really, it is a fantastic feature of Lean that you cannot complete the line

def oops : Empty :=

Nothing in this statement add any elements to empty

[Johan Commelin]

Everything in def oops : Empty := is adding an element to Empty!!!

[Kyle Miller]

If you could replace this sorry with something, that would mean you could prove False, which would mean that Lean's logic is inconsistent:

def oops : Empty := sorry

example : False := by
  have := oops
  contradiction

[provemeifyoucan]

Kyle Miller said:

"you can use emptiness, but you cannot create emptiness"

Well then, why is this code legal?

def notWTF : (b : Bool) -> (h : b) -> if b then Unit else Empty

[provemeifyoucan]

Kyle Miller said:

If you could replace this sorry with something, that would mean you could prove False, which would mean that Lean's logic is inconsistent:

def oops : Empty := sorry

example : False := by
  have := oops
  contradiction

I thought sorry in lean mean 'this definition has no computational content' exactly like Empty

[Johan Commelin]

Because in the false branch you have assumed something that is false.

[Kyle Miller]

That's shorthand for

def notWTF : (b : Bool) -> (h : b = true) -> if b then Unit else Empty

and when b is false, then the second argument is false = true, which is empty, and from that emptiness you can "produce" a value of Empty.

[Johan Commelin]

@provemeifyoucan No, sorry means "just assume this can be done, stop complaining".

[Yaël Dillies]

Eric Wieser said:

Contradiction requires impossible assumptions, not impossible conclusions

You're missing the point, I believe. provemeifyoucan is confused about the fact that the assumptions are not impossible, not the conclusions

[Johan Commelin]

So sorry makes Lean very unsafe.

[Kyle Miller]

sorry is the axiom is that everything is true, which we use to fill in unfinished proofs or values, but its use is recorded and warnings are logged so that we can make sure they're all dealt with eventually

[Johan Commelin]

sorry is not allowed to be used in mathlib. And in general, it shouldn't appear in "end products".

[Kyle Miller]

Well then, why is this code legal?

Here's it written as a tactic proof you can step through in case it makes it clearer.

def notWTF : (b : Bool) -> (h : b = true) -> if b then Unit else Empty := by
  intro b h
  cases b
  · contradiction -- h : false = true is a contradiction
  · exact ()

[Patrick Stevens]

I thought sorry in lean mean 'this definition has no computational content' exactly like Empty

That is instead indicated by the keyword noncomputable, by the way.

[provemeifyoucan]

Johan Commelin said:

It isn't too much of an exaggeration to say that Lean is useful precisely because examples like yours don't work.

This works and it is what I wanted to do.

def Empty2 : Type := Empty -> Unit
def impossible : Empty -> Unit := nofun
def n3 : (n:Nat) -> match n with | .zero => Empty2 | .succ _ => Nat
| n@(.succ _) => n
| .zero => impossible

#eval n3 1 -- works
-- #eval n3 0 -- doesnt

Is lean still useful?

[provemeifyoucan]

provemeifyoucan said:

Johan Commelin said:

It isn't too much of an exaggeration to say that Lean is useful precisely because examples like yours don't work.

This works and it is what I wanted to do.

def Empty2 : Type := Empty -> Unit
def impossible : Empty -> Unit := nofun
def n3 : (n:Nat) -> match n with | .zero => Empty2 | .succ _ => Nat
| n@(.succ _) => n
| .zero => impossible

#eval n3 1 -- works
-- #eval n3 0 -- doesnt

Is lean still useful?

The stranger thing is that it is possible to define impossible as

def impossible2 : Empty -> Unit := fun _ => ()

Which is the same thing. Why is it called nofun haha? I have lots so far!

[Yury G. Kudryashov]

You're just using a type that doesn't support eval for the type of n3 0. It's still a valid expression.

[provemeifyoucan]

Yury G. Kudryashov said:

You're just using a type that doesn't support eval for the type of n3 0. It's still a valid expression.

Thats the point!

[Johan Commelin]

Why are you giving Empty2 that name?

[Johan Commelin]

And also, why are you giving impossible that name?

[Johan Commelin]

Is lean still useful?

Certainly!

[Henrik Böving]

@provemeifyoucan what is it that you are actually after here? An understanding of how empty types work?

[Kyle Miller]

I'm confused about Empty2 being called that. The cardinality of $\varnothing \to X$ is always $1$, it's not empty.

[Kyle Miller]

(impossible is that single function in this set of functions, at least when $X=\mathrm{Unit}$)

[provemeifyoucan]

Henrik Böving said:

provemeifyoucan what is it that you are actually after here? An understanding of how empty types work?

You apparently cant read: I wanted a tactic that closes goals of an empty type. I found one.

[provemeifyoucan]

Kyle Miller said:

I'm confused about Empty2 being called that. The cardinality of $\varnothing \to X$ is always $1$, it's not empty.

What? Are you trying to make up an excuse or smth?

[Kyle Miller]

Make up an excuse for what?

The type Empty2 is certainly not empty. It's well-known that when the domain set is empty, there exists a function. (I just linked to Planet Math because it came up to find a quick reference.)

The nofun function, despite its name, is actually a function. It's called that because there are no cases to consider when making a function whose domain isempty, not that there are no functions.

[Kyle Miller]

You apparently cant read

We try to be a bit more civil that that here. Please assume Henrik is asking his question in good faith. I too am wondering what the context is for your question, what you were doing to end up with the question about trying to construct a function of type (b:Bool) -> if b then Unit else Empty.

[provemeifyoucan]

Kyle Miller said:

The type Empty2 is certainly not empty. It's well-known that when the domain set is empty, there exists a function. (I just linked to Planet Math because it came up to find a quick reference.)

His argument relies on the fact that n^0 = 1. This doesn't look convincing.

That type is empty. Intuitively because you can't use it to compute anything.

[Andrew Yang]

Maybe you are more familiar with set-theoretic foundations? Under such a foundation, a function $A \to B$ is a subset $S \subseteq A \times B$ such that $\forall a \in A, \exists! b \in B, (a, b) \in S$. Now if $A$ is empty, it is a fun exercise to verify that $\varnothing \subseteq A \times B$ indeed satisfies the condition, and thus defines a function $A \to B$. This is called the empty function.

[provemeifyoucan]

Andrew Yang said:

Maybe you are more familiar with set-theoretic foundations? Under such a foundation, a function $A \to B$ is a subset $S \subseteq A \times B$ such that $\forall a \in A, \exists! b \in B, (a, b) \in S$. Now if $A$ is empty, it is a fun exercise to verify that $\varnothing \subseteq A \times B$ indeed satisfies the condition, and thus defines a function $A \to B$. This is called the empty function.

I read the last part as $\varnothing \subseteq \varnothing \times \{\star\} \implies \varnothing \subseteq \varnothing$. Which means... it is not inhabited aka empty function

[Johan Commelin]

@provemeifyoucan Please read #butterfly.
Also, if you can define a term of type False then you show that lean is inconsistent. Can you use impossible to do that?

[provemeifyoucan]

Johan Commelin said:

provemeifyoucan Please read #butterfly.
Also, if you can define a term of type False then you show that lean is inconsistent. Can you use impossible to do that?

I was hoping some of you would do it! To me, inconsistency is the ability to perform bad computations. And computation that doesn't happen can't be bad.

And so far, what I did does not look like it can lead to inconsistencies.

[Johan Commelin]

Ok, then I suggest we stop this discussion. Nobody here is surprised by your impossible and Empty2. Only by the names that you chose.

[provemeifyoucan]

Johan Commelin said:

Ok, then I suggest we stop this discussion. Nobody here is surprised by your impossible and Empty2. Only by the names that you chose.

Nice of you to assume nobody else may be interested in this, because of some dogmatic belief that hold you back from accepting this.

Ive shown the term that closes empty type, btw.

Also, please read #butterfly

[Johan Commelin]

You can't simply call a random type Empty2, define a term of it, and declare victory.
Just like you can't call a random statement "Riemann Hypothesis 2", prove it, and collect 1M bucks.

[Johan Commelin]

If you want to "show the term that closes empty types" then your approach must close goals of type Empty. Not just Empty2.

[provemeifyoucan]

Johan Commelin said:

You can't simply call a random type Empty2, define a term of it, and declare victory.
Just like you can't call a random statement "Riemann Hypothesis 2", prove it, and collect 1M bucks.

Its not a random type. Its an empty type.

Dont write anymore in this thread, please.

[Johan Commelin]

Fwiw, your impossible shows up in dozens of places in mathlib and other projects. It is incredibly useful.

[Johan Commelin]

We just don't give it that name.

[provemeifyoucan]

Johan Commelin said:

Fwiw, your impossible shows up in dozens of places in mathlib and other projects. It is incredibly useful.

Link please

[Johan Commelin]

https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Empty.elim

[provemeifyoucan]

Johan Commelin said:

https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Empty.elim

Nice! Lean can close goals which are empty types.
It would be great to add one convenience tactic to deal with the following

def imp : Empty := by impossible

[Thomas Murrills]

Textual communication can be tricky, as we lose a lot of information about tone and intention (at least, I feel this way); but @provemeifyoucan please rest assured that while people might be repeatedly saying you’re incorrect here, they are all very nice people and are earnestly trying to help (also, they know what they’re talking about!).

Let me try to pinpoint a potential source of confusion. Are you under the impression that a term of type Empty → Unit closes a goal of type Empty? If so, this is the issue, because that is not the case! (Happy to explain why further, but first let me see if my guess is correct.)

[Johan Commelin]

@provemeifyoucan I will write that tactic if you tell me exactly which term should be generated by by impossible (and it typechecks).

[provemeifyoucan]

Thomas Murrills said:

Are you under the impression that a term of type Empty → Unit closes a goal of type Empty? If so, this is the issue, because that is not the case!

Empty → Unit is an empty type and when it's a goal there is a term that closes it, yes.

[Johan Commelin]

I will only believe that a type is empty if you implement an instance of IsEmpty for it.

[Thomas Murrills]

provemeifyoucan said:

Thomas Murrills said:

Are you under the impression that a term of type Empty → Unit closes a goal of type Empty? If so, this is the issue, because that is not the case!

Empty → Unit is an empty type and when it's a goal there is a term that closes it, yes.

Why do you believe Empty → Unit is empty?

[provemeifyoucan]

Thomas Murrills said:

provemeifyoucan said:

Thomas Murrills said:

Are you under the impression that a term of type Empty → Unit closes a goal of type Empty? If so, this is the issue, because that is not the case!

Empty → Unit is an empty type and when it's a goal there is a term that closes it, yes.

Why do you believe Empty → Unit is empty?

I explained it here

[Jireh Loreaux]

Empty → Unit is not an empty type, as others have said. What evidence would it take for you believe it is not empty? (Note: Johan has explained what evidence it would take for him to believe it is empty, an instance of IsEmpty for it.)

[Thomas Murrills]

Hmm, I’m not sure I follow your explanation @provemeifyoucan. There is a unique function $f : \emptyset \to A$ for any set $A$; do you not agree with that? If not, let me ask you: what is your definition of a function, either in terms of sets or types?

[provemeifyoucan]

Erhm, is lean okay?
Screenshot_20240509_110709.png
Screenshot_20240509_110714.png

[Jireh Loreaux]

Yep, that makes sense. You are trying to tell Lean that there are no matches for i : Empty -> Unit, but there is one!

If you delete line 81 (and leave line 82), you will have constructed the function.

[provemeifyoucan]

Jireh Loreaux said:

Yep, that makes sense. You are trying to tell Lean that there are no matches for i : Empty -> Unit, but there is one!

If you delete line 81 (and leave line 82), you will have constructed the function.

Any idea about what I can write here?

def oof (T:Type) : T -> Empty := fun _ => sorry

def empty_fun_b : Empty -> (Empty -> Unit) := Empty.elim
def empty_fun_f : (Empty -> Unit) -> Empty := oof _

[Jireh Loreaux]

It's impossible to write anything there (for empty_fun_f) because the domain, namely Empty -> Unit has a single element (which is the function fun _ => ()), whereas the codomain, namely Empty, has no elements.

[provemeifyoucan]

Does it mean I cannot show that there are no function from any set to empty set?

[Jireh Loreaux]

It's impossible to construct oof T unless you also assume T is empty.

[provemeifyoucan]

Jireh Loreaux said:

It's impossible to construct oof T unless you also assume T is empty.

Does it mean I cannot show that there are no functions from any set to empty set?

[Jireh Loreaux]

provemeifyoucan said:

Does it mean I cannot show that there are no function from any set to empty set?

Of course, unless the set for the domain is empty.

[provemeifyoucan]

Jireh Loreaux said:

provemeifyoucan said:

Does it mean I cannot show that there are no function from any set to empty set?

Of course, unless the set for the domain is empty.

Leans logic is weak then

[Jireh Loreaux]

??? It's weak because it doesn't allow you to build things that don't exist? No, that's what makes it useful. If you could build things that don't exist, then you could prove False.

[provemeifyoucan]

provemeifyoucan said:

Jireh Loreaux said:

It's impossible to construct oof T unless you also assume T is empty.

Does it mean I cannot show that there are no functions from any set to empty set?

Yeah, just pluging in nofun for sorry gives again this error of missing _ case.

[Jireh Loreaux]

Sure. nofun is for when the domain is an empty inductive type.

[provemeifyoucan]

no wait its actually this
Screenshot_20240509_115559.png

[provemeifyoucan]

provemeifyoucan said:

no wait its actually this
Screenshot_20240509_115007.png

Zero missing cases

[Jireh Loreaux]

No, it's not zero missing cases, it's that T is an unspecified type, so Lean cannot give you the cases corresponding to its inductive constructors.

[provemeifyoucan]

A constructorless type!! I wonder what that means.....

[Jireh Loreaux]

It's not constructorless necessarily, it's unspecified (i.e., arbitrary).

[Jireh Loreaux]

For example, T could be Nat or Bool, or ... whatever.

[Jireh Loreaux]

(and because I couldn't tell whether or not your comment above was sarcastic: there are constructorless types, such as False or Empty)

[provemeifyoucan]

Jireh Loreaux said:

provemeifyoucan said:

Does it mean I cannot show that there are no function from any set to empty set?

Of course, unless the set for the domain is empty.

So if we let function be products i.e.
$A \times B$
it is possible to represent function A -> Empty and Empty -> A as $A \to \emptyset$ and $\emptyset \to A$ respectively.
As product they can be written like this
$\emptyset \times A$ and $A \times \emptyset$
If we apply rule that product of an empty set with anything else is an empty set we get an empty set which means
$\emptyset \times A \equiv A \times \emptyset$
because
$\emptyset \equiv \emptyset$

And you are trying to convince me that
$\emptyset \neq \emptyset$

Do you see the problem?

[Yury G. Kudryashov]

A function is not the product. It's a subset $$s \subst A \times B$$ such that $\forall a \in A, \exists! b \in B, (a, b) \in s$. In case of a function $\emptyset \to A$, you get $\forall a \in \emptyset, ...$ which is true, because the empty set has no elements. For $A \to \emptyset$ with nonempty $A$, you get $\forall a \in A, \exists! b \in \emptyset, ...$, which can't be true: take $a \in A$ (this is possible since $A$ is nonempty); then we get $\exists! b \in \emptyset, ...$ which is false, because $\emptyset$ has no elements.

[Jireh Loreaux]

Sure, we can work in set-theoretic terminolgy. Functions are not products. They are subsets of products with the property that for every element of the domain, there is a unique element of the codomain such that the pair is in the subset.

So, a function from Empty -> Unit would be a subset of $\emptyset \times \{*\}$ with that property, and the empty set suffices for this. Crucially, the property is satisfied because the domain is empty.

However, a function from Unit -> Empty would be a subset of $\{*\} \times \emptyset$ with the property, but no such subset exists. Indeed the only subset is the empty set, but there is no pair of the form $(*,b)$ for some b in the empty set.

[Eric Wieser]

Do you see the problem?

You can actually use Lean to prove that

So if we let function be products i.e.

is the problem:

import Mathlib

/-- Functions are not products (if they were, we could prove `False`) -/
example (h : ∀ α β : Type, (α → β) ≃ (α × β)) : False := by
  -- counterexample: use types with two and three elements
  specialize h (α := Fin 2) (β := Fin 3)
  -- count them
  replace h := Fintype.card_congr h
  -- the function has 9 elements, but the product only 6
  have : 9 = 6 := by simpa only [Fintype.card_pi, Fintype.card_fin] using h
  -- this is nonsense
  cases this

[Patrick Stevens]

Meta-point: if you want to be assured that the weight of mathematical opinion is with the statement "there's only one domain which admits a function to the empty set, namely the empty set itself with its identity", the search term you can easily verify with Google is that the empty set is a strict initial object in the category of sets. Whether you believe the weight of mathematical opinion is up to you, but you should expect mathematicians to go with the standard!

[provemeifyoucan]

Eric Wieser said:

Do you see the problem?

You can actually use Lean to prove that

So if we let function be products i.e.

is the problem:

import Mathlib

/-- Functions are not products (if they were, we could prove `False`) -/
example (h : ∀ α β : Type, (α → β) ≃ (α × β)) : False := by
  -- counterexample: use types with two and three elements
  specialize h (α := Fin 2) (β := Fin 3)
  -- count them
  replace h := Fintype.card_congr h
  -- the function has 9 elements, but the product only 6
  have : 9 = 6 := by simpa only [Fintype.card_pi, Fintype.card_fin] using h
  -- this is nonsense
  cases this

I was thinking about this tbh

def fr : (A × (A -> B)) -> A × B
| (a , f) => (a , f a)

def bw : (A × B) -> (A × (A -> B))
| (a, b) => (a, fun _ => b)

def y : (Empty × (Empty -> Unit)) -> (Empty × Unit) := by
  intro m
  have (a, _) := m
  contradiction

def y2 : (Empty × Unit) -> (Empty × (Empty -> Unit)) := by
  intro m
  have (a, _) := m
  contradiction

Should I say that they are inhabited by contradiction?

[provemeifyoucan]

If I just swap arguments I can no longer write code that means same thing

def y7 : (Unit × (Unit -> Empty)) -> (Unit × Empty) := by
  sorry

def y8 : (Unit × Empty) -> (Unit × (Unit -> Empty)) := by
  intro m
  have (_, _) := m
  contradiction

Does this mean A * B != B * A in lean?

[Yaël Dillies]

A × B is indeed not the same thing as B × A, if this is what you mean.

[provemeifyoucan]

Yaël Dillies said:

A × B is indeed not the same thing as B × A, if this is what you mean.

def swap : (A × B) -> (B × A) | (a,b) => (b,a)

def swap_same : (a: A × B) -> a = swap (swap a) := by
  intros a
  rfl

WDYM?

[Yaël Dillies]

I am trying to interpret your "Does this mean A * B != B * A in lean?" :shrug: A × B and B × A are in bijection but they are not "the same".

[provemeifyoucan]

Yaël Dillies said:

I am trying to interpret your "Does this mean A * B != B * A in lean?" :shrug: A × B and B × A are in bijection but they are not "the same".

Hold on, I am trying to do

def same : (a: A × B) -> a = swap (swap a)

at the moment

[Yaël Dillies]

docs#Prod.swap_swap ?

[provemeifyoucan]

So (Empty × (Empty -> Unit)) -> (Empty × Unit) should be same as (Unit × (Unit -> Empty)) -> (Unit × Empty)
What yall think?

[Yaël Dillies]

If by "the same" you mean "in bijection", then yes

[provemeifyoucan]

Yaël Dillies said:

If by "the same" you mean "in bijection", then yes

So it is an empty type then

[provemeifyoucan]

How can I show that Unit -> Empty is an empty type in lean?

[Yaël Dillies]

example : IsEmpty (Unit → Empty) where
  false f := by cases f ()

[Marcus Rossel]

Side note: Your y7 from above can be implemented:

def y7 : (Unit × (Unit -> Empty)) -> (Unit × Empty) :=
  fun (u, f) => (u, f u)

[provemeifyoucan]

Marcus Rossel said:

Side note: Your y7 from above can be implemented:

def y7 : (Unit × (Unit -> Empty)) -> (Unit × Empty) :=
  fun (u, f) => (u, f u)

Now we only need to fill this blank in the way I did for y8 to show something really interesting

def empty : Unit → Empty := sorry

[Eric Wieser]

But Yael proved that blank is impossible to fill above

[provemeifyoucan]

Eric Wieser said:

But Yael proved that blank is impossible to fill above

Maybe there's some tactic I don't know about :laughing:

[Damiano Testa]

There is one: sorry.

[Damiano Testa]

provemeifyoucan said:

Yaël Dillies said:

If by "the same" you mean "in bijection", then yes

So it is an empty type then

I am not sure what you mean when you say "empty type", but this is definitely a different notion that what most people in this chat probably think:

import Mathlib.Logic.IsEmpty

example : Nonempty ((Empty × (Empty → Unit)) → (Empty × Unit)) := by simpa using instIsEmptyEmpty
example : Subsingleton ((Empty × (Empty → Unit)) → (Empty × Unit)) := instSubsingletonForall

example : Nonempty ((Unit × (Unit → Empty)) → (Unit × Empty)) := by simpa using instIsEmptyEmpty
example : Subsingleton ((Unit × (Unit → Empty)) → (Unit × Empty)) := instSubsingletonForall

[Patrick Stevens]

If you can fill in the blank in def empty : Unit -> Empty := sorry, then you can prove literally any mathematical statement. You can always construct something of type Unit; so every statement (regardless of whether it's true) can be proved by "let x : False := empty(); contradiction" (which is pseudocode, sorry, I don't have mathlib or a Lean compiler in my head). So you'd better hope that you can't fill in that blank, because once you've done that, we need to find a different logic that lets us prove less stuff!

[Yury G. Kudryashov]

provemeifyoucan said:

So (Empty × (Empty -> Unit)) -> (Empty × Unit) should be same as (Unit × (Unit -> Empty)) -> (Unit × Empty)
What yall think?

Both types are singletons:

example :
    ((Empty × (Empty -> Unit)) -> (Empty × Unit)) ≃ ((Unit × (Unit -> Empty)) -> (Unit × Empty)) :=
  Equiv.equivOfUnique _ _

[Yury G. Kudryashov]

In more details, Empty × (Empty -> Unit), Empty × Unit, Unit × (Unit -> Empty), and Unit × Empty are all empty types, and there is a unique function from an empty type to any other type (IsEmpty.elim).

[Thomas Murrills]

It’s perhaps worth noting explicitly here that, in terms of sets, the set of all functions from $A$ to $B$ which I’ll denote $A \to B$ (analogous to the type A → B) is not a subset of $A \times B$, but a subset of $\mathcal{P}(A \times B)$ (since each function is a subset of $A \times B$).

And since $\mathcal{P}(\emptyset)$ is singleton (namely, $\mathcal{P}(\emptyset) = \{\emptyset\}$, and so always contains exactly one element, namely $\emptyset$), you’ve always got at least one candidate function (the empty set) when considering $A \to \emptyset$ and $\emptyset \to A$.

To find out which elements of $\mathcal{P}(A \times B)$ are actually functions, we filter out using the criterion Yury mentioned earlier. Importantly, this criterion is asymmetric in $A$ and $B$. So in the generic case, we filter out meaningfully different subsets (i.e. not related by $swap$) in $A \to B$ when compared to $B \to A$.

The empty set (recall that it’s always a candidate function, i.e. $\emptyset \in \mathcal{P}(X)$ for any $X$) fails to meet the criteria of “actually being a function” in the $A \to \emptyset$ case exactly when $A$ is nonempty.

In the case of $\emptyset \to A$, the empty set always does meet the criteria of being a function, and, since $\emptyset \in \mathcal{P}(\emptyset \times A) \cong \mathcal{P}(\emptyset)$ is the unique such element, $\emptyset \to A$ is always singleton.

So to sum up, the point here is that while you are correct that $\emptyset \times A \cong A \times \emptyset \cong \emptyset$

• the function type sticks a $\mathcal{P}$ in front, which always grants us at least one candidate element of $(A \to B) \subset \mathcal{P}(A \times B)$ (as $\emptyset \in \mathcal{P}(X)$ for any $X$)
• the function criterion is asymmetric, so different elements will be filtered out as “non-functions” depending on whether we’re looking at $\mathcal{P}(A \times B)$ or $\mathcal{P}(B \times A)$. So $A \to \emptyset$ may wind up empty by filtering out the empty function while $\emptyset \to A$ may not.

(As an example, to prove to yourself that $A \to B$ in general has a different size than $B \to A$, take $A = \{\star\}$ and $B$ to have $N$ elements. You’ll see there are $N$ elements of $A \to B$ but only one element of $B \to A$. It’s not a stretch for $A \to \emptyset$ to be reduced to 0 elements while $\emptyset \to A$ has 1 element!)

Do you have any specific objections to any part of this? Also happy to clarify anything. (In any case this was fun to type out! :) )