Module lemma_calc 

Lemma-Calc: mechanically CALCULATE the forced auxiliary lemma from a stuck --explain residual goal (UntranslatedGoal). A pure function of the goal and the induction hypothesis — no enumeration, no search, no solver. Every step is deterministic; anything that is not forced is an HONEST DECLINE (CalcVerdict::Decline) with a named reason. The result feeds the same VM sample-check + candidate renderer as the raw residual (--explain in src/main/commands.rs); on decline the caller falls back to the raw candidate, so the calculator only ever ADDS a stronger lemma, never removes information.

Operations (in order), from the procedure trace in the G2b design:

1. subst — apply the induction hypothesis ONCE, left-to-right, with an anti-loop guard. An IH l = r whose l is an exact subtree of the claim rewrites every l to r and is consumed (the claim becomes IH-free).
2. lift (a) — anti-unify the claim against a surviving IH premise: lift each maximal common subterm to a fresh variable, allowing the claim side to carry ONE extra constructor (len ys vs Succ (len ys)). Every diff point must be a common subterm or such a constructor-wrap, else decline (a lemma that needs a term outside the goal and IH is not forced).
3. lift (b) — lift each maximal user-function-application subterm that occurs on BOTH sides of the claim to a fresh variable (typed by the function’s declared return type). Correspondence-preserving: a subterm on only one side is left literal (the calculator stops at the literal remainder; further generalization is The Method’s job).

Identity note (identity_guardrails): a pure ast::Expr transform. It keys on the claim’s SHAPE (constructor-wrap, function-application head), never on function or domain names; the constructor / function names it reads are DATA from the program, threaded through CalcEnv. Holds no FnId/TypeId table.

Structs

CalcEnv

Program facts the calculator reads as DATA: the constructor names (so a constructor-wrap is distinguished from a function application) and each function’s declared return type (to type a lifted variable). Shape-keyed machinery, name-blind: these are looked up, never matched against.

Enums

CalcVerdict

The calculator’s verdict: a forced lemma (a rewritten goal ready for the candidate builder), or an honest decline naming why the lemma is not forced.

Functions

calculate

Calculate the forced lemma for goal, or decline. Mutates a clone; the input is untouched (the caller keeps the raw residual for the decline fallback). reserved names are kept off the fresh-variable stream in addition to the goal’s own binders: the candidate builder resolves givens by name against the PARENT law, so a lifted variable that collides with a parent given would clone the wrong sample domain (name capture). The caller passes the parent law’s given names.