induction over the quotient

Stream: new members

[Alex Brodbelt]

I am trying to solve the following problem by induction where the base cases are all possible remainders under division by 3, So I prove P(0), P(1) and P(2) hold and then want to show that if it holds for
P(3k), P(3k+1), P(3k+2) then it holds P(3(k+1)), P(3(k+1)+1), P(3(k+1)+2).

My idea so far is to rewrite n = 3k + r where k = n / 3 and r = n % 3 and induct on k. But I get stuck as r still depends on n

I am not sure if I have run into a conceptual error or if it is possible to prove this induction principle is equivalent to the standard induction principle. I looked around mathlib to see if I could see examples of how specializations of the standard induction principle where done but I'm not sure how to start or if I understand too well what is going on if I am honest.

import Mathlib.Tactic

structure IsGood (f : ℕ → ℕ) : Prop where
  /-- Satisfies the functional relation-/
  rel: ∀ m n : ℕ, f (m + n) = f m + f n ∨ f (m + n) = f m + f n + 1
  f₂ : f 2 = 0
  hf₃ : f 3 > 0
  f_9999 : f 9999 = 3333

namespace IsGood

variable {f : ℕ → ℕ} (hf : IsGood f)
include hf

lemma f₀ : f 0 = 0 := by
  have  h : f 2 = f 2 + f 0 ∨ f 2 = f 2 + f 0 + 1 := by nth_rewrite 1 3 [← add_zero 2]; apply hf.rel 2 0
  rcases h with ( h₁ | h₂ )
  · rw [hf.f₂, zero_add] at h₁
    exact h₁.symm
  · rw [hf.f₂, zero_add] at h₂
    by_contra hf
    rw [← ne_eq] at hf
    have f0_pos : 0 < f 0 := by rw [lt_iff_le_and_ne]; exact ⟨zero_le (f 0), hf.symm⟩
    have : 0 < f 0 + 1 := by apply add_pos f0_pos (by norm_num)
    rw [← h₂] at this
    exact lt_irrefl 0 this

lemma f₁ : f 1 = 0 := by
  have h : f 2 = 2 * f 1 ∨ f 2 = 2 * f 1 + 1 := by rw [two_mul]; apply hf.rel 1 1
  rw [hf.f₂] at h
  by_contra hf
  rw [← ne_eq] at hf
  have f1_pos : 0 < f 1 := by rw [lt_iff_le_and_ne]; exact ⟨zero_le (f 1), hf.symm⟩
  rcases h with ( h₁ | h₂ )
  · have : 2 * f 1 > 0 := by apply mul_pos (by norm_num) f1_pos
    rw [← h₁] at this
    exact lt_irrefl 0 this
  · have : 2 * f 1 + 1 > 0 := by apply add_pos (mul_pos (by norm_num) f1_pos) (by norm_num)
    rw [← h₂] at this
    exact lt_irrefl 0 this

lemma f₃ : f 3 = 1 := by
    have h : f 3 = f 2 + f 1 ∨ f 3  = f 2 + f 1 + 1 := by apply hf.rel 2 1
    rw [hf.f₁, hf.f₂, add_zero, zero_add] at h
    have not_left : ¬ f 3 = 0 := by apply ne_of_gt hf.hf₃
    rw [or_iff_right (not_left)] at h
    exact h



theorem f_equals_division_by_three (n : ℕ): f n = n / 3:= by
  letI k := n / 3
  letI r := n % 3

  have hn : n = 3 * k + r := symm (Nat.div_add_mod n 3)
  have hr : r < 3 := Nat.mod_lt n (Nat.succ_pos 2)

  rw [hn, Nat.mul_add_div (by norm_num)]

  induction k
  case zero =>
    rw [mul_zero, zero_add, zero_add]
    interval_cases r
    · simp; exact hf.f₀
    · simp; exact hf.f₁
    · simp; exact hf.f₂
  case succ k' ih =>
    rw [mul_add, mul_one, add_assoc, add_comm 3 r, ← add_assoc]
    -- I would hope to be able to use ih to generate these three hypotheses
    have h₁ :  (3 * k' + 0) = k' + 0 / 3 := by sorry
    have h₂ :  (3 * k' + 1) = k' + 1 / 3 := by sorry
    have h₃ :  (3 * k' + 2) = k' + 2 / 3 := by sorry
    have h : f (3 * k' + r + 3) = f ( 3 * k' + r) + f 3 ∨ f (3 * k' + r + 3) = f (3 * k' + r) + f 3 + 1 := by apply hf.rel (3 * k' + r) 3
    -- Maybe useful later on
    -- rw [ih, hf.f₃] at h
    -- This is a dead end
    -- rcases h with (h₁ | h₂)
    -- · sorry
    -- · sorry
    -- This idea does not work either
    -- interval_cases r
    -- · simp; sorry
    -- · simp; sorry
    -- · simp; sorry
    sorry


end IsGood

[Violeta Hernández]

Check out the proof of docs#Nat.twoStepInduction, the same technique should apply

[Violeta Hernández]

By the way, this is an IMO problem, right? Feel free to tag me for a review if you ever PR this into Mathlib!

[Alex Brodbelt]

Violeta Hernández said:

By the way, this is an IMO problem, right? Feel free to tag me for a review if you ever PR this into Mathlib!

yes it is hehe, thanks for the help Violeta!

[Alex Brodbelt]

Violeta Hernández said:

Check out the proof of docs#Nat.twoStepInduction, the same technique should apply

Unfortunately I could not manage a way to formalize my approach, so I opted for a different solution.

I will PR my current solution but I am still curious about how I could do the original way I had intended :sad: