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