Reflexive tactic

Builds a reflexive tactic solving equalities in a monoid. We use Elpi to:

reify an expression into a syntax tree
query a Db of known monoids
call a few Ltac primitives in order to apply the correctness theorem

Note

This example depends on Rocq's Stdlib theories (and ssreflect), unlike the other cookbook examples.

This module contains the reflexive normalizer and its correctness proof (not the point of this demo -- the proofs are not the interesting part):

From elpi Require elpi.
[Loading ML file ppx_deriving.runtime (implicit dependency) ... done]
[Loading ML file re (implicit dependency) ... done]
[Loading ML file re.str (implicit dependency) ... done]
[Loading ML file elpi.util (implicit dependency) ... done]
[Loading ML file elpi.lexer_config (implicit dependency) ... done]
[Loading ML file menhirLib (implicit dependency) ... done]
[Loading ML file stdlib-shims (implicit dependency) ... done]
[Loading ML file elpi.parser (implicit dependency) ... done]
[Loading ML file camlp-streams (implicit dependency) ... done]
[Loading ML file easy-format (implicit dependency) ... done]
[Loading ML file biniou (implicit dependency) ... done]
[Loading ML file yojson (implicit dependency) ... done]
[Loading ML file atdgen-runtime (implicit dependency) ... done]
[Loading ML file elpi.trace.atd (implicit dependency) ... done]
[Loading ML file elpi.trace.runtime (implicit dependency) ... done]
[Loading ML file elpi.runtime (implicit dependency) ... done]
[Loading ML file elpi.compiler (implicit dependency) ... done]
[Loading ML file elpi (implicit dependency) ... done]
[Loading ML file rocq-elpi.elpi ... done]

From Stdlib Require Arith ZArith Psatz List ssreflect.
[Loading ML file rocq-runtime.plugins.ring ... done]
[Loading ML file rocq-runtime.plugins.zify ... done]
[Loading ML file rocq-runtime.plugins.micromega_core ... done]
[Loading ML file rocq-runtime.plugins.micromega ... done]
[Loading ML file rocq-runtime.plugins.btauto ... done]
[Loading ML file rocq-runtime.plugins.nsatz_core ... done]
[Loading ML file rocq-runtime.plugins.nsatz ... done]
[Loading ML file rocq-runtime.plugins.ssrmatching ... done]
[Loading ML file rocq-runtime.plugins.ssreflect ... done]

Import elpi.
Import Arith ZArith Psatz List ssreflect.


Module MonoidTheory.
Interactive Module MonoidTheory started

(* The syntax of terms *)
Inductive lang :=
| var (i : nat)        (* i-th variable in the context *)
| zero : lang          (* Neutral element *)
| add (x y : lang).    (* binary operation *)
lang is defined
lang_rect is defined
lang_ind is defined
lang_rec is defined
lang_sind is defined

(* Interpretation to T *)
Fixpoint interp T (e : T) (op : T -> T -> T) (gamma : list T) (t : lang) : T :=
  match t with
  | var v => nth v gamma e
  | zero => e
  | add x y => op (interp T e op gamma x) (interp T e op gamma y)
  end.
interp is defined
interp is recursively defined (guarded on 5th argument)

(* normalization of parentheses and units *)
Fixpoint normAx t1 acc :=
  match t1 with
  | add t1 t2 => normAx t1 (normAx t2 acc)
  | _ => add t1 acc
  end.
normAx is defined
normAx is recursively defined (guarded on 1st argument)

Fixpoint normA t :=
  match t with
  | add s1 s2 => normAx s1 (normA s2)
  | _ => t
  end.
normA is defined
normA is recursively defined (guarded on 1st argument)

Fixpoint norm1 t :=
 match t with
 | var _ => t
 | zero => t
 | add t1 t2 =>
    match norm1 t1 with
    | zero => norm1 t2
    | t1 =>
        match norm1 t2 with
        | zero => t1
        | t2 => add t1 t2
        end
    end
 end.
norm1 is defined
norm1 is recursively defined (guarded on 1st argument)

Definition norm t := normA (norm1 t).
norm is defined

Section assoc_reflection_proofs.
Variable T : Type.
T is declared

