Zulip Chat Archive

Stream: lean4

Topic: getting started with Lean 4


view this post on Zulip Kevin Buzzard (Feb 21 2021 at 17:39):

OK so I am biting the bullet. I've installed Lean 4 following what it says in the manual, I've installed the Lean 4 VS Code extension and I've disabled the Lean 3 extension. I've made a new directory called Lean4-filters and initialised it as a Lean 4 repo, and I've made a subdirectory in there also called Lean4-filters and in there I've made a new file set.lean.

So far so good -- if I try #eval 2 + 2 then I see 4 in "Problems" at the bottom of the VS Code window, and posting random Lean 4 code into set.lean seems to work fine.

I was thinking of making an experimental filters repo, because of Reid's comment from months back that a filter game might be interesting. I've been teaching filters in my course, and I'm teaching them again this week, and because everything is so close to the axioms I thought it might be a good way to experiment with Lean 4 (NB I will still be teaching them using Lean 3!)

My questions so far:
1) I can't even see an infoview button, I'm reading all output in the "Problems" tab in that panel at the bottom which I never normally use. Is this right?
2) Why do i have a subdirectory Lean4-filters of a directory Lean4-filters? Can I have src or is this no longer recommended? My plan is to just make basic files called logic.lean, set.lean, function.lean and filter.lean and I'd planned on putting them all in src but the manual seemed to indicate that src was not a thing any more and I was supposed to have a subdirectory Foo in my project called Foo as well as some file Foo.lean. Can this be right? Let me stress that all I want to do is prove theorems.
2) Does Lean 4 have either of the following: set X := X -> Prop, function.injective? #print set returns

def MonadStateOf.set.{u, v} : {σ : Type u}  {m : Type u  Type v}  [self : MonadStateOf σ m]  σ  m PUnit :=\nfun (σ : Type u) (m : Type u  Type v) [self : MonadStateOf σ m] => self.2,

and I'm not convinced this is the set I'm looking for. I ask because I think these were defined in lean 3 rather than mathlib. Do I need to import something?

view this post on Zulip Bryan Gin-ge Chen (Feb 21 2021 at 17:53):

What version of Lean 4 are you using? The infoview doesn't work with the M0 version, but it does for fairly recent nightlies. My leanpkg.toml has this line: lean_version = "leanprover/lean4:nightly", and then every once in a while I run elan update leanprover/lean4:nightly.

view this post on Zulip Bryan Gin-ge Chen (Feb 21 2021 at 17:54):

Note that the infoview is much less informative than the Problems tab at the moment. It only shows the tactic state as a string; the errors and messages don't show up there yet.

view this post on Zulip Kyle Miller (Feb 21 2021 at 18:00):

