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?
