Proving theorems about monads

Stream: std4

[Gareth Ma]

Hi! I have a very exciting project idea. Essentially, there are these cool monads in Lean 4 now. However, it seems that their current purpose is only to compute. But this is Lean! So I want to prove things about them.
I decided to start with this:

def ff (n : ℕ) : ℕ := Id.run do
  let mut r := 0
  for _ in [: n] do
    r ← r + 1
  return r

theorem ff' : ff n = n := by sorry

example : ff 5 = 5 := ff'

I have gotten some progress after working on it for couple hours (I am beginner), result can be found at https://github.com/grhkm21/lean4/blob/master/src/monad.lean There are two sorrys, and also a few theorems used are very ad-hoc and specific for the theorem I am proving.
I think this will be very interesting to have more people to help, and I am definitely excited to prove that imperative programs like the one at https://github.com/grhkm21/lean4/blob/master/src/q10.lean (computing sum of primes sublinearly) is correct.
CC @Kevin Buzzard @Bhavik Mehta who discussed on Discord

[Gareth Ma]

push (self advertisement)

[Gareth Ma]

More repo advertisement - I refactored the code of for loop monad a bit. Specifically I removed the fuel variable and modified the behaviour of a for loop such that a range of step := 0 will do nothing instead of doing something. Looking at help might be easier:

def fff (n : ℕ) : ℕ := Id.run do
  let mut r := 0
  -- Syntax: [start : stop : step]
  for _ in [0 : n : 0] do
    r ← r + 1
  return r

#eval fff 5

I changed it to return 0 instead of returning 5, which I think makes more sense? This will make proving statements easier, since now we don't have to deal with the fuel variable when unwrapping to the loop

[Gareth Ma]

https://github.com/grhkm21/lean4/blob/master/src/range.lean#L23

[Alex Keizer]

I'm not super familiar with the for monad, but I'm curious how you removed the fuel variable, and whether your version still has the same expressive power.
The name fuel implies it has to do with ensuring termination for otherwise potentially non-terminating loops, how does your version deal with that?

[Alex Keizer]

The idea is cool, though. It would be very interesting to prove theorems about imperative-style monadic code in Lean.

[Gareth Ma]

The original code called the loop with fuel = range.end:

    Std.Range.forIn range init f = Std.Range.forIn.loop f range.stop range.start range.stop range.step init

I believe my code has the same expressive power. I don't want to spam code lmao but here are the two codes (line highlighted, check it out):
My new code: https://github.com/grhkm21/lean4/blob/master/Lean4/Range.lean (There is a TLDR at the top)
Previous code: https://github.com/leanprover/lean4/blob/3f6c5f17db30c2a2dcaca1b9e9faec4e2cf04b95/src/Init/Data/Range.lean#L23-L33
If you look at the code, it's extremely similar, except that I removed fuel and added a well-foundedness proof.

[Kevin Buzzard]

You might want to move this to #lean4 if it's about a definition in core, or #std4 if it's a question about std4.

[Gareth Ma]

Screenshot-2023-02-27-at-14.27.33.png Hmm... It doesn't let me move it to other streams

[Gareth Ma]

But #std4 is probably more appropriate

[Kevin Buzzard]

Then maybe just start a new thread. I think the right people need to be reading your question. BTW there's no harm in spamming code. Zulip folds it up.

[Eric Wieser]

@Gareth Ma: I can move it to another stream, where would you like it to go?

[Gareth Ma]

#std4 is probably more appropriate, thank you! :)

[Notification Bot]

This topic was moved here from #mathlib4 > Proving theorems about monads by Eric Wieser.

[Mario Carneiro]

There are definitely a number of missing theorems for Range.forIn, but here's a proof anyway:

import Mathlib.Data.Nat.Basic

def ff (n : ℕ) : ℕ := Id.run do
  let mut r := 0
  for _ in [: n] do
    r ← r + 1
  return r

theorem ff' : ff n = n := by
  simp [ff, forIn, Std.Range.forIn]
  let rec foo : ∀ fuel a, fuel + a = n →
      Id.run (Std.Range.forIn.loop (fun x r => ForInStep.yield (r + 1)) fuel a n 1 a) = n
  | 0, a, h => by simp [Std.Range.forIn.loop]; rwa [Nat.zero_add] at h
  | fuel+1, a, h => by
    simp [Std.Range.forIn.loop]; split
    · next h' => exact le_antisymm (h ▸ Nat.le_add_left ..) h'
    · next h' => rw [← Nat.add_right_comm] at h; exact foo _ _ h
  exact foo _ _ rfl

[Gareth Ma]

