mcp/SKILL.md: add pitfalls and tactics from s2n-bignum GHASH proof work

[nebeid]

Motivation

These additions come from sessions of formal GHASH/POLYVAL proof work in s2n-bignum, where each pitfall was hit at least once and caused wasted tactic attempts + backtracking cycles.

The SKILL.md is loaded as LLM context at the start of every HOL Light MCP session, so these corrections directly change what the LLM tries on the first attempt rather than the third.

What changed

Fixes to existing content:

• ONCE_REWRITE_TAC description: "Rewrite only once" → "Rewrite one pass, all topmost matches (not just one match!)". The old description suggests one match; the actual behavior rewrites ALL topmost matching subterms in a single pass. For targeted single-occurrence rewriting, GEN_REWRITE_TAC with conversionals is needed.
• ARITH_TAC description: added "(goal only, ignores hypotheses)". Without this, the natural first attempt on a goal with needed facts in the hypotheses is ARITH_TAC, which fails silently. The fix is UNDISCH_TAC first.

New tactic entries:

• GEN_REWRITE_TAC (RAND_CONV) and GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) — essential for targeted rewriting when ONCE_REWRITE_TAC rewrites too many occurrences
• SUBGOAL_THEN with MP_TAC, SUBST1_TAC, STRIP_ASSUME_TAC — the doc only had ASSUME_TAC
• ABBREV_TAC / EXPAND_TAC — fundamental to s2n-bignum proofs, completely absent before

New pitfall entries:

• SUBST1_TAC silently succeeds even when the LHS doesn't appear in the goal, making FIRST_ASSUM(fun th -> SUBST1_TAC(SYM th)) unreliable. Use EXPAND_TAC instead.
• THEN vs THENL after SUBGOAL_THEN ... SUBST1_TAC — THEN applies the equality proof to ALL subgoals including the main goal after substitution.

Why these specific additions

Each one prevents a concrete failure mode:

• ARITH_TAC ignores hypotheses — Without this note, when seeing m + n < 2 EXP 64 with bounds in hypotheses, the first instinct is ARITH_TAC. It fails. Then ASM_ARITH_TAC. It hangs (30 assumptions with val terms). Then finally UNDISCH_TAC twice + ARITH_TAC. Three wasted round trips. With the note, go straight to UNDISCH_TAC.

• ONCE_REWRITE_TAC semantics — When commuting one word_xor in a goal with five of them, the old description leads to ONCE_REWRITE_TAC[WORD_XOR_SYM]. All five get commuted. The new GEN_REWRITE_TAC examples show the correct syntax.

• ABBREV_TAC / EXPAND_TAC — In ARM proofs, register values are named constantly. Without these, the broken FIRST_ASSUM(fun th -> SUBST1_TAC(SYM th)) pattern gets used. The SUBST1_TAC pitfall entry warns away from that.

• SUBGOAL_THEN variants — Defaulting to ASSUME_TAC for everything means doing SUBGOAL_THEN eq ASSUME_TAC THEN ASM_REWRITE_TAC[] in two steps instead of the direct SUBGOAL_THEN eq SUBST_ALL_TAC.

[jrh13]

Thank you, this is a clear improvement - I will merge :-)