Zulip Chat Archive

Stream: new members

Topic: Proving types are different


view this post on Zulip Horatiu Cheval (Apr 03 2021 at 14:14):

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?

view this post on Zulip David Wärn (Apr 03 2021 at 14:31):

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

view this post on Zulip Eric Wieser (Apr 03 2021 at 14:53):

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

view this post on Zulip Eric Wieser (Apr 03 2021 at 14:55):

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

view this post on Zulip Kevin Buzzard (Apr 03 2021 at 15:01):

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.

view this post on Zulip Horatiu Cheval (Apr 03 2021 at 15:07):

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

view this post on Zulip Adam Topaz (Apr 03 2021 at 15:10):

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

view this post on Zulip Adam Topaz (Apr 03 2021 at 15:10):

(both are "the" terminal type)

view this post on Zulip Marcus Rossel (Apr 03 2021 at 16:22):

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

view this post on Zulip Kevin Buzzard (Apr 03 2021 at 16:22):

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.

view this post on Zulip Kevin Buzzard (Apr 03 2021 at 16:24):

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

view this post on Zulip Marcus Rossel (Apr 03 2021 at 16:33):

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

view this post on Zulip Kevin Buzzard (Apr 03 2021 at 16:35):

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.

view this post on Zulip Kevin Buzzard (Apr 03 2021 at 16:35):

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.

view this post on Zulip Kevin Buzzard (Apr 03 2021 at 16:37):

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.

view this post on Zulip Marcus Rossel (Apr 03 2021 at 16:39):

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?

view this post on Zulip Kevin Buzzard (Apr 03 2021 at 16:40):

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

view this post on Zulip Kevin Buzzard (Apr 03 2021 at 16:41):

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

view this post on Zulip Marcus Rossel (Apr 03 2021 at 16:42):

Ahhh ok, thanks Kevin :)

view this post on Zulip Kevin Buzzard (Apr 03 2021 at 16:44):

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.

view this post on Zulip Bryan Gin-ge Chen (Apr 03 2021 at 16:46):

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.

view this post on Zulip Julian Berman (Apr 03 2021 at 16:46):

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

view this post on Zulip Mario Carneiro (Apr 03 2021 at 22:45):

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.


Last updated: May 06 2021 at 21:09 UTC