Zulip Chat Archive
Stream: new members
Topic: How to perform induction over two steps back
Thobias Rex Smite (Nov 22 2024 at 20:02):
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 (Nov 22 2024 at 20:07):
Perhaps you can use strong induction and then case on 0, 1, n + 2
Thobias Rex Smite (Nov 22 2024 at 20:20):
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 (Nov 22 2024 at 20:42):
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 (Nov 22 2024 at 20:54):
There's an induction principle for that too, something with le
in the name, I think
Ruben Van de Velde (Nov 22 2024 at 20:55):
You probably can't combine that, though
Michael Rothgang (Nov 22 2024 at 21:58):
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 (Nov 22 2024 at 22:45):
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 (Nov 23 2024 at 08:26):
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 (Nov 26 2024 at 12:56):
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
Last updated: May 02 2025 at 03:31 UTC