## Stream: lean4

### Topic: Beginner questions

#### Miguel Raz Guzmán Macedo (Apr 12 2021 at 18:59):

Hello!

1. How do people navigate the code base? I want to know all the functions I can call on a List - how can I do that?
2. What do people recommend as good starting theorem examples in Lean4 to get started? I'm looking at the Advent-of-code-lean4 repo and that's cool, but I haven't found other repos that are building up code alongside the proofs. Any recommendations? I've started looking at lean4/src/Std/Data/, and proving basic properties of those data structures seems neat.
Thanks!

#### Mario Carneiro (Apr 12 2021 at 19:25):

1. So far, I'm using "grep" (aka vscode find in files) to find the files that deal with List and browse around
2. You are going to run into lots and lots of problems when proving theorems about programs right now. (See also "Proving findLeast" thread.) The code there might be helpful, as well as the language reference on tactics

#### Mario Carneiro (Apr 12 2021 at 19:26):

Lean 3 is much better suited for proving theorems about programs ATM

#### Mario Carneiro (Apr 12 2021 at 19:26):

as well as theorems about random mathematics of course

#### Mario Carneiro (Apr 12 2021 at 19:27):

Even if you ultimately want to prove stuff about a lean 4 program, it might be worthwhile to cut your teeth on lean 3 proving because the infrastructure is much more mature and the skills are very transferrable

#### Mario Carneiro (Apr 12 2021 at 19:27):

you might even be able to mostly transliterate the proof

#### Daniel Selsam (Apr 12 2021 at 19:28):

Generally speaking, these functions will be exactly the ones in the List namespace that have an argument of type List _. I don't know of any supported/maintained search facility for this but here is a starting point for now:

import Lean
open Lean Lean.Meta

structure FindOptions where
stage1        : Bool := true
checkPrivate  : Bool := false
checkInternal : Bool := false

def findCore (ϕ : ConstantInfo → MetaM Bool) (opts : FindOptions := {}) : MetaM (Array ConstantInfo) := do
let matches ← if !opts.stage1 then #[] else (← getEnv).constants.map₁.foldM (init := #[]) check
(← getEnv).constants.map₂.foldlM (init := matches) check

where
check matches name cinfo := do
if isPrivateName name && not opts.checkPrivate then pure matches
else if name.isInternal && not opts.checkInternal then pure matches
else if (← ϕ cinfo) then pure (matches.push cinfo)
else pure matches

def find (ϕ : ConstantInfo → MetaM Bool) (opts : FindOptions := {}) : MetaM Unit := do
let cinfos ← findCore ϕ opts
let cinfos := cinfos.qsort (fun p q => p.name.lt q.name)
for cinfo in cinfos do
println! "{cinfo.name} : {← Meta.ppExpr cinfo.type}"

#eval println! "\nAll declarations in namespace 'List':\n"
#eval find λ cinfo => (List).isPrefixOf cinfo.name


#### Mario Carneiro (Apr 12 2021 at 19:29):

Oh hey look it's our old friend #print prefix

#### Sebastian Ullrich (Apr 12 2021 at 19:34):

You can just use auto completion now. It mostly works!

#### Mario Carneiro (Apr 12 2021 at 19:35):

Does foo autocomplete to Foo.Bar.foo yet?

#### Daniel Selsam (Apr 12 2021 at 19:36):

Sebastian Ullrich said:

You can just use auto completion now. It mostly works!

Cool! Does this work in Emacs? I can't seem to figure out how to trigger it.

#### Mario Carneiro (Apr 12 2021 at 19:36):

this will be super helpful for hunting down Lean.?.elabTerm stuff

#### Mario Carneiro (Apr 12 2021 at 19:37):

Oh, also can the hover print the fully qualified name? It's nice to be able to hover over a definition to see the current namespace

#### Mario Carneiro (Apr 12 2021 at 19:38):

(maybe there should be an option for that, I can imagine situations where it is noisy)

#### Sebastian Ullrich (Apr 12 2021 at 19:38):

Don't you see the current namespace from the bread crumb bar?

#### Mario Carneiro (Apr 12 2021 at 19:38):

I see the file path

#### Mario Carneiro (Apr 12 2021 at 19:40):

Oh, hovering over a definition doesn't work

#### Mario Carneiro (Apr 12 2021 at 19:41):

you have to hover on a use of the definition

#### Sebastian Ullrich (Apr 12 2021 at 19:42):