Oh god I overcomplicated it so much hahaha, thank you so much! You are definitely correct that there are a lot of missing theorems for forIn :)

[Eric Wieser]

Doesn't it become pretty hard to even state these theorems as soon as you leave the Id monad?

[Mario Carneiro]

You can state how it computes on lawful monads

[Mario Carneiro]

i.e. forIn_succ type theorems

[Mario Carneiro]

that way we wouldn't have to unfold all the way to Range.forIn.loop which has a bunch of incomprehensible arguments, including fuel which you should never need to deal with directly

[Gareth Ma]

Hi Mario, do you know why the fuel variable is even there? It seems that a version without fuel also works (shown below). Some other people suggested it might be that the compiler/VM can optimise away loops with fuel, but I can't seem to reproduce the behaviour.

-- Syntax: `loop f i stop step b hs`
def loop (f : Nat → β → m (ForInStep β))
  (i stop step : Nat) (b : β) (hs : 0 < step) : m β := do
  if h : stop ≤ i then
    return b
  else
    have : stop - (i + step) < stop - i := by
      rw [← Nat.sub_sub]
      apply Nat.sub_lt _ hs
      exact Nat.zero_lt_sub_of_lt (lt_of_not_ge h)
    match (← f i b) with
    | ForInStep.done b  => pure b
    | ForInStep.yield b => loop f (i + step) stop step b hs
  termination_by _ => stop - i

-- Syntax: `forIn range init f`
protected def forIn (range : Range) (init : β)
  (f : Nat → β → m (ForInStep β)) : m β := do
  if hs : range.step = 0 then
    return init
  else
    loop f range.start range.stop range.step init (Nat.pos_iff_ne_zero.2 hs)

[Mario Carneiro]

my guess is either that termination_by was not ready when this code was written (I would not be surprised if it is one of the very early bits of lean 4) or that structural induction on natural numbers yields better defeqs for some scenario

[Gareth Ma]

I see, maybe I will (later) suggest changing it to without the fuel variables as above, that should simplify some proofs since it reduces one variable/case

[Mario Carneiro]

In this case I would not use that as a justification for changing the definition -- if you want to improve the proof experience you should prove some definitional lemmas instead

[Gareth Ma]

So prove that my definition is equivalent to the existing one? (Also, I did some digging, and this is the original commit from 2020: https://github.com/leanprover/lean4/commit/eacdb5ff83135077d57239d2e1ba2ceeb785a59c)

[Mario Carneiro]

no, to prove that the existing definition has an unfolding lemma resembling yours

[Gareth Ma]

Sorry, can you explain a bit more, I am a bit lost haha

[Gareth Ma]

Mario Carneiro said:

You can state how it computes on lawful monads

Can you explain this a bit more? For example, I want to prove the following:

theorem rangeDecompose (start mid stop : ℕ) (hs : start ≤ mid ∧ mid ≤ stop)
  {f : ℕ → β → Id (ForInStep β)} (hf : ∀ i r, (f i r).isYield) :
  Range.forIn (mkRange' start stop) init f =
    Range.forIn (mkRange' mid stop) (Id.run (Range.forIn (mkRange' start mid) init f)) f := by
  sorry

Which just states that two for loops combined equals to the larger for loop - the hf condition just states that there are no break or other things. How should I generalise this for monads apart from Id?

[Mario Carneiro]

Instead of using Id.run in the middle you should use >>= to connect the two parts

[Mario Carneiro]

theorem rangeDecompose [Monad m] [LawfulMonad m]
  (start mid stop : ℕ) (hs : start ≤ mid ∧ mid ≤ stop)
  {f : ℕ → β → m (ForInStep β)} :
  Range.forIn [start:stop] init f =
    Range.forIn [start:mid] init f >>= λ b => Range.forIn [mid:stop] b f := by
  sorry

[Mario Carneiro]

The hf assumption is a bit awkward / unrealistic for arbitrary monads, but you can do it using SatisfiesM:

def ForInStep.isYield : ForInStep α → Prop := (· matches .yield _)

theorem rangeDecompose [Monad m] [LawfulMonad m]
  (start mid stop : ℕ) (hs : start ≤ mid ∧ mid ≤ stop)
  {f : ℕ → β → m (ForInStep β)} (hf : ∀ i r, SatisfiesM ForInStep.isYield (f i r)) :
  Range.forIn [start:stop] init f =
    Range.forIn [start:mid] init f >>= λ b => Range.forIn [mid:stop] b f := by
  sorry

[Gareth Ma]

Oh wow, I just learned like 20 new syntax in this code or something. Thanks so much! :D