In the software foundations book (archived) the specialize tactic was introduced as a way to simplify a hypothesis.
I don't understand,why it's a valid step within a proof.
The provided example adds to my confusion:
Theorem specialize_example: forall n,
(forall m, m*n = 0)
-> n = 0.
Proof.
intros n H.
specialize H with (m := 1).
simpl in H.
rewrite add_comm in H.
simpl in H.
apply H. Qed.
When I replace the Hypothesis (forall m, m*n = 0) -> n = 0. with 1*n = 0 -> n = 0., I see that we're now successfully proofing n=0 with that new hypothesis.
I don't understand why this is accepted as a proof for the original theorem forall n, (forall m, m*n = 0) -> n = 0.. Aren't we now continuing proofing a new theorem forall n, 1*n = 0 -> n = 0.?
How does proofing the new theorem generalize to be a valid proof for the original theorem?
Aren't we now continuing proofing a new theorem
forall n, 1*n = 0 -> n = 0.?
Indeed, that's what you are proving at first. But then you can go back to your original theorem and look at the starting point (forall m, m*n = 0) . If this statement is true, then it implies 1*n = 0 which by your new theorem implies n=0. This therefore proves the original theorem
(forall m, m*n = 0) -> 1*n = 0 -> n=0
(I don't know the language coq, so if the above line is syntactically not correct, it is simply meant in mathematical sense A=>B=>C).
Dropping the middle part between the two arrows is the original theorem.
Your new theorem is stronger than the original, because it needs less assumptions for the same conclusion.