Hovering over a definition seems a bit redundant, all the information is already there? The breadcrumb bar should look something like image.png

#### Mario Carneiro (Apr 12 2021 at 19:44):

Mine ends at the .lean part

#### Mario Carneiro (Apr 12 2021 at 19:44):

Hovering over a definition seems a bit redundant, all the information is already there?

Ha! Have you forgotten about type inference? Variables?

#### Sebastian Ullrich (Apr 12 2021 at 19:45):

Daniel Selsam said:

Sebastian Ullrich said:

You can just use auto completion now. It mostly works!

Cool! Does this work in Emacs? I can't seem to figure out how to trigger it.

Leo mentioned he was missing company. After that, Ctrl+Space should just work.

#### Daniel Selsam (Apr 12 2021 at 19:45):

Daniel Selsam said:

Sebastian Ullrich said:

You can just use auto completion now. It mostly works!

Cool! Does this work in Emacs? I can't seem to figure out how to trigger it.

I think I figured it out. Auto-complete is automatic in certain circumstances. There is a delay after pressing <term>. and if you press anything during that delay, it will stop autocomplete from ever showing, and then you need to delete the . and type it again.

#### Mario Carneiro (Apr 12 2021 at 19:45):

Oh wait the breadcrumb is working now

#### Sebastian Ullrich (Apr 12 2021 at 19:46):

Mario Carneiro said:

Hovering over a definition seems a bit redundant, all the information is already there?

Ha! Have you forgotten about type inference? Variables?

I can't even tell if hovering over the definition should or should not show the variables. But it could be useful, yeah.

#### Mario Carneiro (Apr 12 2021 at 19:49):

I think it should always show the variables. The only time it should be shown without variables is when you hover over a recursive use of the definition

#### Mario Carneiro (Apr 12 2021 at 19:50):

I don't actually understand the rules for when definitions need extra args. "Right of the colon" doesn't seem to be correct anymore

#### Mario Carneiro (Apr 12 2021 at 19:50):

I have observed that moving a definition from one file to another can cause recursive uses of the definition to need more arguments

#### Mario Carneiro (Apr 12 2021 at 19:51):

so I'm guessing the new rule is that variables are not specified but everything else is

#### Daniel Selsam (Apr 12 2021 at 19:54):

You can sort-of simulate the old right-of-the-colon behavior with a where:

def foo (α : Type) (xs : List α) : Nat → Nat := foo where
foo
| 0   => 0
| n+1 => foo n + 1


#### Miguel Raz Guzmán Macedo (Apr 12 2021 at 19:55):

Thanks for the reccs @Mario Carneiro .
Another question: Say I can prove that one of my functions holds a certain property. Can Lean4 optimize the performance of that function by using that new information?

No

#### Mario Carneiro (Apr 12 2021 at 19:56):

If you want something like that you have to bake it into the definition

#### Mario Carneiro (Apr 12 2021 at 19:57):

There are a few examples of that (I think), like array indexing with Array.get takes an argument of type Fin n, which is a pair of a natural number and a proof that it is in range; in principle that means that the compiler doesn't have to emit bounds checks

#### Yakov Pechersky (Apr 12 2021 at 19:57):

You could do some juggling with typeclasses and instance priorities

#### Daniel Selsam (Apr 12 2021 at 19:57):

Miguel Raz Guzmán Macedo said:

Another question: Say I can prove that one of my functions holds a certain property. Can Lean4 optimize the performance of that function by using that new information?

There is a long term goal to exploit theorems/proofs in various ways during compilation (maybe interactively), but right now Lean will not magically optimize your code based on a theorem in the environment.

#### Mario Carneiro (Apr 12 2021 at 19:58):

You can also use implementedBy to replace a slow definition with a fast one, so for example you can write a slow definition, prove a theorem about it, then write the not-obviously-the-same fast version and use the theorem to prove equivalence and implementedBy to swap it out

#### Mario Carneiro (Apr 12 2021 at 20:00):

Although right now implementedBy is unsafe, in the sense that it doesn't require the two definitions to be equivalent, so your theorem is going to waste

#### Mario Carneiro (Apr 12 2021 at 20:01):

Leo has talked about plans to use simp in the compiler to rewrite slow definitions with fast ones and perform transformations like map f (map g l) = map (f o g) l a la haskell

#### Mario Carneiro (Apr 12 2021 at 20:02):

That approach would be proven correct since it's using an equation that had to be proved

#### Miguel Raz Guzmán Macedo (Apr 12 2021 at 20:03):

