# Can the Equations plugin generate a graph that does not reference the original function?

I’m experimenting with the equations plugin, and I’m surprised by the graphs that it generates. Here is an example:

``````From Equations Require Import Equations.

Inductive Arith :=
| Const (n: nat)
| Plus (a1 a2: Arith).

Equations eval (a: Arith) : nat :=
eval (Const n) := n;
eval (Plus a1 a2) := eval a1 + eval a2.
``````

The resulting `eval_graph` is this; notice how it makes references to `eval`:

``````Inductive eval_graph : Arith -> nat -> Set :=
eval_graph_equation_1 : forall n : nat, eval_graph (Const n) n
| eval_graph_equation_2 : forall a1 a2 : Arith,
eval_graph a1 (eval a1) ->
eval_graph a2 (eval a2) ->
eval_graph (Plus a1 a2) (eval a1 + eval a2)
``````

Is there a way to generate the following graph instead, which doesn’t reference `eval`?

``````Inductive eval_graph' : Arith -> nat -> Prop :=
| eval_graph'_equation1 n : eval_graph' (Const n) n
| eval_graph'_equation2 a1 n1 a2 n2 :
eval_graph' a1 n1 ->
eval_graph' a2 n2 ->
eval_graph' (Plus a1 a2) (n1 + n2).
``````

I think these two graphs are equivalent (see lemmas below), but I find the latter easier to work with.

``````Theorem eval_graph'_correct :
forall a : Arith, eval_graph' a (eval a).
Proof.
induction a.
all: rewrite ?eval_equation_1, ?eval_equation_2.
all: constructor.
all: assumption.
Qed.

Theorem eval_graph'_complete :
forall (a : Arith) n, eval_graph' a n -> n = eval a.
Proof.
induction 1.
all: rewrite ?eval_equation_1, ?eval_equation_2.
all: congruence.
Qed.
``````

It might be possible to generate the more general graph indeed. Equations generates it to derive the elimination principle of the function (eval) mainly, so the extra generality was not needed.

1 Like