Proofs by enumerating cases

[Stanislas Polu]

Hi!

Rookie question: do we have examples of proofs that rely on enumerating all possible cases?

As an example how would one go about proving, as an example, that there is only one prime in 300..310 ?

Any example you could point me at?

Thanks a lot!

-stan

[Mario Carneiro]

Primality proofs are a pretty good example of this. For small primes, the most efficient proof method is trial division, either using odd numbers or prime numbers (if you have already prepared proofs of compositeness as in the sieve of Eratosthenes). The proof of prmlem2 is quite instructive along these lines. It prepares a sieve proof for primes less than 841, asserting that it suffices to check non-divisibility by all prime numbers up to 23 to prove that a number less than 841 is prime. To show this, we don't have to prove that the explicitly given list of primes are in fact prime, but we do have to prove that every odd number not in the list is composite (and thus need not be checked). The key lemma for this is prmlem0, which has a very particular form:

    prmlem0.1 $e |- ( ( -. 2 || M /\ x e. ( ZZ>= ` M ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) ) $.
    prmlem0.2 $e |- ( K e. Prime -> -. K || N ) $.
    prmlem0.3 $e |- ( K + 2 ) = M $.
    prmlem0 $p |- ( ( -. 2 || K /\ x e. ( ZZ>= ` K ) ) -> ( ( x e. ( Prime \ { 2 } ) /\ ( x ^ 2 ) <_ N ) -> -. x || N ) ) $=

Notice that the conclusion of prmlem0 has exactly the same form as the first hypothesis. The statement of the hypothesis is the "inductive step", which asserts that every prime number between M and sqrt(N) does not divide N. The induction proceeds from top to bottom, so the base case is when M is greater or equal to sqrt(N) and so the hypothesis is trivially proven, and then this lemma prmlem0 is applied repeatedly, with the ( K + 2 ) = M step performing re-normalization of the counter into a numeral (the goal is proven backwards, so we initialize it to 3 and then count up by twos until we reach sqrt(N)), and the second side goal is a proof either that the counter is composite, or it is one of the prime numbers about which we have a hypothesis.

So prmlem2 can be proven in a very algorithmic fashion, and although I never wrote a program to do it you can imagine a program spitting out proofs for theorems like prmlem2 that apply prmlem0 repeatedly. (The recursion ends at K = 3, and then we have some fixup stuff for the prime 2 and then we conclude that N is prime. This fixup part is in prmlem1a because it is also shared with the baby version prmlem1, which is similar to prmlem2 but only checks primes < 25 using the bootstrap primes 2 and 3.)

To summarize, and answer your question more generally, if we want to prove the theorem A. x e. ( 300 .. 310 ) ( x e. Prime -> x = 307 ), we would have a lemma like

$e |- ( x e. ( N .. 310 ) -> ( x e. Prime -> x = 307 ) )

$e |- ( K + 1 ) = N
$e |- ( K e. Prime -> K = 307 )

$p |- ( x e. ( K .. 310 ) -> ( x e. Prime -> x = 307 ) )

and then you apply this lemma 10 times, doing some fixup work at the beginning and end of the "loop" to get the desired form of the statement. (If course for a statement like this there are also algorithmic improvements you can apply to decrease proof work, like only checking odd numbers as in prmlem0, or even more elaborate things like checking numbers = 1 or 5 mod 6, or doing modular exponentiation tests for really big numbers. There are lots of options, depending on the scale of proof you are going for.)

Mario

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CACZd_0yuiZLXKkC0XxRA039e7mf%2BYNQM_vB%2BD_diWANUzV4VPw%40mail.gmail.com.

[Stanislas Polu]

Thank you very much Mario. That's extremely helpful, really like the
recursive nature of the goal->subgoal relationship provided by
prmlem0.

I'll play with the 300 .. 310 example to get a hang of it!

Thanks again for your help!

> To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSvEVn-Ccy4VyROmvD%2B3g0h5AdtH%3D9x%3DtqoqRf-vtPm5VA%40mail.gmail.com.