In Coq, while trying to prove a lemma
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))
S n + S n * m simplified into
S(n + (m + n * m))? By definition of
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
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?