Subtypes

Stream: new members

[Brandon Brown]

How does one create subtypes? Say I want a function of two parameters one is an arbitrary natural number, the other is a natural number < 100.

[Bryan Gin-ge Chen]

In this case I would just use fin:

def foo (m : ℕ) (n : fin 100) := sorry

In general, {a // P a} where α : Type and P : α → Prop is notation for the subtype of terms of type α that satisfy P. Subtypes are mentioned briefly in TPiL in chapter 7. See also this mathlib doc page.

[Brandon Brown]

Thanks!

[Brandon Brown]

Why doesn't this work?

[Brandon Brown]

example : ℕ := 4 -- ok
example : {n : ℕ // n ≤ 100} := 4 --error

[Bryan Gin-ge Chen]

Because 4 is not a term of that subtype. You can construct a term like this:

import tactic
example : {n : ℕ // n ≤ 100} := ⟨4, by norm_num⟩
-- dec_trivial also works and doesn't require any import

[Brandon Brown]

But example : fin 100 := 4 works

[Bryan Gin-ge Chen]

That's because 4 is a term of type fin 100:

set_option pp.numerals false
#check (4 : fin 100)
/-
bit0 (bit0 has_one.one) : fin (bit0 (bit0 (bit1 (bit0 (bit0 (bit1 has_one.one))))))
-/

See here. Note how Lean interprets numerals in terms of bit0, bit1 and has_one.one and has_zero.zero.

[Kevin Buzzard]

Just because the thing you defined, {n : ℕ // n ≤ 100} is "pretty much exactly the same thing as" fin 100, doesn't mean that everything that works for fin 100 will work for {n : ℕ // n ≤ 100}. There are lots of extra definitions which have been put on top of fin n, e.g. it has a 0, a 1, an add, and so on. If you want the same for your type you'll have to give it a name and put all these structure on it yourself.

[Kevin Buzzard]

Deleted

[Brandon Brown]

I want to implement a function that adds two lists of the same length element-wise, but I don't know how to make sure the lists are the same size. Should I instead return an option list so that if they're the same size (using if..then..else) then I can do some computation and return some list otherwise none ?

[Jalex Stark]

If you want lists of fixed length, you could use vectors :P
If you're doing it with lists, you probably want something like

example {α : Type} (a b : list α) (length_eq : list.length a = list.length b) : list α := sorry

[Shing Tak Lam]

If you want to define it for vectors, it'd look something like this:

import data.vector

def add_vecs {α : Type} [has_add α] {n : ℕ} : vector α n → vector α n → vector α n := sorry

[Brandon Brown]

Yeah I should do this with vectors I don't know why I'm using lists

[Shing Tak Lam]

Although if you want to define your function by pattern matching/recursion, it may be a bit more complicated than by just using lists.

[Shing Tak Lam]

and when you try to call the function, vectors is not as nice to use compared to lists.

[Brandon Brown]

Actually this works pretty well even for non-equal lists.

def list_add {α : Type u} [has_add α] : list α → list α → list α
| list.nil l2 := l2
| l1 list.nil := l1
| (h1 :: t1) (h2 :: t2) := (h1 + h2) :: (list_add t1 t2)

#reduce list_add [5,1] [5,2] -- [10, 3]
#reduce list_add [1,3] [2,3,3] -- [3, 6, 3]

[Brandon Brown]

I can create a type class instance for it

instance list_has_add {α : Type u} [has_add α] :
has_add (list α) := ⟨list_add⟩

#reduce [1,2] + [3,4] -- [4,6]

I don't know what the brackets for ⟨list_add⟩ are doing. I'm familiar with the angle brackets being used to create sigma types and and-conjunction but not sure what it means in this context

[Shing Tak Lam]

It's the short version for

instance list_has_add {α : Type u} [has_add α] :
has_add (list α) := {add := list_add}

[Brandon Brown]

Oh so {add := list_add} is a structure

[Shing Tak Lam]

has_add is a class, but I think so?

Better wait for an expert to chime in (I think most/all are asleep right now). In the mean time, I think this is the correct section of TPIL.

https://leanprover.github.io/theorem_proving_in_lean/type_classes.html#type-classes-and-instances

Let us start with the first step of the program above, declaring an appropriate class:

class inhabited (α : Type _) :=
(default : α)

The command class above is shorthand for

@[class] structure inhabited (α : Type _) :=
(default : α)

[Brandon Brown]

Ah I didn't catch that. So a type class _is_ a structure

[Shing Tak Lam]

(I think there is a difference? But I'm not sure about this myself, so this is probably when you wait for an expert to come by. I think the Europeans will wake up in a few hours)

[Brandon Brown]

Fair enough, I'm in Chicago so I'm off to bed soon - hopefully will wake to some more clarification. But thanks for your help!

[Mario Carneiro]

there is no difference

[Mario Carneiro]

class is sugar for @[class] structure

[Brandon Brown]

Thanks for clarifying. Then what is an instance ? Is that also syntactic sugar for something I'm familiar with already?

[Mario Carneiro]

instance is sugar for @[instance] def

[Mario Carneiro]

except that with instance the name is optional (else it makes a name by a simple heuristic), while def requires a name

[Mario Carneiro]

However, the @[class] and @[instance] attributes add additional behavior in conjunction with the [foo x] instance binder to trigger type class inference

[Mario Carneiro]

but from a foundational standpoint, an instance is just a def and a class is just a structure (and a structure is just an inductive)

[Brandon Brown]

Thanks! That makes things much clearer.

[Brandon Brown]

Just found this definition of vector in the standard library
def vector (α : Type u) (n : ℕ) := { l : list α // l.length = n }
That seems quite elegant compared to the one in TPIL

[Mario Carneiro]

a lot of people think the dependent family version is better, because it makes it easier to define functions by induction on vectors

[Mario Carneiro]

however, the example in TPIL is mostly there as an example of a dependent type family

[Brandon Brown]

It's weird that in order to create a vector using the subtype version, you have to provide a list along with a proof that it is the right length; which makes me like the TPIL one better now.
def myvec : vector ℕ 2 := ⟨[1,2], dec_trivial⟩

[Mario Carneiro]

You can still create a vector using a cons function with the same type as the TPIL one so that you don't need a side proof

[Mario Carneiro]

it's just a definition now instead of a constructor

[Brandon Brown]

How do you do that?

[Mario Carneiro]

Look up the definition of vector.cons in the core library

[Brandon Brown]

Ah I see, nice. def myvec2 (n : vector ℕ 0): vector ℕ 2 := vector.cons 1 (vector.cons 2 n)