new monadic program verification framework

Stream: general

[Asei Inoue]

@Sebastian Graf

I would like to know how I can use https://github.com/sgraf812/mpl, which has been upstreamed into Lean. I read the README, but I couldn’t understand it very well. For example, with your framework, is it possible to prove the following?

def peasantMul (x y : Nat) : Nat := Id.run do
  let mut x := x
  let mut y := y
  let mut prod := 0
  while x > 0 do
    if x % 2 = 1 then
      prod := prod + y
    x := x / 2
    y := y * 2
  return prod

example (x y : Nat) : peasantMul x y = x * y := by
  sorry

[Eric Wieser]

I think that's unprovable, because while is partial / docs#Lean.Loop.forIn.loop is opaque

[Asei Inoue]

@Eric Wieser Thank you! "I'll give a different example.

how about this?

def Nat.isPrime (n : Nat) : Bool := Id.run do
  if n ≤ 1 then
    return false
  for d in [2:n] do
    if n % d = 0 then
      return false
    if d ^ 2 > n then
      break
  return true

#guard Nat.isPrime 2
#guard Nat.isPrime 3
#guard Nat.isPrime <$> [4, 5, 6, 7] == [false, true, false, true]
#guard Nat.isPrime 103

example (n d : Nat) (h : Nat.isPrime n) (h1 : 2 ≤ d) (h2 : d < n) : ¬ d ∣ n := by
  sorry

[Bhavik Mehta]

Since I also haven't figured out how the new setup works, here's a proof of your example in the old setup:
https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMB0AVJAYxmEJwHUAZAeQHEAoUSWRFDbfIksgZQFMY9egBM+AMzgA5FDmABnAApRQfOAAoAdnABcUlAEodcAEIQI6HQF44ASWE4oAVy3CI9OHGAStgEyI4ARjg0Pg13DzgoAUcoLTEkdDk+MLFoOGFPLQBtACZtDQBdNLdwz284AFI0uGsABiDUELCSyJho2PjEptKqgD04bLgAPjgtYNCSjyxIpABrMJa2oKck+mDoPhA4SnkYHBT0YXQEAH1CCA0Acyg4AG9ARuA4QCbgAF9bzd08AE8wVWO4QCTCOBfH5wY6vTIIc5IdIgQo3Cy6bZyeAvW4SC5GB6Ax4AuCbO7PLo3YAaYDwXQE9SoIyAACI4EgADRwOlYOCACCI4OgmRIkHBWdYMbysIZtF10HtzIcEHAJCSydVORKDkc4Bi5eTrFhPmEScJHMRgOdOaqQnwoPFgAAvElq0nwADuZOpV11QjWkU2SN2+0Op3OV1uD1R8KMXqerxu6MxuJxgIJRPVmNeampujpjOZfPZnO59KzArzwp0YqVhxlGXl1nFPostvl2k12o8uv1JCNtdN5sw1suFYdTtVyg0wiEKBgyiwjhgqkyLuH1UK0l26BgxxAjnQxy8YmO5z4xxXB/E8CXOEP683293Gn3h+UF1QgnofAAHkhwOhVJoqrol4YU0Yp7yEoKgjP+qCBLoAx+MI4EDLo6QADxgUYAA1VSAMREIxWHyTZwKgSAAG6qKgGiAIEEaHYX4kGNoOrrNho44QPhwjjHAAC07FwPaqiEEgWhIHIciOCAqjpH00EjEycjMekZKJOgEiOugFhTHwsz1Ko6BmGAYT2tpGKoMI2RaAhcASXAfhaBcnYWj2GIjh4fGJBk1yWIMXRyEwcDnOgnxwJkp4aBAq6foUKD4eRXQQFgMBICScCABfkfBMlAYjoIAl+Q4UZbEeARxH4aouiBMhRW0XOjnhEgYBgH59TyHAX5anRw7/s1FWGIlwhMu1Q7CBlXRQPaAWnpA9rHDA9oQPkXTVbV/mnheR5rhuxz3o+g3DYFMhjRNU1Motq2fitm6fmIq7buozUQKJFxIPo4XwEZJldBVYScXAci1fKwScjpET8TZGQwMxk3MWASCwHIYT5SRFGIjsDiA3wADk/TqFoXHZIY1hekjlyo+jajpFx/iGAA1OTWyI+aBNo8TcBU2TGMcVUpMio2XSw0YJMBIzLNcbzzPWJj6MNrhPm3Ugm0BYACYT1XITLy3jtM2SjxxzSEwjHP4M0lG9HgfV9mDwL9YjAFAyJwBDLB8MRWggOsMNESRgBBBKGNPI2jAwM+zCoq17RO89jjNU5kwiFOLWpcy7POswMTMKkLOHXVLMuZPLaDyEr1PIvjasazVWs63r4QVQFAd09efCl0bTCYGI/m/WSZooIabFeeAPkaHV227MByiiUypFkUygDJhJEeqEHwNjTkyFwXWIO4rj1urHGA0T7mc4BMiA1Xr5vTIb5ExxYLqDJdDwMD2AASsjEpQDYGjHHwACOxwpI/z+q6jTJX7f98vKWhSnoXYwhgCEWrgdGQ0JtZ7mOMJLAUCuh2AcM4U+59c7emgE/F+78awICZKgpwz895gBznNPyW455YNkMIG+6CCGPXwmERI8AJDizEM4LMvJABlhKCVhAhVRGAAGI4I0FfPgYB1AICUBAdIahqBgDbFoUw5hDAKAAKp2kMICJcuIxFf0kdItQsioDyPUEolRJgzDoA0doskHMuhcK0KyPheIUCEGpKyR0aAugAB84A4E+MAPgBw4CEGqMMLw2FKi8lqJpLQOBXA3iSjJUSMoOggJwM4MkWUwkuWCaE8JiVgo3iZDku0A0SiBOSXuCJUSgkpN4u9LindvqN00jKC2VsvHOBmD5CQzdpzmhUfMLaqBR60JrIXH4w4mR4xmWcS41w1AIlxp7OmQdWZk3/BicWFxwI4QAPxvwevSJ6YRnKqDflEwaJImLqF5IE+6WZUBYC6NcooqT3KfW8pkMQ88j6H1sPYEhpcnKCVUCEsJ6R3JdDyrHXQrILJWRwqeY645+JyHUKNCA41jq7TOvANQvVdSGGOIYZ6uVwjtICl4Y4N4LhMizorUFaCNDciBdbTepchoBVQK7BZiMZma3mdMyUm5llssWZKxlwB0DMNQK0z6qB8XcQIk9MVOKkDnTNF0xIyz0h9I0AM82pI5ANGhoigqqBADBBEYDEahZXKmEWoIpsKkplOybkmAGV/yVzVtsrG+hQ1VEsAipp9TEpxASD6qpKc8I2q/AiLBoD/wvnAi+Iw2brB1NSYldJqhY2JAqb6rKgAKIjgLmoJMKSnerLVUkUkaPDVklcImt+bVCFpusWrJja8lwCrW211GJO11vSKUvcA6/WJsjS2A07YTQ3i7FaG01bI1fNJBYX5dLMioBfBC8IXzpX4SCJ4akvzKH+WANSP4xwADcLVKoeHLn3ZJhFtZXkdtrN+xxgHmNrm0tVw00ARV+lnKAxrUD9KKHwOQGgUbwC8cjLpkRhIrmdgVNZHsrZ/nUJmowI6ywSHdc06tOMo2pOzVHJNGQp7WPQJ8qFIwFWNPacxlyp6GjQiCPFCwt67kTHwki8sZH6mEZ43CqjqgaPWDSkx4TBs/ld33XallqB5BKvoEAA

[Sebastian Graf]

There's some material in #Program verification > Monadic program logic: Request for feedback @ 💬 .
Note that the lack of documentation is due to Std.Do still being a pre-release.
Regarding example code, there's Markus' blog post giving Std.Do a try and the kitchen sink test file I've been using.

Here's a solution using Std.Do for the isPrime variant without the d^2 > n test. The version including the test is doable as well, but it would take me quite a bit of time to recast the wlog d^2 <= n and use that fact to reason about ranges. It's likely that you would need to tweak the loop invariant to

  case inv => exact (⇓ (⟨x, _⟩, xs) => ⌜xs.suff = [] ∧ x = .some false ∨ x = .none ∧ (∀ d, d ∈ xs.pref → d^2 ≤ n ∧ ¬ d ∣ n)⌝)

(The d^2 <= n is new.)

Perhaps someone would like to do that and in the process come up with nice grind theorems that the API around Std.List.Zipper is currently lacking?

[Patrick Massot]

Was this blog post advertised before and I missed it? I think this is a fantastic read (both because the post is nice and the documented feature is awesome) and everybody here should read it, even mathematicians with very little interest in programming.

[Sebastian Graf]

I don't think it was more widely announced than in #Program verification > Monadic program logic: Request for feedback @ 💬 and then referred to a couple of times in discussions

[Patrick Massot]

That answers my question: I was not aware of the Program verification channel (and not subscribed to it).

[Patrick Massot]

I guess we’ll have a proper announcement when the framework is ready to use and documented, but that’s already very exciting.

[Patrick Massot]

Are there plans to make the tactic states less frightening for cases where people want to provide manual proofs?

[Sebastian Graf]

Thanks for giving it a try! So far, UX for mvcgen is top priority. In the small experiments I did so far (and also in the medium-sized one that @Rish Vaishnav is conducting), it appears that the most comfortable way to prove things is by immediately leaving the SPred proof mode and then using grind/the regular arsenal of Lean tactics :) The simplest way to "leave the proof mode" is

  simp_all only [Std.Do.SPred.entails_cons, Std.Do.SPred.entails_nil, Std.Do.SPred.and_cons, Std.Do.SPred.and_nil, Std.Do.SVal.curry_cons, Std.Do.SVal.curry_nil, Std.Do.SVal.uncurry_cons, Std.Do.SVal.uncurry_nil, Std.Do.SVal.getThe_here, Std.Do.SVal.getThe_there, and_imp, true_implies]

