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.
```