Skip to content

Commit 8fc8615

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat(data/synonyms): seed first 27 tactic-synonym entries
Hand-curated tactic and lemma synonyms across Isabelle/HOL, Coq/Rocq, and Lean 4 + mathlib4 — the data backbone for the planned `echidna suggest` CLI verb (ECHIDNA-NOTES-2026-04-27 §4.1) and the variant-tester loop (§4.3). Files: - README.adoc: schema, scope, variant-tester contract. - isabelle.toml: 9 entries — induction (incl. ECHIDNA-discovered `induct → induction` drift), arithmetic, transitivity, `add_le_add → add_mono` drift, image lemmas, definition unfolding, automation cascade, case analysis. - coq.toml: 9 entries — `omega → lia` (Coq ≥ 8.10), real arithmetic, reduction strength, application tactics, automation, induction vs destruct, finishing combinators, inversion vs dependent destruction, definition rewriting. - lean4.toml: 9 entries — simplifier cascade, omega/linarith/nlinarith, term construction (exact/apply/refine/exact?), reflexivity (rfl/ HEq.rfl), destructuring (obtain/rcases/cases/match), goal intro, decide-vs-native_decide trust note, mathlib3-port induction', rewrite tactics. Total 27 entries (target was ≥ 20). Both ECHIDNA-discovered drifts from the 2026-04-26 tropical-resource-typing fix session present. Each file passes Python tomllib validation. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent a41fd7d commit 8fc8615

4 files changed

Lines changed: 543 additions & 0 deletions

File tree

‎data/synonyms/README.adoc‎

Lines changed: 98 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,98 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
= Tactic / Lemma Synonym Tables
3+
:toc: macro
4+
5+
[discrete]
6+
== Purpose
7+
8+
Hand-curated catalogue of *equivalent or near-equivalent*
9+
tactics and lemma names across Isabelle/HOL, Coq/Rocq, and Lean 4 (with
10+
or without mathlib). Used by the planned `echidna suggest` CLI verb
11+
(see `ECHIDNA-NOTES-2026-04-27.md` §4.1) and by the variant-tester
12+
loop (§4.3) to recover from "synonym blindness" failures — proofs that
13+
go through under one name but fail under another.
14+
15+
== Scope
16+
17+
Three files, one per prover system:
18+
19+
[cols="1,2"]
20+
|===
21+
| File | Prover
22+
23+
| `isabelle.toml`
24+
| Isabelle/HOL (Isabelle2025+ — older versions noted per-entry)
25+
26+
| `coq.toml`
27+
| Coq 8.18+ / Rocq
28+
29+
| `lean4.toml`
30+
| Lean 4 + mathlib4
31+
|===
32+
33+
The **first 20+ entries** were seeded by Opus on 2026-04-27 from the two
34+
ECHIDNA-discovered drifts during the tropical-resource-typing fix
35+
session (`induct→induction`, `add_le_add→add_mono`) and from
36+
hand-knowledge of common idiom drift across mathlib / mathcomp /
37+
Isabelle's Main.
38+
39+
== Entry schema
40+
41+
Each `[[synonym]]` entry has:
42+
43+
[cols="1,1,2"]
44+
|===
45+
| Field | Required? | Meaning
46+
47+
| `canonical`
48+
| yes
49+
| Preferred / current name. Variant testers prefer this when emitting
50+
suggestions.
51+
52+
| `aliases`
53+
| yes
54+
| Array of equivalent names. Order is *not* significant.
55+
56+
| `tactic_class`
57+
| no
58+
| Coarse category (`induction`, `arithmetic`, `simplifier`, `case`,
59+
`automation`, `reduction`, `lemma`, `combinator`). Used to constrain
60+
variant search.
61+
62+
| `notes`
63+
| no
64+
| Free-text rationale, version notes, or pitfalls.
65+
66+
| `since`, `until`
67+
| no
68+
| Version range over which the alias applies. Empty means "always".
69+
|===
70+
71+
== Variant-tester contract
72+
73+
When `echidna suggest` encounters a tactic name in a failing proof, it:
74+
75+
1. Looks up the name in the appropriate prover's table.
76+
2. For each entry where the name is `canonical` or in `aliases`, it
77+
tries substituting *every other* alias (and the canonical) in turn.
78+
3. Re-runs the proof with each substitution.
79+
4. Reports successful substitutions, ranked by edit minimality.
80+
81+
The tester is deliberately *mechanical* — no search, no creativity, no
82+
ML. It only catches the cases where the proof author used a name the
83+
prover no longer accepts (or never accepted in this version).
84+
85+
== Open questions tracked elsewhere
86+
87+
- Cross-prover synonym graph (Isabelle `le_trans` ↔ Coq `Rle_trans` ↔
88+
Lean `le_trans`) is intentionally **out of scope** here — that's
89+
`echidna port`, not `echidna suggest`.
90+
- ML-driven synonym discovery from the corpus (mining
91+
`training_data/`) is in §4.4 of the notes, not this layer.
92+
93+
== Maintenance
94+
95+
When a new drift is discovered, add the entry in the file for its
96+
prover, with a `notes` line that quotes the failure mode. Keep
97+
entries terse — long prose belongs in commit messages, not in the
98+
table.

