## Stream: new members

### Topic: Proof by induction on size

#### Keefer Rowan (May 18 2020 at 23:51):

How can I prove something by "induction on size". E.g. suppose size is a function giving the size of some element of type \alpha and predicate is something provable by induction on size, how would I go about introducing induction in a proof like this:

variable α : Type
def size : α → ℕ := by sorry

def predicate (x : α) : Prop := by sorry

example (x : α) : predicate x :=
begin
--induction (size x),
sorry
end


In the commented out induction, I get the error generalize tactic failed, failed to find expression in the target.

#### Jalex Stark (May 18 2020 at 23:56):

This works

import tactic

universes u

variables {α : Type u}
def size : α → ℕ := sorry

def predicate (x : α) : Prop := sorry

example (x : α) : predicate x :=
begin
suffices key : ∀ n, size x = n → predicate x,
{apply key (size x), refl},
intro n,
induction n,
end


Cool, thanks!

#### Jalex Stark (May 18 2020 at 23:59):

I think this is a slightly better way to write the type signature

import tactic

universes u

example
{α : Type u} (size : α → ℕ) (predicate : α → Prop) (x : α) :
predicate x :=
begin
suffices key : ∀ n, size x = n → predicate x,
{apply key (size x), refl},
intro n,
induction n,
end


#### Yury G. Kudryashov (May 19 2020 at 01:36):

There is also

induction hn : size x,


Last updated: May 08 2021 at 20:11 UTC