synonyms

Tactic / Lemma Synonym Tables

Purpose

Hand-curated catalogue of equivalent or near-equivalent tactics and lemma names across Isabelle/HOL, Coq/Rocq, and Lean 4 (with or without mathlib). Used by the planned echidna suggest CLI verb (see ECHIDNA-NOTES-2026-04-27.md §4.1) and by the variant-tester loop (§4.3) to recover from "synonym blindness" failures — proofs that go through under one name but fail under another.

Scope

Per-prover tables

Fourteen files, one per backend with a curated table:

File	Prover
isabelle.toml	Isabelle/HOL (Isabelle2025+ — older versions noted per-entry)
coq.toml	Coq 8.18+ / Rocq
lean4.toml	Lean 4 + mathlib4
agda.toml	Agda
idris2.toml	Idris 2 (base / contrib)
isabelle_afp.toml	Isabelle/AFP naming
metamath.toml	Metamath set.mm
mizar.toml	Mizar MML
hol4.toml	HOL4
hol_light.toml	HOL Light
dafny.toml	Dafny
why3.toml	Why3 / WhyML
fstar.toml	F*
acl2.toml	ACL2

The first 20+ entries were seeded by Opus on 2026-04-27 from the two ECHIDNA-discovered drifts during the tropical-resource-typing fix session (induct→induction, add_le_add→add_mono) and from hand-knowledge of common idiom drift across mathlib / mathcomp / Isabelle’s Main.

Cross-prover dictionaries

Underscore-prefixed files are not per-prover tables. They are loaded as secondary indices by SynonymTable::with_*() / load_cross_prover_dicts (Rust) and SaturationSynonyms.load_*(dir) (Julia), and exist so that corpus items can be joined across systems by semantic_class.

File	Rows (2026-10-22)	Scope
_msc2020.toml	181	MSC2020 codes. 68Qxx (theory of computing) and 68Nxx (theory of software) are complete; 03B/03C/03D/03F cover logic, computability and proof theory; 68M/68P/68T/68V/68W cover systems, data, AI and proof assistants.
_wordnet_math.toml	81	WordNet 3.1 math senses. Undergraduate / textbook pure mathematics.
_conceptnet_seed.toml	53	ConceptNet 5.7 edges, pre-fetched for the offline S5 gate.
_disciplines.toml	41	The 42 TypeChecker disciplines (see docs/architecture/TYPE-DISCIPLINE-EMBEDDING.adoc).
_verification_systems.toml	665	Program verification: bitvectors and machine integers, memory layout and ABI, ownership and slicing, separation logic and region framing, contracts and proof obligations, termination measures, refinement, resource algebras (dioid / tropical / antichain), information flow and epistemic vocabulary, concurrency, and estate layering.

_verification_systems.toml exists because the WordNet and ConceptNet dictionaries are anchored in competition and undergraduate pure mathematics (the same shape as the ProofNet and MiniF2F corpora). The concepts this repository’s own verification surface is written in — zero_extend, wrapping_add, alignment_power_of_two, slice_disjoint, frame_rule, decreases_clause, noninterference_tini — had no semantic_class at all, so the cross-prover join silently dropped them.

Estate layer policy

The vocabulary follows the estate’s language policy, and rows are named to match it:

• ABIs are Idris2 (abi_contract, idris2_abi, foreign_descriptor).

• APIs and FFIs are Zig (zig_api, zig_ffi, calling_convention).

• BEAM native boundaries are SNIFs, never bare NIFs (snif, snif_contract, scheduler_thread, term_lifetime).

• The Rust layer is Rust/Creusot (creusot_annotation, rust_creusot_layer), Julia owns the numeric/ML layer, Chapel the parallel layer.

• Python is not part of the estate. No table, script or verification path may require a Python runtime.

Entry schema

Each entry has:

Field	Required?	Meaning
canonical	yes	Preferred / current name. Variant testers prefer this when emitting suggestions.
aliases	yes	Array of non-empty names; relation says how they relate to canonical. Order is not significant.
tactic_class	no	Coarse category (induction, arithmetic, simplifier, case, automation, reduction, lemma, combinator). Used to constrain variant search.
notes	no	Free-text rationale, version notes, or pitfalls.
since, until	no	Version range over which the alias applies. Empty means "always".

Lexicon v2 fields

Owner decisions 2026-10-19 (D2, D4) in docs/decisions/2026-10-19-lexicon-v2-and-identity-arbitration.adoc. All fields are optional; v1 rows load unchanged. The schema of record is the Nickel contract schema.ncl; scripts/lexicon-check.sh (or just lexicon-check) applies it to every table here and to the fixtures in tests/lexicon_fixtures/, and CI runs it in the rust-ci check job.

Field	Meaning
relation	How aliases relate to canonical: synonym (default, interchangeable), specialisation (each alias is a special case), generalisation, false_friend (looks alike, is not; never substituted) or phrase (canonical is a multi-token idiom). Only synonym and phrase rows feed the variant tester; the others are reported by SynonymTable::related. Phrase substitution runs one way for now: an alias at a tactic site can be replaced by the phrase spelling, but the extractors see single identifiers, so a canonical phrase in a proof is not yet replaced by an alias.
phrase	Token list of a multi-token idiom. Required with, and only allowed with, relation = "phrase".
false_friends	Look-alike names in other tables, each { name, table } where table is the other file’s stem.
evidence	The witness behind the row: { kind = "none" } (default), "curated", "probe" with tests and failures, or "kernel" with format, checked_by and a 64-hex BLAKE3 term_hash; counts are integers that fit a u32. Evidence attests the row’s relation, whatever it is, but lifts into the arbiter’s FidelityEvidence (SynonymEntry::fidelity_evidence) only for an identity claim: a synonym or phrase row that is not lossy. There probe lifts to DeclaredCorrespondence and kernel to KernelTranslation; none, curated (provenance, not fidelity evidence) and every other row lift to None. A lexicon row never raises a verdict above its own evidence.
fidelity, residue	exact or lossy; a lossy row must say what is lost in residue.
scope	{ library, version } the relation holds in.

Corpus-mined candidates (owner decision D4) are flag-only: they carry evidence = { kind = "none" } and never set semantic_class on their own.

Nickel checks shape and the cross-field rules; serde checks that checked_by names a ProverKind and format an ExchangeFormat when Rust loads a table (tests/lexicon_v2_test.rs).

Variant-tester contract

When echidna suggest encounters a tactic name in a failing proof, it:

1. Looks up the name in the appropriate prover’s table.

2. For each entry where the name is canonical or in aliases, it tries substituting every other alias (and the canonical) in turn.

3. Re-runs the proof with each substitution.

4. Reports successful substitutions, ranked by edit minimality.

The tester is deliberately mechanical — no search, no creativity, no ML. It only catches the cases where the proof author used a name the prover no longer accepts (or never accepted in this version).

Open questions tracked elsewhere

• Cross-prover synonym graph (Isabelle le_trans ↔ Coq Rle_trans ↔ Lean le_trans) is intentionally out of scope here — that’s echidna port, not echidna suggest.

• ML-driven synonym discovery from the corpus (mining training_data/) is in §4.4 of the notes, not this layer.

Maintenance

When a new drift is discovered, add the entry in the file for its prover, with a notes line that quotes the failure mode. Keep entries terse — long prose belongs in commit messages, not in the table.