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: Sep 28 2023 at 11:01 UTC