How to perform induction over two steps back

Stream: new members

[Thobias Rex Smite]

Hello everyone, I'm trying to use the induction tactic but I was only able to use it for one step induction (with hi : f (n-1))
In this case I need f(n-2):

import Mathlib.Data.Nat.Notation
import Mathlib.Tactic

example : ∀ n : ℕ, ∃ x y : ℕ, 13 ^ n = x ^ 2 + y ^ 2 := by
  intro n
  induction' n with n hn
  -- Induction two steps behind
  . use 1; use 0; linarith  -- n = 0
  . use 12; use 5; linarith -- n = 1
  . -- Inductive hn : ∃ x y, 13^(n-2) = x^2 + y^2
    -- 13^n = 13^2 * 13^(n-2)
    --      = 13^2 (x^2 + y^2)
    --      = 13^2 * x^2 + 13^2 * y^2
    sorry

Any Ideas?

[Ruben Van de Velde]

Perhaps you can use strong induction and then case on 0, 1, n + 2

[Thobias Rex Smite]

Ow, I found the principle:

import Mathlib.Data.Nat.Notation
import Mathlib.Tactic

#check Nat.pow_add

example : ∀ n : ℕ, ∃ x y : ℕ, 13 ^ n = x ^ 2 + y ^ 2 := by
  intro n
  induction' n using Nat.twoStepInduction with n hn
  . use 1; use 0; linarith -- n = 0
  . use 3; use 2; linarith -- n = 1
  . obtain ⟨x,y,hn⟩ := hn
    use 13 * x; use 13 * y;
    rw [Nat.pow_add, hn]
    linarith

Never used this using before

[Thobias Rex Smite]

Now I was not interested in letting n = 0, since the theorem becomes uninteresting:

import Mathlib.Data.Nat.Notation
import Mathlib.Tactic

#check Nat.pow_add
#check Nat.pow_sub_mul_pow


example : ∀ n : ℕ, n > 0 → ∃ x y : ℕ, 13 ^ n = x ^ 2 + y ^ 2 := by
  intro n hn0
  induction' n using Nat.strong_induction_on with n hn
  . -- case n = 1
  . -- case n = 2
  . -- inductive n > 2

How could I express that the induction should start on 1 (given n > 0)?

[Ruben Van de Velde]

There's an induction principle for that too, something with le in the name, I think

[Ruben Van de Velde]

You probably can't combine that, though

[Michael Rothgang]

You could also start the induction at 0: the statement is vacuously true there :-)
(Though you'd have to check if the inductive step works this way, though, or you need to also check n=2.)

[Thobias Rex Smite]

import Mathlib.Data.Nat.Notation
import Mathlib.Tactic
import Mathlib.Data.PNat.Defs


#check ℕ+


theorem collares_theorem (k : ℕ) : (∃x y,k=x^2+y^2) →
  ∀ n : ℕ, ∃ x y : ℕ, k ^ n = x ^ 2 + y ^ 2 := by
  intro h n
  induction' n using Nat.twoStepInduction with n hn
  . use 1; use 0; linarith  -- n = 0
  . simp only [pow_one]
    exact h                 -- n = 1
  . obtain ⟨x,y,hn⟩ := hn
    use k * x; use k * y;
    rw [Nat.pow_add, hn]
    linarith

example : ∀ n : ℕ, ∃ x y : ℕ, 13 ^ n = x ^ 2 + y ^ 2 := by
  apply collares_theorem
  use 3; use 2
  linarith

example : ((C : Prop) → ((A → C) → (B → C) → C)) → (¬A → B) :=
  λ (x : (C : Prop) → ((A → C) → (B → C) → C)) (y : A → False) =>
  have xB : (A → B) → (B → B) → B := x B
  have fu : A → B := λ u : A ↦ @False.elim B (y u)
  have xBfu : (B → B) → B := xB fu
  have fv : B → B := λ v ↦ v
  show B from xBfu fv

[Kevin Buzzard]

Thobias Rex Smite said:

Now I was not interested in letting n = 0, since the theorem becomes uninteresting:

That sounds like quite a bad reason for not including n=0! Indeed I I'd say that the vast majority of theorems proved by induction are not interesting at n=0. Surely the only reason you shouldn't include n=0 is when the claim is false? If you explicitly add n>0 as a hypothesis then your theorem becomes more annoying to use because users need to supply this unnecessary extra hypotheses whenever they apply it.

[Bernardo Borges]

Maybe using a type that doesn't have 0, like PNat will allow you to perform induction that starts naturally on 1. Then you just use twoStepInduction again