Zulip Chat Archive

Stream: general

Topic: a short tutorial on data-structures in lean


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 13 2020 at 07:22):

But it means you won't have anything.

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 13 2020 at 07:23):

You can import stuff after prelude, I think

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 13 2020 at 07:24):

This doesn't compile for me

view this post on Zulip Johan Commelin (May 13 2020 at 07:25):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Egbert Rijke (May 13 2020 at 07:26):

Ah it was meant to be open list

view this post on Zulip 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?

view this post on Zulip Egbert Rijke (May 13 2020 at 07:26):

otherwise I have to keep typing list.cons right?

view this post on Zulip Egbert Rijke (May 13 2020 at 07:27):

Using emacs mode

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 13 2020 at 07:29):

Egbert Rijke said:

Using emacs mode

I hope that it will tell you about errors somehow.

view this post on Zulip Egbert Rijke (May 13 2020 at 07:29):

Yep, it shows me lots of red

view this post on Zulip Egbert Rijke (May 13 2020 at 07:30):

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

view this post on Zulip Johan Commelin (May 13 2020 at 07:31):

Red is not good (-;

view this post on Zulip Egbert Rijke (May 13 2020 at 07:32):

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

view this post on Zulip Johan Commelin (May 13 2020 at 07:32):

Error?

view this post on Zulip Egbert Rijke (May 13 2020 at 07:33):

type mismatch

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 13 2020 at 07:33):

Which types?

view this post on Zulip Johan Commelin (May 13 2020 at 07:33):

Aah, annoying

view this post on Zulip Johan Commelin (May 13 2020 at 07:33):

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

view this post on Zulip Johan Commelin (May 13 2020 at 07:34):

But can you manually say which types it complains about?

view this post on Zulip Johan Commelin (May 13 2020 at 07:34):

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

view this post on Zulip Kenny Lau (May 13 2020 at 07:35):

why not call it List

view this post on Zulip Johan Commelin (May 13 2020 at 07:35):

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

view this post on Zulip Egbert Rijke (May 13 2020 at 07:36):

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

view this post on Zulip Johan Commelin (May 13 2020 at 07:36):

Do you have more code in your file?

view this post on Zulip Johan Commelin (May 13 2020 at 07:36):

But the fact that it uses notation seems bad

view this post on Zulip Johan Commelin (May 13 2020 at 07:36):

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

view this post on Zulip Kevin Buzzard (May 13 2020 at 07:36):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Egbert Rijke (May 13 2020 at 07:43):

BTW I really appreciate both your help

view this post on Zulip Johan Commelin (May 13 2020 at 07:46):

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

view this post on Zulip Egbert Rijke (May 13 2020 at 07:48):

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

view this post on Zulip Johan Commelin (May 13 2020 at 08:07):

@Egbert Rijke But which type does it report?

view this post on Zulip Johan Commelin (May 13 2020 at 08:08):

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

view this post on Zulip Johan Commelin (May 13 2020 at 08:08):

Also, which Lean version are you using?

view this post on Zulip 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)

view this post on Zulip Johan Commelin (May 13 2020 at 08:10):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Egbert Rijke (May 13 2020 at 08:12):

Ah great! Thanks Sebastian! And hello :)

view this post on Zulip Kevin Buzzard (May 13 2020 at 08:12):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Egbert Rijke (May 13 2020 at 08:13):

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

view this post on Zulip Kevin Buzzard (May 13 2020 at 08:13):

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

view this post on Zulip Kevin Buzzard (May 13 2020 at 08:13):

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

view this post on Zulip 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

view this post on Zulip Marc Huisinga (May 13 2020 at 08:13):

try

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

view this post on Zulip Marc Huisinga (May 13 2020 at 08:14):

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

view this post on Zulip Egbert Rijke (May 13 2020 at 08:14):

That works!

view this post on Zulip Johan Commelin (May 13 2020 at 08:14):

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

view this post on Zulip Kevin Buzzard (May 13 2020 at 08:14):

2019 :-)

view this post on Zulip Egbert Rijke (May 13 2020 at 08:14):

Haha really?

view this post on Zulip Kevin Buzzard (May 13 2020 at 08:15):

yeah it is like months old!

view this post on Zulip Johan Commelin (May 13 2020 at 08:15):

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

view this post on Zulip 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

view this post on Zulip Egbert Rijke (May 13 2020 at 08:15):

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

view this post on Zulip Kevin Buzzard (May 13 2020 at 08:16):

What you should do depends on what you already did

view this post on Zulip Egbert Rijke (May 13 2020 at 08:16):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 13 2020 at 08:17):

#install

view this post on Zulip Johan Commelin (May 13 2020 at 08:17):

Too bad... that doesn't work

view this post on Zulip Kevin Buzzard (May 13 2020 at 08:17):

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

view this post on Zulip Kevin Buzzard (May 13 2020 at 08:18):

is what it should have linked to

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 13 2020 at 08:19):

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

view this post on 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.

view this post on Zulip Egbert Rijke (May 13 2020 at 08:20):

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

view this post on Zulip Johan Commelin (May 13 2020 at 08:20):

At least now we know the bug (-;

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Egbert Rijke (May 13 2020 at 09:22):

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

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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) (-:

view this post on Zulip 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.

view this post on Zulip Scott Morrison (May 13 2020 at 10:47):

Maybe we can yoink lean out of homebrew...

view this post on Zulip 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.

view this post on Zulip Reid Barton (May 13 2020 at 11:58):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 13 2020 at 12:23):

You got this working for all OS's?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 13 2020 at 17:03):

Johan Commelin said:

#install


Last updated: May 11 2021 at 13:22 UTC