Danila Fedorin 8cd053a242 Migrate Reaching.lean to projections via a generic Trace.steps ...

Finish the projection migration for reaching definitions by replacing the
accumulator-style runOfTrace*From definitions and their hand-rolled
re-association lemmas with a single analysis-agnostic projection:
Trace.steps / Traceₗ.steps, the chronological List of executed
(index, statement) pairs. Its four simp lemmas are one-line inductions,
with all re-association falling out of mathlib's List.append_assoc and
List.reverse_append.

Run is now an abbrev for List (State × BasicStmt) (latest-first, so
LastAssign keeps its first-match structure) and runOfTrace is just
steps.reverse.

Also hoist the generic reaches_final_post into Forward.lean, letting
analyze_correct' be stated directly about S.Post (prog.trace hrun).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

2026-07-02 09:01:09 -05:00

5.1 KiB

Raw Permalink Blame History

View Raw