Zulip Chat Archive

Stream: new members

Topic: Induction on something not in local context


view this post on Zulip Riccardo Brasca (Oct 24 2020 at 15:05):

Let us suppose I have two predicates a : polynomial ℤ → Prop and b: polynomial ℤ → Prop and I want to prove that a implies b, so the lemma would be lemma example (p : polynomial ℤ) : a p → b p. How can I write a proof of something like this by induction on p.nat_degree? I mean, p.nat_degree does not appear in a or in b, so induction p.nat_degree does not work.

Something better is cases hd : p.nat_degree with d, it gives two goal, when p.nat_degree = 0 and p.nat_degree = d + 1, but there is no induction hypothesis regarding a → b. I see the reason: formally speaking, what I want to prove by induction is lemma example (p : polynomial ℤ) (d : ℕ) (hd : d = p.nat_degree) : a p → b p, but it very strange to state the theorem this way. So what is the best way of doing it? I tried to play with set d := p.nat_degree with hd and revert hd but it didn't worked.

Thanks!

view this post on Zulip Reid Barton (Oct 24 2020 at 15:08):

What generally happens is that I suggest writing something like your example as an auxiliary lemma and then applying it to d = _ and hd = rfl, and then Mario points out that the blah tactic does exactly this automatically, but I can never remember what blah is.

view this post on Zulip Riccardo Brasca (Oct 24 2020 at 15:09):

Indeed my real question is what tactic does it automatically, I guess there is one :D

view this post on Zulip Reid Barton (Oct 24 2020 at 15:09):

It should be some variation on induction and generalizing though, so since you now understand exactly what tactic state you want to see after the tactic, you can experiment until you find it.

view this post on Zulip Riccardo Brasca (Oct 24 2020 at 15:13):

Ah, generalize' hd : p.nat_degree = d produces the hypothesis I want, then it suffices revert hd.

view this post on Zulip Reid Barton (Oct 24 2020 at 15:14):

If you use induction d next then I bet you can skip revert even.

view this post on Zulip Riccardo Brasca (Oct 24 2020 at 15:16):

Yes! (I need strong induction, so I think I have to use revert, but it doesn't matter.)

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 16:16):

See the first line of the proof of src#continuous_equiv_fun_basis

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 16:18):

unfreezingI is needed to unfreeze [fintype ι] instance; probably not required in your case.

view this post on Zulip Yury G. Kudryashov (Oct 24 2020 at 16:19):

tactic#induction says:

induction h : t will introduce an equality of the form h : t = C x y, asserting that the input term is equal to the current constructor case, to the context.


Last updated: May 11 2021 at 21:10 UTC