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 ?
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).
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
?c2 for the two cases.
Last updated: Aug 13 2022 at 05:18 UTC