Lean FRO Meeting

Stream: Lean Together 2025

[Jireh Loreaux]

A thread for discussion about the Lean FRO talk.

[Rob Lewis]

180k Loogle queries per day!! @Joachim Breitner (since Leo just attributed the graph to you) do you have stats on the number of unique queriers?

[Riccardo Brasca]

Quoting from the zoom chat: "...So about 1000 per day"

[Julian Berman]

Number of website uses vs #loogle in-editor uses I think might also be an interesting number if you have it to share.

[Jireh Loreaux]

Regarding the issue that Mathlib build parallelism may be slower on a per declaration vs. per file level basis: wouldn't per file generally be slower than per declaration (especially in files with many transitive imports) due to the start-up time loading the environment?

[Jireh Loreaux]

partial_fixpoint :mind_blown:

[Joachim Breitner]

Riccardo Brasca said:

Quoting from the zoom chat: "...So about 1000 per day"

Yes, I made a stupid time calculation mistake and overestimated it by 150×. Sorry.

[Joachim Breitner]

Julian Berman said:

Number of website uses vs #loogle in-editor uses I think might also be an interesting number if you have it to share.

We don’t have good numbers on website users, I fear, (yet).

[Riccardo Brasca]

@Joachim Breitner can you post here the code (or the slides) to see partial_fixpoint in action?

[Joachim Breitner]

code from the demo

variable (f : α → Option α)

def whileSome (x : α) : α :=
  match f x with
  | none => x
  | some x' => whileSome x'
partial_fixpoint

/-- info: 10 -/
#guard_msgs in
#eval whileSome (fun x => do guard (x < 10); pure (x+1)) 1

theorem whileSome_none : whileSome (fun _ => none) x = x := by
  simp [whileSome]

section

example : whileSome (fun x => do guard (x < 10); pure (x+1)) 1 = 10 := by
  -- simp [whileSome]
  repeat (rw [whileSome]; simp [guard, failure])
  done

section

--example : whileSome (fun x => pure x) 1 = ??

section

/-- Soundness is not in danger -/
def findNat (f : Nat → Option α) (i : Nat) : α :=
  match f i with
  | none => findNat f (i+1)
  | some x' => x'
partial_fixpoint

section

/-- Within Option monad, we can prove partial correctness -/

def whileSome' (x : α) : Option α :=
  match f x with
  | none => x
  | some x' => whileSome' x'
partial_fixpoint

theorem whileSome'_correct : whileSome' f x = some r → f r = none := by
  apply whileSome'.partial_correctness
  intros whileSome ih x r hyp
  split at hyp
  · simp_all
  · apply ih _ _ hyp

section


/-! Essentially any monadic function works -- useful for program verification -/

def ack : (n m : Nat) → Option Nat
  | 0,   y   => some (y+1)
  | x+1, 0   => ack x 1
  | x+1, y+1 => do ack x (← ack (x+1) y)
partial_fixpoint

/-! Even nested recursion-/

structure Tree where cs : List Tree

def Tree.rev (t : Tree) : Option Tree := do
  Tree.mk (← t.cs.reverse.mapM (Tree.rev ·))
partial_fixpoint

