1
$\begingroup$

In Coq, while trying to prove a lemma mult_n_Sm for mult_comm, I have this equation in a proof:

S n * S m = S n * m + S n      (* simpl. *)
S (m + n * S m) = m + n * m + S n

Lets look at right hand side of the equation. S n * m + S n was simplified into m + n*m + S n.( by definition of nat, S n = n + 1, hence (n+1)*m = m + n*m).

but if you use plus_comm (the commutative theorem) on the right hand side then perform simpl, it was simplified like following:

(* rewrite <- plus_comm *)
S n * S m = S n + S n * m      (* simpl. *) 
S (m + n * S m) = S (n + (m + n * m))

How was S n + S n * m simplified into S(n + (m + n * m))? By definition of plus, S n + S n * m = S ( n + S n * m ), but what was used to change S n * m into m + n * m without invoking mult_comm and mult_n_Sm itself?

It feels like the simpl. tactic used something that I tried to prove, forming an undesirable cyclic proof. How to inspect what atomic tactics simpl had performed under the hood?

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.