ReidemeisterSchreier/Discrete/Presentations/Automation.lean
1/-
2PUBLIC_PAGE_SNAPSHOT
3generated_at: 2026-05-27T09:47:29+09:00
4lean_source: lean4/ReidemeisterSchreier/Discrete/Presentations/Automation.lean
5translation_root: data/translation
6purpose: identifies the local data snapshot used to build pages/
7placement: after imports, never before imports
8-/
9/-!
10# Small proof automation for relator calculations
12This file provides lightweight tactics that sit on top of the normal-closure
13and `RelatorEquivalent` API. They intentionally do not contain
14downstream-specific rewriting rules.
16The basic `relator_equivalent` tactic handles routine goals from hypotheses,
17reflexivity, relator-set membership, normal-closure membership, quotient
18equality, products, inverses, powers, conjugates, and two-sided contexts.
20The `relator_equivalent!` variant additionally uses `simp_all`, so it may
21strongly simplify the local context. If either tactic fails, state the missing
22intermediate relator-equivalence lemma explicitly, make relator-family
23membership visible, or convert a quotient equality back through
25-/
27namespace ReidemeisterSchreier.Discrete.Presentations
29/-- Try the standard reusable steps in a relator calculation:
31* use an existing hypothesis;
32* close reflexive `RelatorEquivalent` goals;
33* turn membership in the relator set or its normal closure into
34 `RelatorEquivalent _ _ 1`;
35* recursively split products, inverses, powers, contexts, and conjugates;
36* simplify the definition of `RelatorEquivalent`;
37* move to quotient equality and simplify.
39This is deliberately general. It is meant to clear routine endpoints in
40longer application proofs, not to encode downstream-specific rewrite rules.
41-/
42macro "relator_equivalent" : tactic =>
43 `(tactic|
44 repeat first
45 | assumption
46 | exact RelatorEquivalent.refl _ _
47 | apply RelatorEquivalent.of_mem; assumption
48 | apply RelatorEquivalent.of_mem_normalClosure; assumption
49 | apply RelatorEquivalent.mul
50 | apply RelatorEquivalent.mul_eq_one
51 | apply RelatorEquivalent.inv
52 | apply RelatorEquivalent.inv_eq_one
53 | apply RelatorEquivalent.pow
54 | apply RelatorEquivalent.pow_eq_one
55 | apply RelatorEquivalent.zpow
56 | apply RelatorEquivalent.zpow_eq_one
57 | apply RelatorEquivalent.context
58 | apply RelatorEquivalent.conj
59 | apply RelatorEquivalent.conj_eq_one
60 | simp only [RelatorEquivalent]
61 | rw [relatorEquivalent_iff_eq_in_presentedQuotient]; simp only)
63/-- A more aggressive variant of `relator_equivalent`.
66as the target. -/
67macro "relator_equivalent!" : tactic =>
68 `(tactic|
69 first
70 | relator_equivalent
71 | simp_all only [RelatorEquivalent]
72 | rw [relatorEquivalent_iff_eq_in_presentedQuotient]; simp_all only)
74end ReidemeisterSchreier.Discrete.Presentations