induction 10

Stream: new members

[Răzvan Flavius Panda]

Trying to solve: https://github.com/hrmacbeth/math2001/blob/e660f42b13ddcb6d12b52ba036d6bd071a0cfb9b/Math2001/06_Induction/01_Induction.lean#L108

I know there is a solution to it using by_contra but that tactic was not introduced yet so I would rather not use it.

I've got:

theorem Nat.even_of_pow_even {a n : ℕ} (ha : Even (a ^ n)) : Even a := by
  dsimp [Even] at *
  simple_induction n with k ih
  ·

Goal state:

a : ℕ
ha : ∃ k, a ^ 0 = 2 * k
⊢ ∃ k, a = 2 * k

I don't know how to make progress on this first subgoal since I can not rewrite a since ha lhs is a ^ 0.

[metakuntyyy]

Eh, here is what is said in the book: Also deduce that for all natural numbers and , if is even then is even. (This part is not an induction problem.) This doesn't render correctly, but it's listed here: https://hrmacbeth.github.io/math2001/06_Induction.html#recurrence-relations

[metakuntyyy]

It's pointless trying to prove it via induction. Here's what I came up with

import Mathlib

theorem Nat.even_of_pow_even {a n : ℕ} (ha : Even (a ^ n)) : Even a := by
  revert ha
  contrapose!
  intro ha
  have h1 := not_even_iff_odd.mp ha
  apply not_even_iff_odd.mpr

and then you can use the theorem that you've proved before

theorem Odd.pow {a : ℕ} (ha : Odd a) (n : ℕ) : Odd (a ^ n) := by
  sorry

I don't know what solution the author intended.

[Răzvan Flavius Panda]

It's just weird it would put an exercise under induction chapter and it's not solvable via induction.

[metakuntyyy]

What I even find weirder is that the author doesn't give you the tactics/tools necessary to tackle it. It's hard to give advice when you are only allowed to use a subset of facts/tactics.

[Răzvan Flavius Panda]

Yeah, tactics used to solve it were not introduced.

[metakuntyyy]

I'm certainly not an expert in trying to prove something with a reduced set of tools so I don't want to say that there isn't an idiomatic way to solve it with the reduced "power". In that case, use your "superpower" of the things you already know and prove it that way. At the end of the day you'll know more whether you "cheat" or not and if you want to formalise harder stuff you will have access to the full power/knowledge of mathlib anyways. I think that those tutorials are mostly used to get one acquainted to entry level stuff. It would be silly if one could use the more overpowered tactics for those facts that are solved by a one liner.

Pedagogically it is helpful to know how to solve a problem when the big guns fail. I, for example, loved the natural number game. It was a very good introduction to tactics, exact, have, ring,....

[Răzvan Flavius Panda]

I really like natural numbers game since it didn't use calc tactic. Just doing tactic after tactic was very fun.