proof(coq): add step_R_eq_or_touches_region region-invariance lemma

[hyperpolymath]

Summary

Adds the region-invariance lemma for the step relation — the missing piece of metatheoretic infrastructure that should eventually close ~10 of preservation's remaining 22 goals (the congruence cases where sibling-typing transfer is the only blocker).

What's in

Inductive touches_region : expr -> Prop

19 constructors, one per step-reducible compound form:

• TR_here — base case (ERegion r e)
• TR_StringConcat1, TR_StringConcat2 — congruence into the two arms
• TR_Let, TR_LetLin, TR_App1, TR_App2, TR_If, TR_Pair1, TR_Pair2, TR_Fst, TR_Snd, TR_Inl, TR_Inr, TR_Case, TR_StringLen, TR_Borrow, TR_Drop, TR_Copy — congruence into each Step1/Step variant

Lemma step_R_eq_or_touches_region (Qed)

Lemma step_R_eq_or_touches_region :
  forall mu R e mu' R' e',
    (mu, R, e) -->> (mu', R', e') ->
    R = R' \/ touches_region e.

For any step from (mu, R, e) to (mu', R', e'), either the region environment is preserved (the left disjunct), or the expression contains a region operation at a step-reducible position (the right disjunct).

Proof by induction on the step, with the same remember + revert structure used inside preservation itself. Three case classes:

1. Atom steps (R kept literally in the constructor's conclusion — S_StringNew, S_StringConcat, S_StringLen, S_Let_Val, S_LetLin_Val, S_App_Fun, S_If_True, S_If_False, S_Fst, S_Snd, S_Case_Inl, S_Case_Inr, S_Drop, S_Copy): close by left; reflexivity.

2. Region steps (S_Region_Enter, S_Region_Exit, S_Region_Step): close by right; apply TR_here.

3. Congruence steps (S_X_StepK): close by IH on the inner step + appropriate TR_X constructor.

What's not in

The tactic that would apply this lemma inside preservation to actually close goals. The intended pattern is documented as a comment-sketch:

pose proof (step_R_eq_or_touches_region _ _ _ _ _ _ Hstep) as Hdis.
destruct Hdis as [HeqR | HTR].
- subst.  (* unifies R = R' so sibling typing transfers *)
  edestruct (IHHstep _ _ _ _ _ _ eq_refl eq_refl _ _ _ HtypingOfInnerExpr)
    as [Gout Hout].
  eexists. econstructor; eauto.
- (* touches_region — needs region weakening, separately tracked *)
  ...

In isolation the pose proof step works (verified by inserting a diagnostic). In match goal with [H : step _ _ |- _] => ... form across all goals via all: try solve [...], the subsequent destruct/subst/IH chain hits ltac edge cases on these specific goal shapes. The lemma remains usable for future per-case manual proofs — that's the next-session deliverable.

Why land this separately

The lemma is reusable infrastructure regardless of whether the wholesale tactic ever lands. Future closures of the 22 remaining goals will reach for step_R_eq_or_touches_region per-case anyway. Banking the Qed-closed lemma now means the next session opens with one fewer prerequisite to write.

Verification

$ coqc -Q . Ephapax Semantics.v
(builds clean; Admitted preservation unchanged at 22 goals)

Refs

• standards#124 (proof-debt audit epic)
• ephapax#102 (910 → 29 via remember-cfg)
• ephapax#104 (PROOF STATUS docs correction)
• ephapax#106 (29 → 22 via universal-IH revert)

Test plan

• coqc -Q . Ephapax Semantics.v builds clean
• New Qed step_R_eq_or_touches_region at line 3293
• Preservation count unchanged at 22 (no regression)
• CI green

🤖 Generated with Claude Code