Zulip Chat Archive

Stream: general

Topic: induction h vs rw h for `h : i = i'`


view this post on Zulip Eric Wieser (Oct 28 2020 at 10:38):

I was surprised to see tidy? generate induction h when h is an equality. I'm a little puzzled by the meaning of this, especially since rw h fails. The goal state was

h: i = i'
 (eq.rec si, _ _) = (eq.rec si h)

and after induction h becomes

 (eq.rec si, _ _) = (eq.rec si _)

Can someone explain to me the intuition here?

view this post on Zulip Chris Hughes (Oct 28 2020 at 10:59):

I don't know exactly what's going on here, but the reason rw doesn't work is probably because there is a term in the goal whose type contains i, which means that it is harder to generate the motive (the argument called C in the type of eq.rec) when making the proof term. induction on equality is basically just substitution, but the induction tactic has better support for computing the motive than rw, and makes the substitution everywhere. I think somehow it's easier to compute the motive when you rewrite at all your hypotheses, and also easier when one side of the equality is just a local constant.

view this post on Zulip Eric Wieser (Oct 28 2020 at 11:04):

Thanks, your wording made me realize that induction h is doing the same thing as subst h (which unlike rw h, also works)

view this post on Zulip Eric Wieser (Oct 28 2020 at 11:05):

For more context of what's going on, I'm trying to prove the trivial-but-somehow-not-refl statement in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Difficulty.20with.20dependent.20rewrites/near/214686669


Last updated: May 13 2021 at 21:12 UTC