Stream: Beginner Questions

Topic: splitting cases in goal with schematic variables

view this post on Zulip Bilel Ghorbel (Dec 08 2021 at 11:18):

As the title says, I am trying to prove a goal that contains schematic variables. This can only done after splitting cases. I figure out that the cases proof method doesn't create different schematic variables in the different goals. What workarounds are there in this case ?

view this post on Zulip Manuel Eberl (Dec 08 2021 at 11:22):

Instantiate the schematic variables with an if … then … else? But I would try to avoid working with schematic goals anyway (unless you have a very good reason not to).

view this post on Zulip Manuel Eberl (Dec 08 2021 at 11:25):

Generating separate schematic variables for each of the cases in a case split would be unsound in general. Like, when you do a case split on a bound variable. If your goal is something like ∀(x::nat). prime x = ?c, that goal is obviously unprovable. But if you do a case split on prime x, you could easily prove it if that case split created new schematic variables ?c1 and ?c2 for the two cases.

Last updated: Aug 13 2022 at 05:18 UTC