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

Using Coq
1

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

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