Zulip Chat Archive

Stream: new members

Topic: Uniqueness of inductive types

Patrick Johnson (Nov 15 2021 at 15:04):

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 (Nov 15 2021 at 15:07):

You can only prove it if they have different cardinalities

Kyle Miller (Nov 15 2021 at 16:22):

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 (Nov 15 2021 at 16:28):

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 (Nov 15 2021 at 16:54):

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 (Nov 15 2021 at 17:06):

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 (Nov 15 2021 at 17:09):

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

Kyle Miller (Nov 15 2021 at 17:12):

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 :=
    intro l,
    induction l with x xs ih,
    { refl },
    { simp! [ih], },
  right_inv :=
    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.

Last updated: Dec 20 2023 at 11:08 UTC