Zulip Chat Archive

Stream: new members

Topic: Generalization


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

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

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

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

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

view this post on Zulip Ruben Van de Velde (Mar 10 2021 at 12:38):

I don't think it can make anything unprovable

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

view this post on Zulip Guilherme Espada (Mar 10 2021 at 13:15):

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

view this post on Zulip Eric Wieser (Mar 10 2021 at 13:38):

tactic#specialize works too

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

view this post on Zulip Guilherme Espada (Mar 10 2021 at 15:24):

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

view this post on Zulip Eric Wieser (Mar 10 2021 at 18:30):

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

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