From 623a188efa4997ff64e8c3dd8cd8bb5f459d63aa Mon Sep 17 00:00:00 2001 From: Nevine Ebeid Date: Mon, 6 Apr 2026 14:54:50 +0000 Subject: [PATCH] mcp/SKILL.md: add pitfalls and tactics from s2n-bignum GHASH proof work - Fix ONCE_REWRITE_TAC description: 'one pass, all topmost matches' not 'only once' - Add GEN_REWRITE_TAC examples with RAND_CONV and LAND_CONV conversionals - Note that ARITH_TAC ignores hypotheses (goal only) - Add SUBGOAL_THEN variants: MP_TAC, SUBST1_TAC, STRIP_ASSUME_TAC - Add ABBREV_TAC / EXPAND_TAC pair - Add pitfalls: SUBST1_TAC silent success, THEN vs THENL after SUBST1_TAC, ONCE_REWRITE_TAC all-matches semantics, ARITH_TAC ignoring hypotheses Co-authored-by: Kiro (Claude Opus 4.6) --- mcp/SKILL.md | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/mcp/SKILL.md b/mcp/SKILL.md index 75ca4b62..af3482eb 100644 --- a/mcp/SKILL.md +++ b/mcp/SKILL.md @@ -47,15 +47,17 @@ Always read the goal state carefully before choosing a tactic. The structured JS |--------|----------| | `REWRITE_TAC[thm1; thm2]` | Rewrite goal using equations (left-to-right) | | `ASM_REWRITE_TAC[thms]` | Rewrite using hypotheses AND given theorems | -| `ONCE_REWRITE_TAC[thm]` | Rewrite only once (avoids looping) | +| `ONCE_REWRITE_TAC[thm]` | Rewrite one pass, all topmost matches (not just one match!) | | `GEN_REWRITE_TAC I [thm]` | Rewrite at top level only | +| `GEN_REWRITE_TAC (RAND_CONV) [thm]` | Rewrite only the operand of the top-level application | +| `GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [thm]` | Rewrite inside the LHS of a binary operator | | `SIMP_TAC[thms]` | Conditional rewriting (handles side conditions) | | `ASM_SIMP_TAC[thms]` | Conditional rewriting with hypotheses | ### Automation | Tactic | Solves | |--------|--------| -| `ARITH_TAC` | Linear arithmetic over naturals and integers | +| `ARITH_TAC` | Linear arithmetic over naturals and integers (goal only, ignores hypotheses) | | `REAL_ARITH_TAC` | Linear arithmetic over reals | | `MESON_TAC[thms]` | First-order logic with given lemmas | | `ASM_MESON_TAC[thms]` | First-order logic with hypotheses + lemmas | @@ -80,6 +82,11 @@ Always read the goal state carefully before choosing a tactic. The structured JS | `FIRST_ASSUM MATCH_MP_TAC` | Same but keeps the hypothesis | | `UNDISCH_TAC \`term\`` | Move a hypothesis back to the goal as antecedent | | `SUBGOAL_THEN \`P\` ASSUME_TAC` | Assert and prove an intermediate fact | +| `SUBGOAL_THEN \`P\` MP_TAC` | Assert, prove, and add as antecedent of goal | +| `SUBGOAL_THEN \`P\` SUBST1_TAC` | Assert, prove, and substitute the equality in goal | +| `SUBGOAL_THEN \`P\` STRIP_ASSUME_TAC` | Assert, prove, and split conjunctions into separate assumptions | +| `ABBREV_TAC \`x = expr\`` | Replace `expr` with `x` in goal, add `expr = x` as assumption | +| `EXPAND_TAC "x"` | Expand an abbreviation introduced by `ABBREV_TAC` | ### Combinators | Combinator | Meaning | @@ -142,8 +149,12 @@ apply_tactic "SUBGOAL_THEN `intermediate_fact` ASSUME_TAC" ## Pitfalls - **`REWRITE_TAC[GSYM thm]` can loop.** Use `ONCE_REWRITE_TAC[GSYM thm]` instead. +- **`ONCE_REWRITE_TAC` rewrites ALL topmost matches, not just one.** If the goal has `f a b` and `f c d`, and the theorem matches `f x y`, both get rewritten in one pass. For targeted single-occurrence rewriting, use `GEN_REWRITE_TAC` with conversionals like `RAND_CONV`, `LAND_CONV`. - **`FIRST_X_ASSUM` consumes the hypothesis.** Use `FIRST_ASSUM` when you need to reuse it. +- **`ARITH_TAC` ignores hypotheses.** Use `UNDISCH_TAC \`needed_fact\`` to bring assumptions into the goal first. `ASM_ARITH_TAC` uses hypotheses but can hang with many `val(...)` terms. - **`ASM_ARITH_TAC` hangs with many assumptions.** Discard irrelevant ones first with `REPEAT (FIRST_X_ASSUM (K ALL_TAC))` or targeted `UNDISCH_TAC` + `DISCH_TAC`. +- **`SUBST1_TAC` silently succeeds even when the LHS doesn't appear in the goal.** It just does nothing. This makes `FIRST_ASSUM(fun th -> SUBST1_TAC(SYM th))` unreliable — it picks the first assumption where the tactic "succeeds" (which is all of them). Use `EXPAND_TAC "name"` to expand abbreviations instead. +- **`THEN` vs `THENL` after `SUBGOAL_THEN ... SUBST1_TAC`.** `THEN` applies the proof to ALL subgoals (both the equality proof and the main goal). Use `THENL [equality_proof; ALL_TAC]` to target only the first subgoal. - **`WORD_RULE` hangs on `val(word(...))`.** Normalize via `VAL_WORD_EQ` first. - **Natural number subtraction is truncating.** `n - m = 0` when `m >= n`. Use `ARITH_TAC` for goals involving subtraction. - **`*` is right-associative for `num`.** Use explicit parentheses to avoid surprises.