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?



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.