Recurrence proofs from The Mechanics

Stream: new members

[Michael Bucko]

I wrote two new proofs from The Mechanics. The succ case in the first proof seems way too long. Does there exist a tactic that would solve such (simple) recurrent cases immediately?

Proofs

import Mathlib
import Lean

def c : ℕ → ℤ
  | 0 => 7
  | n + 1 => 3 * c n - 10

example (n : ℕ) : Odd (c n) := by
  induction n with
  | zero => simp [c] ; use 3 ; simp
  | succ n ih =>
    simp [c]
    cases ih with
    | intro k hk =>
      rw [hk]
      have : 3 * (2 * k + 1) - 10 = 2 * (3 * k - 4) + 1 := by ring
      rw [this]
      use (3 * k - 4)


def S : ℕ → ℚ
  | 0 => 1
  | n + 1 => S n + 1 / 2 ^ (n + 1)

example (n : ℕ) : S n = 2 - 1 / 2 ^ n := by
  induction n with
  | zero => simp [S] ; norm_num
  | succ n ih => simp [S, ih] ; simp [pow_succ] ; ring

[Ilmārs Cīrulis]

This is my try:

import Mathlib
import Lean

def c : ℕ → ℤ
  | 0 => 7
  | n + 1 => 3 * c n - 10

example (n : ℕ) : Odd (c n) := by
  induction n with
  | zero => exact Int.odd_iff.mpr rfl
  | succ n ih =>
    have H: Even (10: ℤ) := Int.even_iff.mpr rfl
    have H0: Odd (3: ℤ) := Int.odd_iff.mpr rfl
    have H1: Odd (3 * c n) := Odd.mul H0 ih
    exact Odd.sub_even H1 H

[Ilmārs Cīrulis]

I believe one has to write one's own tactic for this.
Maybe some kind of arithmetics in modulus 2?

Then instead of Odd (c n) one could prove that c n ≡ 1 [ZMOD 2].
7 would become 1, 3 -> 1, 10 -> 0... then 3 * c n - 10 ≡ c n [ZMOD 2] after simplication and by induction c n ≡ 1 [ZMOD 2].

But I haven't written any tactics yet, so I can't help much. :|

[Ilmārs Cīrulis]

I don't know how easily such result can be used to prove your example, but for ZMod 2 instead of ℤ there is such result.

import Mathlib
import Lean

def c': ℕ → ZMod 2
| 0 => 7
| n + 1 => 3 * c' n - 10

example (n: ℕ): c' n = 1 := by
  induction n with
  | zero => rfl
  | succ n ih =>
    rw [c']
    exact Mathlib.Tactic.Ring.sub_congr (congrArg (HMul.hMul 3) ih) rfl rfl

Last line suggested by exact?, maybe it can be replaced by simp after some preparation.

[Ilmārs Cīrulis]

Anyway, apologies for yapping.

[Mauricio Collares]

Lessness said:

  | succ n ih =>
    have H: Even (10: ℤ) := Int.even_iff.mpr rfl
    have H0: Odd (3: ℤ) := Int.odd_iff.mpr rfl
    have H1: Odd (3 * c n) := Odd.mul H0 ih
    exact Odd.sub_even H1 H

Probably less readable, but you can write it as

| succ n ih => exact (Int.odd_iff.mpr rfl) |>.mul ih |>.sub_even (Int.even_iff.mpr rfl)

or

| succ n ih => exact (by decide : Odd (3 : ℤ)) |>.mul ih |>.sub_even (by decide)