Variable unit : T.
unit is declared

Variable op : T -> T -> T.
op is declared

Hypothesis op_assoc : forall a b c, op a (op b c) = op (op a b) c.
op_assoc is declared

Hypothesis unit_l : forall a, op unit a = a.
unit_l is declared

Hypothesis unit_r : forall a, op a unit = a.
unit_r is declared

Lemma normAxA t1 t2 : normAx t1 (normA t2) = normA (add t1 t2).
1 goal
  
  T : Type
  unit : T
  op : T -> T -> T
  op_assoc : forall a b c : T, op a (op b c) = op (op a b) c
  unit_l : forall a : T, op unit a = a
  unit_r : forall a : T, op a unit = a
  t1, t2 : lang
  ============================
  normAx t1 (normA t2) = normA (add t1 t2)

Proof. by []. Qed.

No more goals.


Lemma normAx_add {t1 t2 s} : normAx t1 t2 = s -> exists s1 s2, s = add s1 s2.
1 goal
  
  T : Type
  unit : T
  op : T -> T -> T
  op_assoc : forall a b c : T, op a (op b c) = op (op a b) c
  unit_l : forall a : T, op unit a = a
  unit_r : forall a : T, op a unit = a
  t1, t2, s : lang
  ============================
  normAx t1 t2 = s -> exists s1 s2 : lang, s = add s1 s2

Proof.
elim: t1 t2 s => /= [i||w1 H1 w2 H2] t2 s <-; try by do 2 eexists; reflexivity.
1 goal
  
  T : Type
  unit : T
  op : T -> T -> T
  op_assoc : forall a b c : T, op a (op b c) = op (op a b) c
  unit_l : forall a : T, op unit a = a
  unit_r : forall a : T, op a unit = a
  w1 : lang
  H1 :
    forall t2 s : lang,
    normAx w1 t2 = s -> exists s1 s2 : lang, s = add s1 s2
  w2 : lang
  H2 :
    forall t2 s : lang,
    normAx w2 t2 = s -> exists s1 s2 : lang, s = add s1 s2
  t2, s : lang
  ============================
  exists s1 s2 : lang, normAx w1 (normAx w2 t2) = add s1 s2

by case E: (normAx _ _); case/H1: E => s1 [s2 ->]; do 2 eexists; reflexivity.
No more goals.

Qed.
Lemma norm1_zero {l t} : norm1 t = zero -> interp T unit op l t = unit.
1 goal
  
  T : Type
  unit : T
  op : T -> T -> T
  op_assoc : forall a b c : T, op a (op b c) = op (op a b) c
  unit_l : forall a : T, op unit a = a
  unit_r : forall a : T, op a unit = a
  l : list T
  t : lang
  ============================
  norm1 t = zero -> interp T unit op l t = unit

Proof.
by elim: t => [||s1 + s2] //=; case E1: (norm1 s1); case E2: (norm1 s2) => //= -> // ->.
No more goals.

Qed.
Lemma norm_zero {l t} : norm t = zero -> interp T unit op l t = unit.
1 goal
  
  T : Type
  unit : T
  op : T -> T -> T
  op_assoc : forall a b c : T, op a (op b c) = op (op a b) c
  unit_l : forall a : T, op unit a = a
  unit_r : forall a : T, op a unit = a
  l : list T
  t : lang
  ============================
  norm t = zero -> interp T unit op l t = unit

Proof.
rewrite /norm; case E: (norm1 t) => [||x y] //; first by rewrite (norm1_zero E).
1 goal
  
  T : Type
  unit : T
  op : T -> T -> T
  op_assoc : forall a b c : T, op a (op b c) = op (op a b) c
  unit_l : forall a : T, op unit a = a
  unit_r : forall a : T, op a unit = a
  l : list T
  t, x, y : lang
  E : norm1 t = add x y
  ============================
  normA (add x y) = zero -> interp T unit op l t = unit

by move/normAx_add=> [] ? [].
No more goals.

