Stream: Beginner Questions

Topic: trace decomposition

sadra (Jun 11 2026 at 09:37):

Hi
I'm trying to prove that a trace in my semantics decomposes into 3 different sections as follows

lemma split_call_trace:
  assumes ‹prg ⊢ (cstk, loc, conc) →* (f # cstk, loc', conc')›
  shows ‹∃ lcall ccall lent cent.
    prg ⊢ (cstk, loc, conc) →* (cstk, lcall, ccall) ∧
    prg ⊢ (cstk, lcall, ccall) → (f # cstk, lent, cent) ∧
    prg ⊢ (f # cstk, lent, cent) →* (f # cstk, loc', conc')›

I tried to use cases to get rid of the trivial case where no steps are taken e.g x ->* x. and induct in the step case. However, I can't go any further and get stuck when the single separated step isn't the the one where the call occurs (the one that appends the call stack). I think I need something similar to a loop invariant which weakens the goal. That is to say either lcall ccall lent cent exists in order to satisfy the goal or we are yet to encounter it. I'm unsure of how to set something like that up. Could you please guide me or point me to resources where a similar thing is done?

Last updated: Jun 24 2026 at 14:35 UTC