Induction on something not in local context

Stream: new members

[Riccardo Brasca]

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!

[Reid Barton]

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.

[Riccardo Brasca]

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

[Reid Barton]

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.

[Riccardo Brasca]

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

[Reid Barton]

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

[Riccardo Brasca]

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

[Yury G. Kudryashov]

See the first line of the proof of src#continuous_equiv_fun_basis

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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.