‎data/synonyms/coq.toml‎

Lines changed: 150 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,150 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
#
3+
# Coq / Rocq tactic and lemma synonyms.
4+
# Schema: see data/synonyms/README.adoc.
5+
# Seeded 2026-04-27 by Opus.
6+
7+
# ---------------------------------------------------------------------------
8+
# Linear integer arithmetic (omega → lia)
9+
# ---------------------------------------------------------------------------
10+
11+
[[synonym]]
12+
canonical = "lia"
13+
aliases = ["omega"]
14+
tactic_class = "arithmetic"
15+
since = "Coq 8.10"
16+
notes = """
17+
`omega` was deprecated in Coq 8.10 and removed in 8.13. All new
18+
proofs must use `lia` (Linear Integer Arithmetic). Variant tester
19+
should auto-substitute `omega → lia` on Coq ≥ 8.10.
20+
"""
21+
22+
[[synonym]]
23+
canonical = "lra"
24+
aliases = ["fourier", "psatz"]
25+
tactic_class = "arithmetic"
26+
notes = """
27+
Real linear arithmetic. `lra` is the modern Coq name; `fourier` was
28+
the original ssreflect tactic; `psatz` covers the polynomial case.
29+
"""
30+
31+
# ---------------------------------------------------------------------------
32+
# Reduction tactics
33+
# ---------------------------------------------------------------------------
34+
35+
[[synonym]]
36+
canonical = "cbn"
37+
aliases = ["simpl", "compute", "vm_compute", "lazy"]
38+
tactic_class = "reduction"
39+
notes = """
40+
Reduction strength + strategy:
41+
`simpl` — smart head-reduction with heuristics (legacy).
42+
`cbn` — call-by-name, more predictable than `simpl`.
43+
`compute` — full reduction via the bytecode VM.
44+
`vm_compute` — compute, but produces an opaque proof (faster).
45+
`lazy` — call-by-need.
46+
Prefer `cbn` for new proofs; switch to `compute`/`vm_compute` when
47+
`cbn` is too slow. WARN: `vm_compute` introduces a Reject-class
48+
trust hit if used in proof bodies that affect kernel checking — see
49+
`axiom_tracker.rs`.
50+
"""
51+
52+
# ---------------------------------------------------------------------------
53+
# Application tactics
54+
# ---------------------------------------------------------------------------
55+
56+
[[synonym]]
57+
canonical = "apply"
58+
aliases = ["eapply", "refine"]
59+
tactic_class = "lemma"
60+
notes = """
61+
`apply L` — unify L's conclusion with the goal, fail on residual evars.
62+
`eapply L` — same, but defer evars (becomes new goals).
63+
`refine L` — partial term construction; user supplies the term shape.
64+
When `apply` fails with "Cannot find an instance for variable X",
65+
try `eapply` first.
66+
"""
67+
68+
# ---------------------------------------------------------------------------
69+
# Automation
70+
# ---------------------------------------------------------------------------
71+
72+
[[synonym]]
73+
canonical = "auto"
74+
aliases = ["eauto", "intuition", "tauto", "firstorder"]
75+
tactic_class = "automation"
76+
notes = """
77+
Increasing search-completeness:
78+
`auto` — search a hint database, no backtracking on evars.
79+
`eauto` — like auto but with `eapply`.
80+
`intuition` — propositional intuitionistic search + auto leaves.
81+
`tauto` — pure propositional decision.
82+
`firstorder` — first-order logic search.
83+
Cascade in order; fail-fast tactics suit batch testing.
84+
"""
85+
86+
# ---------------------------------------------------------------------------
87+
# Induction
88+
# ---------------------------------------------------------------------------
89+
90+
[[synonym]]
91+
canonical = "induction"
92+
aliases = ["elim", "destruct"]
93+
tactic_class = "induction"
94+
notes = """
95+
`induction x` — apply x's induction principle, with IH.
96+
`elim x` — apply, no IH binding (legacy / SSReflect-adjacent).
97+
`destruct x` — case-split, NO induction (constructors only).
98+
Confusing `destruct` with `induction` is a common pitfall on
99+
recursively-defined datatypes.
100+
"""
101+
102+
# ---------------------------------------------------------------------------
103+
# Combinators
104+
# ---------------------------------------------------------------------------
105+
106+
[[synonym]]
107+
canonical = "now"
108+
aliases = ["solve", "easy"]
109+
tactic_class = "combinator"
110+
notes = """
111+
`now <tac>` — run tac; require it to fully close the goal.
112+
`solve [t1 | t2]` — try alternatives, require one to close.
113+
`easy` — automation tactic comparable to mathlib's `decide`.
114+
For "this should just work" finishing, `now (auto)` or `now lia` are
115+
the canonical idioms.
116+
"""
117+
118+
# ---------------------------------------------------------------------------
119+
# Inversion / inductive case-split
120+
# ---------------------------------------------------------------------------
121+
122+
[[synonym]]
123+
canonical = "inversion"
124+
aliases = ["inversion_clear", "dependent destruction"]
125+
tactic_class = "case"
126+
notes = """
127+
`inversion H` — split on an inductive hypothesis; keeps H.
128+
`inversion_clear H` — same, but clear H from the context.
129+
`dependent destruction` — for dependent inductive types where plain
130+
`inversion` produces a "Cannot solve a
131+
unification problem" error.
132+
Fall back to `dependent destruction` (from Coq.Program.Equality) when
133+
inversion fails on dependently-typed indices.
134+
"""
135+
136+
# ---------------------------------------------------------------------------
137+
# Definition rewriting
138+
# ---------------------------------------------------------------------------
139+
140+
[[synonym]]
141+
canonical = "unfold"
142+
aliases = ["change", "fold", "rewrite_strat"]
143+
tactic_class = "reduction"
144+
notes = """
145+
`unfold X` — replace X by its definition (recursively).
146+
`change (...) with X` — replace a specific term shape with X.
147+
`fold X` — inverse of unfold (re-fold definitions).
148+
When unfold loops or produces unwieldy goals, prefer `change` for
149+
surgical control.
150+
"""

