The split rules that are generated by datatype declarations deal only with
case expressions that use patterns with one constructor each. However, I’m dealing with goals that contain
case expressions that use patterns with multiple constructors. For example, there may be
case expressions of the following form:
case x of None ⇒ … | Some False ⇒ … | Some True ⇒ …
My experience is that the Simplifier cannot really cope with such case expressions. How can I assist it?
By the way, how are such
case expressions represented internally? My impression is that they are just syntactic sugar for more fundamental expressions, but I don’t know what these expressions are.
Through some study and experiments I probably found out how the desugaring of such
case expressions works. Apparently,
case expressions with one constructor per pattern are internally represented as full applications of
case expressions with multiple constructors per pattern, like the above one, are internally represented as nested applications of such eliminator functions, for example
case_option … (case_bool … …) x. This, in turn, should mean that also such more complex
case expressions work with the default split rules.
Maybe I have to search for other reasons why simplification of my goals doesn’t work. If anyone has some idea what else could go wrong in the presence of such
case expressions, please tell me.
Why not use multiple split rules?
definition test where ‹test a = (case a of None ⇒ None | Some True ⇒ Some (1::nat) | Some False ⇒ Some 0)› lemma ‹test a = A› apply (auto simp: test_def split: option.splits bool.splits) (*proof (prove) goal (3 subgoals): 1. a = None ⟹ None = A 2. ⋀x2. x2 ⟹ a = Some True ⟹ Some (Suc 0) = A 3. ⋀x2. ¬ x2 ⟹ a = Some False ⟹ Some 0 = A *)
This is also what I was about to write. :wink:
In addition, to see the internal representation, one can disable the case syntax:
declare [[show_cases=false]] term "case xs of Some True # xs ⇒ xs | _ ⇒ " term "case xs of Some (x, y) # xs ⇒ xs | _ ⇒ "
The second example shows that the "λ(x, y). xs" syntax is still treated differently (not subject to the
show_cases option), even though internally, this is still a
case_prod (λx y. xs).
As I wrote above, split rules for the outer and the inner case distinction are already registered. Simplification didn’t work nevertheless, but this had probably to do with something else.
What confused me a bit initially was that the simplification attempt failed entirely. However, I suppose now that splitting is not something that is done individually and if subsequent rewriting fails the splitting is undone. Is this how it works? Unfortunately, the Isabelle/Isar Reference Manual doesn’t say much about what splitting actually is and how it works. Is there some thorough documentation of that?
without reproducer, be careful with
.splits(the latter is more powerful, as it also splits on cases in assumptions)
splitting should be done eagerly, but you might have some interaction with congruence rules
yield something interesting?
My goals are similar to the following one:
(∃ys. (case xs of  ⇒ None | _ # xs' ⇒ Some xs') = Some ys) ⟷ ¬ List.null xs
I rather have the impression that the basic automated provers are not powerful enough to solve such goals, which I find somewhat surprising. For example,
simp cannot do anything about the above goal, while
auto yields the following subgoals:
⋀ys. (case xs of  ⇒ None | x # xs' ⇒ Some xs') = Some ys ⟹ List.null xs ⟹ False ¬ List.null xs ⟹ ∃ys. (case xs of  ⇒ None | x # xs' ⇒ Some xs') = Some ys
I would think that both of these subgoals should be easily solvable, but apparently this isn’t the case. Am I missing something?
Regarding the splitting behavior of the Simplifier: Why doesn’t
simp do anything about the initial goal shown above and just fails? I mean, it should be at least able to apply a split rule, right? I can manually apply a split rule with
lemma "(∃ys. (case xs of  ⇒ None | _ # xs' ⇒ Some xs') = Some ys) ⟷ ¬ List.null xs" by (auto simp: List.null_def split: list.splits)
simp also works
Cool! Thank you very much for this solution.
It might provide for a much simpler and more elegant solution to my actual problem. This problem is developing an automated prover that merely recurses through some terms using introduction rules, solving rather simple proof obligations along the way. I’m developing this prover using Eisbach. Your solution gives me hope that I might get away with a simple combination of standard proof methods with appropriate parameters instead of having to use goal matching and recursion to process those terms more manually.
So I get that split rules like those in
list.splits do not get considered by default. Perhaps I should read more about split rules. Is there more documentation on the topic of splitting in Isabelle beyond what’s written in the Isabelle/Isar Reference manual in the section on the Simplifier?
So I get that split rules like those in
list.splitsdo not get considered by default. Perhaps I should read more about split rules.
So I carefully studied the section on the Simplifier in the Isabelle/Isar Reference Manual and found almost at the end, in Subsection 9.3.6, the following, which seems to explain the situation quite well:
Case splits should be allowed only when necessary; they are expensive and hard to control. Case-splitting on if-expressions in the conclusion is usually beneficial, so it is enabled by default in Isabelle/HOL and Isabelle/FOL/ZF.
Last updated: Dec 07 2023 at 08:19 UTC