a short tutorial on data-structures in lean

Stream: general

[Egbert Rijke]

Hello!

I am the teaching assistant of Alex Simpson for a course on Logic with computers, and we want to introduce our students to lean. We only intend to cover the very basics, and we want the students to make basic exercises about lists in lean. I tried looking up the existing tutorials, but they are all covering much more ground that we will be able to do (we only have two weeks, in which the students will make one set of exercises). And I tried doing it from scratch in lean, but then it complains that the inductive data type of lists is already defined.

Does anyone have any suggestions, or tried teaching something similar?

With kind regards,
Egbert

[Kevin Buzzard]

I made a complete new copy of the natural numbers by working in a namespace mynat. You could work in a namespace hidden and then redefine lists there. A good exercise for students is of course proving that the reverse of the reverse of a list is the same list. When I was learning about lists in Lean I translated the software foundations exercises about lists from Coq into Lean. using this technique.

[Kevin Buzzard]

namespace hidden

inductive list (T : Type)
| nil : list
| cons (hd : T) (tl : list) : list

-- lemmas go here

end hidden

If you want to make things a bit less technical you could even define list nat instead.

[Egbert Rijke]

The suggestion about a hidden namespace is nice, thank you!

That is exactly the sort of exercises we are thinking of :)

[Johan Commelin]

@Egbert Rijke If you want to throw away the stuff defined in core, then you can use prelude.

[Johan Commelin]

But it means you won't have anything.

[Egbert Rijke]

prelude will be a bit too radical, for then we won't be able to use equality either

[Johan Commelin]

You can import stuff after prelude, I think

[Egbert Rijke]

Another question: why does lean say that I'm using sorry in the definition of concat_list

namespace hidden

inductive list (A : Type) : Type
| nil : list
| cons : A → list → list

open mylist

definition concat_list {A : Type} : list A → list A → list A :=
begin
  intros x y,
  induction x,
  { exact y},
  { exact (cons x_a x_ih)},
end

reduce concat_mylist (cons 1 (cons 2 (cons 3 nil))) (cons 4 (cons 5 nil))

end

[Kevin Buzzard]

This doesn't compile for me

[Johan Commelin]

@Egbert Rijke What does open mylist do there. You don't have a mylist namespace, right?

[Egbert Rijke]

