Chapter 2 inspired error

Stream: new members

[imran saleh]

Hi,

I'm reading the "Theorem Proving in Lean" textbook, and when messing around with the example code I get an error I don't understand. The error is that in chapter 2 when the vec namespace is defined, I try to define

variable a : α

followed by

variable e : empty α

where (recall) empty is defined as

constant empty : Π α : Type u, vec α 0

In my mind, the types should check out since I've given the function the only argument it needs. Yet I get the error:

invalid type ascription, term has type
vec α 0 : Type
but is expected to have type
Sort ? : Type ?

and I don't understand what this error means (as someone who has just begun learning Lean, and so doesn't know what "Sort" refers to here). Note, this also relates to difficulties completing exercise 3 in Chapter 2.

Any help is appreciated. Thanks in advance.

[Yaël Dillies]

Whoops, sorry, I misunderstood the error.

[Andrew Yang]

variable e : empty α means that e is a variable of Type empty α, but empty α is a term rather than a Type.
You probably want def e := empty α instead. (Though there are still some subtleties inside).

[Yaël Dillies]

Sorry, misunderstood again.

[Yaël Dillies]

It's not clear to me what you're trying to achieve. Also look at #backticks and #mwe

[Logan Murphy]

Here's one way to "use" the definition provided in TPIL to construct the empty vector over α :

constant α : Type

universe u

constant vec : Type u → ℕ → Type u

namespace vec

constant empty : Π α : Type u, vec α 0

end vec

noncomputable def e : vec α 0 := vec.empty α

As Andrew said, vec.empty is a term -- a function, which, given any type α , returns something of type vec α 0. If you want to make use of this function, you can do so as done in the definition of e here. I'm telling Lean that e will be something of type vec α 0, and to do this, I tell it to use the function vec.empty.

The decorator noncomputable is just here because vec.empty is an opaque constant, rather than a function with an actual definition.

[Logan Murphy]

When you make a variable or a constant, you can only really provide the type of something. But as Andrew pointed out, vec.empty is not a type.

[imran saleh]

Yaël Dillies said:

It's not clear to me what you're trying to achieve. Also look at #backticks and #mwe

I guess I'm trying to understand what the error means and why I can't define an empty vector

[imran saleh]

Logan Murphy said:

Here's one way to "use" the definition provided in TPIL to construct the empty vector over α :

constant α : Type

universe u

constant vec : Type u → ℕ → Type u

namespace vec

constant empty : Π α : Type u, vec α 0

end vec

noncomputable def e : vec α 0 := vec.empty α

As Andrew said, vec.empty is a term -- a function, which, given any type α , returns something of type vec α 0. If you want to make use of this function, you can do so as done in the definition of e here. I'm telling Lean that e will be something of type vec α 0, and to do this, I tell it to use the function vec.empty.

The decorator noncomputable is just here because vec.empty is an opaque constant, rather than a function with an actual definition.

Thanks. By this logic, in exercise 3 in the same chapter, I would again need to use the noncomputable decorator when creating the variables it asks for? (because it is asking us to define more opaque constants which seem like they would be noncomputable as well)

[Logan Murphy]

You don't need noncomputable to do the exercises in TPIL -- this was just for expository purposes, to highlight the difference between "declaring" a constant and "defining" something using that constant. I'm just looking at the exercise now...

[Kevin Buzzard]

imran saleh said:

Yaël Dillies said:

It's not clear to me what you're trying to achieve. Also look at #backticks and #mwe

I guess I'm trying to understand what the error means and why I can't define an empty vector

Can you write the code which gives the error which you'd like advice on as a #mwe using #backticks ? Do you see that this is what everyone else is doing in this thread? It makes it much easier to communicate clearly.

[Logan Murphy]

Yeah, the exercise is just trying to get you to figure out what the type signatures of functionsvec.add and vec.reverse should be, and to define some variables that can act as inputs to these functions

[Logan Murphy]

To do the exercise, you don't need defat all, so certainly don't need noncomputable.

[Logan Murphy]

(deleted)

[Kevin Buzzard]

(four backticks for code in spoilers)

[Logan Murphy]

Thanks, Kevin

[Logan Murphy]

Example solution (Spoiler!)

universe u

constant vec : Type u → ℕ → Type u

namespace vec

constant empty : Π α : Type u, vec α 0

constant add : Π {n : ℕ}, vec ℕ n → vec ℕ n → vec ℕ n

constant reverse : Π {α : Type}, Π {n : ℕ}, vec α n → vec α n

end vec

variable vec1 : vec ℕ 3

variable vec2 : vec ℕ 3

#check vec.add vec1 vec2

variable vec3 : vec string 37

#check vec.reverse vec3

-- note, when things are defined within namespaces, you can do some syntactic simplification.
-- for example, these are alternative notations for the above #check statements

#check vec1.add vec2
#check vec3.reverse

[Kevin Buzzard]

oh maybe you need to do ````lean to get syntax highlighting?

[Logan Murphy]

Yep, fixed!