0

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?

3 Answers 3

3

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.

2
  • Thanks! Now it's starting to make sense. That's valid coq syntax btw. :) Nov 5 at 21:15
  • ah, nice! good to know : )
    – Sebastian
    Nov 5 at 21:20
1

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.

2
  • Just to ensure I understand it correctly: The original theorem with the brackets it reads as "for any natural number n, if we can multiply it with a natural number m, and no matter what m is, the product is zero, then we know that n must be zero" and your modified theorem without brackets reads as "for any natural numbers n and m, if their product is zero it means that n is zero"? Nov 6 at 12:12
  • 1
    Yes, exactly. And this is the reason why you are free to choose m with specialize in the "with parenthesis" variant. If you try to prove the "without parenthesis" variant, you see that you introduce m, so you can't choose it, and the premise doesn't have a forall you can instantiate.
    – M Soegtrop
    Nov 6 at 13:48
0

[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...

2
  • Of course I want to be respectful to the material and not ask for any exercise solutions. I am a little confused because (as you can see in the link in the question) my question is about an example, not an exercise. Is there another place in software-foundations where my question is part of an exercise? Nov 7 at 6:54
  • 2
    I had it with myself really. :) I had no trouble replying to you in English, but I had written some code that makes explicit what you were asking and then I have dropped it as I thought I was spoiling a basic exercise: because LF in particular is a progression and like that at every step, you have to figure it out, a bit like a Project Euler... I don't think you asked an inappropriate question, nor my comment was motivated by it in particularly, it was more of a qualifier for what I was writing and, maybe, if a memento at all, only to those who are replying, myself to begin with... Cheers. Nov 7 at 11:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.