subtype coercion to supertype

Stream: new members

[Kevin Kappelmann]

I was wondering if I use subtypes (and coercions to their supertype) correctly. For example, let's define a subtype of lists of length, say, at most 5:

def short_list (α : Type*) := {l : list α // l.length ≤ 5}

Now, given some sl : short_list α, I naturally would like to re-use functions from list. For example:

variables (α : Type*) (sl : short_list α)
/- What I would like to have -/
#check list.length sl -- error - expected list but got short_list
/- What also does not work -/
#check list.length (sl : list α) -- error since no coercion to list is known
/- What works but is not what I want -/
#check list.length sl.val

So what I ended up doing is this:

instance short_list_to_list : has_coe (short_list α) (list α) := ⟨λ sl, sl.val⟩

@[simp, elim_cast]
lemma coe_short_list (sl : short_list α) : (↑sl : list α) = sl.val :=
by refl

/- Works -/
#check list.length (sl : list α)
/- Does not work -/
#check list.length sl

Is this the best I can do? Is it the right thing to do? If so, shouldn't these kind of coercions be created automatically?

[Kevin Buzzard]

I guess that short_list alpha is a wrapper for subtype, so even if there was a coercion from subtype it wouldn't trigger for short_lists.

[Kevin Buzzard]

import data.subtype

def short_list (α : Type*) := {l : list α // l.length ≤ 5}

instance subtype_coe_thing (α : Type*) (P : α → Prop) :
has_coe {a : α // P a} α := ⟨λ x, x.val⟩

variables (α : Type*) (sl : short_list α)
variable (sl' : {l : list α // l.length ≤ 5})

-- #check list.length (sl : list α) -- fails
#check list.length (sl' : list α) -- works

[Kevin Buzzard]

--instance short_list_to_list : has_coe (short_list α) (list α) := by apply_instance -- fails

instance short_list_to_list : has_coe (short_list α) (list α) :=
  by unfold short_list; apply_instance -- works

I could imagine that sometimes people make these wrapper definitions precisely to switch _off_ some automatic coercion!

[Kevin Kappelmann]

Oh great, that's exactly what I was looking for - thanks a lot Kevin :)

[Kevin Buzzard]

I'm not sure it is :-(

[Kevin Buzzard]

I still had to coerce to list alpha.

[Kevin Kappelmann]

Hah, yeah - let me rephrase: the subtype_coe_thing part was exactly what I was having in my mind, that is a general coercion from subtypes to supertypes. The explicit coercion to list is still not "perfect".

[Kevin Kappelmann]

Moreover, I'd be very interested why that kind of automatic coercion is not enabled/built in. On a similar note, one cannot cast datatypes if the carrier type has a coercion. For example:

#check (([1,2,3] : list ℕ) : list ℤ) -- fails

variables {β γ : Type} [has_coe β γ]
instance option_to_option : has_coe (list β) (list  γ) := ⟨λ l, l.map (λ b, (↑b : γ))⟩

#check (([1,2,3] : list ℕ) : list ℤ) -- works