Stream: Coq users

Topic: Extracting interval


view this post on Zulip 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)

view this post on Zulip Paolo Giarrusso (Jan 15 2021 at 14:40):

hm, this came up here on Zulip

view this post 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

view this post on Zulip 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: Mar 29 2024 at 01:40 UTC