Proof by induction on size

Stream: new members

[Keefer Rowan]

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]

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

[Keefer Rowan]

Cool, thanks!

[Jalex Stark]

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]

There is also

induction hn : size x,