Generalization

Stream: new members

[Guilherme Espada]

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]

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

[Scott Morrison]

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]

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]

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]

I don't think it can make anything unprovable

[Guilherme Espada]

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

[Guilherme Espada]

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

[Eric Wieser]

tactic#specialize works too

[Mario Carneiro]

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]

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

[Eric Wieser]

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

[Kevin Buzzard]

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