Here's some code I wrote a month ago for some basic set operations, including some macro_rules for set builder notation, in case it's useful to get started. (Notes: Set.mk is what mathlib calls set_of. setOf was an experiment for turning things with a HasMem instance into sets. I didn't make any general typeclasses for set notation beyond HasMem.)

view this post on Zulip Kevin Buzzard (Feb 21 2021 at 19:06):

OK so here's an attempt at a proof:

#check Classical.em -- what you think it is

example (p : Prop) : ¬ ¬ p  p := by
  intro h
  cases (Classical.em p)
  focus
    assumption
  focus
    admit

I'm stuck at admit because I can't figure out how to see the tactic state and I can't figure out how to name the two cases given by cases -- cases (Classical.em p) with h1 h2 doesn't seem to work. Kyle's example doesn't seem to ever create new variable names in tactic mode. I'll upgrade to nightly and see if I have any better luck.

view this post on Zulip Shing Tak Lam (Feb 21 2021 at 19:12):

This works, although I don't know what the style guide for Lean 4 code is like

#check Classical.em -- what you think it is

example (p : Prop) : ¬ ¬ p  p := by
  intro h
  cases (Classical.em p) with
  | inl hp =>
    assumption
  | inr hnp =>
    apply False.elim
    exact h hnp

view this post on Zulip Kyle Miller (Feb 21 2021 at 19:17):

@Kevin Buzzard When I wrote the proofs, I used curly braces and semicolons since that seemed to be the most reliable way to see the tactic state where you want it. I then removed the scaffolding when I was done. (In Lean4, semicolon replaces comma for separating tactics.)

view this post on Zulip Frédéric Dupuis (Feb 21 2021 at 19:17):

My usual trick for seeing the tactic state was to use the by { tactic; tactic; tactic; } syntax. Maybe this has now changed, but back in early January this seemed to be the easiest way to do it.

view this post on Zulip Frédéric Dupuis (Feb 21 2021 at 19:19):

Ah, so I guess it wasn't just me :-)

view this post on Zulip Kyle Miller (Feb 21 2021 at 19:22):

Another trick I used was to put { } somewhere in a tactic proof to see what the goal was there. This is also useful for filling out the arms of a cases statement while you're working.

view this post on Zulip Kevin Buzzard (Feb 21 2021 at 19:30):

@Shing Tak Lam yes I saw this approach in the Lean 4 manual but I don't think this style is suitable for mathematician learners, they got on really well in NNG with induction n with d hd and then just dealing with the two cases separately. The pipe thing is super-cool for more advanced use but I'm actively thinking of how far we are from making a filter game in Lean 4.

view this post on Zulip Kevin Buzzard (Feb 21 2021 at 19:31):

Of course we're a long way, but it's just an experiment.

view this post on Zulip Marc Huisinga (Feb 21 2021 at 19:33):

I've disabled the Lean 3 extension

This should not be necessary anymore.

I can't even see an infoview button

If you're using the "nightly" version of lean4 (not the "stable" version), the infoview should open when you open a file and also any time you click anywhere in a tactic proof.

view this post on Zulip Marc Huisinga (Feb 21 2021 at 19:36):

Also note that if you installed the lean4 vscode extension back at Lean Together, you may want to uninstall and replace it with the current version on the marketplace.

view this post on Zulip Kevin Buzzard (Feb 21 2021 at 19:41):

Thanks for the {;} trick both of you -- this is exactly what I needed.

view this post on Zulip Kevin Buzzard (Feb 21 2021 at 19:44):

case inr
p : Prop
h : ¬¬p
 : ¬p
⊢ ¬p

The unnamed assumption came from cases (Classical.em p). I had understood that it was impossible to not name the outputs of tactics -- but right now I find it's impossible for me to name them. intro h works -- is there any way I can name the goals coming from the cases tactic? I know I can clear the goal with assumption but exact hnp is shorter...

view this post on Zulip Kevin Buzzard (Feb 21 2021 at 19:47):

my first proof:

example (p : Prop) : ¬ ¬ p  p := by
  intro h;
  cases (Classical.em p);
  { assumption };
  { apply False.elim;
    apply h;
    assumption }

The semicolons are great for now because with the nightly I can see the tactic state by clicking on a tactic. Don't forget the semicolon!

view this post on Zulip Kevin Buzzard (Feb 21 2021 at 19:52):

-- compiles
example (p : Prop) : ¬ ¬ p  p := by
  intro h;
  cases (Classical.em p);
    assumption;
  admit

-- copied from the manual
open Lean in
macro "begin " ts:tactic,*,? "end"%i : term => do
  -- preserve position of the last token, which is used
  -- as the error position in case of an unfinished proof
  `(by { $[$ts:tactic]* }%$i)

-- fails
example (p : Prop) : ¬ ¬ p  p :=
begin
  intro h,
  cases (Classical.em p),
    assumption,-- error "unknown identifier 'assumption'"
  admit
end

The begin/end macro is from here . Is the issue that I have two goals?

view this post on Zulip Mario Carneiro (Feb 22 2021 at 01:03):

By the way, I think it would be nice for _ to work in this context, as in

example (p : Prop) : ¬ ¬ p  p := by
  intro h
  cases (Classical.em p)
  focus
    assumption
  focus
    _

should show the goal state at the _

view this post on Zulip Mario Carneiro (Feb 22 2021 at 01:05):

Using {} seems to work in that position

view this post on Zulip Bryan Gin-ge Chen (Feb 22 2021 at 01:10):

I think the community Lean 3 feature to show the expected term in the info view is helpful too; hopefully that's also on the roadmap.

view this post on Zulip Mario Carneiro (Feb 22 2021 at 01:13):

I took a look at the source for cases just in case but indeed it seems that cases e with a b is no longer supported at all

view this post on Zulip Kevin Buzzard (Feb 22 2021 at 02:15):

I think that beginner mathematician users need that, people who play the natural number game just write a stream of tactics and know to only ever look at the top goal. There's no harm in doing it like that if you're not attempting to write professional code and just want to close the goals.

view this post on Zulip Mario Carneiro (Feb 22 2021 at 02:20):

I am thinking about writing a dirtyCases tactic that acts like lean 3 cases (including the ability to refer to generated names)

view this post on Zulip Sebastian Ullrich (Feb 25 2021 at 09:23):

Kevin Buzzard said:

2) Why do i have a subdirectory Lean4-filters of a directory Lean4-filters?

The subdirectory doesn't need to match the outer directory - after all a git repo can be cloned into arbitrarily-named directories. You should instead choose a name that makes sense for others to import (even if the package is not meant to be imported, for consistency), e.g. Filters (if they import it, they seem to be using Lean 4, so no need for the prefix). That's not much longer than src anymore, is it?

view this post on Zulip Sebastian Ullrich (Feb 25 2021 at 09:24):

Also note that with the new layout, single-file packages do not need a subdirectory at all


Last updated: May 07 2021 at 13:21 UTC