for which I implemented a tactic mleave in nightly. (This is only an option if your monad stack can be completely interpreted away, i.e., there's no polymorphic base layer such as in StateT Nat m Nat.)

Other than that, I agree that the SPred proof mode (which is very much inspired by Iris' proof mode) is a little wonky and perhaps scary to use. Using simp will immediately destroy the metadata for working in that proof mode, so if you want to stay in the proof mode you have to be quite careful.
I'm tempted to get rid of the proof mode entirely, but that would mean you will be having a hard time proving things about StateT Nat m Nat.

TLDR; future support for the proof mode unclear.

In the meantime, if you can show me what exactly frightens you, then maybe I can try and improve?

[Patrick Massot]

I’m sorry my message was super vague. I was simply playing with Markus’s example and looking at the tactic state:

5 goals
l : List Int
b : MProd (Option Bool) (HashSet Int)
rpref : List Int
x : Int
suff : List Int
h✝ : l = rpref.reverse ++ x :: suff
h : (fun x =>
      match x with
      | (⟨earlyReturn?, seen⟩, traversalState) =>
        earlyReturn? = none ∧
            (∀ (x : Int), x ∈ seen ↔ x ∈ traversalState.rpref) ∧
              ¬List.ExistsPair (fun a b => a + b = 0) traversalState.pref ∨
          earlyReturn? = some true ∧ List.ExistsPair (fun a b => a + b = 0) l ∧ l = traversalState.pref,
      ()).fst
  (b, { rpref := rpref, suff := x :: suff, property := ⋯ })
a✝ : -x ∈ b.snd
⊢
h✝ : ⌜True⌝
⊢ₛ
match ForInStep.done ⟨some true, b.snd⟩ with
| ForInStep.yield b' =>
  (fun x =>
        match x with
        | (⟨earlyReturn?, seen⟩, traversalState) =>
          earlyReturn? = none ∧
              (∀ (x : Int), x ∈ seen ↔ x ∈ traversalState.rpref) ∧
                ¬List.ExistsPair (fun a b => a + b = 0) traversalState.pref ∨
            earlyReturn? = some true ∧ List.ExistsPair (fun a b => a + b = 0) l ∧ l = traversalState.pref,
        ()).fst
    (b', { rpref := x :: rpref, suff := suff, property := ⋯ })
| ForInStep.done b' =>
  (fun x =>
        match x with
        | (⟨earlyReturn?, seen⟩, traversalState) =>
          earlyReturn? = none ∧
              (∀ (x : Int), x ∈ seen ↔ x ∈ traversalState.rpref) ∧
                ¬List.ExistsPair (fun a b => a + b = 0) traversalState.pref ∨
            earlyReturn? = some true ∧ List.ExistsPair (fun a b => a + b = 0) l ∧ l = traversalState.pref,
        ()).fst
    (b', { rpref := l.reverse, suff := [], property := ⋯ })
l : List Int
b : MProd (Option Bool) (HashSet Int)
rpref : List Int
x : Int
suff : List Int
h✝ : l = rpref.reverse ++ x :: suff
h : (fun x =>
      match x with
      | (⟨earlyReturn?, seen⟩, traversalState) =>
        earlyReturn? = none ∧
            (∀ (x : Int), x ∈ seen ↔ x ∈ traversalState.rpref) ∧
              ¬List.ExistsPair (fun a b => a + b = 0) traversalState.pref ∨
          earlyReturn? = some true ∧ List.ExistsPair (fun a b => a + b = 0) l ∧ l = traversalState.pref,
      ()).fst
  (b, { rpref := rpref, suff := x :: suff, property := ⋯ })
a✝ : ¬-x ∈ b.snd
⊢
h✝ : ⌜True⌝
⊢ₛ
match ForInStep.yield ⟨none, b.snd.insert x⟩ with
| ForInStep.yield b' =>
  (fun x =>
        match x with
        | (⟨earlyReturn?, seen⟩, traversalState) =>
          earlyReturn? = none ∧
              (∀ (x : Int), x ∈ seen ↔ x ∈ traversalState.rpref) ∧
                ¬List.ExistsPair (fun a b => a + b = 0) traversalState.pref ∨
            earlyReturn? = some true ∧ List.ExistsPair (fun a b => a + b = 0) l ∧ l = traversalState.pref,
        ()).fst
    (b', { rpref := x :: rpref, suff := suff, property := ⋯ })
| ForInStep.done b' =>
  (fun x =>
        match x with
        | (⟨earlyReturn?, seen⟩, traversalState) =>
          earlyReturn? = none ∧
              (∀ (x : Int), x ∈ seen ↔ x ∈ traversalState.rpref) ∧
                ¬List.ExistsPair (fun a b => a + b = 0) traversalState.pref ∨
            earlyReturn? = some true ∧ List.ExistsPair (fun a b => a + b = 0) l ∧ l = traversalState.pref,
        ()).fst
    (b', { rpref := l.reverse, suff := [], property := ⋯ })
case pre1
l : List Int
⊢
h✝ : ⌜True⌝
⊢ₛ
(fun x =>
      match x with
      | (⟨earlyReturn?, seen⟩, traversalState) =>
        earlyReturn? = none ∧
            (∀ (x : Int), x ∈ seen ↔ x ∈ traversalState.rpref) ∧
              ¬List.ExistsPair (fun a b => a + b = 0) traversalState.pref ∨
          earlyReturn? = some true ∧ List.ExistsPair (fun a b => a + b = 0) l ∧ l = traversalState.pref,
      ()).fst
  (⟨none, ∅⟩, { rpref := [], suff := l, property := ⋯ })
case h_1
l : List Int
r✝ : MProd (Option Bool) (HashSet Int)
x✝ : Option Bool
heq✝ : r✝.fst = none
h : (fun x =>
      match x with
      | (⟨earlyReturn?, seen⟩, traversalState) =>
        earlyReturn? = none ∧
            (∀ (x : Int), x ∈ seen ↔ x ∈ traversalState.rpref) ∧
              ¬List.ExistsPair (fun a b => a + b = 0) traversalState.pref ∨
          earlyReturn? = some true ∧ List.ExistsPair (fun a b => a + b = 0) l ∧ l = traversalState.pref,
      ()).fst
  (r✝, { rpref := l.reverse, suff := [], property := ⋯ })
⊢
⊢ₛ false = true ↔ List.ExistsPair (fun a b => a + b = 0) l
case h_2
l : List Int
r✝ : MProd (Option Bool) (HashSet Int)
x✝ : Option Bool
a✝ : Bool
heq✝ : r✝.fst = some a✝
h : (fun x =>
      match x with
      | (⟨earlyReturn?, seen⟩, traversalState) =>
        earlyReturn? = none ∧
            (∀ (x : Int), x ∈ seen ↔ x ∈ traversalState.rpref) ∧
              ¬List.ExistsPair (fun a b => a + b = 0) traversalState.pref ∨
          earlyReturn? = some true ∧ List.ExistsPair (fun a b => a + b = 0) l ∧ l = traversalState.pref,
      ()).fst
  (r✝, { rpref := l.reverse, suff := [], property := ⋯ })
⊢
⊢ₛ a✝ = true ↔ List.ExistsPair (fun a b => a + b = 0) l

[Patrick Massot]

Note this is showing 5 goals, but each one of them looks rather frightening to me.

[Patrick Massot]

However keep in mind I know nothing about program verification, I’m a mathematician. So maybe this is simply unavoidable.

[Markus Himmel]

I think this is just because mvcgen doesn't do any kind of simp at the end; after all_goals simp the goals become much more manageable.

[Markus Himmel]

To give an anecdotal data point: in my first version I didn't use grind at all, and I didn't have any trouble understanding the goals and finishing the proofs using the usual Lean tactics.

[Asei Inoue]

@Bhavik Mehta Thank you!! great work!!

[Asei Inoue]

@Sebastian Graf Thank you for answering my question. I’m going to take my time and carefully read the material you shared with me. Thanks again.

[Patrick Massot]

Indeed all_goals simp at * after the mvcgen does wonders. Maybe it would make sense to do this (probably with a curated simp set) and then also some rcases to nicely split the invariant?

[Patrick Massot]

In Markus example, the splitting thing could be try rcases h with ⟨h₁, h₂, h₃⟩|⟨h₁, h₂, h₃⟩ based and the shape of the invariant.

[Patrick Massot]

And that could be opt-in, with something like mvcgen!.

[Sebastian Graf]

I think this is just because mvcgen doesn't do any kind of simp at the end; after all_goals simp the goals become much more manageable.

Indeed. I'm beginning to think that the default for mvcgen should be to run simp on the subgoals it produces after all... The worry here is performance, of course, but something like mvcgen -simp should provide an escape hatch.

some rcases to nicely split the invariant

I think this is something that @Rish Vaishnav also requested in https://github.com/leanprover/lean4/issues/9364.

• I'm unsure how to do this reliably... taking the hyp names from the invariant syntax reeks a bit unhygienic to me, but maybe that worry is unfounded.
• (It is not always necessary to split Ors and doing so duplicates goals.)
• I would prefer if this issue had a solution that is orthogonal to mvcgen, but I'm having trouble seeing how that could work. What makes loop invariants so special compared to e.g., induction hypotheses? Can we find a solution that handles both?

[Patrick Massot]

I think doing a full simp would be confusing in addition to being potentially slow. Actually in Markus’s example, doing dsimp only at * is already clearing the frightening part.

[Patrick Massot]

Probably dsimp only at * is a bit extreme, you could also use basic logic lemmas to get rid of stuff like True → … or turn `true = false ↔ …$ into $¬ …$ etc.

[Sebastian Graf]

Indeed. I did mean simp only; what lemmas to include is a good question. Rish argues that we might want to do mleave (the simp set in #general > new monadic program verification framework @ 💬 ) by default. (This set includes currently includes true_implies and and_imp.) I'm yet undecided.

[Patrick Massot]

About hygiene, the standard solution for all other tactics is to let users provide names. That would be someing like mvcgen [pairsSumToZero] with ⟨h₁, h₂, h₃⟩|⟨h₁, h₂, h₃⟩, except it needs a way to provide the invariant somewhere.

[Patrick Massot]

But don’t take my messages too seriously. I don’t know anything about program verification and I played only with Markus’s example. I mostly wanted to say I’m enthusiastic and I’d like to show this to people, but without frightening them.

[Sebastian Graf]

What makes matters more complicated is that the invariant is actually a subgoal produced by mvcgen and is specified by the user after using mvcgen. Also there might be many different invariants to specify.

Perhaps a specialized tactic provide_invariant inv => ... that works like case inv => by exact ... with a few extra goodies is the solution here. That tactic could investigate the remaining goals after instantiating inv and rcases accordingly. I think I like this idea.

[Ruben Van de Velde]

Fwiw, I had the same reaction, and I proved the first subgoal manually (with lots of simp?) and found it somewhat enlightening

[Ruben Van de Velde]

It did turn out that importing Mathlib.Tactic broke mvcgen

[Sebastian Graf]

Ruben Van de Velde said:

It did turn out that importing Mathlib.Tactic broke mvcgen

Yes, I already heard that from another user. MWE was

import Std.Tactic.Do
import Lean.Elab.Tactic.Do.VCGen -- comment this out to get the expected "failed to synthesize ..." error

example : True := by mvcgen

It's pretty strange. I must be doing something wrong because it doesn't happen for bv_decide. Will investigate, but unfortunately it doesn't reproduce in Lean's testsuite.

[Robin Arnez]

You redefine the syntax in Lean.Elab.Tactic.Do.VCGen:

syntax (name := mvcgen_step) "mvcgen_step" optConfig
 (num)? (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? : tactic

syntax (name := mvcgen_no_trivial) "mvcgen_no_trivial" optConfig
  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? : tactic

syntax (name := mvcgen) "mvcgen" optConfig
  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? : tactic

The first two should probably be moved to Init.Tactics and in general all of them removed from Lean.Elab.Tactic.Do.VCGen.

[Robin Arnez]

Actually no they are already in Std.Tactic.Do.Syntax, just remove them from Lean.Elab.Tactic.Do.VCGen then.

[Sebastian Graf]

Huh, thanks for checking! That would explain why I can't reproduce it, I've already removed these vestiges in my dev branch.

[Bhavik Mehta]

Sebastian Graf said:

Here's a solution using Std.Do for the isPrime variant without the d^2 > n test.

For the sake of comparison, here's the solution for the simpler version in the old setup. The two important points to note are that it's about double the length of Sebastian's solution, but about a third of the length of my solution to the original

https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMB0AVJAYxmEJwGUBTGAKBojEoDs5yYATO9ygMzgDkUOYAGcAClFCU4AChYAuASgCUcRQCEIEdGoC8cAJLscUAK4t2EGnDjA+LQCZEcAIxw0zazbhRqpqCx4kdBFKTx5oOHZbFgBtACZ5JgBdSKsvW3s4AFJIuH0ABjdUD3SbHxg/AKCQzxsAWjqM3IA9ODi4AD44FncmWrgGrywfJABrT3LKtzNQmgBiAHNTJCgowRhhcUkQaTj5pZW1oVEJKTgAZn3l1aUNk+3pAB4AEi6YgBYAGjgAVm+ANm+AHYUrp9DFAsFKN8YDNvpCQjCZkkrodbptTjsXPlLjRBmhRHB0JQQCAkKlKCImAByeAhEluCBwADu0FGcAAbpQoABPFmUdA6ZnANBwAAGwCY7FMxGAECYYpwSpoAAEYgKkFgAPpIERagWgFHcPgAGVEG3C6HY6AASpRCAB5GlwADegCbgOCARuA1HA8DzGHAtQBfV0gCAkLk+j2AJMJWNB4MHZDpFGaRPBPaoZAwo3BY97Y27lP0XVgoyH5P0wxHpKXYzIZKXFIXc3Aq8BI7XZOTFBmW+TABBERJbbcjWbAcFLSGUqmjlfD7ekMlTFu01rg2dL6FU8l0nmXOEt1rtjpYWsDdEoAA8kOBibILD71pnUOx2z6ooBiIm6z9cinaTnYZ92kUKJHm/R9ji2M4WH0BFpB3CceU8VAkEjRRXDAhR9CwPkFkkKVPBEUBxxidYMQeb593CKADCYfUAEctUPdAEBhVBRG+OwtSYSgFko81hHYG1zCY1cWJRGwULQuBAGAiWw4EHfcoCQJgFkoak2nvAY2mUb4WByYA8jgQoEJw/ofB4SVpEAC/J2G+AB+LVAEvyfo8MlKJSKEdgOXYLU7B4LUw18yhGIAL25CAJLgEJ4D4BCeHMOByVLQAywnPGwRFMHhLMISlZCUlS1I09o5G0uJpwPMS4D4GQcB5YABSiaymHlaE4BwcwRSc1R9BwSweLgayRAgLE4O+DqmC6xD+iI8A4BiAkRCitSeOUzBwrgArVPUzTSsacqjJ0FA4AAKmQ1DpGYbgoCTH1l1ubciUqq0dBqvrWsG4bRuqNqJq6nr2v6myvukMb2s6mAnL0foqLE48nQ017ZEbXqgc+kbQZ+8aIe67weB0Bs+VmkieCSIsbHcmUSHlIdhTQTwAB9umAHRdC6YmkvgRbGbgQh5REJK3FsVA8g6GbiPXJh0D5GJ9x2EAtT5pgRG+K9zT1EKtWgPzwBSY7ufSHDFd1PL9MFgp+kIE24EgAWUNF/pJIun03vqxrBpanjscmyHVHJVGPqGjHqqx8Gfah0yiYliFvhQqL0igZl5thl7Ff5tiOLgK7uXj3nrZ4hY4HttnHe8SgwHQIhpGAEWEJr2RFpMSltC5LViR4eAUPJ0opPg6rZDqhqrQ91rvf+832rd4fmtHsOpsj6Lo54WOkFzjLo8WzjUBRIA

[Bhavik Mehta]

Is there a easy workaround for the mathlib import breaking mvcgen? I'd like to use both in my example

[Sebastian Graf]

Unfortunately I don't think there is. I pushed a fix (#9505 lean4#9505), but it appears you'll have to wait for the next RC to use it with Mathlib.

[Bhavik Mehta]

(lean4#9505)

[Bhavik Mehta]

Patrick Massot said:

I mostly wanted to say I’m enthusiastic and I’d like to show this to people, but without frightening them.

Here's another basic example with some explanation, which might be useful for your purpose!

[Kim Morrison]

lean#9622 cleans up two rough edges you noticed here

[Patrick Massot]

Thinking again about this, I started fantasizing teaching my old intro to effective algebra class using this. And I remember the first thing I taught to explain the relevance of algorithm was:

import Std.Tactic.Do
import Std.Do.Triple.SpecLemmas

def naive_expo (x n : Nat) : Nat := Id.run do
  let mut y := 1
  for _ in [:n] do
    y := y*x
  return y

def fast_expo (x n : Nat) : Nat := Id.run do
  let mut x := x
  let mut y := 1
  let mut e := n
  for _ in [:n] do -- simulating a while loop running at most n times
    if e % 2 = 1 then
      y := x * y
      e := e - 1
    else
      x := x*x
      e := e/2
    if e = 0 then break
  return y

Does anyone want want to take up the challenge of proving those function both compute x^n? Changing the implementation is ok as long as the algorithms are recognizable.

[Kim Morrison]

import Std.Tactic.Do
import Std.Do.Triple.SpecLemmas

open Std.Do

def naive_expo (x n : Nat) : Id Nat := do
  let mut y := 1
  for _ in [:n] do
    y := y*x
  return y

theorem naive_expo_correct (x n : Nat) : naive_expo x n = x^n := by
  generalize h : naive_expo x n = r
  apply Id.by_wp h
  mvcgen
  case inv => exact ⇓⟨r, xs⟩ => ⌜r = x^xs.pref.length⌝
  case step ih =>
    simp at ih ⊢
    simp [Nat.pow_add_one, ih]
  case a.pre1 =>
    simp
  case a.post.success h =>
    simpa using h

[Kim Morrison]

(desperately cribbing from Bhavik's example above :-)

[Kim Morrison]

and I claim/hope that all the sorries in

theorem fast_expo_correct (x n : Nat) : fast_expo x n = x^n := by
  generalize h : fast_expo x n = r
  apply Id.by_wp h
  mvcgen
  case inv => exact ⇓⟨⟨e, x', y⟩, xs⟩ => ⌜y * x'^e = x^n ∧ e ≤ n - xs.pref.length⌝
  case step.isTrue ih =>
    simp at ih ⊢
    mvcgen
    case isTrue h' =>
      simp
      sorry
    case isFalse h' =>
      simp
      sorry
  case step.isFalse ih =>
    simp at ih ⊢
    mvcgen
    case isTrue h' =>
      simp
      sorry
    case isFalse h' =>
      simp
      sorry
  case a.pre1 =>
    simp
  case a.post.success h =>
    simp at h ⊢
    sorry

are entirely conventional. :-)

[Kim Morrison]

(i.e. all I have done here is written down my guess as to the relevant loop invariant, and then used the not-yet-existing code action that takes us from the monadic verification world to the normal world)

[Kim Morrison]

The nested calls to mvcgen are perhaps the wrong way to drive this machine, @Sebastian Graf will know better.

[Patrick Massot]

Which version of Lean are you using here? Your code doesn’t seem to work in the playground.

[Patrick Massot]

And indeed it works in the playground if I force latest nightly.

[Bhavik Mehta]

Kim Morrison said:

The nested calls to mvcgen are perhaps the wrong way to drive this machine, Sebastian Graf will know better.

I'm using split there instead of mvcgen, it looks to me like there's a missing [spec] for ite. But as you say, Sebastian will know better

[Bhavik Mehta]

here's a proof for both, where I edited the function slightly to change the position of the break

import Std.Tactic.Do
import Std.Do.Triple.SpecLemmas

def naive_expo (x n : Nat) : Nat := Id.run do
  let mut y := 1
  for _ in [:n] do
    y := y*x
  return y

def fast_expo (x n : Nat) : Nat := Id.run do
  let mut x := x
  let mut y := 1
  let mut e := n
  for _ in [:n] do -- simulating a while loop running at most n times
    if e = 0 then break
    if e % 2 = 1 then
      y := x * y
      e := e - 1
    else
      x := x*x
      e := e/2

  return y

open Std.Do

theorem naive_expo_correct (x n : Nat) : naive_expo x n = x^n := by
  generalize h : naive_expo x n = r
  apply Id.by_wp h
  mvcgen
  case inv => exact ⇓⟨y, xs⟩ => ⌜y = x ^ xs.pref.length⌝
  all_goals simp_all [Nat.pow_add_one]

theorem fast_expo_correct (x n : Nat) : fast_expo x n = x^n := by
  generalize h : fast_expo x n = r
  apply Id.by_wp h
  mvcgen
  case inv => exact ⇓⟨⟨e, x', y⟩, xs⟩ => ⌜x' ^ e * y = x ^ n ∧ e ≤ n - xs.pref.length⌝
  all_goals simp_all
  case isFalse x _ _ ih =>
    obtain ⟨e, y, x'⟩ := b
    split
    case isTrue =>
      simp_all
      constructor
      · rw [← Nat.mul_assoc, ← Nat.pow_add_one, ← ih.1]
        have : e - 1 + 1 = e := by grind
        rw [this]
      · grind
    case isFalse =>
      simp_all
      constructor
      · rw [← Nat.pow_two, ← Nat.pow_mul]
        grind
      · grind
  case a.post b ih =>
    obtain ⟨e, y, x'⟩ := b
    dsimp at ih ⊢
    rw [← ih.1, ih.2, Nat.pow_zero, Nat.one_mul]

theorem same_func (x n : Nat) : fast_expo x n = naive_expo x n := by
  rw [naive_expo_correct, fast_expo_correct]

[Bhavik Mehta]

I'm surprised by the block

have : e - 1 + 1 = e := by grind
rw [this]

I expected just grind to solve that goal...

[Aaron Liu]

I tried

import Std.Tactic.Do
import Std.Do.Triple.SpecLemmas

def fastExpo (x n : Nat) : Nat := Id.run do
  let mut x := x
  let mut y := 1
  let mut e := n
  for _ in [:n] do -- simulating a while loop running at most n times
    if e % 2 = 1 then
      y := x * y
      e := e - 1
    else
      x := x*x
      e := e/2
    if e = 0 then break
  return y

open Std.Do

@[simp]
theorem Id.pure_run {α : Type u} (x : Id α) : pure x.run = x := rfl

theorem fastExpo_spec (x n : Nat) : fastExpo x n = x ^ n := by
  rw [← Id.run_pure (fastExpo x n)]
  refine Id.by_wp (Eq.refl (Id.run (pure (fastExpo x n)))) (· = x ^ n) ?_
  rw [fastExpo, Id.pure_run]
  mvcgen
  case inv =>
    exact ⇓⟨⟨e, x', y⟩, xs⟩ => ⌜y * x'^e = x^n ∧ e + xs.pref.length ≤ n⌝
  case ifTrue h₁ h₂=>
    obtain ⟨e, x', y⟩ := b
    match e with
    | 0 => simp at h₁
    | 1 => simpa [Nat.mul_comm] using h.left
  case ifFalse h₁ h₂ =>
    obtain ⟨e, x', y⟩ := b
    match e with
    | 0
    | 1 => simp at h₂
    | 2 => simp at h₁
    | e + 1 + 2 =>
      simp only [Nat.add_mod_right] at h₁
      obtain he | he := e.mod_two_eq_zero_or_one.symm
      · rw [Nat.add_mod, he] at h₁
        simp at h₁
      rw [← Nat.dvd_iff_mod_eq_zero] at he
      obtain ⟨k, rfl⟩ : ∃ k, 2 * k = e := ⟨e / 2, Nat.mul_div_cancel' he⟩
      simp only [List.length_reverse, SVal.curry_nil, Nat.add_one_sub_one, List.length_cons,
        SPred.entails_nil, forall_const] at h ⊢
      constructor
      · rw [← h.left]
        simp only [Nat.pow_succ]
        ac_rfl
      · refine le_of_eq_of_le ?_ h.right
        ac_rfl
  case ifTrue h₁ h₂ =>
    obtain ⟨e, x', y⟩ := b
    match e with
    | 0 => simpa using h.left
    | 1 => simp at h₁
    | n + 2 => simp at h₂
  case ifFalse h₁ h₂ =>
    obtain ⟨e, x', y⟩ := b
    simp only [List.length_reverse, SVal.curry_nil, List.length_cons, SPred.entails_nil,
      forall_const] at h ⊢
    constructor
    · rw [← h.left]
      rw [Nat.mod_two_not_eq_one, ← Nat.dvd_iff_mod_eq_zero] at h₁
      rw [← Nat.pow_two, ← Nat.pow_mul, Nat.mul_div_cancel' h₁]
    · have := h.right
      simp only [Nat.div_eq_zero_iff, reduceCtorEq, false_or, Nat.not_lt] at h₂
      omega
  case pre1 => simp
  case post.success r =>
    obtain ⟨e, x', y⟩ := r
    obtain rfl : e = 0 := by
      simp only [List.length_reverse, List.length_range', Nat.sub_zero, Nat.add_one_sub_one,
        Nat.div_one, SVal.curry_nil] at h
      omega
    simpa using h.left

[Patrick Massot]

Nice!

[Sebastian Graf]

Great work! Another nice example.

Strange. Generally, whenever you need to do mvcgen twice, there's a bug in mvcgen. In the case above, the internal use of the split tactic fails. I added this test case to my kitchen sink test file on my dev branch and there it appears I've already fixed the issue. On my dev branch I tell the split tactic which if to split rather than letting it figure out from the shape of the goal (where it first tries to split on the if in a stateful hypothesis ...)

[Patrick Massot]

Using xs.pref.length seems a bit artificial. Isn’t there simply a way to access the current value of the loop variable?

[Bhavik Mehta]

I think "current value" is a bit tricky, since it needs to make sense both before the loop starts and after it ends: xs.pref.length takes n+1 values, but the loop variable only takes n values

[Patrick Massot]

I’m not sure I understand this explanation, but the important point is that Sebastian can take notes that could be useful when all this will be documented.

[Shreyas Srinivas]

can these two lines by automated?

generalize h : <definition = generalized result variable>
  apply Id.by_wp h
  mvcgen

[Sebastian Graf]

Good question. The generalize is telling the system "focus on this subexpression, it represents the computation". That is similar to conv at focusOnThisSubexpression. Alas, the by_wp theorems are very specific to the particular monad. But maybe we can somehow maintain a database of by_wp theorems per monad and shorten it to

by_wp at fast_expo x n
mvcgen

where by_wp is a new tactic. Is that one saved line worth explaining what by_wp does? Hard to tell. Note that you will only need to do this once per functional correctness property. Larger proofs are likely specifying properties in terms of Hoare triples rather than through pure Props.

[Shreyas Srinivas]

Thanks to @Bhavik Mehta's examples I am beginning to learn how this framework functions.

[Shreyas Srinivas]

I have another feedback

[Shreyas Srinivas]

For some reason the mvcgen tactic decides to output stuff with no notation

[Shreyas Srinivas]

From discussions in iris, I know that the infoview doesn't support complex formatting, but I would have hoped it could at least use the correct notation

[Bhavik Mehta]

Which notation are you hoping to see? Something which resembles the imperative syntax? For me, the tactic does display notation, so presumably the notation you want is different

[Shreyas Srinivas]

Yeah, but I also think it would be nice to have the verification conditions appear in a different colour than the code in between

[Bhavik Mehta]

I think that's not specific to the tactic, that's either a notation printing change or an infoview change

[Shreyas Srinivas]

Yes but I know this isn't supported by the infoview. We have similar problems in iris-lean

[Bhavik Mehta]

But I agree that the goal state after running the tactic could be quite a lot more readable

[Shreyas Srinivas]

It might be better to change the way the tactic behaves by having one tactic show the goal in {{Pre-condition}} def {{Post Condition}} format with suitable indentation and syntax highlighting, and then do the case split in a separate tactic

[Shreyas Srinivas]

Currently I get these four cases, out of which 3 have metavariables (in Bhavik's second example)

[Sebastian Graf]

To be fair, all examples so far used Id. If you use StateM you'll begin to see actual stateful hypothesis to the left of |-s. Often these aren't terribly useful and all tactics try to frame as many pure facts as possible into the regular, local Lean context. In Id, every hypothesis can and will be framed into the local context.

[Shreyas Srinivas]

For what it is worth, I think the infoview needs to support some custom formatting. In Iris we have this weird situation where the Iris hyps and goals are essentially just rendered as one big blob with no highlighting

[Shreyas Srinivas]

We'll run into this same situation in CSLib when people start formulating different logical theories

[Shreyas Srinivas]

CC : @Marc Huisinga

EDIT : The other thread : #iris-lean > Minor UX quibble @ 💬 for reference

[Sebastian Graf]

In Iris we have this weird situation where the Iris hyps and goals are essentially just rendered as one big blob with no highlighting

Yeah, the pretty-printing in Std.Do is basically a copy of that. See the examples in https://github.com/leanprover/lean4/blob/master/tests/lean/run/spredProofMode.lean. Why is missing highlighting problematic? Do you have a concrete complaint?

show the goal in {{Pre-condition}} def {{Post Condition}} format

This won't support multiple named stateful hypotheses, hence the chosen formatting of the proof mode

[Shreyas Srinivas]

Sebastian Graf said:

In Iris we have this weird situation where the Iris hyps and goals are essentially just rendered as one big blob with no highlighting

Yeah, the pretty-printing in Std.Do is basically a copy of that. See the examples in https://github.com/leanprover/lean4/blob/master/tests/lean/run/spredProofMode.lean. Why is missing highlighting problematic? Do you have a concrete complaint?

Readability and mapping it to more traditional notation as a beginner.

[Shreyas Srinivas]

For example:

PostCond (Nat × Std.List.Zipper { stop := n, step_pos := Nat.zero_lt_one }.toList) PostShape.pure

this would be easier to read with notation

[Shreyas Srinivas]

Screenshot from 2025-07-31 16-21-38.png
This would be more readable with indentation

[Shreyas Srinivas]

to be fair some of this is just complaining about how infoview renders anything in general

[Shreyas Srinivas]

but they stand out here because of the size of the goals

[Sebastian Graf]

Readability and mapping it to more traditional notation as a beginner.

Is there a traditional notation you have in mind that supports giving names to multiple stateful hypotheses? Perhaps similar to {{P}} x {{Q}} as you suggest, but that would look weird with one line per stateful hyp in P.

Shreyas Srinivas said:

For example:

PostCond (Nat × Std.List.Zipper { stop := n, step_pos := Nat.zero_lt_one }.toList) PostShape.pure

this would be easier to read with notation

What kind of notation do you have in mind?

[Shreyas Srinivas]

Sebastian Graf said:

Readability and mapping it to more traditional notation as a beginner.

Is there a traditional notation you have in mind that supports giving names to multiple stateful hypotheses? Perhaps similar to {{P}} x {{Q}} as you suggest, but that would look weird with one line per stateful hyp in P.

1. One line per stateful hypothesis. Iris already does something similar.
2. Colours for hypothesis names, maybe even different from regular hypotheses to keep the two separate visually (which we also miss in Iris, a bigger rendering of the entails symbol). This requires better ability to control how infoview is rendered as Mario mentioned in the other thread
3. Indented rendering of the structure type itself, but this is a lean-wide issue.
4. EDIT : PostCond doesn't need to appear as a word. Some bracketing notation would look better.

Shreyas Srinivas said:

For example:

PostCond (Nat × Std.List.Zipper { stop := n, step_pos := Nat.zero_lt_one }.toList) PostShape.pure

this would be easier to read with notation

What kind of notation do you have in mind?

Basically along the general ideas I described above.

[Shreyas Srinivas]

Also, the effects in the PostShape could be rendered separately

[Shreyas Srinivas]

I understand that this is purely determined by the monad, so there is no need to include the PostShape.pure rendering inside the goal

[Shreyas Srinivas]

It's extraneous in some sense. It's part of and determined by the (monadic) "context" rather than the goal.

[Sebastian Graf]

In the reference manual, I want to demonstrate that proving stuff about for loops with early return is somewhat frustrating without mvcgen. I came up with the following example:

import Std

def nodup (l : List Int) : Bool := Id.run do
  let mut seen : Std.HashSet Int := ∅
  for x in l do
    if x ∈ seen then
      return false
    seen := seen.insert x
  return true

@[simp, grind]
theorem Std.HashSet.Nodup_toList [Hashable α] [BEq α] [LawfulHashable α] [EquivBEq α] [LawfulBEq α] (m : Std.HashSet α) :
    m.toList.Nodup := by
  simpa using Std.HashMap.distinct_keys (m := m.inner)

@[simp, grind]
theorem Std.HashSet.Nodup_append_toList_insert [Hashable α] [BEq α] [LawfulHashable α] [EquivBEq α] [LawfulBEq α] (m : Std.HashSet α) (x : α) (h : x ∉ m) :
    ((m.insert x).toList ++ tl).Nodup ↔ (m.toList ++ x :: tl).Nodup := by
  grind

theorem nodup_correct_directly (l : List Int) : nodup l ↔ l.Nodup := by
  simp only [nodup, bind_pure_comp, map_pure, Id.run_bind]
  suffices h :
      ∀ seen,
        match MProd.fst (Id.run (forIn (β := MProd (Option Bool) (Std.HashSet Int)) l ⟨none, seen⟩ (fun x ⟨_, seen⟩ =>
          if x ∈ seen then pure (ForInStep.done (α := MProd (Option Bool) (Std.HashSet Int)) ⟨some false, seen⟩)
          else pure (ForInStep.yield (α := MProd (Option Bool) (Std.HashSet Int)) ⟨none, seen.insert x⟩)))) with
        | some true => False
        | some false => ¬(seen.toList ++ l).Nodup
        | none => (seen.toList ++ l).Nodup by
    replace h := h ∅
    split
    · simp only [Id.run_pure]; grind
    · cases ‹Bool› <;> simp_all only [Id.run_pure]; grind
  induction l
  case nil => simp
  case cons hd tl ih =>
    intro seen
    replace ih := ih (seen.insert hd)
    simp only [List.forIn_cons]
    if hif : hd ∈ seen
    then simp_all only [↓reduceIte, pure_bind, Id.run_pure]; grind
    else split <;> simp_all

Which is indeed quite painful. But perhaps someone can make this proof more succinct so that I don't oversell mvcgen? I tried to golf a bit, but the inability of grind to prove

example : Id.run (pure true) = true := by
  grind [Id.run_pure]

is getting in the way. (Have to reach out and see whether this is a bug.)

[Alfredo Moreira-Rosa]

and whith mvcgen ?

[Sebastian Graf]

On my branch (soon master) the proof is

theorem nodup_correct (l : List Int) : nodup l ↔ l.Nodup := by
  generalize h : nodup l = r
  apply Id.by_wp h
  mvcgen
  case inv =>
    exact Invariant.withEarlyReturn
      (onReturn := fun ret seen => ⌜ret = false ∧ ¬l.Nodup⌝)
      (onContinue := fun xs seen => ⌜(∀ x, x ∈ seen ↔ x ∈ xs.pref) ∧ xs.pref.Nodup⌝)
  all_goals mleave; grind

(Without the additional simp and grind lemmas.)

[Bhavik Mehta]

here's what I got:

theorem nodup_correct_directly (l : List Int) : nodup l ↔ l.Nodup := by
  rw [nodup]
  generalize hl' : (∅ : Std.HashSet Int) = l'
  convert_to _ ↔ l.Nodup ∧ ∀ x ∈ l, x ∉ l'
  · simp [← hl']
  clear hl'
  simp only [bind_pure_comp, map_pure, Id.run_bind]
  induction l generalizing l'
  case nil => simp_all
  case cons x _ _ => by_cases x ∈ l' <;> aesop (add simp [forall_and])

[Bhavik Mehta]

It's relatively short, but has the cost of importing tactics from mathlib

[Bhavik Mehta]

while this example doesn't make it clear, I believe the case where mvcgen really shines over the older approaches is with nested loops or more subtle control flows

[Kim Morrison]

Sebastian Graf said:

On my branch (soon master) the proof is

theorem nodup_correct (l : List Int) : nodup l ↔ l.Nodup := by
  generalize h : nodup l = r
  apply Id.by_wp h
  mvcgen
  case inv =>
    exact Invariant.withEarlyReturn
      (onReturn := fun ret seen => ⌜ret = false ∧ ¬l.Nodup⌝)
      (onContinue := fun xs seen => ⌜(∀ x, x ∈ seen ↔ x ∈ xs.pref) ∧ xs.pref.Nodup⌝)
  all_goals mleave; grind

(Without the additional simp and grind lemmas.)

It would be lovely if there was some way for a tactic for postpone itself, and say "leave goal 1 for the user. goal 2 will depend on via a metavariable; as soon as this metavariable is assign, resume with the following tactics".

This would allow omitting all_goals mleave; grind, perhaps.

[Kim Morrison]

I wonder if

mvcgen
case inv =>
    exact Invariant.withEarlyReturn

could be turned into a single step, i.e. specifying the invariant as part of the mvcgen call, so it could take care of cleanup steps itself.

[Sebastian Graf]

Sebastian Graf said:

In the reference manual, I want to demonstrate that proving stuff about for loops with early return is somewhat frustrating without mvcgen.

Latest master has a fix for the grind bug and thanks to Bhavik's template I could shorten the proof to

theorem nodup_correct_directly (l : List Int) : nodup l ↔ l.Nodup := by
  rw [nodup]
  generalize hseen : (∅ : Std.HashSet Int) = seen
  change ?lhs ↔ l.Nodup
  suffices h : ?lhs ↔ l.Nodup ∧ ∀ x ∈ l, x ∉ seen by grind
  clear hseen
  induction l generalizing seen with grind [Id.run_pure, Id.run_bind]

with only Core tactics. I think this is as short as it gets. Observations:

• We are relying on grind to do the case splits on control flow (probably fine).
• We are relying on grind being able to reason about monadic programs using lemmas Id.run_pure and Id.run_bind. Id.run_seqLeft for example is not an e-matchable lemma, and I imagine that it won't be able to reason about StateM either. (Needs testing. The StateT.run_* lemmas are certainly sufficiently first-order.)
• The previous two points are important, because as soon as grind fails to reason about a single construct in the chain (like Id.run (pure ...) in the previous post), we have to fall back to manual splitting and taking apart the control flow. So it's a separation of concerns argument: mvcgen focuses just on breaking down control flow and monadic computations, so that the remaining pure VCs can be reliably discharged by grind without knowing about Id.run_pure, etc.
• We are relying on change C[?lhs] to match out sub-program ?lhs in a context C. This could be tedious and brittle when C is large, although I'm not sure whether that would be a problem in practice.

[Sebastian Graf]

Kim Morrison said:

It would be lovely if there was some way for a tactic for postpone itself, and say "leave goal 1 for the user. goal 2 will depend on via a metavariable; as soon as this metavariable is assign, resume with the following tactics".

So mvcgen currently generates roughly two kinds of goals: (1) inv<n> invariants (of type Std.Do.Invariant), which I think corresponds to your "goal 1", and (2) vc<n> goals which is everything else. I imagine that at some point (probably next Q) I'll add syntax like

mvcgen [...] using
  invariants 1 => Invariant.withEarlyReturn
      (onReturn := fun ret seen => ⌜ret = false ∧ ¬l.Nodup⌝)
      (onContinue := fun xs seen => ⌜(∀ x, x ∈ seen ↔ x ∈ xs.pref) ∧ xs.pref.Nodup⌝)
  with grind

which expands to something like

mvcgen -leave [...]
case inv1 1 => by mleave; exact Invariant.withEarlyReturn
   (onReturn := fun ret seen => ⌜ret = false ∧ ¬l.Nodup⌝)
   (onContinue := fun xs seen => ⌜(∀ x, x ∈ seen ↔ x ∈ xs.pref) ∧ xs.pref.Nodup⌝)
all_goals mleave; grind

In particular, note that this instantiates the invariant before doing mleave (which is simp only [...] at *, done automatically on every subgoal as part of mvcgen +leave), so that grind is immediately applicable. Not sure if its worth saving the keystrokes for with grind.

specifying the invariant as part of the mvcgen call

Yes, exactly :)

[Sebastian Graf]

Here's where I'm drafting a reference manual entry/tutorial: https://hackmd.io/@sg-fro/BJRlurP_xg

[Sebastian Graf]

The linked tutorial should be "complete enough" now. As always, I'm open for feedback! Though I'll be away for a month now, so I can't really incorporate feedback until after that.

[Sebastian Graf]

lean4#9927 implements the syntax I was alluding to earlier. This syntax will not yet make it into 4.23. Full syntax example:

  mvcgen
  using invariants
  | 1 => Invariant.withEarlyReturn
      (onReturn := fun ret seen => ⌜ret = false ∧ ¬l.Nodup⌝)
      (onContinue := fun traversalState seen =>
        ⌜(∀ x, x ∈ seen ↔ x ∈ traversalState.prefix) ∧ traversalState.prefix.Nodup⌝)
  with mleave -- mleave is a no-op here, but we are just testing the grammar
  | vc1 => grind
  | vc2 => grind
  | vc3 => grind
  | vc4 => grind
  | vc5 => grind

or in short

  mvcgen
  using invariants
  | 1 => Invariant.withEarlyReturn
      (onReturn := fun ret seen => ⌜ret = false ∧ ¬l.Nodup⌝)
      (onContinue := fun traversalState seen =>
        ⌜(∀ x, x ∈ seen ↔ x ∈ traversalState.prefix) ∧ traversalState.prefix.Nodup⌝)
  with grind

More examples in the test file.

I'm very much open to bike-shedding suggestions!

• Note that the using invariants | <n> => syntax might feel a little... "unleanish". Maybe somebody has a better idea.
• The with $tac | $lhs => $rhs has the same semantics as all_goals (try $tac); case $lhs => $rhs, so I think that's far more "leanish".

[Ruben Van de Velde]

I like it :)

[Ruben Van de Velde]

Can the using invariants bit go on the same line as mvcgen as well?

[Sebastian Graf]

Yes!

[Asei Inoue]

@Markus Himmel

Thank you for writing nice article! but your code does not work!

image.png

[Asei Inoue]

@Sebastian Graf

markdown layout looks broken (code block does not work)

image.png

[Sebastian Graf]

Asei Inoue said:

Thank you for writing nice article! but your code does not work!

That's the unfortunate consequence of working with pre-releases :)
I enshrined Markus' code as a test case here: https://github.com/leanprover/lean4/blob/master/tests/lean/run/pairsSumToZero.lean

Asei Inoue said:

markdown layout looks broken (code block does not work)

Thanks, fixed!

[Frederick Pu]

i think user should be able to annotate invariants and hints in a dafney/verus style way

import Mathlib
import Std

set_option pp.letVarTypes true

/-
  simple tail assertion `have : Even y`
-/
def double_proof (x : Nat) : Nat := Id.run <| do
  let y := 2 * x;
  have : Even y := by
    use x
    ring
  return y

def double (x : Nat) : Nat := Id.run <| do
  let y := 2 * x;
  return y

theorem even_double : ∀ x, Even (double x) := by
  intro x
  have : double = double_proof := rfl
  rw [this]
  unfold double_proof
  extract_lets y this
  (expose_names; exact this)

example : ∀ n : ℤ, 2 ∣ n * (n + 1) := by
  exact fun n => Int.two_dvd_mul_add_one n
/-
  loop invariant example
-/
def sumN_proof (n : Nat) : Nat := Id.run <| do
  let mut out := 0
  have : (out : Nat) = ((0:ℕ) - 1 : ℤ) * 0 / 2 := rfl
  for i in List.range n do
    let prev := out
    out := out + i
    let new := out
    have : prev = (i-1 : ℤ) * i / 2 → new = (i + 1 - 1 : ℤ) * ((i + 1)) / 2 := by
      intro h
      have : new = prev + i := by tauto
      zify at this
      rw [this, h]
      qify
      rw [Int.cast_div, Int.cast_div]
      field_simp
      push_cast
      ring
      convert Int.two_dvd_mul_add_one (↑i + 1 - 1 : ℤ)
      ring
      norm_num
      convert Int.two_dvd_mul_add_one (↑i - 1 : ℤ)
      ring
      norm_num

  return out

def sumN (n : Nat) : Nat := Id.run <| do
  let mut out := 0
  for i in List.range n do
    out := out + i
  return out

theorem sumN_spec (n : Nat) : ⦃⌜True⌝⦄ sumN n ⦃⇓r => r = n * (n + 1) / 2⦄ := by
  have : sumN = sumN_proof := by rfl
  intro n
  rw [this]
  unfold sumN_proof
  /-
    this : sumN = sumN_proof
    n : ℕ
    ⊢ (let out : ℕ := 0;
        have this : ↑out = (↑0 - 1) * 0 / 2 := sumN_proof._proof_1;
        do
        let r ←
          forIn (List.range n) out fun i r =>
              let out : ℕ := r;
              let prev : ℕ := out;
              let out : ℕ := out + i;
              let new : ℕ := out;
              have this : ↑prev = (↑i - 1) * ↑i / 2 → ↑new = (↑i + 1 - 1) * (↑i + 1) / 2 := ⋯;
              do
              pure PUnit.unit
              pure (ForInStep.yield out)
        have out : ℕ := r
        pure out).run =
      n * (n + 1) / 2
  -/

and have proof automation such as extract_lets unify to the prove the goal. a lot of people already are doing this with a subtype style pattern. I think this approach + the mvcgen could allow this trick to generalize to for loops too

[Frederick Pu]

how would i construct the loop invariant?

/-
  loop invariant example
-/
def sumN_proof (n : Nat) : Id Nat := do
  let mut out := 0
  have : (out : Nat) = ((0:ℕ) - 1 : ℤ) * 0 / 2 := rfl
  for i in List.range n do
    let prev := out
    out := out + i
    let new := out
    have : prev = (i-1 : ℤ) * i / 2 → new = (i + 1 - 1 : ℤ) * ((i + 1)) / 2 := by
      intro h
      have : new = prev + i := by tauto
      zify at this
      rw [this, h]
      qify
      rw [Int.cast_div, Int.cast_div]
      field_simp
      push_cast
      ring
      convert Int.two_dvd_mul_add_one (↑i + 1 - 1 : ℤ)
      ring
      norm_num
      convert Int.two_dvd_mul_add_one (↑i - 1 : ℤ)
      ring
      norm_num

  return out

def sumN (n : Nat) : Id Nat := do
  let mut out := 0
  for i in List.range n do
    out := out + i
  return out

open Std Do

#check Invariant.withEarlyReturn
#check PostCond
theorem sumN_spec (n : Nat) :
  sumN n = n * (n + 1) / 2:= by
  /-
  unexpected token '⌜'; expected '_' or identifier
  -/
  have : sumN = sumN_proof := by rfl
  rw [this]
  unfold sumN_proof
  generalize h : sumN n = r
  apply Id.of_wp_run_eq h
  mvcgen
  /-
   n : ℕ
   this : sumN = sumN_proof
   r : Id ℕ
   h : sumN n = r
   ⊢ Invariant (List.range n) ℕ PostShape.pure
  -/

[Asei Inoue]

@Sebastian Graf

When is the official release of Std.Do?

[Sebastian Graf]

Frederick Pu said:

i think user should be able to annotate invariants and hints in a dafney/verus style way

Interesting. Why maintain the erased variant double besides the verified variant double_proof? Why not just double_proof?

Incidentally, in my prototype library mpl I implemented an extension to def elaboration that implements Dafny/Verus-style intrinsic verification syntax, exploiting definitional equivalence between an erased and refined definition of sumN in much the same way. Here's an example of that: https://github.com/sgraf812/mpl/blob/1dbf6bc75ff5398f59b77ae320f1f0a0781b721e/MPL/Experimental/Do.lean#L426-L437
I haven't implemented that syntax in Lean yet because we wanted to rewrite do elaboration first. But something like that is on our agenda.

Frederick Pu said:

how would i construct the loop invariant?

Here you go. In the next RC, you will be able to write mvcgen invariant? to get a suggestion to write mvcgen invariant\n · ⇓⟨xs, out⟩ => _.
Below you still need to prove the non-linear inductive step though:

import Std

def sumN (n : Nat) : Id Nat := do
  let mut out := 0
  for i in List.range n do
    out := out + i
  return out

open Std Do

#check Invariant.withEarlyReturn
#check PostCond
theorem sumN_spec (n : Nat) :
  sumN n = n * (n + 1) / 2:= by
  generalize h : sumN n = r
  apply Id.of_wp_run_eq h
  rw [List.range_eq_range']
  mvcgen invariants
  · ⇓⟨xs, out⟩ => ⌜out = xs.prefix.length * (xs.prefix.length + 1) / 2⌝
  with grind -- TODO

[Sebastian Graf]

Asei Inoue said:

Sebastian Graf

When is the official release of Std.Do?

If all goes well, then the next RC will properly release Std.Do. It's my first day after a month of parental leave, though, and I need to ascertain that there are no remaining big TODOs.

[Frederick Pu]

ideally the invariant keyword could bind the for loop variables directly. something like

macro_rules
  | `(doElem| assert $xs* => $p) => `(doElem| assertGadget (fun $xs* => $p))
  | `(doElem| assert => $p) => `(doElem| assertGadget $p)
  | `(doElem| invariant $xs* => $p
              for $decls:doForDecl,* do $body) => `(doElem|
              for $decls:doForDecl,* do $body)

but i think that would require the ability to create expr mdata during the do elaboration process. Idk if that's alerady a feature or not. But having a mdata:doElem would be really handy for extending do notation without having to interact with the core do elaboration procedure

[Frederick Pu]

something like annotate (e : term) (elem : doElem) : doElem so that it behaves exactly like doElem except whatever doElem becomes in the final expr gets wrapped with the meta data value of e (using a function def annotateDo {elemType : Type*} {alpha : elemType -> Type*} (elem : elemType) (e : alpha elem) := elem) where where elemType is the type of term that (elem: doElem becomes).

[Frederick Pu]

then you could have something like

syntax "invariant " term "by " term : doElem

macrorules
| `(invariant $inv by $proof
       for $forDecl do $forBody) =>
    `(annotate $inv (annotateDo $forBody $proof))
        for $forDecl do annotate $proof $forBody)

obviously this still won't work because the $forBody will not be correct elaborated form of that do block but if there were a way efficiently getting that elaboration result this would make implement refinement style tings much nicer and allow for usable unification hints for invariants

[Asei Inoue]

Hi. Thank you for writing nice document: https://hackmd.io/@sg-fro/BJRlurP_xg
I have read this!

I want to write some proof by myself but I don't go further anymore.
How to fill this sorry?

import Std.Tactic.Do
import Lean

set_option mvcgen.warning false

open Std.Do

def peasantMul (x y : Nat) : Nat := Id.run do
  let mut cur_x := x
  let mut cur_y := y
  let mut prod := 0
  for _ in [0: x] do
    if cur_x = 0 then
      break
    if cur_x % 2 = 1 then
      prod := prod + cur_y
    cur_x := cur_x / 2
    cur_y := cur_y * 2
  return prod

#guard peasantMul 3 4 = 12
#guard peasantMul 6 7 = 42
#guard peasantMul 12 100 = 1200

example (x y : Nat) : peasantMul x y = x * y := by
  generalize h : peasantMul x y = s
  apply Id.of_wp_run_eq h

  mvcgen
  case inv1 => exact ⇓⟨_, ⟨cur_x, cur_y, prod⟩⟩ => ⌜cur_x * cur_y + prod = x * y⌝
  all_goals mleave

  all_goals sorry

[Asei Inoue]

uhhh... :(

import Std.Tactic.Do
import Lean

set_option mvcgen.warning false

open Std.Do

def peasantMul (x y : Nat) : Nat := Id.run do
  let mut cur_x := x
  let mut cur_y := y
  let mut prod := 0
  for _ in [0: x] do
    if cur_x = 0 then
      break
    if cur_x % 2 = 1 then
      prod := prod + cur_y
    cur_x := cur_x / 2
    cur_y := cur_y * 2
  return prod

#guard peasantMul 3 4 = 12
#guard peasantMul 6 7 = 42
#guard peasantMul 12 100 = 1200

example (x y : Nat) : peasantMul x y = x * y := by
  generalize h : peasantMul x y = s
  apply Id.of_wp_run_eq h

  mvcgen +leave
  case inv1 =>
    exact Invariant.withEarlyReturn
      (onReturn := fun ret cur_x cur_y prod => ⌜ret = prod ∧ cur_x = 0⌝)
      /- Application type mismatch: The argument
        fun xs cur_x cur_y prod => ⌜cur_x * cur_y + prod = x * y⌝
      has type
        (xs : List.Cursor ?m.599) → (cur_x cur_y prod : Nat) → SPred (?m.620 xs cur_x cur_y prod)
      but is expected to have type
        List.Cursor ?m.599 → Nat → Assertion ?m.597
      in the application
        @Invariant.withEarlyReturn ?m.597 ?m.598 ?m.599 Nat ?m.601 fun xs cur_x cur_y prod => ⌜cur_x * cur_y + prod = x * y⌝ -/
      (onContinue := fun xs cur_x cur_y prod => ⌜cur_x * cur_y + prod = x * y⌝)
  all_goals grind

[pandaman]

The issue is that the invariant doesn't have information about how many times the loop has run, so it's not strong enough to conclude the postcondition after the loop is completed. In this case, we can track the current value of cur_x in the invariant:

Solution (without early termination)

import Std.Tactic.Do
import Lean

set_option mvcgen.warning false

open Std.Do

def peasantMul (x y : Nat) : Nat := Id.run do
  let mut curX := x
  let mut curY := y
  let mut prod := 0
  for _ in [0:x] do
    -- I don't know how to handle early return with Std.Do
    -- if curX = 0 then
    --   break
    if curX % 2 = 1 then
      prod := prod + curY
    curX := curX / 2
    curY := curY * 2
  return prod

#guard peasantMul 3 4 = 12
#guard peasantMul 6 7 = 42
#guard peasantMul 12 100 = 1200

example (x y : Nat) : peasantMul x y = x * y := by
  generalize h : peasantMul x y = s
  apply Id.of_wp_run_eq h

  mvcgen
  invariants
  -- Associate curX with the current loop index (represented as cursor) to get an invariant strong enough to derive postcondition
  . ⇓⟨cursor, ⟨curX, curY, prod⟩⟩ => ⌜curX = x / 2^cursor.prefix.length ∧ curX * curY + prod = x * y⌝
  case vc1.step.isTrue pref cur suff hcur state curX _ curY prod _ h inv =>
    -- Invariant preserves when curX % 2 = 1
    change curX = x / 2^pref.length ∧ curX * curY + prod = x * y at inv
    refine ⟨?_, ?_⟩
    . simp [inv, Nat.div_div_eq_div_mul]
      grind
    . have : curX = (curX / 2) * 2 + 1 := by grind
      grind
  case vc2.step.isFalse pref cur suff hxur state curX _ curY prod _ h inv =>
    -- Invariant preserves when curX % 2 ≠ 1
    change curX = x / 2^pref.length ∧ curX * curY + prod = x * y at inv
    refine ⟨?_, ?_⟩
    . simp [inv, Nat.div_div_eq_div_mul]
      grind
    . have : curX = (curX / 2) * 2 := by grind
      grind
  case vc3.a.pre =>
    -- Invariant holds at the beginning of the loop
    grind
  case vc4.a.post.success state h =>
    -- Invariant implies the postcondition after running the loop x times
    obtain ⟨curX, curY, prod⟩ := state
    simp at h
    have : curX = 0 := by
      have : x < 2^x := Nat.lt_two_pow_self
      have : x / 2^x = 0 := by simpa
      grind
    grind

[Sebastian Graf]

@pandaman is spot on. Invariant.withEarlyReturn does not apply to your use case because there is no early return in the loop. Also, you need to keep fun ret (cur_x, cur_y, prod) => ... tupled up in the parameter list. In the next release, there will be an alias abbrev cursor.pos := cursor.prefix.length.

[Asei Inoue]

Thank you. I understand early break is not early return!

[Sebastian Graf]

Indeed; break is handled by simply returning ForInStep.done; return x additionally adds a new optional phantom let mut variable for x. Details in the docstring for Invariant.withEarlyReturn.

[Asei Inoue]

@Sebastian Graf

I succeeded in proving the specification in the case where an early return is used!
Thank you.
However, I feel that this function should really use break instead of return.
If I want to use break, how should I modify the proof?

import Lean

set_option mvcgen.warning false

open Std.Do

def peasantMul (x y : Nat) : Nat := Id.run do
  let mut curX := x
  let mut curY := y
  let mut prod := 0
  for _ in [0:x] do
    if curX = 0 then
      return prod
    if curX % 2 = 1 then
      prod := prod + curY
    curX := curX / 2
    curY := curY * 2
  return prod

attribute [grind =] Nat.div_div_eq_div_mul

@[grind ->]
theorem div2_mul2_odd (x : Nat) (odd : x % 2 = 1) : x = (x / 2) * 2 + 1 := by
  grind

@[grind ->]
theorem div2_mul2_even (x : Nat) (even : x % 2 = 0) : x = (x / 2) * 2 := by
  grind

@[grind =, simp]
theorem div_pow_self_two_eq_zero (n : Nat) : n / 2 ^ n = 0 := by
  have : n < 2 ^ n := Nat.lt_two_pow_self
  simp_all

example (x y : Nat) : peasantMul x y = x * y := by
  generalize h : peasantMul x y = s
  apply Id.of_wp_run_eq h

  mvcgen invariants
  · Invariant.withEarlyReturn
    (onContinue := fun cursor ⟨curX, curY, prod⟩ =>
      ⌜curX = x / 2 ^ cursor.prefix.length ∧ curX * curY + prod = x * y⌝)
    (onReturn := fun ret ⟨curX, curY, prod⟩ => ⌜ret = prod ∧ prod = x * y⌝)
  with (simp_all <;> grind)

[Sebastian Graf]

Here you go. I think there's a nonconfluence problem between the simp and grind lemmas that I didn't try to resolve:

import Lean

set_option mvcgen.warning false

open Std.Do

def peasantMul (x y : Nat) : Nat := Id.run do
  let mut curX := x
  let mut curY := y
  let mut prod := 0
  for _ in [0:x] do
    if curX = 0 then
      break
    if curX % 2 = 1 then
      prod := prod + curY
    curX := curX / 2
    curY := curY * 2
  return prod

attribute [grind =] Nat.div_div_eq_div_mul

@[grind ->]
theorem div2_mul2_odd (x : Nat) (odd : x % 2 = 1) : x = (x / 2) * 2 + 1 := by
  grind

@[grind ->]
theorem div2_mul2_even (x : Nat) (even : x % 2 = 0) : x = (x / 2) * 2 := by
  grind

@[grind =, simp]
theorem div_pow_self_two_eq_zero (n : Nat) : n / 2 ^ n = 0 := by
  have : n < 2 ^ n := Nat.lt_two_pow_self
  simp_all

example (x y : Nat) : peasantMul x y = x * y := by
  generalize h : peasantMul x y = s
  apply Id.of_wp_run_eq h

  mvcgen invariants
  · ⇓⟨cursor, curX, curY, prod⟩ =>
      ⌜curX = x / 2 ^ cursor.pos ∧ curX * curY + prod = x * y⌝
  with (simp_all <;> grind)
  grind

[Asei Inoue]

@Sebastian Graf Thank you!

[Asei Inoue]

I am thinking about how loop invariants should be formulated when a for loop can terminate via break.
It seems that we have to consider an invariant that holds both when the loop finishes normally and when it exits by a break.
I wonder if, in cases where the same logic could be written with a return, it is often easier to prove things using return instead.

In the following code example, I couldn’t find an invariant that holds “both when the loop ends by break and when it ends normally,” and thus the proof doesn’t go through.

import Lean

open Std.Do

def sumWhilePositive (xs : List Int) : Int := Id.run do
  let mut out := 0
  for x in xs do
    if x ≤ 0 then
      break
    out := out + x
  return out

set_option mvcgen.warning false

@[grind =, simp]
theorem takeWhile_simplify_false {α : Type} (P : α → Bool) (pref suff : List α) (cur : α) (h : P cur = false) :
    List.takeWhile P (pref ++ cur :: suff) = List.takeWhile P pref := by
  fun_induction List.takeWhile with simp_all

theorem sumWhilePositive_spec (xs : List Int) :
    sumWhilePositive xs = (xs.takeWhile (· > 0)).sum := by
  generalize h : sumWhilePositive xs = s
  apply Id.of_wp_run_eq h

  mvcgen invariants
  · ⇓⟨cursor, out⟩ => ⌜cursor.prefix.all (· > 0) ∧ (cursor.prefix.takeWhile (· > 0)).sum = out⌝
  with grind

  case vc1 =>
    expose_names
    simp_all
   -- impossible to prove (invariant is incorrect)
    sorry

  case vc2 =>
    expose_names
    sorry

[Sebastian Graf]

In general, if your loop looks like

let mut out := ...
for x in xs do
   ... return out ...
return out

it is equivalent to

let mut out := ...
for x in xs do
   ... break ...
return out

and you should be able to prove all the same lemmas about it using mvcgen. What does your proof look like if you use return? It should be easy to adapt it to work with break. Certainly, cursor.prefix.all (· > 0) won't hold for the early return case either, so I don't see why you would include it in your invariant.

[Asei Inoue]

@Sebastian Graf

and you should be able to prove all the same lemmas about it using mvcgen. What does your proof look like if you use return?

Thank you. So, are you saying that we can use the same invariant for both the proof with return and the proof with break? However, as the following code shows, I thought that in general we need to modify the invariant.

Am I missing something?

import Lean

open Std.Do

def takeWhileReturn {α : Type} (p : α → Bool) (l : List α) : List α := Id.run do
  let mut result := []
  for x in l do
    if ! p x then
      return result
    result := result ++ [x]
  return result

set_option mvcgen.warning false

@[grind =, simp]
theorem takeWhile_simplify_false {α : Type} (P : α → Bool) (pref suff : List α) (cur : α) (h : P cur = false) :
    List.takeWhile P (pref ++ cur :: suff) = List.takeWhile P pref := by
  fun_induction List.takeWhile with simp_all

@[grind =, simp]
theorem takeWhile_all {α : Type} (P : α → Bool) (l : List α) (h : l.all P) :
    List.takeWhile P l = l := by
  fun_induction List.takeWhile with simp_all

theorem takeWhileReturn_spec {α : Type} (p : α → Bool) (l : List α) :
    takeWhileReturn p l = l.takeWhile p := by
  generalize h : takeWhileReturn p l = r
  apply Id.of_wp_run_eq h

  mvcgen invariants
  · Invariant.withEarlyReturn
    (onContinue := fun cursor result =>
      ⌜cursor.prefix.all p ∧ result = (cursor.prefix).takeWhile p⌝)
    (onReturn := fun ret result => ⌜ret = result ∧ result = l.takeWhile p⌝)
  with (simp at * <;> grind)

def takeWhileBreak {α : Type} (p : α → Bool) (l : List α) : List α := Id.run do
  let mut result := []
  for x in l do
    if ! p x then
      break
    result := result ++ [x]
  return result

theorem takeWhileBreak_spec {α : Type} (p : α → Bool) (l : List α) :
    takeWhileBreak p l = l.takeWhile p := by
  generalize h : takeWhileBreak p l = r
  apply Id.of_wp_run_eq h

  mvcgen invariants
  · ⇓⟨cursor, result⟩ => ⌜cursor.prefix.all p ∧ result = (cursor.prefix).takeWhile p⌝
  with (simp at * <;> grind)

  case vc1 =>
    expose_names
    simp_all
    -- impossible to show?
    sorry

[Sebastian Graf]

Here's how you can make it work:

import Lean

open Std.Do

def takeWhileReturn {α : Type} (p : α → Bool) (l : List α) : List α := Id.run do
  let mut result := []
  for x in l do
    if ! p x then
      return result
    result := result ++ [x]
  return result

set_option mvcgen.warning false

@[grind =, simp]
theorem takeWhile_simplify_false {α : Type} (P : α → Bool) (pref suff : List α) (cur : α) (h : P cur = false) :
    List.takeWhile P (pref ++ cur :: suff) = List.takeWhile P pref := by
  fun_induction List.takeWhile with simp_all

@[grind =, simp]
theorem takeWhile_all {α : Type} (P : α → Bool) (l : List α) (h : l.all P) :
    List.takeWhile P l = l := by
  fun_induction List.takeWhile with simp_all

@[grind =, simp]
theorem takeWhile_all' {α : Type} (P : α → Bool) (l : List α) (h : List.takeWhile P l = l) :
    l.all P := by
  fun_induction List.takeWhile with simp_all

theorem takeWhileReturn_spec {α : Type} (p : α → Bool) (l : List α) :
    takeWhileReturn p l = l.takeWhile p := by
  generalize h : takeWhileReturn p l = r
  apply Id.of_wp_run_eq h

  mvcgen invariants
  · Invariant.withEarlyReturn
    (onContinue := fun cursor result =>
      ⌜result = cursor.prefix ∧ result = cursor.prefix.takeWhile p⌝)
    (onReturn := fun ret result => ⌜ret = result ∧ result = l.takeWhile p⌝)
  with (simp at * <;> grind)


def takeWhileBreak {α : Type} (p : α → Bool) (l : List α) : List α := Id.run do
  let mut result := []
  for x in l do
    if ! p x then
      break
    result := result ++ [x]
  return result

theorem takeWhileBreak_spec {α : Type} (p : α → Bool) (l : List α) :
    takeWhileBreak p l = l.takeWhile p := by
  generalize h : takeWhileBreak p l = r
  apply Id.of_wp_run_eq h

  mvcgen invariants
  · ⇓⟨cursor, result⟩ => ⌜(cursor.suffix = [] ∨ result = cursor.prefix) ∧ result = cursor.prefix.takeWhile p⌝
  with (simp at * <;> grind)

Alas, I see that coming up with cursor.suffix = [] ∨ result = cursor.prefix is non-obvious. It is the exact reason why I defined Invariant.withEarlyReturn. Perhaps it would be a good idea to define Invariant.withBreak as well.

However, I'm working on a revamped do elaborator this Q and it is likely that the current elaboration of for loops will change anyway. I hope that I can make it a bit easier to handle early return and break in this kind of proof.

[Asei Inoue]

Thank you for your reply!

Perhaps it would be a good idea to define Invariant.withBreak as well.

I think so!

However, I'm working on a revamped do elaborator this Q and it is likely that the current elaboration of for loops will change anyway. I hope that I can make it a bit easier to handle early return and break in this kind of proof.

Will the improvements to the do elaborator make Lean’s already impressive do syntax even more powerful, and further enhance the already excellent Std.Do framework? I’m really looking forward to the release!

[Sebastian Graf]

The plan is to make do elaborators user-definable and extensible in the first place and perhaps adding support for return, continue and break-at-label. Then it might finally be possible to implement invariant syntax and thus enable intrinsic verification of monadic functions, augmenting Std.Do, yes. Thanks for the praise :)

[Asei Inoue]

@Sebastian Graf

I'm sorry if you've already answered this somewhere, but I have one question.
As far as I understand, Lean currently makes functions opaque when they use a while loop, which prevents us from proving properties about them.
Is there any plan to allow proving properties—using tools like mvcgen—for functions that contain while loops, provided that we can prove that the while loop definitely terminates?

[Sebastian Graf]

Non-opaque while needs a change to WF preprocessing. We have sketched out a plan for what to do, but we haven't added it to our roadmap yet. We'll announce when we have more concrete plans.