The Mechanics Of Proof - induction

Stream: new members

[Michael Bucko]

Paragraph 6 - induction. How can I make those proofs better?

2 proofs

import Mathlib
import Lean

example (n : ℕ) : Even n ∨ Odd n := by
  induction n
  case zero => left ; use 0
  case succ k ih =>
    rcases ih with ⟨w, hw⟩ | ⟨w, hw⟩
    · right ; use w ; linarith
    · left ; use w + 1 ; linarith


example {a b d : ℤ} (h : a ≡ b [ZMOD d]) (n : ℕ) : a ^ n ≡ b ^ n [ZMOD d] := by
  induction n with
  | zero => rw [pow_zero a, pow_zero b]
  | succ k ih =>
    rw [pow_succ, pow_succ]
    have h1 : a^k * a ≡ a^k * b [ZMOD d] := Int.ModEq.mul_left (a^k) h
    have h2 : a^k * b ≡ b^k * b [ZMOD d] := Int.ModEq.mul_right b ih
    exact h1.trans h2

[Ilmārs Cīrulis]

These theorems can be found in the Mathlib. But I assume you already know that. :sweat_smile:
The second looks good, the first I would write differently but your way is good too.

(I'm beginner too, just in case.)

import Mathlib
example (n : ℕ) : Even n ∨ Odd n := Nat.even_or_odd n
example {a b d : ℤ} (h : a ≡ b [ZMOD d]) (n : ℕ) : a ^ n ≡ b ^ n [ZMOD d] := Int.ModEq.pow n h

[Michael Bucko]

Even if a proof from The Mechanics had already been done, it's okay. For me, it's more about learning by doing.

And since my proofs are still often quite ugly in Lean, many help me make them better.

[Michael Bucko]

Still, your point is a good one :thank_you: . Eventually, I'll try to reuse as much as possible from what had already been done.

[Ilmārs Cīrulis]

import Mathlib

example (n : ℕ) : Even n ∨ Odd n := by
  induction n with
  | zero => simp
  | succ n ih =>
    obtain ⟨w, hw⟩ | ⟨w, hw⟩ := ih <;> subst n
    . simp
    . have H: 2 * w + 1 + 1 = 2 * (w + 1) := by ring
      rw [H]
      simp

That's how I did it, but I used the fact that simp is quite powerful with all the Mathlib imported.

(Is it possible to merge lines have H: 2 * w + 1 + 1 = 2 * (w + 1) and rw [H] into one somehow?)

[Ilmārs Cīrulis]

(Smth like this - change 2 * w + 1 + 1 into 2 * ( w + 1) by ring. Something like this could be done in Coq, but I don't know about Lean...)

[Michael Bucko]

I need to experiment more with simp.

[Yakov Pechersky]

I think aiming to prove these lemmas in one go is counterproductive. It's often useful to prove other helpful side lemmas. I don't think Mechanics of Proof is against that

[Yakov Pechersky]

So in your Even n or Odd n, a more powerful statement is Even n => Odd (n + 1), then upgraded to an iff; and Even n => not Even (n + 1), then upgraded to an iff. Then linking Even n => not Odd n, then upgrading to an iff. Then using that with (em _).imp_right, which is shorthand for splitting on the cases using docs#Or.imp_right