‎data/synonyms/isabelle.toml‎

Lines changed: 138 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,138 @@
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
#
3+
# Isabelle/HOL tactic and lemma synonyms.
4+
# Schema: see data/synonyms/README.adoc.
5+
# Seeded 2026-04-27 by Opus.
6+
7+
# ---------------------------------------------------------------------------
8+
# Induction tactics
9+
# ---------------------------------------------------------------------------
10+
11+
[[synonym]]
12+
canonical = "induction"
13+
aliases = ["induct"]
14+
tactic_class = "induction"
15+
since = "Isabelle2016"
16+
notes = """
17+
Isabelle2025 / Main: `induction rule: finite_induct` *binds* the
18+
IH names (`insert.IH`); `induct rule:` does not. ECHIDNA-discovered
19+
2026-04-26 during the tropical-resource-typing fix. Use `induction`
20+
unconditionally for Isabelle ≥ 2025.
21+
"""
22+
23+
[[synonym]]
24+
canonical = "finite_induct"
25+
aliases = ["finite_subset_induct", "finite_ne_induct"]
26+
tactic_class = "induction"
27+
notes = """
28+
Different finite-set induction principles. `finite_induct` is the
29+
plain "empty + insert" rule; `finite_subset_induct` adds an enclosing
30+
finite set as a hypothesis; `finite_ne_induct` requires non-emptiness.
31+
Switch when the IH binds wrongly.
32+
"""
33+
34+
# ---------------------------------------------------------------------------
35+
# Linear arithmetic
36+
# ---------------------------------------------------------------------------
37+
38+
[[synonym]]
39+
canonical = "linarith"
40+
aliases = ["arith", "presburger"]
41+
tactic_class = "arithmetic"
42+
notes = """
43+
Linear arithmetic on integers and reals. `arith` is the historical
44+
name still working in many cases; `presburger` is the dedicated
45+
Presburger-arithmetic engine; `linarith` is mathlib-style and the
46+
preferred name in Isabelle Sledgehammer output.
47+
"""
48+
49+
# ---------------------------------------------------------------------------
50+
# Order-theoretic transitivity
51+
# ---------------------------------------------------------------------------
52+
53+
[[synonym]]
54+
canonical = "order_trans"
55+
aliases = ["le_trans", "dual_order.trans", "less_trans"]
56+
tactic_class = "lemma"
57+
notes = """
58+
Transitivity of ≤. `le_trans` is the legacy name (still in HOL/Main
59+
in many entries), `order_trans` is the locale-qualified version,
60+
`dual_order.trans` the dual-poset reflection. When sledgehammer
61+
suggests one and it doesn't apply, try the others verbatim.
62+
"""
63+
64+
# ---------------------------------------------------------------------------
65+
# Monotonicity drift (ECHIDNA-discovered)
66+
# ---------------------------------------------------------------------------
67+
68+
[[synonym]]
69+
canonical = "add_mono"
70+
aliases = ["add_le_add", "add_le_imp_le_diff", "add_left_mono"]
71+
tactic_class = "lemma"
72+
notes = """
73+
Monotonicity of `+` w.r.t. `≤`. `add_le_add` was the standard name
74+
in HOL/Library; `add_mono` is the type-class / locale form preferred
75+
in Isabelle ≥ 2024. ECHIDNA-discovered drift 2026-04-26.
76+
"""
77+
78+
# ---------------------------------------------------------------------------
79+
# Set / image
80+
# ---------------------------------------------------------------------------
81+
82+
[[synonym]]
83+
canonical = "image_iff"
84+
aliases = ["image_def", "image_eq", "image_image"]
85+
tactic_class = "lemma"
86+
notes = """
87+
Membership characterisation of `f \\` A`. `image_iff` is the
88+
quantifier form, `image_def` the unfolded definitional form.
89+
Use `image_iff` when rewriting under `∀` quantifiers; `image_def`
90+
for raw unfolding.
91+
"""
92+
93+
# ---------------------------------------------------------------------------
94+
# Definition unfolding
95+
# ---------------------------------------------------------------------------
96+
97+
[[synonym]]
98+
canonical = "simp add"
99+
aliases = ["unfold", "subst"]
100+
tactic_class = "reduction"
101+
notes = """
102+
Three ways to expand a definition: `unfold X` unfolds *and stops*;
103+
`simp add: X` unfolds and continues simplification; `subst X` rewrites
104+
once non-recursively. When unfolding causes loops, prefer `subst`
105+
or `simp only [X]` (the latter via `simp only`).
106+
"""
107+
108+
# ---------------------------------------------------------------------------
109+
# Automation cascade
110+
# ---------------------------------------------------------------------------
111+
112+
[[synonym]]
113+
canonical = "auto"
114+
aliases = ["force", "fastforce", "blast", "metis"]
115+
tactic_class = "automation"
116+
notes = """
117+
Increasing aggressiveness: `auto` (general), `force` (more
118+
backtracking), `fastforce` (reverse-priority), `blast` (proof search
119+
without simp), `metis` (resolution-based, accepts hint lemmas).
120+
Variant tester should try the cascade in order; failure of one
121+
doesn't predict failure of the next.
122+
"""
123+
124+
# ---------------------------------------------------------------------------
125+
# Case analysis
126+
# ---------------------------------------------------------------------------
127+
128+
[[synonym]]
129+
canonical = "cases"
130+
aliases = ["case_tac", "case"]
131+
tactic_class = "case"
132+
notes = """
133+
`cases` is the Isar method (`apply (cases x)`).
134+
`case_tac` is the apply-style legacy with `arg`-quoting.
135+
Bare `case` is the Isar block-level introduction (different syntax,
136+
same semantic role). When porting from Isabelle2009-era proofs,
137+
substitute `case_tac x` → `cases x`.
138+
"""

0 commit comments

Comments
 (0)