Jonas Oberhauser (Jan 15 2021 at 10:53): Jonas Oberhauser (Jan 15 2021 at 10:53):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)
Paolo Giarrusso (Jan 15 2021 at 14:40):hm, this came up here on Zulip
Paolo Giarrusso (Jan 15 2021 at 14:42):https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Induction.20scheme.20for.20a.20range.20of.20Z does it for Z
Paolo Giarrusso (Jan 15 2021 at 14:43):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