def Tree.rev' (t : Tree) : Option Tree := do
  let mut cs := []
  for c in t.cs do
    cs := (← c.rev') :: cs
  return Tree.mk cs
partial_fixpoint

[Joachim Breitner]

And feel free to play around with https://github.com/leanprover/lean4/pull/6355 (put leanprover/lean4-pr-releases:pr-release-6355 into the toolchain)

[Edward van de Meent]

i can't wait to read the reference manual entry on this!

[Joachim Breitner]

Edward van de Meent said:

i can't wait to read the reference manual entry on this!

Nice, a volunteer to review my reference manual PR once it's there! ;-)

[Edward van de Meent]

feel free to ping me for that!

[Sebastian Ullrich]

Jireh Loreaux said:

Regarding the issue that Mathlib build parallelism may be slower on a per declaration vs. per file level basis: wouldn't per file generally be slower than per declaration (especially in files with many transitive imports) due to the start-up time loading the environment?

I'm not sure I get you, the start-up overhead will be included in either case. The gist is that when you already have more independent files than CPU core at most points of the build, there is nothing to further speed up through more parallelization.

[Eric Taucher]

The transition to the talk that followed was not definitive so didn't get a chance to clap in chat channel.
:clap:

[Pietro Monticone]

:video_camera: Video recording: https://youtu.be/QcLBbzQiTYY

[Edward van de Meent]

I have another small question about the partial_fixpoint feature... Joachim Breitner mentioned that a condition for using this is that "all the recursive calls are in tail position". What does that mean?

[Joachim Breitner]

That's for the non-monadic, more general case. A tail position is the RHS of the function, and for every match or if in tail position, their branches are tail positions, and the body of a let in tail position is in tail position.

Not tail positions are in particular the discriminants of matches, the conditions of ifs, and in general function arguments.

[Joachim Breitner]

In other words: a tail recursive function either returns a value, or calls itself with different arguments.

[Ayhon]

In the talk, Leonardo de Moura mentioned that a planned feature for Lean in 2025 is "support for monadic code reasoning". I'm curious about how that support would look like. Are there any ideas already being considered?

[Sebastian Graf]

Hi Ayhon, as the person implementing that support, let me share my budding plans. I'm only one week into the project, so there are still a lot of open questions.

The general idea for now is to provide a tactic that generates verification conditions for a given do-block + some postcondition. Currently, I model "do-block + some postcondition" using the SatisfiesM framework from Batteries.

Example: def fib_impl n := Id.run do ... could be a linear-time implementation of the fibonacci function making use of local state and other functional-imperative features. Then we could specify correctness of fib_impl as fib_impl n = fib_spec n, for all n, and for fib_spec implemented by the usual recursion.
Using the SatisfiesM, this is equivalent (apply SatisfiesM_Id_eq) to SatisfiesM (fun r => r = fib_spec n) (fib_impl n), at which point we can unfold fib_impl and apply the tactic.
The goal is for the tactic to yield a bunch of sub-goals, broadly falling in 3 categories:

1. Loop invariants (e.g., 0 <= i, i <= n, a = fib_spec (i-1), b = fib_spec i)
2. Pure sub-goals (i.e., no SatisfiesM), hopefully dischargable by simp, assumption or grind in the future
3. Impure sub-goals (i.e., involving SatisfiesM) about effectful functions from the base monad being used (in case of Id there really should be none)

The goal is to target what Lean's do notation expands to, including local state, local control flow (early return, break, continue), and reasoning about try/catch for law-abiding implementations.

As I work towards a basic prototype, one of the most important questions becomes: What are the requirements?
You can help me to collect requirements by handing me short, self-contained programs that are painful for you to verify at the moment.

[Jakob von Raumer]

Missed the talk, will have to catch up soon. We'll likely have properties on monadic functions coming out of the Sail->Lean project at some point as well, so this is really good news!

[Patrick Massot]

Sebastian, did you talk to the people who thought about this in CMU? I think this includes at least Jeremy Avigad, Mario Carneiro and Wojciech Nawrocki.

[Sebastian Graf]

No, I haven't talked to anyone yet. Thanks for listing a few stakeholders; I'll reach out to these people before long!

[Patrick Massot]

It’s a really important topic, and indeed the requirements are not clear at all. I only know those people had some rather extensive brainstorming about those requirements a couple of years ago.

[Sorrachai Yingchareonthawornchai]

An example is the greedy algorithm for constructing graph spanners. My implementation is based on this lecture note.

I show you a minimal instance of unweighted graphs here.

I hope it is relevant to your question.

[Shreyas Srinivas]

@Sorrachai Yingchareonthawornchai : we can implement this without monadic verification

[Shreyas Srinivas]

Especially if we only want to verify the correctness and not complexity.

[Shreyas Srinivas]

The idea is to express the loop as a (tail?) recursive procedure and use standard induction and cases tactics.

[Sorrachai Yingchareonthawornchai]

That's nice to know. Is there a way to prove the time complexity of the algorithm?

[Shreyas Srinivas]

So the idea that many of us converged on in separate ways is to model all computational models as query models. Let’s discuss in DM

[Kim Morrison]

Mathlib doesn't contain any time complexity results, and for now at least we think that the design space for setting up such proofs is so large, and relatively unexplored in Lean, that we'd prefer this happened outside Mathlib.