getting started with Lean 4

Stream: lean4

[Kevin Buzzard]

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?

[Bryan Gin-ge Chen]

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.

[Bryan Gin-ge Chen]

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.

[Kyle Miller]

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.)

section Logic

theorem andComm' : p ∧ q → q ∧ p := λ (And.intro x y) => And.intro y x

theorem andComm : p ∧ q ↔ q ∧ p := Iff.intro andComm' andComm'

theorem orComm' : p ∨ q → q ∨ p
| Or.inl x => Or.inr x
| Or.inr x => Or.inl x

theorem orComm : p ∨ q ↔ q ∨ p := Iff.intro orComm' orComm'

end Logic



def Set (α : Type u) : Type u := α → Prop

@[reducible]
def Set.mk (p : α → Prop) : Set α := p

class HasMem (α : outParam $ Type u) (β : Type v) where
    mem : α → β → Prop

infix:50 " ∈ " => HasMem.mem

instance : HasMem α (Set α) where
    mem x s := s x

syntax "{ " ident (" : " term)? " | " term " }" : term

macro_rules
  | `({ $x : $type | $p }) => `(Set.mk (λ ($x:ident : $type) => $p))
  | `({ $x | $p })         => `(Set.mk (λ ($x:ident : _) => $p))

abbrev setOf (b : β) [HasMem α β] : Set α := {x | x ∈ b}


namespace Set

theorem ext {s t : Set α} (h : (x : α) → x ∈ s ↔ x ∈ t) : s = t := by
    funext x
    exact propext (h x)

def univ {α : Type u} : Set α := λ _ => True

def subset (s t : Set α) : Prop := ∀ {x}, x ∈ s → x ∈ t
def inter (s t : Set α) : Set α := {x | x ∈ s ∧ x ∈ t}
def union (s t : Set α) : Set α := {x | x ∈ s ∨ x ∈ t}

infixl:70 " ∩ " => inter
infixl:65 " ∪ " => union
infix:50 " ⊆ " => subset

@[simp] theorem memUniv (a : α) : a ∈ univ := trivial

@[simp] theorem memInter (x : α) (s t : Set α) : x ∈ s ∩ t ↔ x ∈ s ∧ x ∈ t := Iff.rfl
@[simp] theorem memUnion (x : α) (s t : Set α) : x ∈ s ∪ t ↔ x ∈ s ∨ x ∈ t := Iff.rfl

theorem interComm (s t : Set α) : s ∩ t = t ∩ s := by
    apply ext
    simp
    intro
    rw andComm
    exact Iff.rfl

theorem unionComm (s t : Set α) : s ∪ t = t ∪ s := by
    apply ext
    simp
    intro
    rw orComm
    exact Iff.rfl

end Set

[Kevin Buzzard]

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.

[Shing Tak Lam]

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

[Kyle Miller]

@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.)

[Frédéric Dupuis]

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.

[Frédéric Dupuis]

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

[Kyle Miller]

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.

[Kevin Buzzard]

@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.

[Kevin Buzzard]

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

[Marc Huisinga]

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.

[Marc Huisinga]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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...

[Kevin Buzzard]

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!

[Kevin Buzzard]

-- 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?

[Mario Carneiro]

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 _

[Mario Carneiro]

Using {} seems to work in that position

[Bryan Gin-ge Chen]

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.

[Mario Carneiro]

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

[Kevin Buzzard]

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.

[Mario Carneiro]

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

[Sebastian Ullrich]

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?

[Sebastian Ullrich]

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