Equality with Types

Stream: new members

[Monica Omar]

how can I show that two types aren't equal?
for example: for the natural numbers, integers, etc...

[Ruben Van de Velde]

Why?

[Monica Omar]

curiosity

[Ruben Van de Velde]

(This is generally not a thing you need to express, and in particular you can't prove that Nat and Int are not equal)

[Monica Omar]

why not tho

[Eric Rodriguez]

Name one way in that they are intrinsically different

[Eric Rodriguez]

As far as I know (and I know I'm going to get subtly corrected but I don't remember the other way) the only way to prove two types are not equal is that they don't have the same cardinality

[Kevin Buzzard]

Right -- for all we know, Lean is running the cardinality model, where there's precisely one type of each cardinality, and Nat and Int and Rat are all secretly internally equal to the aleph_null type but just with different structures attached. In particular, they could all secretly be equal to each other.

[Monica Omar]

Kevin Buzzard said:

Right -- for all we know, Lean is running the cardinality model, where there's precisely one type of each cardinality, and Nat and Int and Rat are all secretly internally equal to the aleph_null type but just with different structures attached. In particular, they could all secretly be equal to each other.

yeah, but we also know they aren't equal to each other

[Patrick Massot]

No we don’t.

[Eric Wieser]

And if we do, we're using a notion of "equal" that Lean doesn't know about isn't Lean's =

[Damiano Testa]

You can prove that they are not isomorphic as monoids: maybe this is closer to what you had in mind? Or showing that the image of Nat.cast is not everything?

[Patrick Massot]

The good news is that this question is completely irrelevant. You wouldn’t be able to do anything with the answer.

[Monica Omar]

Eric Wieser said:

And if we do, we're using a notion of "equal" that Lean doesn't know about isn't Lean's =

yeah - haha

[Monica Omar]

true true. it's a completely unnecessary question, but we were just curious

[Eric Wieser]

Kevin Buzzard said:

Right -- for all we know, Lean is running the cardinality model, where there's precisely one type of each cardinality, and Nat and Int and Rat are all secretly internally equal to the aleph_null type but just with different structures attached. In particular, they could all secretly be equal to each other.

As an exercise, you could define your own IntThatEqualsNat which is isomorphic as a ring to the integers, but satisfies example : IntThatEqualsNat = Nat := rfl

[Eric Wieser]

I don't think it would be a very rewarding exercise though

[Kevin Buzzard]

In set theory, the naturals are defined via some weird construction involving sets of sets, and then the integers are defined perhaps as some equivalence classes of ordered pairs, so they're also just some weird sets of sets, and now someone could ask whether the naturals and the integers are equal by coincidence, and now you realise that this is a really weird question because now all of a sudden it really matters what your definition of things like "ordered pair" is, and there are three definitions of an ordered pair on Wikipedia, and so in set theory now you realise that whether the naturals and the integers are equal is not really even a well-defined question because it depends on things which mathematicians don't think or care about. My point is -- do you know for sure that the naturals and the integers in set theory are not coincidentally equal, given that their definitions are under the hood totally weird?

[Monica Omar]

I totally agree. But shouldn't we care about whether or not they are "equal"?

[Kevin Buzzard]

Definitely not! It's a totally pathological question as I just attempted to explain. It depends on things which are not mathematics.

[Kevin Buzzard]

There is a model of Lean where they are equal, and there is a model of Lean where they are not equal, so we know for sure that the question is independent of Lean's axioms. This is a very good reason not to care about the question.

[Jireh Loreaux]

Eric Wieser said:

As an exercise, you could define your own IntThatEqualsNat which is isomorphic as a ring to the integers, but satisfies example : IntThatEqualsNat = Nat := rfl

There's a really easy way to do this:

import Mathlib

def Int' := Nat

example : Int' = Nat := rfl

instance : Countable Int' := instCountableNat
instance : Infinite Int' := instInfiniteNat

noncomputable section

def int'EquivInt : Int' ≃ ℤ :=
  Cardinal.eq.mp (by simp) |>.some

instance : CommRing Int' := int'EquivInt.commRing

#check (-1 : Int')

[Jireh Loreaux]

So @Monica Omar, this is what people are saying when they say it's not a meaningful question to ask. In the above the type Int' is equal (definitionally!) to ℕ, but as a ring, it is isomorphic to ℤ (so in essence, it is ℤ, despite the fact that it's equal to ℕ).

[Eric Wieser]

I claim noncomputable section is cheating, no computer scientist would believe that those "are" the integers!

[Monica Omar]

yeah, that says they are isomorphic, but doesn't say anything about equality

[Eric Wieser]

Did you miss the example : Int' = Nat := rfl bit?

[Simone Castellan]

Kevin Buzzard ha scritto:

Right -- for all we know, Lean is running the cardinality model, where there's precisely one type of each cardinality

Do you have a reference for this? Curious about these nonsensical things

[Monica Omar]

Eric Wieser said:

Did you miss the example : Int' = Nat := rfl bit?

but that's not the integers, that's the naturals? Int' is Nat and Nat = Nat

[Eric Wieser]

Why is Int' not the integers?

[Monica Omar]

because it's defined as Nat

[Eric Wieser]

Definitions of types don't mean anything though(besides cardinality), only the operations matter

[Eric Wieser]

And it has the + and * and - operators of the integers

[Eric Wieser]

No mathematician would ask "Wait, are these Coq integers, Lean integers, or the integers from that zulip thread"

[Monica Omar]

but like -1 isn't in Nat

[Jireh Loreaux]

But -1 is in Int' !!

[Eric Wieser]

Well, you can write -1 : Int' with the above and everything works

[Eric Wieser]

(I think the computable approach makes it a bit clearer what is going on here; you represent {...,-2, -1, 0, 1, 2,...} with the naturals {..., 3, 1, 0, 2, 4, ...}

[Jireh Loreaux]

I was just about to implement the computable approach, give me a minute.

[Monica Omar]

but (-1 : Int) isn’t in Nat?

[Eric Wieser]

import Mathlib

def Int' := Nat
instance : CommRing Int' := (Denumerable.equiv₂ ℕ ℤ).commRing

-- Equal to `Nat`
example : Int' = Nat := rfl

-- Isomorphic to `ℤ`
def int'EquivInt : Int' ≃+* ℤ := (Denumerable.equiv₂ ℕ ℤ).ringEquiv

-- Peek under the hood at the Nat we're using
def toNat (i : Int') : Nat := i

#check (-10 : Int')  -- -10
example : (-10 : Int').toNat = 19 := rfl

[Eric Wieser]

Too slow, sorry @Jireh Loreaux

[Jireh Loreaux]

to make it really clear Eric, add the line

example (-10 : Int') = (19 : ℕ) := rfl

[Jireh Loreaux]

(deleted)

[Jireh Loreaux]

Monica Omar said:

but like -1 isn't in Nat

Lean disagrees with you:

lemma neg_one_in_nat : (-1 : Int') ∈ @Set.univ ℕ := True.intro

#print neg_one_in_nat -- -1 ∈ Set.univ

set_option pp.explicit true
#print  neg_one_in_nat
-- @Membership.mem Int' (Set ℕ) (@Set.instMembershipSet ℕ) (-1) (@Set.univ ℕ)

[Monica Omar]

but that’s Int’, not Int

[Monica Omar]

and also my point of saying -1 isn’t in Nat is that there are no negative numbers in Nat

[Riccardo Brasca]

What is surely true is that there is not n : ℕ such that (1 : ℕ) + n = 0, but that's all you can say.

[Jireh Loreaux]

Just swap the names of Int and Int'? Look, I'm not claiming ℕ = ℤ, because that's independent of Lean's type theory. The above is just to show you that it is possible (within Lean's type theory) that they could be equal. There are also models where ℕ ≠ ℤ.

[Monica Omar]

okay I was just confused what equality of types actually means

[Damiano Testa]

Monica Omar said:

and also my point of saying -1 isn’t in Nat is that there are no negative numbers in Nat

This is also easy to prove, btw:

example : {n : Nat} → (h : n < 0) → False := by decide

[Eric Wieser]

But it's also easy to disprove if you redefine < like we did the arithmetic operators above

[Monica Omar]

yeah, and I thought saying that they technically have different elements and evaluations means that they are nonequal types

[Damiano Testa]

As has already been commented, I think that it is very easy to find reasons why the structures you put on Nat and Int are different, but wondering about whether these structures are defined on the same type or not is neither meaningful nor decidable.

[Monica Omar]

can we prove the undecidability of it

[Eric Wieser]

No, because the axiom of choice says you can't prove undecidability of anything (in the sense of Decidable (ℕ = ℤ))

[Monica Omar]

lol

[Eric Wieser]

So if you could, the axiom of choice would be inconsistent

[Damiano Testa]

If the axiom of choice were inconsistent, though, you would then be able to prove that it is undecidable (among other things).

[Jireh Loreaux]

I think Damiano meant provable, not decidable above.

[Damiano Testa]

Also, by "not meaningful" I meant that it is not a meaningful mathematical question. I find that whenever this issue comes up on Zulip, there is always something to be learned.

[Monica Omar]

right, so this is just some non-mathematical meta-philosophical nonsense

[Monica Omar]

this being my question

[Monica Omar]

lol this went from me trying to find some easy example of non-equal non-empty Types for class next week, to having some meta-philosophical meltdown

[Damiano Testa]

In particular, I feel like no one picked up Eric's challenge:

Eric Rodriguez said:

As far as I know (and I know I'm going to get subtly corrected but I don't remember the other way) the only way to prove two types are not equal is that they don't have the same cardinality

Let's see how many of these examples we can prove!

example : (Unit × Unit) ≠ Unit := sorry
example : (Unit × Unit) = Unit := sorry
example {α} [Nonempty α] : (α × Unit) ≠ α := sorry
example {α} [Nonempty α] : (α × Unit) = α := sorry

[Jireh Loreaux]

Isn't the answer none? Because Lean doesn't know the model behind the inductive Prod type?

[Damiano Testa]

Honestly, I am not sure: you are probably right, but I was wondering whether you could deduce a contradiction from non-well-foundedness of "first projections". Not sure.

[Jireh Loreaux]

Like, I think it's the case that the only way to prove (within Lean) that two types are equal is if they are equal by definition, and the only way to prove that two types are not equal is if they have different cardinalities.

[Jireh Loreaux]

I could be wrong though, I'm not a type theorist!

[Kevin Buzzard]

Monica Omar said:

yeah, and I thought saying that they technically have different elements and evaluations means that they are nonequal types

I think you are confusing the elements (terms) with their names. If Nat = Int (which I hope we've now established is actually possible) then this certainly doesn't mean that (0 : Nat) = (0 : Int), because the typeclass inference search which finds the term whose name is 0 in a type will behave differently depending on whether it's looking for a Nat or an Int. In fact if Nat = Int then it's necessarily true that there is some concrete natural n such that (n : Nat) and (n : Int) are different terms, because (-1 : Int) must correspond to some natural under the identification Nat = Int.

An analogue would perhaps be the question which we are fond of setting the undergraduates: prove that $\mathbb{R}-\{-1\}$ is a group, if the group law is defined by $x\star y=xy+x+y$. If we made this a Group in Lean then it would have a 1 (in the sense that one of the terms would now have the new name 1), but this 1 wouldn't be the $1\in\R$.

[Damiano Testa]

Right, I do not have any proof to any of the examples above, but would be very interested in any proof!

[Kevin Buzzard]

The proof that all of those examples are undecidable is "rfl doesn't work and they have the same cardinality"

[Damiano Testa]

Hmm, maybe. Although sometimes by rfl works, where rfl does not.

[Damiano Testa]

Anyway, I am happy to believe that the type equalities above are undecidable.

[Jireh Loreaux]

Damiano, I think the idea is this. There's a model of Lean where all types with the same cardinality are equal (because under the hood you define them all to be the same type), and there's another model where any two distinct types (not defined with def, so inductives) are actually different under the hood.

[Damiano Testa]

Yes, I read this idea, but maybe I have not yet internalised that it is really consistent to have all types of the same cardinality being equal.

[Jireh Loreaux]

Just extend the Int' = Nat idea above to all denumerable types (and do the same thing for other cardinalities)

[Damiano Testa]

I can see how this would work for any finite number of types being made equal. What I am missing is that you can actually to this for all types of the same cardinality.

[Jireh Loreaux]

What is the distinction exactly between finite and all types?

[Damiano Testa]

I meant that you can prove that finitely many types are equal to one another, but not that all products Unit, Unit x Unit, Unit x Unit x Unit, ... are all the same.

[Damiano Testa]

(At least, I am not seeing how, that is all I was saying.)

[Damiano Testa]

In this case, maybe you can prove that Unit x anything is anything?

[Damiano Testa]

Anyway, idle speculation! :smile:

[Jireh Loreaux]

They will all be equal by rfl in that model (I think). I think that's wrong actually.

[Damiano Testa]

The thing is that, when you talk about "model", you have already committed to it being consistent.

[Jireh Loreaux]

I think when we say model here we mean within ZFC + ω inaccessible cardinals or something. (If you can't tell, I'm getting out of my depth now)

[Damiano Testa]

I am also out of my depth, so maybe I should stop continuing to ask questions in this thread! :smile:

[Monica Omar]

@Damiano Testa, I think @Eric Rodriguez meant (please correct me if I'm wrong) that you can prove they aren't equal if they have non-equal cardinality or if one is countable and the other isn't

so, for example, Real ≠ Nat would be easy to prove in Lean

[Damiano Testa]

Right, this is why my examples all have the same cardinality.

[Monica Omar]

Jireh Loreaux said:

Like, I think it's the case that the only way to prove (within Lean) that two types are equal is if they are equal by definition, and the only way to prove that two types are not equal is if they have different cardinalities.

Based on this whole discussion, I think this is true

I'm not a type theorist either tho, so we could be wrong haha

[Notification Bot]

Monica Omar has marked this topic as resolved.

[Notification Bot]

Bulhwi Cha has marked this topic as unresolved.

[Bulhwi Cha]

I'm fine with not being able to prove ℕ ≠ ℤ in Lean, but I hate to see newcomers puzzled by this fact.

I've met a few Koreans online who said that the set.mm database seems fundamentally different from ordinary mathematics. It was my fault for not properly explaining the foundational details of Metamath and its ZFC-based math library. To be honest, I still don't know much about these aspects.

But I also realized that some math majors in South Korea might suspect most libraries of formalized mathematics are nonstandard because these libraries look eccentric. Most of them have never heard about type theory.

Kevin Buzzard said:

In set theory, the naturals are defined via some weird construction involving sets of sets, and then the integers are defined perhaps as some equivalence classes of ordered pairs, so they're also just some weird sets of sets, and now someone could ask whether the naturals and the integers are equal by coincidence, and now you realise that this is a really weird question because now all of a sudden it really matters what your definition of things like "ordered pair" is, and there are three definitions of an ordered pair on Wikipedia, and so in set theory now you realise that whether the naturals and the integers are equal is not really even a well-defined question because it depends on things which mathematicians don't think or care about. My point is -- do you know for sure that the naturals and the integers in set theory are not coincidentally equal, given that their definitions are under the hood totally weird?

Despite what Kevin Buzzard said above, I fear I might fail to make a good impression of Lean on Korean mathematicians when I have to say "You can't prove ℕ ≠ ℤ in Lean." The only solution I can think of is to study mathematical logic and explain the foundations of proof assistants to them as professionally as Mario Carneiro does.

[Jireh Loreaux]

Bulhwi Cha said:

Despite what Kevin Buzzard said above, I fear I might fail to make a good impression of Lean on Korean mathematicians when I have to say "You can't prove ℕ ≠ ℤ in Lean."

I claim that this basically never needs to come up. What you can prove is that:

example : ¬ Function.Surjective ((↑) : ℕ → ℤ) := by
  intro h
  obtain ⟨x, hx⟩ := h (-1)
  have : (0 : ℤ) ≤ -1 := x.cast_nonneg.trans_eq hx
  norm_num at this

which is all that a mathematician ever really means when they say ℕ ≠ ℤ, they just normally don't phrase it that way.

[Mario Carneiro]

@Damiano Testa said:

I can see how this would work for any finite number of types being made equal. What I am missing is that you can actually to this for all types of the same cardinality.

Damiano Testa said:

I meant that you can prove that finitely many types are equal to one another, but not that all products Unit, Unit x Unit, Unit x Unit x Unit, ... are all the same.

Let me expound on the cardinality model a bit. We take as the "types" all cardinal numbers (initial ordinals), and the elements of those sets are the elements of the type. For each type former, we need to map everything back to an initial ordinal and we do so using a copious serving of the axiom of choice: for example, we define [[A -> B]] to be |[[A]] -> [[B]]|, and fix an equivalence $\eta_{A,B}: ([[A]] \to [[B]])\simeq |[[A]] \to [[B]]|$ which we use to define the constructors and destructors for the type, i.e. $[[\lambda x:A,e]]=\eta_{A,B}(x:[[A]]\mapsto [[e]])$ and $[[f\;a]]=\eta^{-1}_{A,B}(f)(a)$.

Most operations can't even tell that the $\eta$ functions are being inserted, except for equality on types, which is defined as equality of these cardinals, which means for example that Nat = Int is true in this model, with the result of cast being $\eta_{Nat}\circ \eta^{-1}_{Int}$, which will be something random picked out by the axiom of choice.

[Damiano Testa]

Mario, thank you for your answer: it clears up some doubts.

[Mark Fischer]

Do homotopy type theory or univalent foundations change this at all?

[Adam Topaz]

I think $\N$ and $\Z$ are equal in HoTT.

[Adam Topaz]

(both being sets)

[Kevin Buzzard]

But this is a different kind of equal -- they are equal in many ways in HoTT. Things can only be equal in one way in Lean, this is the axiom of Lean which means that HoTT = is incompatible with Lean's =.