# CBV with pretty syntax

**URL:** <https://discourse.rocq-prover.org/t/cbv-with-pretty-syntax/1937>\
**Category:** Using Rocq\
**Created:** [April 19, 2023, 10:49pm UTC](https://discourse.rocq-prover.org/t/cbv-with-pretty-syntax/1937 "2023-04-19T22:49:26Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![trj2059](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/trj2059/32/831_2.png) [@trj2059](https://discourse.rocq-prover.org/u/trj2059)\
**Post date:** [April 19, 2023, 10:49pm UTC](https://discourse.rocq-prover.org/t/cbv-with-pretty-syntax/1937/1 "2023-04-19T22:49:26Z")

</div>

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?

---

<div class="post-metadata">

**Author:** ![lthery](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lthery/32/14_2.png) [@lthery](https://discourse.rocq-prover.org/u/lthery)\
**Post date:** [April 20, 2023, 7:12am UTC](https://discourse.rocq-prover.org/t/cbv-with-pretty-syntax/1937/2 "2023-04-20T07:12:48Z")

</div>

There are several things you can try:

- use unfolding at some position.

```coq
unfold mult at 1 

```

- use rewriting

```coq
 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.
   rewrite Nat.add_0_l.

```

- use explicite `change`

```coq
  change (2 * sum (S n)) with (sum (S n) + 1 * sum (S n)).

```

Hope this helps