Equivalence of fuel and nonfuel functions

Stream: new members

[Eric Paul]

I want to show that if the nonfuel version of my function terminates, it reaches the same result as the fueled version for some fuel. However, I've been struggling to prove this. Here is a MWE

opaque step : List a → Option (List a)

def evalFuel : Nat → List a → Option a
| 0, _ => none
| _+1, [x] => some x
| n+1, xs =>
  match step xs with
  | some xs' => evalFuel n xs'
  | none => none

def eval : List a → Option a
| [x] => some x
| xs =>
  match step xs with
  | some xs' => eval xs'
  | none => none
partial_fixpoint

example : eval xs = some x → ∃n, evalFuel n xs = some x := by sorry

I attempted to define a different version of eval that tracked how many steps it took and use that for the fuel, but I wasn't able to get that to work. Does anyone have suggestions or pointers to similar proofs?

[Robin Arnez]

Are you aware of partial_correctness?

opaque step : List a → Option (List a)

def evalFuel : Nat → List a → Option a
  | 0, _ => none
  | _+1, [x] => some x
  | n+1, xs =>
    match step xs with
    | some xs' => evalFuel n xs'
    | none => none

def eval : List a → Option a
  | [x] => some x
  | xs =>
    match step xs with
    | some xs' => eval xs'
    | none => none
partial_fixpoint

attribute [elab_as_elim] eval.partial_correctness

example : eval xs = some x → ∃ n, evalFuel n xs = some x := by
  intro h
  refine eval.partial_correctness _ ?_ xs x h
  · intro f ih a r h'
    split at h'
    · exists 1
    split at h'
    · rename_i h''
      specialize ih _ _ h'
      obtain ⟨n, hn⟩ := ih
      exists n + 1
      simp only [evalFuel, h'', hn]
    · simp at h'

[Eric Paul]

I'd totally missed that and that's just what I need! Thank you so much for the help!