ComplCoq

: Completion on Coq Hint Rewrite DBs :

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.

Demo

Install

$ 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

Example

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.