ComplCoq is a Coq plugin that automatizes algebraic reasoning using completion procedures of term rewriting systems.
ComplCoq currently supports Coq v8.5 and v8.6.
$ git clone https://github.com/mir-ikbch/compl_coq
$ cd compl_coq
for v8.6: $ git checkout 8.6
$ export COQLIB=path_to_your_coqlib
$ export COQBIN=path_to_your_coqbin
$ coq_makefile -f Make -o Makefile
$ make
$ make install
Require Setoid.
Require Import Completion.Completion.
Parameter A : Set.
Parameter op : A -> A -> A.
Axiom ax : forall a b c, op (op a b) (op b c) = b.
Complete ax : dbname sig op.
Print Rewrite HintDb dbname.
Goal forall a b c, op (op (op a b) (op b c)) (op (op b c) c) = op b c.
intros.
autorewrite with dbname.
reflexivity.
Qed.
Parameter G : Set.
Parameter e : G.
Parameter mul : G -> G -> G.
Parameter i : G -> G.
Axiom assoc : forall x y z, mul (mul x y) z = mul x (mul y z).
Axiom inv : forall x, mul (i x) x = e.
Axiom iden : forall x, mul e x = x.
Axiom comm : forall x y, mul x y = mul y x.
Complete inv iden, AC (mul, assoc, comm) : dbname sig e mul i.
Print Rewrite HintDb dbname2.
Ltac autorewrite_gr := autorewrite_ac dbname2 sig e mul i.
Goal forall a b c, mul (mul b c) (mul a (mul (i c) b)) = mul a (mul b b).
intros.
autorewrite_gr.
reflexivity.
Qed.