Splitting with nested patterns · General

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.

Wolfgang Jeltsch (Aug 12 2023 at 13:55):

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_⟨type-of-scrutinee⟩ and 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.

Mathias Fleury (Aug 13 2023 at 06:41):

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
*)

Dmitriy Traytel (Aug 13 2023 at 06:46):

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).

Wolfgang Jeltsch (Aug 13 2023 at 11:47):

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?

Mathias Fleury (Aug 13 2023 at 11:50):

without reproducer, be careful with .splitvs .splits(the latter is more powerful, as it also splits on cases in assumptions)

Mathias Fleury (Aug 13 2023 at 11:51):

splitting should be done eagerly, but you might have some interaction with congruence rules

Mathias Fleury (Aug 13 2023 at 11:52):

supply [[simp_trace]]

Wolfgang Jeltsch (Aug 13 2023 at 19:54):

(∃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?

Wolfgang Jeltsch (Aug 13 2023 at 19:58):

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 (subst list.split).

Mathias Fleury (Aug 14 2023 at 15:35):

lemma "(∃ys. (case xs of [] ⇒ None | _ # xs' ⇒ Some xs') = Some ys) ⟷ ¬ List.null xs"
  by (auto simp: List.null_def split: list.splits)

Mathias Fleury (Aug 14 2023 at 15:36):

Wolfgang Jeltsch (Aug 14 2023 at 16:58):

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?

Wolfgang Jeltsch (Aug 14 2023 at 20:48):

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:

Stream: General

Topic: Splitting with nested patterns

Wolfgang Jeltsch (Aug 11 2023 at 22:25):