Email Gateway (Aug 22 2022 at 17:14): Email Gateway (Aug 22 2022 at 17:14):From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
Dear Isabelle users,
I need a definition of a function taking a natural n as an input and
returning the nth prime number.
But: I don't want an inductive definition because in my proof I don't
want to imply the assumption that primes are infinitely many.
Is anyone aware of such a definition?
(my goal is to give a proof of the infinitude of primes: to this end I
want to show that assuming we have r many prime numbers, I can always
construct a prime that is bigger than p_r )
Many thanks in advance,
Best wishes,
Angeliki
Email Gateway (Aug 22 2022 at 17:14):From: David Cock <david.cock@inf.ethz.ch>
Angeliki,
Whether or not the definition is inductive doesn't affect the end
function. From the existence of any function "N -> Nth prime", one can
trivially show the infinitude of primes from the infinitude of the
natural numbers. Indeed, that such a function exists at all is a
proof that there are infinitely many primes.
The textbook proof of this should be possible in HOL, if you really
want to avoid defining a function. There's nothing special about
inductive functions in HOL, they just happen to be defined as the LFP of
a set of recurrent equations. They're logically exactly equivalent to
any other function.
David
Email Gateway (Aug 22 2022 at 17:14):From: Peter Lammich <lammich@in.tum.de>
Hi,
maybe you could use a choice operator (THE or SOME), and define
something along the lines of:
nth_prime n == THE p. is_prime p & card { p'. p'<p & is_prime p' } = n
(I have no idea whether this is suited for your purpose)
Alternatively, a non-constructive inductive definition might be
p_0 = 1
p_(n+1) = LEAST p. is_prime p & p>p_n
OR
p_(n+1) = SOME p. is_prime p & p>p_n (may skip primes, but probably
enough to show infinitude)
Both definitions come with no further assumptions, however, in order to
show any interesting facts about them, you'll have to come up with a
large enough prime.
You would then prove "is_prime (p_n)" by induction on n,
in each step coming up with the next-larger prime.
Email Gateway (Aug 22 2022 at 17:14):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
It is a bit hard to say what the best approach is for your use case.
Defining an ‘n-th prime’ function before you have even shown that there
are infinitely many of them (i.e. that there /is/ an n-th prime for
every n in the first place) is probably always going to involve
something like the "The" operator (unique choice) or its variant
"Least", and one can certainly do that, but it might get somewhat ugly.
Can you perhaps phrase your proof differently? E.g. something like ‘For
each prime number p, there exists a larger prime number p'’?
In the proof of this, you can, of course, refer to the prime numbers up
to p e.g. with {q. prime q ∧ q ≤ p}.
Manuel
Email Gateway (Aug 22 2022 at 17:14):From: Stefan Berghofer <berghofe@in.tum.de>
Hi Angeliki,
a (constructive) proof of the existence of infinitely many primes can e.g. be found in the paper
"A comparison of the mathematical proof languages Mizar and Isar"
http://www21.in.tum.de/~wenzelm/papers/romantic.pdf
by Markus Wenzel and Freek Wiedijk. You can find a formalization of this proof in section 7 of the
document
http://isabelle.in.tum.de/dist/library/HOL/HOL-Proofs-Extraction/document.pdf
together with an explanation of how a program can be extracted from this proof.
Greetings,
Stefan
Email Gateway (Aug 22 2022 at 17:14):From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
On 2018-05-08 15:50, David Cock wrote:
Whether or not the definition is inductive doesn't affect the end
function. From the existence of any function "N -> Nth prime", one
can trivially show the infinitude of primes from the infinitude of the
natural numbers. Indeed, that such a function exists at all is a
proof that there are infinitely many primes.
indeed- so let me rephrase my question: I should have written that I
want this enumerating function to be defined only on a segment of the
naturals, i.e. up to some r \in nat , having assumed that there exist r
many primes
The textbook proof of this should be possible in HOL, if you really
want to avoid defining a function. There's nothing special about
inductive functions in HOL, they just happen to be defined as the LFP
of a set of recurrent equations. They're logically exactly equivalent
to any other function.David
On 08/05/18 16:34, Dr A. Koutsoukou-Argyraki wrote:
Dear Isabelle users,
I need a definition of a function taking a natural n as an input and
returning the nth prime number.
But: I don't want an inductive definition because in my proof I don't
want to imply the assumption that primes are infinitely many.Is anyone aware of such a definition?
(my goal is to give a proof of the infinitude of primes: to this end I
want to show that assuming we have r many prime numbers, I can always
construct a prime that is bigger than p_r )Many thanks in advance,
Best wishes,
Angeliki
Email Gateway (Aug 22 2022 at 17:14):From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
Dear Stefan,
many thanks for the papers!
In fact my intention is to formalise a different proof, my motivation is
that the proof I am considering also provides some computational
content- in particular it gives that assuming we have r many primes,
we can always construct some prime P >p_r and we moreover have that
P \leq 4^r +1.
Thanks again for the papers though, it is very interesting material
indeed.
Best,
Angeliki
Email Gateway (Aug 22 2022 at 17:14):From: David Cock <david.cock@inf.ethz.ch>
How about "f(r) = THE n. |{m. m <=n /\ prime m }| = r". When you try
to prove anything about it you'll be forced to show that there exists a
unique n satisfying the predicate (and by implication all smaller r). I
think you won't have said anything about any larger r, but it's gonna
be hard to avoid sneaking the assumption in if you're already inside
HOL. In principle the proof automation might be able to infer it by
itself if you let it (but probably wouldn't). Sticking to manual
deduction should be safe.
David
Email Gateway (Aug 22 2022 at 17:15):From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
Hi Manuel! thank you for your answer.
Indeed I"ll use LEAST after all. I can't phrase the proof in the way
that you suggest, because the specific
proof that I want to formalise will require a combinatorial argument
requiring the number r of the first r primes-
which is the source of my difficulty.
Best, Angeliki
Last updated: Apr 26 2024 at 04:17 UTC