Beginner questions

Stream: lean4

[Miguel Raz Guzmán Macedo]

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]

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]

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

[Mario Carneiro]

as well as theorems about random mathematics of course

[Mario Carneiro]

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]

you might even be able to mostly transliterate the proof

[Daniel Selsam]

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]

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

[Sebastian Ullrich]

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

[Mario Carneiro]

Does foo autocomplete to Foo.Bar.foo yet?

[Daniel Selsam]

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]

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

[Mario Carneiro]

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]

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

[Sebastian Ullrich]

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

[Mario Carneiro]

I see the file path

[Mario Carneiro]

Oh, hovering over a definition doesn't work

[Mario Carneiro]

you have to hover on a use of the definition

[Sebastian Ullrich]

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]

Mine ends at the .lean part

[Mario Carneiro]

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

Ha! Have you forgotten about type inference? Variables?

[Sebastian Ullrich]

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]

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]

Oh wait the breadcrumb is working now

[Sebastian Ullrich]

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]

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]

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]

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]

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

[Daniel Selsam]

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]

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?

[Mario Carneiro]

No

[Mario Carneiro]

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

[Mario Carneiro]

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]

You could do some juggling with typeclasses and instance priorities

[Daniel Selsam]

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]

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]

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]

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]

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

[Miguel Raz Guzmán Macedo]

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

[Julian Berman]

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

Oh, that is handy. Neat!

[Julian Berman]

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

[Julian Berman]

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

[Julian Berman]

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]

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

[Miguel Raz Guzmán Macedo]

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]

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

[Miguel Raz Guzmán Macedo]

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

[Miguel Raz Guzmán Macedo]

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]

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]

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

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

[Miguel Raz Guzmán Macedo]

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]

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

[Daniel Selsam]

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.

[Miguel Raz Guzmán Macedo]

Oh lord.

[Miguel Raz Guzmán Macedo]

:sweat_smile:

[Daniel Selsam]

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

[Daniel Selsam]

And quite clean/elegant

[Miguel Raz Guzmán Macedo]

Ok, that's not too bad then.

[Daniel Selsam]

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]

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

[Miguel Raz Guzmán Macedo]

Maybe I should have a HashSet Bool...

[Daniel Selsam]

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]

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

[Miguel Raz Guzmán Macedo]

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

[Miguel Raz Guzmán Macedo]

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

[Miguel Raz Guzmán Macedo]

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]

Why does the mkZZZ fail?

[Miguel Raz Guzmán Macedo]

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

[Daniel Selsam]

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

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

[Miguel Raz Guzmán Macedo]

Neat, didn't know about the deriving trick.

[Miguel Raz Guzmán Macedo]

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

[Daniel Selsam]

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]

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]

Ugh, this is so weird.

[Miguel Raz Guzmán Macedo]

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

[Daniel Selsam]

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]

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

[Miguel Raz Guzmán Macedo]

the import is underlined and says expected command.

[Joe Hendrix]

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]

Oh neat, thanks a lot @Joe Hendrix

[Miguel Raz Guzmán Macedo]

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

[Joe Hendrix]

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

[Miguel Raz Guzmán Macedo]

That's pretty cool stuff.

[Miguel Raz Guzmán Macedo]

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

[Joe Hendrix]

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