Ah that brings me to another question, how can I know myself if it compiles? (I feel embarrassed to ask, but I really don't know)

[Kevin Buzzard]

I think you want namespace list and not open list; that way you will be using the correct list.cons. It might be better to use mylist; this might be worth experimenting with if you're going to get name clashes, but I think you should be able to get away with it in your own namespace.

[Egbert Rijke]

Ah it was meant to be open list

[Johan Commelin]

Egbert Rijke said:

Ah that brings me to another question, how can I know myself if it compiles? (I feel embarrassed to ask, but I really don't know)

What kind of setup do you have?

[Egbert Rijke]

otherwise I have to keep typing list.cons right?

[Egbert Rijke]

Using emacs mode

[Kevin Buzzard]

The "sorry" error is because reduce isn't a Lean command -- it's #reduce, which confused Lean about where the end of your proof was.

[Kevin Buzzard]

namespace hidden

inductive list (A : Type) : Type
| nil : list
| cons : A → list → list

namespace list

definition concat_list {A : Type} : list A → list A → list A :=
begin
  intros x y,
  induction x,
  { exact y},
  { exact (cons x_a x_ih)},
end

#reduce concat_list (cons 1 (cons 2 (cons 3 nil))) (cons 4 (cons 5 nil))

end list

end hidden

[Johan Commelin]

Egbert Rijke said:

Using emacs mode

I hope that it will tell you about errors somehow.

[Egbert Rijke]

Yep, it shows me lots of red

[Egbert Rijke]

With Kevin's fixes it shows me less red, but it still shows me some

[Johan Commelin]

Red is not good (-;

[Egbert Rijke]

so it is complaining about concat_list in the line where we #reduce

[Johan Commelin]

Error?

[Egbert Rijke]

type mismatch

[Egbert Rijke]

I don't know how to copy the error message because it disappears as soon as i stop hovering over it

[Johan Commelin]

Which types?

[Johan Commelin]

Aah, annoying

[Johan Commelin]

You should use a real editor (-; [/joking]

[Johan Commelin]

But can you manually say which types it complains about?

[Johan Commelin]

Is it still confusing _root_.list with hidden.list?

[Kenny Lau]

why not call it List

[Johan Commelin]

@Egbert Rijke If I copy Kevin's code, I don't get errors.

[Egbert Rijke]

in concat_list [1, 2, 3] term [1, 2, 3] has type list ?m1 : Type

[Johan Commelin]

Do you have more code in your file?

[Johan Commelin]

But the fact that it uses notation seems bad

[Johan Commelin]

I don't get the [1,2,3] notation

[Kevin Buzzard]

My code compiles fine here, no warnings, no errors.

[Kevin Buzzard]

Are you sure you have an exact copy of my code? The code you posted had several problems, switching between list and mylist, the missing # and so on.

[Kevin Buzzard]

If you are using it and see errors, then tell us which version of Lean you're using, which editor, etc, and we can debug.

[Kevin Buzzard]

My code does not mention [1,2,3] and this will point to the constructor for the usual list, not your own one. There are always issues with list ?m1 which is why I suggested that you might want to bake nat into the coefficients of your list.

[Johan Commelin]

Kevin Buzzard said:

... you might want to bake nat into the coefficients of your list.

I don't think that is in the spirit of functional programming...

[Egbert Rijke]

Ah, yes it was not an exact copy. But now I'm using an exact copy and it still complains (in a different spot) Screen-Shot-2020-05-13-at-09.38.53.png

[Egbert Rijke]

BTW I really appreciate both your help

[Johan Commelin]

@Egbert Rijke I can't decipher the error message from your screenshot...

[Egbert Rijke]

type mismatch at application cons 3 nil term nil has type ...

[Johan Commelin]

@Egbert Rijke But which type does it report?

[Johan Commelin]

What does #check cons 3 nil says? Is it what you expect?

[Johan Commelin]

Also, which Lean version are you using?

[Egbert Rijke]

#check cons 3 nil gives the same error, which is what I expect. Let me write the type (it will take a minute because it is complicated)

[Johan Commelin]

Can you copy paste the entire file that you are working in?

[Kevin Buzzard]

I am certain that there will be a way to see the errors properly in emacs, but because I don't use it for Lean I can't help. Just to be clear, you are using Lean 3, right?

[Egbert Rijke]

the type of nil in the error message is Π (A : Type), list A : Type 1 while it is expected to be list ?m_1

[Sebastian Ullrich]

@Egbert Rijke Hey Egbert! You can use C-c ! C-w to copy the error at the cursor position, and C-c ! l to open the list of errors. See also https://github.com/leanprover/lean-mode#key-bindings-and-commands for more tips.

[Egbert Rijke]

Ah great! Thanks Sebastian! And hello :)

[Kevin Buzzard]

Well, nil is expecting you to tell it the type of the elements of the list.

[Egbert Rijke]

namespace hidden

inductive list (A : Type) : Type
| nil : list
| cons : A → list → list

namespace list

definition concat {A : Type} : list A → list A → list A :=
begin
  intros x y,
  induction x,
  { exact y},
  { exact (cons x_a x_ih)},
end

#reduce concat (cons 1 (cons 2 (cons 3 nil))) (cons 4 (cons 5 nil))

end list

end hidden

[Sebastian Ullrich]

You are probably using an older version of Lean than the others because the default inference for constructors recently changed in leanprover-community

[Egbert Rijke]

If I say lean --version in my terminal, it says 3.4.2

[Kevin Buzzard]

#check @list.nil gives me list.nil : Π {A : Type}, list A

[Kevin Buzzard]

and you have a different type, so maybe you are not up to date.

[Sebastian Ullrich]

It now defaults to the old | nil {} : list, which will give you the same type as Kevin posted

[Marc Huisinga]

try

inductive list (A : Type) : Type
| nil {} : list
| cons : A → list → list

[Marc Huisinga]

(this works for me when using the old lean web editor, which is 3.4 too)

[Egbert Rijke]

That works!

[Johan Commelin]

@Egbert Rijke Your lean is ancient :grimacing: :rofl:

[Kevin Buzzard]

2019 :-)

[Egbert Rijke]

Haha really?

[Kevin Buzzard]

yeah it is like months old!

[Johan Commelin]

Which is a lot, given that Lean is still a toddler

[Marc Huisinga]

this "old" behavior is explained here:
https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html#constructors-with-arguments

[Egbert Rijke]

Ok let me update lean. Can I do that with brew (I'm on a mac)?

[Kevin Buzzard]

What you should do depends on what you already did

[Egbert Rijke]

I have no idea how I installed lean at the time :P

[Kevin Buzzard]

I would be tempted to just work through https://github.com/leanprover-community/mathlib/blob/master/docs/install/macos.md then

[Johan Commelin]

#install

[Johan Commelin]

Too bad... that doesn't work

[Kevin Buzzard]

https://github.com/leanprover-community/mathlib#installation

[Kevin Buzzard]

is what it should have linked to

[Sebastian Ullrich]

@Egbert Rijke To be clear, you are using the latest official version. It's just that the community took over after that and extended Lean 3 at https://github.com/leanprover-community/lean/. If you don't need mathlib at all, 3.4.2 is probably sufficient, especially if TPL etc are still written against it.

[Johan Commelin]

Otoh, you won't be able to offload the mentoring of your students to Zulip (-;

[Egbert Rijke]

Ok, thanks Sebastian. Given that my students will probably just install the official version, it might be best to stick with that.

[Egbert Rijke]

Haha, @Johan Commelin no that's why I'm asking all the stupid questions now :)

[Johan Commelin]

At least now we know the bug (-;

[Kevin Buzzard]

@Egbert Rijke it is not at all a given that your students will install the official version. If you Google for how to install lean you will probably end up with instructions for how to install the modern version. However if your students set up a project and explicitly write that it is a lean 3.4 2 project then it will be because the installer just downloads the correct version of lean for the project

[Egbert Rijke]

I'm not sure that I'm familiar with this infrastructure of projects and installers. I just installed lean via brew, isn't that how it is supposed to go?

[Kevin Buzzard]

There are links to the installation instructions for the modern version above, I have no idea how to install the old version on a Mac

[Kevin Buzzard]

We have seen issues before where students write code and their instructor is on 3.4.2 and can't compile it

[Egbert Rijke]

Ah, that would be me in two weeks :sweat_smile:

[Kevin Buzzard]

Students come here for help and often don't say "oh by the way this has to work in 3.4.2"

[Kevin Buzzard]

So if you are serious about not updating then you should make this very clear at the start

[Rob Lewis]

Hi Egbert! Expecting them all to get the same version is just asking for trouble. They won't, and it will be a nightmare.

The most flexible installation is with the version manager, elan. Have everyone install that (https://leanprover-community.github.io/get_started.html#install). You should create a "project" yourself. It's just a git repository with a special file in the root. Everyone else can clone your project, work on the files you give them or add their own, and elan should make sure they're using whichever Lean version you want.

[Rob Lewis]

(You should also delete whatever you have installed and follow the new installation directions. But if you set up a project that works for you with your current install, it should work for your students too.)

[Rob Lewis]

For an example of a project, see https://github.com/leanprover-community/tutorials . You can delete everything except leanpkg.toml. Add whatever Lean files you want in the src directory.

[Kevin Buzzard]

This is a great idea, this is the way to do it. If you make the project, you control which version of lean will be used

[Egbert Rijke]

Hi Rob! Great to see you again :)

Ok that setup might actually be great, because we can include files with the basic definitions already in there using sorry, and make the students fill them out. Thanks!

[Rob Lewis]

And if they're slightly competent with git, you can have them commit their own work, pull your updates, etc.

[Egbert Rijke]

They might be! Surely they are more competent on a computer than I am (unless you give me Agda) (-:

[Sebastian Ullrich]

I didn't actually know Lean was packaged in Homebrew. I truly believe only elan should ever be packaged system-wide, with Lean downloaded per-project by it.

[Scott Morrison]

Maybe we can yoink lean out of homebrew...

[Reid Barton]

Yes, this is a slightly weird thing where if you actually use Lean (or GHC, or Rust, etc.) directly, you almost certainly don't want to have your package manager install it, because it will probably install an old version or be missing packages you want or something.

[Reid Barton]

It's worth the minor effort of managing the installation yourself.

[Reid Barton]

The package manager packages are mostly useful if other things depend on them (like Haskell or Rust binaries?) but for Lean there aren't any such things.

[Patrick Massot]

@Egbert Rijke You could also prepare a zipped folder with everything needed for your student (Lean+libraries+VScode+extension, all in one folder). This is what I did in my class.

[Kevin Buzzard]

You got this working for all OS's?

[ROCKY KAMEN-RUBIO]

I was scared of namespaces when I first started doing data structures exercises so I just defined mylist and myvec like NNG does with nats. I found it useful to adapt exercises from this set of Haskell/functional programming problems https://wiki.haskell.org/H-99:_Ninety-Nine_Haskell_Problems

[Mario Carneiro]

Johan Commelin said:

#install