Source: ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Automation
1/-!
2# Reidemeister Schreier / Discrete / Presentations / Automation
4This module defines the small proof automation used in relator calculations:
5it closes elementary `RelatorEquivalent` goals and reduces normal-closure
6membership goals to the standard closure lemmas.
7-/
9namespace ReidemeisterSchreier.Discrete.Presentations
11/-- Try the standard reusable steps in a relator calculation:
13* use an existing hypothesis;
14* close reflexive `RelatorEquivalent` goals;
15* turn membership in the relator set or its normal closure into
16 `RelatorEquivalent _ _ 1`;
17* recursively split products, inverses, powers, contexts, and conjugates;
18* simplify the definition of `RelatorEquivalent`;
19* move to quotient equality and simplify.
21This is deliberately general. It is meant to clear routine endpoints in
22longer application proofs, not to encode downstream-specific rewrite rules.
23-/
24macro "relator_equivalent" : tactic =>
25 `(tactic|
26 repeat first
27 | assumption
28 | exact RelatorEquivalent.refl _ _
29 | apply RelatorEquivalent.of_mem; assumption
30 | apply RelatorEquivalent.of_mem_normalClosure; assumption
31 | apply RelatorEquivalent.mul
32 | apply RelatorEquivalent.mul_eq_one
33 | apply RelatorEquivalent.inv
34 | apply RelatorEquivalent.inv_eq_one
35 | apply RelatorEquivalent.pow
36 | apply RelatorEquivalent.pow_eq_one
37 | apply RelatorEquivalent.zpow
38 | apply RelatorEquivalent.zpow_eq_one
39 | apply RelatorEquivalent.context
40 | apply RelatorEquivalent.conj
41 | apply RelatorEquivalent.conj_eq_one
42 | simp only [RelatorEquivalent]
43 | rw [relatorEquivalent_iff_eq_in_presentedQuotient]; simp only)
45/-- A more aggressive variant of `relator_equivalent`.
47This tactic uses `simp_all`, so it strongly simplifies the local context as well
48as the target. -/
49macro "relator_equivalent!" : tactic =>
50 `(tactic|
51 first
52 | relator_equivalent
53 | simp_all only [RelatorEquivalent]
54 | rw [relatorEquivalent_iff_eq_in_presentedQuotient]; simp_all only)
56end ReidemeisterSchreier.Discrete.Presentations