Bilel Ghorbel (Dec 08 2021 at 11:18): 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 ?
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).
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: Apr 25 2024 at 20:15 UTC