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
On Sat, Jun 6, 2020 at 12:54 AM 'Stanislas Polu' via Metamath <
[email protected]> wrote:
> 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
>
> --
> 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 [email protected].
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/metamath/CACZd_0yuiZLXKkC0XxRA039e7mf%2BYNQM_vB%2BD_diWANUzV4VPw%40mail.gmail.com
> <https://groups.google.com/d/msgid/metamath/CACZd_0yuiZLXKkC0XxRA039e7mf%2BYNQM_vB%2BD_diWANUzV4VPw%40mail.gmail.com?utm_medium=email&utm_source=footer>
> .
>
--
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CAFXXJSvEVn-Ccy4VyROmvD%2B3g0h5AdtH%3D9x%3DtqoqRf-vtPm5VA%40mail.gmail.com.
