I have lots of lemmas with assumptions of the form a <= b < c. In each lemma the difference c-a can be written without any variables (so I could prove for example c-a = 5 by lia).

I would like to automatically generate cases b=a, b=a+1, b=a+2, ..., b=a+(c-a-1).

What is the most robust way to do this? (one fragile way is to assume c has the form a+S x, and then generate the cases a ... a+x)

hm, this came up here on Zulip

https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Induction.20scheme.20for.20a.20range.20of.20Z does it for Z

you can probably add some `Ltac`

on top to use the new principle. Without further assumptions, I guess that you'd have to give `5`

by hand.

Last updated: Jun 18 2024 at 00:02 UTC