Proving types are different

Stream: new members

[Horatiu Cheval]

How can I, in general, prove this sort of statements?

example : (unit × unit) ≠ unit := sorry

or

example : ℕ ≠ ℤ := sorry

My guess is that in general, no two inductive types are equal, is that the case?

[David Wärn]

I think Lean is consistent with the assertion that two types are equal iff they have the same cardinality (?). So you can't prove either of these

[Eric Wieser]

Right, the only proofs I've seen about types are ones that prove they can't be equal due to different cardinalities

[Eric Wieser]

Or ones that prove indexed families are equal given their indices are equal, such as list A = list B if A = B

[Kevin Buzzard]

Lean could be set up with int defined to be equal to nat but with a different zero, one, addition and multiplication. Similarly prod could be set up in such a way that prod X unit is definitionally equal to X. Asking if two types are distinct is asking the wrong kind of question, because it depends on what is going on under the hood.

[Horatiu Cheval]

Oh, interesting, I didn't know that, thank you all for the clarifications

[Adam Topaz]

In my nonformal opinion, unit x unit is equal to unit.

[Adam Topaz]

(both are "the" terminal type)

[Marcus Rossel]

@David Wärn where does this notion of equality come from?
So far I've only heard that types are definitionally equal if they are beta-reducible to each other in the context of CiC (I'm guessing this is only vaguely accurate).

[Kevin Buzzard]

For sure a category has only one terminal type up to unique isomorphism. However if you believe that it has one terminal type up to equality then I guess you're doing HoTT -- this is what Voevodsky believed.

[Kevin Buzzard]

@Marcus Rossel David (and Horatiu, in their question) is talking about Lean's eq, which I think some people call structural equality. It's an inductively defined proposition, which is weaker than definitional equality.

[Marcus Rossel]

@Kevin Buzzard what I'm wondering is, since eq is defined as:

inductive eq {α : Sort u} (a : α) : α → Prop
| refl [] : eq a

... how can we show anything to be equal that is not already definitionally equal? With n + 0 = n I guess it makes sense intuitively, as we can just unfold the definition of addition and then get definitionally equal terms. But with nat = int I don't see how this would work.

[Kevin Buzzard]

You should think about the 0 + n = n example. For any explicit natural number like 37, 0 + 37 = 37 is definitionally true. But if n : nat is arbitrary then0 + n = n is not definitional because you cannot unfold either side any more.

[Kevin Buzzard]

nat = int is not provable or disprovable in Lean, because it's "false" but the system has no way of expressing the reason it's false.

[Kevin Buzzard]

You can show things to be equal which aren't definitionally equal because the conclusion of nat.rec is forall n, C n and if C n is 0 + n = n then your proof involves an irreducible constant nat.rec.

[Marcus Rossel]

I think I misunderstand what is meant by "Lean is consistent with the assertion that two types are equal iff they have the same cardinality". Does this mean that all types of equal cardinality are equal?

[Kevin Buzzard]

No, it means the weaker statement that if you have two types of the same cardinality then it is not possible to prove that they are unequal. nat = int in Lean is undecidable (assuming that Lean has no bugs and that Lean's dependent type theory is consistent).

[Kevin Buzzard]

Had the designers done things in a different way (defining int to be a type wrapper for nat), then it could have been provable.

[Marcus Rossel]

Ahhh ok, thanks Kevin :)

[Kevin Buzzard]

Actually I am slightly overstepping the mark -- I do not actually know how to prove (on paper) that it is impossible to prove nat = int in Lean with the current definitions of nat and int.

[Bryan Gin-ge Chen]

I could be mistaken, but I think each time we declare an inductive type in Lean we’re effectively adding a bunch of new axioms to the system. Somehow this makes the undecidability of nat = int less surprising to me.

[Julian Berman]

Why doesn't foo = bar for heterogeneous types invoke some typeclass, and for nat and int one that says "no we're not equal" in a sense other than definitional equality

[Mario Carneiro]

Kevin Buzzard said:

Actually I am slightly overstepping the mark -- I do not actually know how to prove (on paper) that it is impossible to prove nat = int in Lean with the current definitions of nat and int.

There is another model for lean to help with this. If the "minimal model" is the one where types are cardinals and you define all the core inductive constants by bijecting the obvious definition to its cardinal, the "maximal model" is the one where types are "codes" that represent the way the type was constructed. You can think of the set of codes as being an inductive type with constructors pi : code -> code -> code, univ : nat -> code, and mu : nat -> inductive_spec -> list code -> code, where the nat parameter in mu is an arbitrary disambiguator so that even if two inductives have the same specification, you can still make countably many distinct copies of it. That way, nat and int have different disambiguators (and different specifications), so they are not equal.