Square, curly and normal brackets

Stream: new members

[yuppie]

Hey everybody,

I am still trying to do the lean exercises in section 2, i.e. defining vector addition, matrix addition and matrix multiplication. And this is what I have so far:

import data.vector

def vec_add (α:Type) [has_add α]: Π n : nat, vector α n → vector α n → vector α n
| _ ⟨ [],    h ⟩ _ := ⟨ [], h ⟩
| _ _ ⟨ [],    h ⟩ := ⟨ [], h ⟩
| (nat.succ n) v w :=
vector.cons (vector.head(v)+vector.head(w)) (vec_add n (vector.tail(v)) (vector.tail(w)))
#check vec_add

instance vec_has_add (α:Type)[has_add α](n:nat) : has_add (vector α n) :=
⟨vec_add α n⟩
#check vec_has_add

def scal_mul(α:Type)[has_mul α]: Π n : nat, α → vector α n → vector α n
| 0 a v := v
| (nat.succ n) a v := vector.cons (vector.head(v)*a) (scal_mul n (a) (vector.tail(v)))
#check scal_mul

This somehow works. But I what exactly is the difference between declaring a variable \alpha:Type in the beginning of a file and putting (\alpha:Type) in front of the colon of every declaration? What is the difference between normal brackets and curly braces?

E.g. in the definition of vec_add I had to make everything a a dependent type depending on n since otherwise the recursion wouldn't work out. Is it also possible to skip (\alpha:Type) in front of the colon and make everything a dependent type depending on \alpha?

It is hard to spell out but I have a bunch of problems which seem very similar to each other making me feel that I didn't get something conceptually.

[Johan Commelin]

The difference is that variable (α : Type) saves you some typing.

[Johan Commelin]

The difference between () and {} is in how you can call such declarations. If you use def foo {α : Type} then α is implicit which means that you don't pass that argument to foo when you call it.

[Johan Commelin]

This is useful, if α can be figured out by looking at other arguments (for example a : α might be another argument to foo.

[Johan Commelin]

If at some point you do want to tell Lean the argument α, you can write @foo α, and the @ will make all arguments to foo explicit.

[yuppie]

Oh thanks for the quick answer. I see.

[yuppie]

And writing variable \a:Type is somehow a "fixed constant" and every definition depending on it is fixed as well and cannot be instantiated with another type?

[yuppie]

I mean variable \a:Type is not syntactic sugar for inserting (a:Type) in front of every definition nor {a:Type}. It is really something else.

[Johan Commelin]

No, it is such syntactic sugar

[Johan Commelin]

And it is a bit smart, because it only gets inserted when needed

[Johan Commelin]

So it is not a "fixed constant"

[yuppie]

And is it sugar for normal brackets or curly braces?

[Johan Commelin]

Depends on what you put after the variables keyword

[Johan Commelin]

You can write variables {G : Type} [group G] (g : G)

[Johan Commelin]

And if halfway your file you need to switch, you can write variables (G) and from then on G will be explicit

[yuppie]

Ahhh, I see!

[yuppie]

Thanks. This clarified a lot.

[Rob Lewis]

If you write variable A : Type with no parentheses it's explicit, the same as (A : Type).

[Kevin Buzzard]

Thanks. This clarified a lot.

It took me ages to learn this. It was only looking through the mathlib source code and noticing Johannes constantly writing variable (X : Type) when he'd already got a variable X and finally asking someone what was going on, that it all dawned on me. @yuppie you should write up a brief variables.md file and PR it to the mathlib docs directory. Just a brief thing explaining the contents of this thread.

[yuppie]

Yeah I can do that although evidently I have no idea about it ;) Do you mean into the mathlib repo? Is that the right place for explanations of the lean core syntax?

[Kevin Buzzard]

I think so, and I want to make that doc directory grow. I certainly wrote stuff in it which explained simp and I wrote it exactly when I was in the same situation as you -- I had figured out some stuff about simp about 30 minutes previously and I just thought "sod it, I don't want to have to figure all of this out again, let me write it down". I've spent my entire life figuring out stuff and then just writing it down. In maths I ended up with this page http://wwwf.imperial.ac.uk/~buzzard/maths/research/notes/index.html and people love those notes, I get fan mail, google indexes them highly, it works great. Why not do the same with Lean? When people work stuff out, just write it down quick before you forget it all again.

[yuppie]

Ok I'll do it :)

[Bryan Gin-ge Chen]

Maybe the relevant section(s) in TPiL could be improved as well, though I don't have any concrete suggestions. @Jeremy Avigad

[Kevin Buzzard]

We don't need to keep hassling Jeremy. These facts could easily be in there and I just missed them first time around. TPIL is a brilliant document, I learnt so much from it, the mathlib docs can just build around it. @Sebastien Gouezel 's comment from the other day about how hard it was to use a new (to him) part of the library made me start thinking about this. @Calle Sönne was figuring out how to use equalisers in the category theory library at Xena last week and I was hugely encouraging him to just write something once he'd figured it out. It would be really nice to just get a bunch of users explaining stuff they understand as they understand it.

[Jeremy Avigad]

@Bryan Gin-ge Chen @Kevin Buzzard Don't worry about hassling me. I keep adding things to my list. I feel guilty that I am falling behind with corrections, but I am planning to catch up on Tuesday.

But I agree that it would be good to have more documentation for mathlib. The docs folder is great. But it is also not hard to set up a new Sphinx document with the same style as TPIL. I'll be happy to do that if there is community interest in putting together a nice mathlib reference.

[yuppie]

I have been experimenting with the different types of variable declarations. Here is a code snippet:

import data.vector

variables {α:Type}

def vec_add [has_add α] : Π n : nat, vector α n → vector α n → vector α n
| 0 _ _ := vector.nil
| (n+1) v w :=
vector.cons (vector.head(v)+vector.head(w)) (vec_add n (vector.tail(v)) (vector.tail(w)))
#check vec_add
#check @vec_add

def vec_add_2 [has_add α](n:nat) : vector α n → vector α n → vector α n
| 0 _ _ := vector.nil
| (n+1) v w :=
vector.cons (vector.head(v)+vector.head(w)) (vec_add_2 n (vector.tail(v)) (vector.tail(w)))
#check vec_add_2
#check @vec_add_2

The check commands indicate that both declarations are of the same type but the first implementation type checks and the second does not. Somehow it interprets the first (explicit) argument as a vector and not as a natural number which is necessary for the recursion.

My question: What is the difference between the two declarations (Pi after the colon vs. (n:nat) before the colon)? How do I make the implementation of vec_add_2 type check?

[Johan Commelin]

You can only pattern match on things after the colon

[Johan Commelin]

So you can use

| 0 _ _
| (n+1) foo bar

in the second example. You only have two arguments to match on.

[Anne Baanen]

To add: If you put arguments before the colon, they will be bound for the whole declaration. So within the definition of vec_add_2, the expression vec_add_2 has type vector α n → vector α n → vector α n

[Johan Commelin]

Right... that's an important thing to know for recursive definitions. And it took me some time to understand this. (I admit, I should probably have read TPIL...)

[yuppie]

I tried to write this stuff up and opened a PR but I am not sure whether I could and should have assigned this to a specific reviewer. How do you handle things here?

[Kevin Buzzard]

You don't need to assign it to anyone.

[yuppie]

Ok I hope this is kind of what you thought about.

[Johan Commelin]

@yuppie Thanks for the PR

[Chris B]

Sorry, wrong thread.