Qed.
Lemma norm1_var {l t j} : norm1 t = var j -> interp T unit op l t = nth j l unit.
1 goal
  
  T : Type
  unit : T
  op : T -> T -> T
  op_assoc : forall a b c : T, op a (op b c) = op (op a b) c
  unit_l : forall a : T, op unit a = a
  unit_r : forall a : T, op a unit = a
  l : list T
  t : lang
  j : nat
  ============================
  norm1 t = var j -> interp T unit op l t = nth j l unit

Proof.
elim: t => [i [->]||s1 + s2] //=; case E1: (norm1 s1); case E2: (norm1 s2) => //=.
2 goals
  
  T : Type
  unit : T
  op : T -> T -> T
  op_assoc : forall a b c : T, op a (op b c) = op (op a b) c
  unit_l : forall a : T, op unit a = a
  unit_r : forall a : T, op a unit = a
  l : list T
  j : nat
  s1, s2 : lang
  _i_ : nat
  E1 : norm1 s1 = var _i_
  E2 : norm1 s2 = zero
  ============================
  (var _i_ = var j -> interp T unit op l s1 = nth j l unit) ->
  (zero = var j -> interp T unit op l s2 = nth j l unit) ->
  var _i_ = var j ->
  op (interp T unit op l s1) (interp T unit op l s2) = nth j l unit

goal 2 is:
 (zero = var j -> interp T unit op l s1 = nth j l unit) ->
 (var _i_ = var j -> interp T unit op l s2 = nth j l unit) ->
 var _i_ = var j ->
 op (interp T unit op l s1) (interp T unit op l s2) = nth j l unit

  by rewrite (norm1_zero E2) unit_r => + _ H => ->.
1 goal
  
  T : Type
  unit : T
  op : T -> T -> T
  op_assoc : forall a b c : T, op a (op b c) = op (op a b) c
  unit_l : forall a : T, op unit a = a
  unit_r : forall a : T, op a unit = a
  l : list T
  j : nat
  s1, s2 : lang
  E1 : norm1 s1 = zero
  _i_ : nat
  E2 : norm1 s2 = var _i_
  ============================
  (zero = var j -> interp T unit op l s1 = nth j l unit) ->
  (var _i_ = var j -> interp T unit op l s2 = nth j l unit) ->
  var _i_ = var j ->
  op (interp T unit op l s1) (interp T unit op l s2) = nth j l unit

by rewrite (norm1_zero E1) unit_l => _ + H => ->.
No more goals.

Qed.
Lemma norm_var {l t j} : norm t = var j -> interp T unit op l t = nth j l unit.
1 goal
  
  T : Type
  unit : T
  op : T -> T -> T
  op_assoc : forall a b c : T, op a (op b c) = op (op a b) c
  unit_l : forall a : T, op unit a = a
  unit_r : forall a : T, op a unit = a
  l : list T
  t : lang
  j : nat
  ============================
  norm t = var j -> interp T unit op l t = nth j l unit

Proof.
rewrite /norm; case E: (norm1 t); rewrite /= ?(norm1_var E) //; first by move=> [->].
1 goal
  
  T : Type
  unit : T
  op : T -> T -> T
  op_assoc : forall a b c : T, op a (op b c) = op (op a b) c
  unit_l : forall a : T, op unit a = a
  unit_r : forall a : T, op a unit = a
  l : list T
  t : lang
  j : nat
  _x_, _y_ : lang
  E : norm1 t = add _x_ _y_
  ============================
  normAx _x_ (normA _y_) = var j -> interp T unit op l t = nth j l unit

by move/normAx_add=> [] ? [].
No more goals.

Qed.
Lemma norm1_add {l t s1 s2} : norm1 t = add s1 s2 -> interp T unit op l t = op (interp T unit op l s1) (interp T unit op l s2).
1 goal
  
  T : Type
  unit : T
  op : T -> T -> T
  op_assoc : forall a b c : T, op a (op b c) = op (op a b) c
  unit_l : forall a : T, op unit a = a
  unit_r : forall a : T, op a unit = a
  l : list T
  t, s1, s2 : lang
  ============================
  norm1 t = add s1 s2 ->
  interp T unit op l t = op (interp T unit op l s1) (interp T unit op l s2)

