Add proof reconstruction for Admitted/Section-local theorems

[spitters]

Summary

• Add _reconstruct_proof_state() function to interactive.py that reconstructs an open proof state when rocq_start in position mode returns proof_finished=True inside an Admitted proof
• Hook it into run_start: when position mode detects proof_finished=True, attempt reconstruction before returning
• Two-strategy approach:
  1. pet.start(thm_name) for top-level theorems
  2. Replay from file start through Section preamble for Section-local theorems
• Replay tactics from Proof. to cursor position (block first, sentence-by-sentence fallback)

Motivation

The most common use case for rocq_start in position mode is inspecting and proving Admitted theorems. Without this patch, get_state_at_pos returns proof_finished=True for any position inside an Admitted proof body, making interactive proving impossible. Users must manually remove Admitted from the file before they can work on the proof.

This is especially painful for Section-local theorems where pet.start(thm_name) also fails — the only way to get an open proof state is to replay the entire Section preamble.

Test plan

• 9 unit tests covering: basic reconstruction, cursor at proof start, strategy 1 → strategy 2 fallback, Section-local, no lemma found, file not found, Local Lemma keyword, both strategies fail, sentence-by-sentence fallback
• Additional tests for comment/terminator stripping, Program Definition, Global Instance keywords
• Integration tests for run_start position mode: trigger, skip, failure preservation
• All 627 tests pass (612 upstream + 15 new)

🤖 Generated with Claude Code

[gbdrt]

I cannot reproduce this issue locally.

With a simple file a.v:

Theorem foo n m: n + m = m + n.
Proof. Admitted.

rocq_start(file="a.v", line=1, character=0) returns:

{ "success":true,
  "state_id":3,
  "goals":"n, m : nat\n|-n + m = m + n",
  "file":"a.v",
  "theorem":"@pos(1,0)",
  "proof_finished":false}