# CBV with pretty syntax

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?

There are several things you can try:

• use unfolding at some position.
``````unfold mult at 1
``````
• use rewriting
`````` Require Import PeanoNat.

Lemma sum_closed_expr_basic : forall n : nat, 2 * sum n = n * (n + 1).
Proof.
intros. induction n.
simpl.
reflexivity.
rewrite Nat.mul_succ_l.
rewrite Nat.mul_succ_l.
rewrite Nat.mul_0_l.
• use explicite `change`
``````  change (2 * sum (S n)) with (sum (S n) + 1 * sum (S n)).