Why is `specialize` not an invalid tactic within a proof?

Question

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?

Answer 1

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.

Answer 2

[I'd rather post this as a comment but I am still too new to SO.]

I am reluctant to reply to the first part of your question not to spoil the exercise: Logical Foundations in particular is a journey and a progression as opposed to a compendium of recipes, and the intellectual component of that exercise, and not spoiling it, I think is crucial.

As for your doubts about the validity of such a transformation, maybe I see what you mean: if we are proving a theorem that is supposed to hold for all n, how is it that we can prove it for just some n? But now notice that it is not on n that we are specializing above, then if you also think how apply-ing on hypotheses as opposed to goals works...

Answer 3

Your premise is (forall m, m*n = 0). This means you may assume in your proof, that for every possible m, you have m*n=0. If you may assume this for any possible m, you may also assume it for a specific m like 1.

Note that if you would leave away the parenthesis:

Theorem specialize_example: forall n,
     forall m, m*n = 0
  -> n = 0.

the theorem would not hold any more - the obvious counter example is m=0. The statement with and without parenthesis is very different. With parenthesis you may choose m as you like - without parenthesis your theorem must hold for every possible value of m.