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! On Sat, Jun 6, 2020 at 10:47 AM Mario Carneiro <[email protected]> wrote: > > 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. > > -- > 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. -- 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_0x4NqNr7p-prr0GPwE5SmA87eHNnk591fwZVVZcYJqe0w%40mail.gmail.com.