Proof.
elim: t s1 s2 => [||w1 + w2 + s1 s2] //=.
1 goal
  
  T : Type
  unit : T
  op : T -> T -> T
  op_assoc : forall a b c : T, op a (op b c) = op (op a b) c
  unit_l : forall a : T, op unit a = a
  unit_r : forall a : T, op a unit = a
  l : list T
  w1, w2, s1, s2 : lang
  ============================
  (forall s3 s4 : lang,
   norm1 w1 = add s3 s4 ->
   interp T unit op l w1 = op (interp T unit op l s3) (interp T unit op l s4)) ->
  (forall s3 s4 : lang,
   norm1 w2 = add s3 s4 ->
   interp T unit op l w2 = op (interp T unit op l s3) (interp T unit op l s4)) ->
  match norm1 w1 with
  | var i =>
      match norm1 w2 with
      | var i0 => add (var i) (var i0)
      | zero => var i
      | add x y => add (var i) (add x y)
      end
  | zero => norm1 w2
  | add x y =>
      match norm1 w2 with
      | var i => add (add x y) (var i)
      | zero => add x y
      | add x0 y0 => add (add x y) (add x0 y0)
      end
  end = add s1 s2 ->
  op (interp T unit op l w1) (interp T unit op l w2) =
  op (interp T unit op l s1) (interp T unit op l s2)

by case E1: (norm1 w1); case E2: (norm1 w2) => //= ++ [<- <-] /=;
  do 2! [ move=> /(_ _ _ (refl_equal _)) -> | move=> _];
  rewrite ?(norm1_zero E1) ?(norm1_zero E2) ?(norm1_var E1) ?(norm1_var E2).
No more goals.

Qed.
Lemma normAxP {l t1 t2} : interp T unit op l (normAx t1 t2) = op (interp T unit op l t1) (interp T unit op l t2).
1 goal
  
  T : Type
  unit : T
  op : T -> T -> T
  op_assoc : forall a b c : T, op a (op b c) = op (op a b) c
  unit_l : forall a : T, op unit a = a
  unit_r : forall a : T, op a unit = a
  l : list T
  t1, t2 : lang
  ============================
  interp T unit op l (normAx t1 t2) =
  op (interp T unit op l t1) (interp T unit op l t2)

Proof. by elim: t1 t2 => [||s1 Hs1 s2 Hs2] t2 //=; rewrite Hs1 Hs2 !op_assoc. Qed.

No more goals.


Lemma normAP {l} t : interp T unit op l (normA t) = interp T unit op l t.
1 goal
  
  T : Type
  unit : T
  op : T -> T -> T
  op_assoc : forall a b c : T, op a (op b c) = op (op a b) c
  unit_l : forall a : T, op unit a = a
  unit_r : forall a : T, op a unit = a
  l : list T
  t : lang
  ============================
  interp T unit op l (normA t) = interp T unit op l t

Proof. by elim: t => //= x Hx y Hy; rewrite normAxP Hy. Qed.

No more goals.


Lemma norm_add {l t s1 s2} : norm t = add s1 s2 -> interp T unit op l t = op (interp T unit op l s1) (interp T unit op l s2).
1 goal
  
  T : Type
  unit : T
  op : T -> T -> T
  op_assoc : forall a b c : T, op a (op b c) = op (op a b) c
  unit_l : forall a : T, op unit a = a
  unit_r : forall a : T, op a unit = a
  l : list T
  t, s1, s2 : lang
  ============================
  norm t = add s1 s2 ->
  interp T unit op l t = op (interp T unit op l s1) (interp T unit op l s2)

Proof.
rewrite /norm; case E: (norm1 t) => [||x y]; rewrite //= (norm1_add E).
1 goal
  
  T : Type
  unit : T
  op : T -> T -> T
  op_assoc : forall a b c : T, op a (op b c) = op (op a b) c
  unit_l : forall a : T, op unit a = a
  unit_r : forall a : T, op a unit = a
  l : list T
  t, s1, s2, x, y : lang
  E : norm1 t = add x y
  ============================
  normAx x (normA y) = add s1 s2 ->
  op (interp T unit op l x) (interp T unit op l y) =
  op (interp T unit op l s1) (interp T unit op l s2)

