Unfold repeat until loop

Stream: lean4

[Gavin Zhao]

I have a repeat ... until loop that only runs for one iteration. Is it possible to sort of "unfold" the monadic action that represents the loop so that I can prove the result of its execution?

abbrev M := StateT Nat (Except String)

def repeat_example : M Nat := do
  let final_loop_state ← (do
    let mut loop_state := (false, 1)
    repeat
      let (_, n) := loop_state
      let x ← get
      loop_state ← pure (true, n + x)
    until loop_state.1
    pure loop_state.2
  )
  pure final_loop_state

theorem unfold_repeat : repeat_example.run 2 = .ok (3, 2) :=
  by
    sorry

I know this might not be idiomatic Lean, but this code is machine-generated so I can't really change it.

[Aaron Liu]

repeat is opaque

[Aaron Liu]

repeat .. until is also opaque

[Aaron Liu]

that means you're not allowed to unfold it

[Gavin Zhao]

Hmm so what would be alternatives that are not opaque but still represent loops? Maybe while?

[Aaron Liu]

while is also opaque

[Aaron Liu]

anything that lets you represent an infinite loop will usually be opaque

[Gavin Zhao]

repeat is opaque

I'm surprised the reference manual doesn't mention it.

[Gavin Zhao]

anything that lets you represent an infinite loop will usually be opaque

That makes sense. Thank you for the info! I'll have to think of other representations.

[Devon Tuma]

for loops unfold into List.forIn if you know the looping is bounded

[Devon Tuma]

Or at least loops over lists do

[Gavin Zhao]

Yeah, but unfortunately this one uses a boolean variable as the termination variable (i.e. repeat ... until) so that pattern doesn't hold.

[Gavin Zhao]

As you mentioned, for for loops over lists I did find that it can unfold it.