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?