elim: x y s1 s2 {E} => //= [>[<- <- //=]|>[<- <-]|x + y + w s1 s2]; rewrite ?normAP //= ?unit_l //.
1 goal
  
  T : Type
  unit : T
  op : T -> T -> T
  op_assoc : forall a b c : T, op a (op b c) = op (op a b) c
  unit_l : forall a : T, op unit a = a
  unit_r : forall a : T, op a unit = a
  l : list T
  t, x, y, w, s1, s2 : lang
  ============================
  (forall y0 s3 s4 : lang,
   normAx x (normA y0) = add s3 s4 ->
   op (interp T unit op l x) (interp T unit op l y0) =
   op (interp T unit op l s3) (interp T unit op l s4)) ->
  (forall y0 s3 s4 : lang,
   normAx y (normA y0) = add s3 s4 ->
   op (interp T unit op l y) (interp T unit op l y0) =
   op (interp T unit op l s3) (interp T unit op l s4)) ->
  normAx x (normAx y (normA w)) = add s1 s2 ->
  op (op (interp T unit op l x) (interp T unit op l y))
    (interp T unit op l w) =
  op (interp T unit op l s1) (interp T unit op l s2)

by rewrite normAxA -!op_assoc => ++ E => /(_ _ _ _ E) ->.
No more goals.

Qed.
Lemma normP_ l t1 t2 : norm t1 = norm t2 -> interp T unit op l t1 = interp T unit op l t2.
1 goal
  
  T : Type
  unit : T
  op : T -> T -> T
  op_assoc : forall a b c : T, op a (op b c) = op (op a b) c
  unit_l : forall a : T, op unit a = a
  unit_r : forall a : T, op a unit = a
  l : list T
  t1, t2 : lang
  ============================
  norm t1 = norm t2 -> interp T unit op l t1 = interp T unit op l t2

Proof.
case E: (norm t2) => [?||??] => [/norm_var|/norm_zero|/norm_add] ->.
3 goals
  
  T : Type
  unit : T
  op : T -> T -> T
  op_assoc : forall a b c : T, op a (op b c) = op (op a b) c
  unit_l : forall a : T, op unit a = a
  unit_r : forall a : T, op a unit = a
  l : list T
  t1, t2 : lang
  _i_ : nat
  E : norm t2 = var _i_
  ============================
  nth _i_ l unit = interp T unit op l t2

goal 2 is:
 unit = interp T unit op l t2
goal 3 is:
 op (interp T unit op l _x_) (interp T unit op l _y_) = interp T unit op l t2

  by rewrite (norm_var E).
2 goals
  
  T : Type
  unit : T
  op : T -> T -> T
  op_assoc : forall a b c : T, op a (op b c) = op (op a b) c
  unit_l : forall a : T, op unit a = a
  unit_r : forall a : T, op a unit = a
  l : list T
  t1, t2 : lang
  E : norm t2 = zero
  ============================
  unit = interp T unit op l t2

goal 2 is:
 op (interp T unit op l _x_) (interp T unit op l _y_) = interp T unit op l t2

  by rewrite (norm_zero E).
1 goal
  
  T : Type
  unit : T
  op : T -> T -> T
  op_assoc : forall a b c : T, op a (op b c) = op (op a b) c
  unit_l : forall a : T, op unit a = a
  unit_r : forall a : T, op a unit = a
  l : list T
  t1, t2, _x_, _y_ : lang
  E : norm t2 = add _x_ _y_
  ============================
  op (interp T unit op l _x_) (interp T unit op l _y_) =
  interp T unit op l t2

by rewrite (norm_add E).
No more goals.

Qed.
End assoc_reflection_proofs.
End MonoidTheory.
Module MonoidTheory is defined

Now, let's build the tactic. This is the correctness theorem of our normalizer:

Import MonoidTheory.
Definition normP {T e op gamma t1 t2} p1 p2 p3 H := @normP_ T e op p1 p2 p3 gamma t1 t2 H.
normP is defined

About normP.
normP :
forall {T : Type} {e : T} {op : T -> T -> T} {gamma : list T} {t1 t2 : lang},
(forall a b c : T, op a (op b c) = op (op a b) c) ->
(forall a : T, op e a = a) ->
(forall a : T, op a e = a) ->
norm t1 = norm t2 -> interp T e op gamma t1 = interp T e op gamma t2

