Library UniMath.Tactics.Groups_Tactics

Require Import UniMath.Algebra.Monoids.
Require Import UniMath.Algebra.Groups.
Require Import UniMath.Tactics.Utilities.
Require Import UniMath.Tactics.Monoids_Tactics.

Local Open Scope multmonoid.

Ltac gr_preclean G := monoid_clean (grtomonoid G).

Ltac gr_preclean_in G t := monoid_clean_in (grtomonoid G) t.

Ltac gr_preclean_all G := monoid_clean_all (grtomonoid G).

Ltac gr_prezap G := monoid_zap (grtomonoid G).

Ltac gr_group_in G x s t :=
  assocop_group_in (grtomonoid G) (@op (grtomonoid G)) x s t.

Ltac gr_group G s t := assocop_group (grtomonoid G) (@op (grtomonoid G)) s t.

Ltac gr_clean G :=
  gr_preclean G; repeat rewrite (grlinvax G); repeat rewrite (grrinvax G);
  repeat (gr_preclean G;
          match goal with
            | |- context [?y × ?x × (@grinv G ?x)] ⇒
              rewrite (assocax G y x (@grinv G x)), (grrinvax G);
            gr_clean G
            | |- context [?y × (@grinv G ?x) × ?x] ⇒
              rewrite (assocax G y (@grinv G x) x), (grlinvax G);
            gr_clean G
          end);
  gr_preclean G.