CBV with pretty syntax

Using Coq
1

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?

2

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.
   rewrite Nat.add_0_l.
  • use explicite change 
  change (2 * sum (S n)) with (sum (S n) + 1 * sum (S n)).

Hope this helps