normP is not universe polymorphic
Arguments normP {T}%_type_scope {e} {op}%_function_scope 
  {gamma}%_list_scope {t1 t2} (p1 p2 p3)%_function_scope 
  H
normP is transparent
Expands to: Constant Top.normP
Declared in toplevel input, characters 4071-4076

Open Scope Z_scope.
Goal forall x y z t, (x + y) + (z + 0 + t) = x + (y + z) + t.
1 goal
  
  ============================
  forall x y z t : Z, x + y + (z + 0 + t) = x + (y + z) + t

Proof.
intros.
1 goal
  
  x, y, z, t : Z
  ============================
  x + y + (z + 0 + t) = x + (y + z) + t

change (interp Z Z.zero Z.add (x::y::z::t::nil)
             (add (add (var 0) (var 1)) (add (add (var 2) zero) (var 3)))
        =
        interp Z Z.zero Z.add (x::y::z::t::nil)
              (add (add (var 0) (add (var 1) (var 2))) (var 3))).
1 goal
  
  x, y, z, t : Z
  ============================
  interp Z Z.zero Z.add (x :: y :: z :: t :: nil)
    (add (add (var 0) (var 1)) (add (add (var 2) zero) (var 3))) =
  interp Z Z.zero Z.add (x :: y :: z :: t :: nil)
    (add (add (var 0) (add (var 1) (var 2))) (var 3))

apply: normP Z.add_assoc Z.add_0_l Z.add_0_r _.
1 goal
  
  x, y, z, t : Z
  ============================
  norm (add (add (var 0) (var 1)) (add (add (var 2) zero) (var 3))) =
  norm (add (add (var 0) (add (var 1) (var 2))) (var 3))

reflexivity.
No more goals.

Qed.

Now let's implement a tactic that does the change step (reification) and applies the correctness lemma for us:

Elpi Db monoid.db lp:{{
  pred is_monoid
    term % type
    ->
    term, % zero
    term, % op
    term, % assoc
    term, % unit_l
    term. % unit_r
}}.
Elpi Tactic monoid.
Elpi Accumulate Db monoid.db.
Elpi Accumulate lp:{{

% [mem L X N] asserts that X is at position N in L.
% The list is open-ended, that is it terminates with an Elpi unification
% variable, so that the list can be extended with new elements if needed.
% e.g. mem (3 :: L) 4 N ---> L = 4 :: L1, N = 1
% Note: we build a Rocq list, since we have to generate that anyway. We could
% use an Elpi list or any other data structure here, but then we would need
% to convert back anyway.
pred mem -> term, term, term.
mem {{ lp:X :: _     }} X {{ O      }} :- !.
mem {{ _    :: lp:XS }} X {{ S lp:N }} :- mem XS X N.

% Give that [mem] works with open ended lists we need a way to close it (assign
% nil to the tail) at the very end of reification.
pred close -> term.
close {{ nil }} :- !.
close {{ _ :: lp:XS }} :- close XS.

% [quote Zero Op T AstT L] recognizes Zero and Op in T and generates the
% corresponding AstT using the "context" L for variables standing for
% terms that are not Zero nor Op
pred quote term, term, term -> term, term.
quote Zero Op  {{ lp:Op lp:T1 lp:T2 }} {{ add lp:R1 lp:R2 }} L :- !,
  quote Zero Op T1 R1 L,
  quote Zero Op T2 R2 L.
quote Zero _   Zero {{ zero }} _ :- !.
quote _    _   T {{ var lp:R }} L :- mem L T R.

% This preliminary version of the tactic takes as arguments the monoid signature
% and changes the goal [A = B] into [interp L AstA = interp L AstB]
solve (goal _ _ {{ @eq lp:T lp:A lp:B }} _ [trm Zero, trm Op] as G) GS :-
  quote Zero Op A AstA L,
  quote Zero Op B AstB L,
  close L,
  % We are very low level here, we assign a term directly to the goal handler
  % while one could use ltac primitives (as we do later)
  Ty = {{   (interp lp:T lp:Zero lp:Op lp:L lp:AstA)
          = (interp lp:T lp:Zero lp:Op lp:L lp:AstB) }},
  % This implements the "change" tactic
  refine {{ (_ : lp:Ty) }} G GS.

:name "error"
solve _ _ :- coq.error "Not an equality / no signature provided".

}}.
Tactic Notation "monoid" constr(zero) constr(add) := elpi monoid (zero) (add).

