Zulip Chat Archive

Stream: new members

Topic: Proof by induction on size


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Keefer Rowan (May 18 2020 at 23:59):

Cool, thanks!

view this post on Zulip 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

view this post on Zulip 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