Zulip Chat Archive
Stream: new members
Topic: advice on pen+paper maths proof before I create a lean proof
rzeta0 (Jan 30 2025 at 20:31):
I'm doing the MoP Exercise on strong induction - there is only one exercise for that section, ex 6.4.3:
Show that for all natural numbers , there exist natural numbers and $$$x$, with odd, such that .
Start with a case split on the parity of , using the lemma
even_or_odd
.
I wanted to check that my pen-n-paper maths strategy was correct before I try writing the code:
- for odd we need to show there exists and odd such that . This only works if otherwise is always even. For the "there exists" we can choose $x=n$ since n is odd.
- There is no need for induction for the above first case ?!
- for even we need to show there exists and odd such that . We can't have because is odd and we need to be even, but is odd. We can use and choose , which works.
- Again there was no need for induction for this second case ?!
Clearly I must be deeply in error somewhere?
Edward van de Meent (Jan 30 2025 at 20:34):
if is even, choosing and results in you needing to prove that . This is false, so the choices are wrong.
Ruben Van de Velde (Jan 30 2025 at 20:35):
And if is even, you can't set to be anyway, because has to be odd
Ruben Van de Velde (Jan 30 2025 at 20:35):
Your argument for odd is correct, though
rzeta0 (Jan 30 2025 at 20:35):
silly me !
Ruben Van de Velde (Jan 30 2025 at 20:36):
Maybe it helps to take an example - say , what are the values for and ?
Edward van de Meent (Jan 30 2025 at 20:40):
(spoiler, these are unique)
Last updated: May 02 2025 at 03:31 UTC