Let's test the tactic:

Goal forall x y z t, (x + y) + (z + 0 + t) = x + (y + z) + t.
1 goal
  
  ============================
  forall x y z t : Z, x + y + (z + 0 + t) = x + (y + z) + t

Proof.
  intros.
1 goal
  
  x, y, z, t : Z
  ============================
  x + y + (z + 0 + t) = x + (y + z) + t

  monoid 0 Z.add.
1 goal
  
  x, y, z, t : Z
  ============================
  interp Z 0 Z.add (x :: y :: z :: t :: nil)
    (add (add (var 0) (var 1)) (add (add (var 2) zero) (var 3))) =
  interp Z 0 Z.add (x :: y :: z :: t :: nil)
    (add (add (var 0) (add (var 1) (var 2))) (var 3))

  (* OK, the goal was reified for us, we can use normP now *)
  apply: normP Z.add_assoc Z.add_0_l Z.add_0_r _.
1 goal
  
  x, y, z, t : Z
  ============================
  norm (add (add (var 0) (var 1)) (add (add (var 2) zero) (var 3))) =
  norm (add (add (var 0) (add (var 1) (var 2))) (var 3))

  reflexivity.
No more goals.

Qed.

Now let's register the monoid for Z in the Db:

Elpi Accumulate monoid.db lp:{{

  is_monoid {{ Z }}
            {{ 0 }} {{ Z.add }}
            {{ Z.add_assoc }} {{ Z.add_0_l }} {{ Z.add_0_r }}.

}}.

Now let's improve the tactic. This time we don't expect the signature but rather look it up in the Db:

Ltac my_compute := vm_compute.
my_compute is defined

Elpi Accumulate monoid lp:{{

:before "error"
solve (goal _ _ {{ @eq lp:T lp:A lp:B }} _ [] as G) GL :-
  is_monoid T Zero Op Assoc Ul Ur,
  quote Zero Op A AstA L,
  quote Zero Op B AstB L,
  close L,
  % This time we use higher level combinators, closer to the standard ltac1 ones
  refine {{ @normP lp:T lp:Zero lp:Op lp:L lp:AstA lp:AstB lp:Assoc lp:Ul lp:Ur _ }} G [SubG],
  coq.ltac.thenl [
    coq.ltac "my_compute", % https://github.com/coq/coq/issues/10769
    coq.ltac "reflexivity",
  ] SubG GL.

}}.
Tactic Notation "monoid" := elpi monoid.

Let's test it once more:

Goal forall x y z t, (x + y) + (z + 0 + t) = x + (y + z) + t.
1 goal
  
  ============================
  forall x y z t : Z, x + y + (z + 0 + t) = x + (y + z) + t

Proof.
  intros.
1 goal
  
  x, y, z, t : Z
  ============================
  x + y + (z + 0 + t) = x + (y + z) + t

  monoid.
No more goals.

  Show Proof.
(fun x y z t : Z =>
 normP Z.add_assoc Z.add_0_l Z.add_0_r
   (eq_refl
    <:
    norm (add (add (var 0) (var 1)) (add (add (var 2) zero) (var 3))) =
    norm (add (add (var 0) (add (var 1) (var 2))) (var 3))))

Qed.
Elpi Accumulate monoid.db lp:{{

  is_monoid {{ Z }}
            {{ 1 }} {{ Z.mul }}
            {{ Z.mul_assoc }} {{ Z.mul_1_l }} {{ Z.mul_1_r }}.

}}.
Goal forall x y z t, (x * y) * (1 * (z + t)) = x * y * (z + t).
1 goal
  
  ============================
  forall x y z t : Z, x * y * (1 * (z + t)) = x * y * (z + t)

Proof.
  intros.
1 goal
  
  x, y, z, t : Z
  ============================
  x * y * (1 * (z + t)) = x * y * (z + t)

  monoid.
No more goals.

Qed.