feat: extend if h: hypothesis scope after early return

[TomasPuverle]

Extend the scope of hypothesis if h: ... inside of do notation after a return, continue and break. This PR makes it easier to work with "early return" code.

The tests demonstrate the usefulness but here's a MWE:

def testSingleArm (val : Nat) : Nat := Id.run do
  if h: val != 0 then
    return 0
  -- h not in scope here
  return 1

def safeDiv (a b : Nat) (_ : b ≠ 0): Nat := a / b

def earlyReturn (a b : Nat) : Option Nat := Id.run do
  if zh : b = 0 then
    return none

  return safeDiv a b zh

def earlyBreak : Nat := Id.run do
  let mut sum := 0
  for val in [2, 0, 1] do
    if zh : val = 0 then
      break

    sum := sum + safeDiv 10 val zh

  return sum

def earlyContinue : Nat := Id.run do
  let mut sum := 0
  for val in [1, 0, 2] do
    if zh : val = 0 then
      continue

    sum := sum + safeDiv 10 val zh

  return sum

Here's some discussion on Zulip and additional motivation in this RFC #5598

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 4771741fa288466a2de48569483205ad0690c8ef --onto 5e8718dff9d7906e1d4ca7020256dae7c05e49c2. (2024-10-02 04:48:29)

[nomeata]

I see the motivation, but I am worried about the implementation complexity. This would require an analysis that determines whether one branch or the other of an if is guaranteed to fall through. Is that worth it, when you can just be explicit and use else.

Ah, this is a PR, not an RFC. Sorry, I’m slighty sick… but it seems that your code misses for example cases where the then-branch is itself an if or a case with a return in each branch… so still concerned about the complexity of getting this to work reliably.

[Kha]

This module is currently frozen pending a rewrite, so I'll close this PR. Please open an RFC prior to a PR to get feedback on whether a contribution is desired.

[TomasPuverle]

Hi @Kha and @nomeata,

Thanks for your replies. I think someone mentioned that this part of the code is frozen after I posted the PR. I wasn't really expecting for the code to get merged but for the purpose of a RFC, I started a discussion on Zulip (linked above) and used this PR as a "proof of concept" for the idea (including the tests to demonstrate its benefits)

If this code is getting rewritten, please LMK if I can help at some point!

[TomasPuverle]

Is that worth it, when you can just be explicit and use else.

Ideally yes but as I pointed out in the motivation & Zulip discussion, this doesn't seem to be the case, unfortunately, even in the source of Lean itself. (It's also sort of related to my RFC about unless h: ...: #5598 )

[Kha]

I wasn't really expecting for the code to get merged but for the purpose of a RFC, I started a discussion on Zulip (linked above) and used this PR as a "proof of concept" for the idea (including the tests to demonstrate its benefits)

You can mark PRs as drafts to avoid any confusion on this point :)