Wow, Lean people are cooking up cool stuff. Nice!

#### Julian Berman (Apr 12 2021 at 20:29):

@Miguel Raz Guzmán Macedo another few things that may help -- you can find repos tagging themselves with lean4 in GitHub which I've clicked on a few times just to see -- https://github.com/topics/lean4

#### Miguel Raz Guzmán Macedo (Apr 12 2021 at 20:30):

Oh, that is handy. Neat!

#### Julian Berman (Apr 12 2021 at 20:30):

also I think @Kevin Buzzard's mathlib4 noodling repo has some more theorem-y lean4 code -- https://github.com/kbuzzard/mathlib4_experiments

#### Julian Berman (Apr 12 2021 at 20:31):

it's only a file or two, but yeah I flipped through it to learn some tricks myself.

#### Julian Berman (Apr 12 2021 at 20:31):

Also also I wrote up my own small list of lean4 repos to keep an eye on here: https://github.com/Julian/tree-sitter-lean/issues/1 (which contains nothing other than what I just shared) :) but if you find good examples I'd love to hear them myself too

#### Miguel Raz Guzmán Macedo (Apr 13 2021 at 19:19):

Alright, so this has been a nice detour - I want to go back to beginner questions.

#### Miguel Raz Guzmán Macedo (Apr 13 2021 at 19:20):

I'm trying to implement the basics of Linear Temporal Logic, I think it makes for a nice side project for now.

#### Miguel Raz Guzmán Macedo (Apr 13 2021 at 19:20):

I'm using this document as reference: https://www.dc.fi.udc.es/~cabalar/vv/T4-LTL.pdf

#### Miguel Raz Guzmán Macedo (Apr 13 2021 at 19:20):

It's "almost" set theory and propositions with a few more operators sprinkled on top.

#### Miguel Raz Guzmán Macedo (Apr 13 2021 at 19:21):

Right now, I want to try and add the definition of a \Sigma:

open Std
structure Sigma where
props : HashSet Prop := []


#### Miguel Raz Guzmán Macedo (Apr 13 2021 at 19:21):

After that, I want to try and define the state s, as a function that takes in a set of propositions and returns a boolean

def state (S : Sigma) (s : HashSet Prop) : Bool :=
...


#### Daniel Selsam (Apr 13 2021 at 19:27):

@Miguel Raz Guzmán Macedo It doesn't seem like you have asked a question yet, but I'll save you some time to mention that you can't have a HashSet of Prop. You can't hash a Prop, nor can you compare it for equality.

#### Miguel Raz Guzmán Macedo (Apr 13 2021 at 19:28):

Ah, thanks @Daniel Selsam yeah I was getting to that.

#### Miguel Raz Guzmán Macedo (Apr 13 2021 at 19:28):

ok, so if I have that p q r : Prop, and I want to have them in a Set for easy inclusion comparisons, how could I do that?

#### Miguel Raz Guzmán Macedo (Apr 13 2021 at 19:29):

