Zulip Chat Archive

Stream: new members

Topic: Induction on something not in local context


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!

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.

Riccardo Brasca (Oct 24 2020 at 15:09):

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

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.

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.

Reid Barton (Oct 24 2020 at 15:14):

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

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.)

Yury G. Kudryashov (Oct 24 2020 at 16:16):

See the first line of the proof of src#continuous_equiv_fun_basis

Yury G. Kudryashov (Oct 24 2020 at 16:18):

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

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: Dec 20 2023 at 11:08 UTC