Zulip Chat Archive

Stream: general

Topic: a short tutorial on data-structures in lean


Egbert Rijke (May 13 2020 at 07:15):

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 (May 13 2020 at 07:19):

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 (May 13 2020 at 07:20):

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 (May 13 2020 at 07:20):

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

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

Johan Commelin (May 13 2020 at 07:22):

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

Johan Commelin (May 13 2020 at 07:22):

But it means you won't have anything.

Egbert Rijke (May 13 2020 at 07:23):

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

Johan Commelin (May 13 2020 at 07:23):

You can import stuff after prelude, I think

Egbert Rijke (May 13 2020 at 07:24):

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 (May 13 2020 at 07:24):

This doesn't compile for me

Johan Commelin (May 13 2020 at 07:25):

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

Egbert Rijke (May 13 2020 at 07:26):

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 (May 13 2020 at 07:26):

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 (May 13 2020 at 07:26):

Ah it was meant to be open list

Johan Commelin (May 13 2020 at 07:26):

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 (May 13 2020 at 07:26):

otherwise I have to keep typing list.cons right?

Egbert Rijke (May 13 2020 at 07:27):

Using emacs mode

Kevin Buzzard (May 13 2020 at 07:27):

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 (May 13 2020 at 07:27):

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 (May 13 2020 at 07:29):

Egbert Rijke said:

Using emacs mode

I hope that it will tell you about errors somehow.

Egbert Rijke (May 13 2020 at 07:29):

Yep, it shows me lots of red

Egbert Rijke (May 13 2020 at 07:30):

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

Johan Commelin (May 13 2020 at 07:31):

Red is not good (-;

Egbert Rijke (May 13 2020 at 07:32):

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

Johan Commelin (May 13 2020 at 07:32):

Error?

Egbert Rijke (May 13 2020 at 07:33):

type mismatch

Egbert Rijke (May 13 2020 at 07:33):

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

Johan Commelin (May 13 2020 at 07:33):

Which types?

Johan Commelin (May 13 2020 at 07:33):

Aah, annoying

Johan Commelin (May 13 2020 at 07:33):

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

Johan Commelin (May 13 2020 at 07:34):

But can you manually say which types it complains about?

Johan Commelin (May 13 2020 at 07:34):

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

Kenny Lau (May 13 2020 at 07:35):

why not call it List

Johan Commelin (May 13 2020 at 07:35):

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

Egbert Rijke (May 13 2020 at 07:36):

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

Johan Commelin (May 13 2020 at 07:36):

Do you have more code in your file?

Johan Commelin (May 13 2020 at 07:36):

But the fact that it uses notation seems bad

Johan Commelin (May 13 2020 at 07:36):

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

Kevin Buzzard (May 13 2020 at 07:36):

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

Kevin Buzzard (May 13 2020 at 07:37):

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 (May 13 2020 at 07:38):

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 (May 13 2020 at 07:39):

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 (May 13 2020 at 07:41):

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 (May 13 2020 at 07:41):

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 (May 13 2020 at 07:43):

BTW I really appreciate both your help

Johan Commelin (May 13 2020 at 07:46):

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

Egbert Rijke (May 13 2020 at 07:48):

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

Johan Commelin (May 13 2020 at 08:07):

@Egbert Rijke But which type does it report?

Johan Commelin (May 13 2020 at 08:08):

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

Johan Commelin (May 13 2020 at 08:08):

Also, which Lean version are you using?

Egbert Rijke (May 13 2020 at 08:09):

#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 (May 13 2020 at 08:10):

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

Kevin Buzzard (May 13 2020 at 08:11):

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 (May 13 2020 at 08:11):

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 (May 13 2020 at 08:11):

@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 (May 13 2020 at 08:12):

Ah great! Thanks Sebastian! And hello :)

Kevin Buzzard (May 13 2020 at 08:12):

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

Egbert Rijke (May 13 2020 at 08:12):

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 (May 13 2020 at 08:12):

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 (May 13 2020 at 08:13):

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

Kevin Buzzard (May 13 2020 at 08:13):

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

Kevin Buzzard (May 13 2020 at 08:13):

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

Sebastian Ullrich (May 13 2020 at 08:13):

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

Marc Huisinga (May 13 2020 at 08:13):

try

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

Marc Huisinga (May 13 2020 at 08:14):

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

Egbert Rijke (May 13 2020 at 08:14):

That works!

Johan Commelin (May 13 2020 at 08:14):

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

Kevin Buzzard (May 13 2020 at 08:14):

2019 :-)

Egbert Rijke (May 13 2020 at 08:14):

Haha really?

Kevin Buzzard (May 13 2020 at 08:15):

yeah it is like months old!

Johan Commelin (May 13 2020 at 08:15):

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

Marc Huisinga (May 13 2020 at 08:15):

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

Egbert Rijke (May 13 2020 at 08:15):

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

Kevin Buzzard (May 13 2020 at 08:16):

What you should do depends on what you already did

Egbert Rijke (May 13 2020 at 08:16):

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

Kevin Buzzard (May 13 2020 at 08:17):

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

Johan Commelin (May 13 2020 at 08:17):

#install

Johan Commelin (May 13 2020 at 08:17):

Too bad... that doesn't work

Kevin Buzzard (May 13 2020 at 08:17):

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

Kevin Buzzard (May 13 2020 at 08:18):

is what it should have linked to

Sebastian Ullrich (May 13 2020 at 08:18):

@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 (May 13 2020 at 08:19):

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

Egbert Rijke (May 13 2020 at 08:19):

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

Egbert Rijke (May 13 2020 at 08:20):

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

Johan Commelin (May 13 2020 at 08:20):

At least now we know the bug (-;

Kevin Buzzard (May 13 2020 at 09:18):

@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 (May 13 2020 at 09:20):

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 (May 13 2020 at 09:21):

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 (May 13 2020 at 09:21):

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

Egbert Rijke (May 13 2020 at 09:22):

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

Kevin Buzzard (May 13 2020 at 09:22):

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

Kevin Buzzard (May 13 2020 at 09:23):

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

Rob Lewis (May 13 2020 at 09:23):

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 (May 13 2020 at 09:24):

(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 (May 13 2020 at 09:25):

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 (May 13 2020 at 09:26):

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 (May 13 2020 at 09:27):

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 (May 13 2020 at 09:29):

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

Egbert Rijke (May 13 2020 at 09:29):

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

Sebastian Ullrich (May 13 2020 at 09:42):

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 (May 13 2020 at 10:47):

Maybe we can yoink lean out of homebrew...

Reid Barton (May 13 2020 at 11:57):

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 (May 13 2020 at 11:58):

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

Reid Barton (May 13 2020 at 11:59):

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 (May 13 2020 at 12:00):

@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 (May 13 2020 at 12:23):

You got this working for all OS's?

ROCKY KAMEN-RUBIO (May 13 2020 at 12:55):

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 (May 13 2020 at 17:03):

Johan Commelin said:

#install


Last updated: Dec 20 2023 at 11:08 UTC