(Also, I don't see many tutorials about using datastructures in Lean, so that would be a nice resource to know about.)

#### Daniel Selsam (Apr 13 2021 at 19:29):

This is not possible. You probably need to create a DSL/inductive-type for the kinds of Props are you interested in (and define hash and beq on it), and then write a denote function that maps them to actual Props if necessary.

Oh lord.

:sweat_smile:

#### Daniel Selsam (Apr 13 2021 at 19:30):

It is not so bad, this is a well-trodden path

#### Daniel Selsam (Apr 13 2021 at 19:31):

And quite clean/elegant

#### Miguel Raz Guzmán Macedo (Apr 13 2021 at 19:31):

Ok, that's not too bad then.

#### Daniel Selsam (Apr 13 2021 at 19:32):

Basically a Prop has no computational content. You can't write executable code that manipulates them directly. You need to "reify" them into data that can be manipulated.

#### Miguel Raz Guzmán Macedo (Apr 13 2021 at 19:32):

Well all the Props I care about are Booleans, I just need them to have different names.

#### Miguel Raz Guzmán Macedo (Apr 13 2021 at 19:33):

Maybe I should have a HashSet Bool...

#### Daniel Selsam (Apr 13 2021 at 19:35):

I don't know what you are trying to do, but my off-the-cusp guess is that you'll want something like:

import Std.Data.HashSet
open Std (HashSet)

namespace LTL

inductive Property
| reachable : Nat → Nat → Property
| sink      : Nat → Property
deriving Repr, Hashable, BEq, DecidableEq

axiom Reachable (n₁ n₂ : Nat) : Prop
axiom Sink (n : Nat) : Prop

def Property.denote : Property → Prop
| reachable n₁ n₂ => Reachable n₁ n₂
| sink n          => Sink n

structure Sigma where
props : HashSet Property := {}

end LTL


#### Daniel Selsam (Apr 13 2021 at 19:36):

^ I just made up Reachable and Sink, you would replace those with whatever properties you actually care about

#### Miguel Raz Guzmán Macedo (Apr 13 2021 at 19:37):

Nice, that's super cool you did that. Thanks!

#### Miguel Raz Guzmán Macedo (Apr 13 2021 at 19:37):

(This is my first actual dive into Lean4 so I'm taking it slow.)

#### Miguel Raz Guzmán Macedo (Apr 13 2021 at 19:46):

Alright I think this is much more barebones but it might be good enough for what I need:

structure ZZZ (α : Type u) where
props : Array Bool

def mkZZZ (a : Array Bool) : ZZZ Bool :=
{ props := a  }

#eval mkZZZ #[true, false]


#### Miguel Raz Guzmán Macedo (Apr 13 2021 at 19:46):

Why does the mkZZZ fail?

#### Miguel Raz Guzmán Macedo (Apr 13 2021 at 19:46):

I also tried calling it \Sigma but Lean complained so :shrug:

#### Daniel Selsam (Apr 13 2021 at 19:52):

It just doesn't know how to print the result to the screen. Just add:

structure ZZZ (α : Type u) where
props : Array Bool


#### Miguel Raz Guzmán Macedo (Apr 13 2021 at 19:54):

Neat, didn't know about the deriving trick.

#### Miguel Raz Guzmán Macedo (Apr 13 2021 at 19:55):

I now get a term has type ZZZ Bool / failed to syntehsize Lean.Eval ?m.2068 prompt.

#### Daniel Selsam (Apr 13 2021 at 19:57):

It works for me:

structure ZZZ (α : Type u) where
props : Array Bool
deriving Repr

def mkZZZ (a : Array Bool) : ZZZ Bool :=
{ props := a  }

#eval mkZZZ #[true, false] -- prints { props := #[true, false] }


Note: I am using a very recent commit 292bab5a11dc05e019068a579a42eac251bf587f

#### Daniel Selsam (Apr 13 2021 at 19:58):

Miguel Raz Guzmán Macedo said:

I also tried calling it \Sigma but Lean complained so :shrug:

You can name your structure Sigma if you are in a namespace. In the example I posted above, I declare Sigma inside LTL namespace.

#### Miguel Raz Guzmán Macedo (Apr 13 2021 at 20:03):

Ugh, this is so weird.

#### Miguel Raz Guzmán Macedo (Apr 13 2021 at 20:03):

the import ... open ... lines don't work for me either.

#### Daniel Selsam (Apr 13 2021 at 20:05):

The example in https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Beginner.20questions/near/234390590 does not require any imports nor opens.

#### Miguel Raz Guzmán Macedo (Apr 13 2021 at 20:05):

Yes - I tried using a HashSet String for the time being.

#### Miguel Raz Guzmán Macedo (Apr 13 2021 at 20:06):

the import is underlined and says expected command`.

#### Joe Hendrix (Apr 13 2021 at 20:06):

It's been a while since I looked at this, but here is a link to how we formalized temporal logic in Lean 3. It's in terms of properties over traces.

#### Miguel Raz Guzmán Macedo (Apr 13 2021 at 20:07):

Oh neat, thanks a lot @Joe Hendrix

#### Miguel Raz Guzmán Macedo (Apr 13 2021 at 20:07):

Oh no way, I was just building this to show it off to some Galois people on twitter later :sweat_smile:

#### Joe Hendrix (Apr 13 2021 at 20:08):

We also defined a data structure for LTL formulas that was polymorphic over the underlying state predicates.

#### Miguel Raz Guzmán Macedo (Apr 13 2021 at 20:10):

That's pretty cool stuff.

#### Miguel Raz Guzmán Macedo (Apr 13 2021 at 20:10):

I see there's no Until / Release operators yet.

#### Joe Hendrix (Apr 13 2021 at 20:28):

@Miguel Raz Guzmán Macedo Yes, I noticed that as well. We have it in the semantics file. I don't actually recall what the formula datatype was used for actually.

Last updated: May 07 2021 at 13:21 UTC