Uniqueness of inductive types

Stream: new members

[Patrick Johnson]

Given two definitions of inductive types, can we prove that the types are distinct? For example:

inductive A : Type
| mk1 : A

inductive B : Type
| mk1 : B
| mk2 : B

Can we always prove something like lemma a_ne_b : A ≠ B? In this particular case it can be proved using heterogeneous equality, because they have different cardinalities. But is it possible in general?

[Reid Barton]

You can only prove it if they have different cardinalities

[Kyle Miller]

The mental model I have is that Lean is only promising that it's able to implement the type for you in some way. Since everything is typechecked, elements don't need to know what type they're from, so in principle it could reuse representations between different types.

For example, it wouldn't be wrong for Lean to take

inductive my_list (α : Type*)
| nil : my_list
| cons : α → my_list → my_list

and compile it like this:

def my_list (α : Type*) := list α
def my_list.nil {α : Type*} : my_list α := list.nil
def my_list.cons {α : Type*} (x : α) (xs : my_list α) : my_list α := list.cons x xs
def my_list.rec ...
...

Lean only lets you prove things that are independent of how it might be implementing things behind the scenes, which is why list α = my_list α is neither provable nor disprovable.

[Kyle Miller]

Also, it turns out that even if the arguments to a type constructor are different, the resulting types might be the same. In fact, there must be cases where this happens by a diagonalization argument: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/disjointness.20of.20inductive.20type.20constructors.2C.20heq/near/204877510

[Stuart Presnell]

Could we prove a weaker relation between list and my_list in this case? Is there a suitable notion of isomorphism or equivalence?

[Kyle Miller]

You could create an docs#equiv and show it carries my_list.nil to list.nil and my_list.cons to list.cons (i.e., show it's an isomorphism)

[Stuart Presnell]

Ok. And since we don't have univalence we couldn't derive from this isomorphism that they're equal. :)

[Kyle Miller]

Just to be completely explicit:

import tactic

inductive my_list (α : Type*)
| nil : my_list
| cons : α → my_list → my_list

variables {α : Type*}

def my_list.to_list : my_list α → list α
| my_list.nil := list.nil
| (my_list.cons x xs) := list.cons x xs.to_list

def list.to_my_list : list α → my_list α
| list.nil := my_list.nil
| (list.cons x xs) := my_list.cons x xs.to_my_list

def my_list_equiv : my_list α ≃ list α :=
{ to_fun := my_list.to_list,
  inv_fun := list.to_my_list,
  left_inv :=
  begin
    intro l,
    induction l with x xs ih,
    { refl },
    { simp! [ih], },
  end,
  right_inv :=
  begin
    intro l,
    induction l with x xs ih,
    { refl },
    { simp! [ih], },
  end }

lemma my_list_equiv.nil : my_list_equiv (my_list.nil : my_list α) = list.nil := rfl
lemma my_list_equiv.cons (x : α) (xs : my_list α) :
  my_list_equiv (my_list.cons x xs) = list.cons x (my_list_equiv xs) := rfl

-- Forgetting the definition of `my_list_equiv`, similar lemmas for `my_list_equiv.symm` follow.