Hi, I’m looking for a way to show the individual steps in the “simpl” tactic, but without having to use the

delta conversion so I can “trace” the steps using “pretty” syntax. So for example if I have

Lemma sum_closed_expr_basic : forall n : nat, 2 * sum n = n * (n + 1).

Proof.

intros. induction n.

- simpl.

reflexivity. - cbv delta [mult].

On the last step. You get the following as the current proof state.

(fix mul (n0 m : nat) {struct n0} : nat :=

match n0 with

| 0 => 0

| S p => m + mul p m

end) 2 (sum (S n)) =

(fix mul (n0 m : nat) {struct n0} : nat :=

match n0 with

| 0 => 0

| S p => m + mul p m

end) (S n) (S n + 1)

Is there a way to symbolically evaluate the mult definition without expanding the entire definition? So I would for the left hand side have this:

(S (S 0)) * sum (S n)

Which (ideally) we could symbolically evaluate expression step by step.

= (S (S 0)) * sum (S n)

= (sum S n) + ((S 0) * (sum S n))

= … ((sum S n) + (0 * (sum S n))

= … (0)

= (sum S n) + ((S 0) * (sum S n)) + 0

Is there anything in Coq that would allow a readable piece by piece evaluation of expressions?