## Stream: new members

### Topic: Generalization

#### Guilherme Espada (Mar 10 2021 at 12:09):

What is the point of the generalizing statement on induction? Can anyone give a simple example that it helps solve? I've tried googling it, but the docs don't give examples.

Thanks

#### Scott Morrison (Mar 10 2021 at 12:12):

Search for induction.*generalizing in mathlib (turn regexes on if necessary in the search box) and you'll find heaps of examples.

#### Scott Morrison (Mar 10 2021 at 12:16):

Say you have an n m : nat in the context. If you write induction n, then you're doing the induction for some fixed value of m. If you write induction n generalizing m, you're just "reverting" the hypothesis m, obtaining a "for all m, ..." statement in the goal, and then doing an induction argument for that (generalizing will automatically re-introduce m).

#### Guilherme Espada (Mar 10 2021 at 12:25):

This helped. In other words, it adds a forall in the induction hypothesis correct?
I guess then my further question is the following: Why is just generalizing not correct? Can generalizing in induction make something unprovable?

#### Ruben Van de Velde (Mar 10 2021 at 12:38):

Generalizing "too much" just makes your induction step more tedious, because you have to instantiate the induction hypothesis with your fixed m

#### Ruben Van de Velde (Mar 10 2021 at 12:38):

I don't think it can make anything unprovable

#### Guilherme Espada (Mar 10 2021 at 13:13):

Alright, that's useful to know. Thanks!
Aditionally, how do I turn \forall x x = y into, for example, z = y?

#### Guilherme Espada (Mar 10 2021 at 13:15):

Seems have does it, but I was wondering if there was a better way

#### Eric Wieser (Mar 10 2021 at 13:38):

tactic#specialize works too

#### Mario Carneiro (Mar 10 2021 at 14:36):

Generalizing too much can make things unprovable, because you lose access to the relation to the original arguments to the induction. Plus you generally can't generalize everything, for example if you are inducting on list A then A can't be generalized.

#### Guilherme Espada (Mar 10 2021 at 15:24):

But can't you always just specialize and restore the relation?

#### Eric Wieser (Mar 10 2021 at 18:30):

If you generalize, then while your hypothesis got stronger, so did your goal.

#### Kevin Buzzard (Mar 11 2021 at 07:47):

I think that just generalising a variable before an induction can never make a provable-with-induction thing unprovable and conversely sometimes it's essential, like in that level of the natural number game which causes people problems

Last updated: May 11 2021 at 22:14 UTC