Newbie question : Equality of Types

Stream: new members

[Madir Mabbott]

I have a few weeks of messing around with Lean 4, working through the Foundations of Mathematics 2024; so far up to section 9 : Bijections and Isomorphisms. Reached an impasse this morning on what seems to be a very basic question when testing my own knowledge of the fundamentals.

In my understanding types are first class objects so can be compared for equality. Indeed, the code fragment below shows that the Nat type is equal to itself, by simple reflection. However, I am stuck trying to demonstrate inequality of types - to take a simple practical example, demonstrating Nat and Int are unequal.

   def equalTypes (A B: Type) := (A = B)
   example : equalTypes ℕ ℕ := rfl
   example : ¬ equalTypes ℕ ℤ := by unfold equalTypes; intro h; sorry

Is this just a newbie gap in my knowledge of the appropriate tactic to apply, or am I missing something conceptual? (Of course, one could present a specific term to demonstrate the distinction between the naturals and the integers, but my concern is how to demonstrate the abstract case of two quite general types A and B.)

[Yaël Dillies]

You are missing something fundamental. This is unprovable

[Paul Rowe]

This question comes up with some frequency. The short answer is that you are not missing a simple tactic or anything. Surprisingly, it is not possible to prove that ℕ and ℤ are distinct types.

Consider that, since they have the same cardinality, the terms of the two types could be represented internally by the same underlying objects. Of course the interpretation of those objects will be different when they are viewed as terms of type ℕ versus terms of type ℤ. For example, the object representing 0 : ℕ could be wildly different from the object representing 0 : ℤ.

Notice that one typical tactic for proving equality of collections of things is ext. If you try that instead of rfl in showing that ℕ is the same type as itself, you get an error no applicable extensionality theorem found for Type.

Fortunately, type (in)equality doesn't really come up naturally in doing the mathematics found in a typical curriculum.

[Gareth Ma]

Is it possible to prove types are different by some structural property about the types? For example, to prove that \N has a minimum element but \Z doesn't?

def p (α : Type) [LT α] := ∀ a : α, ∃ b : α, b < a

theorem t_nat : ¬p ℕ := by
  rw [p]
  push_neg
  use 0
  simp

theorem t_int : p ℤ :=
  fun a ↦ ⟨a - 1, by omega⟩

axiom thing {α β : Type} [hα : LT α] [hβ : LT β] : α = β ↔ (∀ p : (γ : Type) → [LT γ] → Prop, p α ↔ p β)

example : ℕ ≠ ℤ := by
  apply thing.not.mpr
  push_neg
  use p
  simp [t_nat, t_int]

[Gareth Ma]

The axiom is definitely wrong because the instance $[LT \gamma]$ can be any instance of that type (? if that makes sense), but I wonder if a variant can be done

[Gareth Ma]

Or why not

[Luigi Massacci]

I think (might be wrong) the point is that you should distinguish the types from the structures on the type. $\mathbb{Z}$ doesn't have an ordering "by default". If you put the usual one, then yes you can prove that it is not order isomorphic to $\mathbb{N}$. But this doesn't mean that the underlying carriers aren't the same

[Luigi Massacci]

Just that the two structures you put on top of them interpret the elements differently

[Gareth Ma]

That makes sense, but I wonder if you can prove that every possible ordering you put on $\mathbb{Z}$ will have this property. Then that'll prove the types are not equal. But now that I think about it, since $\mathbb{Z}$ is isomorphic to $\mathbb{N}$, the statement is false

[Luigi Massacci]

What do you mean every possible ordering? There is an isomorphism $\mathbb{Z} \to \mathbb{N}$, so you could stick the usual ordering of $\mathbb{N}$ to $\mathbb{Z}$ that way, and then in your new order structure on $\mathbb{Z}$, there would be a least element (since it would be order-isomorphic to $\mathbb{N}$)

[Luigi Massacci]

Ok you saw it by yoursef

[Luigi Massacci]

I mean the mathematician's answer is that in any case you really shouldn't care. After all in ZFC you could ask the following question: "Is $\pi = (\mathbb{Z}_{37}, +)$ ?" After all they are both some kind of monstrous sets of sets, so this is well posed. Suppose the answer were "Yes". Would you care? Of course not, that is just an artifact of the implementation. Probably if you took a different encoding of ordered pairs, it would no longer be true. So it's not really a "mathematical" question, since as a mathematician you care only about the sets modulo their interpretation. It's kind of the same idea here. The question of whether $\mathbb{N} = \mathbb{Z}$ as types, is about the encoding, and so not really meaningful mathematically

[Kyle Miller]

Gareth Ma said:

Is it possible to prove types are different by some structural property about the types? For example, to prove that \N has a minimum element but \Z doesn't?

Orderings are auxiliary data to a type and not part of the type itself. That's to say, the ordering is not a structural property of a type.

A good model (at least according to me, who is neither a type theorist nor logician) is that in Lean, every type expression refers to some set (the type itself, so to speak). This mapping from type expressions to sets need not be injective. In fact there's a Cantor-style argument to prove that it definitely is not injective, though it's a nonconstructive proof and it only shows the mere existence of two type expressions that yield the same type.

In principle the expression ℕ could refer to the same set as ℤ does. But it also doesn't need to. So by some model theory, whether or not they are equal is unprovable.

[Madir Mabbott]

Appreciate the explanations and discussions. Thanks.

[Gareth Ma]

Yeah this is interesting, my mental picture is clearer too

[Gareth Ma]

Thanks

[Jireh Loreaux]

There's a thread with much more detail about this question which you may find interesting @Madir Mabbott and @Gareth Ma : https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Equality.20with.20Types

[Paul Rowe]

This question comes up frequently enough that it would be nice to have a polished explanation we could point people to. Is this question addressed in any of the learning resources?

[Gareth Ma]

(The start of that thread is not really useful for # new members lol, it's just a bunch of experienced Lean users shoving the idea that type equality is not useful)

[Madir Mabbott]

The type-theoretic explanations for this are initially quite a lot to swallow. I suppose as an everyday mathematician I've become attached to particular models for Nat and Int and have grown to expect these to be canon. However, I found two mathematically-oriented justifications from that earlier thread quite illuminating:
Kevin Buzzard said:

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.

Damiano Testa said:

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

So this really sharpens up one's feel for the formal distinction between a structure and a particular model, even when that model is unique up to isomorphism.