Email Gateway (Aug 12 2023 at 12:58): Email Gateway (Aug 12 2023 at 12:58):From: Wolfgang Jeltsch <wolfgang@well-typed.com>
Hi!
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.
All the best,
Wolfgang
Email Gateway (Aug 12 2023 at 13:57):From: Wolfgang Jeltsch <wolfgang@well-typed.com>
Hi, again!
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.
All the best,
Wolfgang
Email Gateway (Aug 13 2023 at 13:23):From: Thomas Sewell <tals4@cam.ac.uk>
Indeed, there is one case constant per datatype.
Its name is usually obvious, e.g. "term case_option" in a theory file will tell you the type of the case constant for option.
To break up a goal with a multi-level case structure, you probably just need to add the split rules for all the case constants that are involved, e.g. both option and bool in the case you showed.
If that doesn't work, you probably need to inspect the goal after the splitting and try to figure out what is blocking the simplifier from taking further steps.
The ML sublanguage of Isabelle sometimes helps in learning which constants are involved in certain syntax. For instance, the below makes it clear that a constant called Option.option.case_option is applied to various terms to make a case split:
ML ‹ @{term "case x of None => 1 | _ => 2"} ›
Good luck with it,
Thomas.
Email Gateway (Aug 14 2023 at 14:37):From: Wolfgang Jeltsch <wolfgang@well-typed.com>
Wait, I need to explicitly add these split rules? I thought the split
rules that have been automatically generated for a datatype are already
registered to be taken into account by the Simplifier, analogously to
the datatype’s simplification rules already being part of the simpset.
Is this not the case?
All the best,
Wolfgang
Email Gateway (Aug 14 2023 at 15:50):From: Tobias Nipkow <nipkow@in.tum.de>
On 14/08/2023 16:37, Wolfgang Jeltsch wrote:
Am Sonntag, dem 13.08.2023 um 13:22 +0000 schrieb Thomas Sewell:
To break up a goal with a multi-level case structure, you probably
just need to add the split rules for all the case constants that are
involved, e.g. both option and bool in the case you showed.Wait, I need to explicitly add these split rules? I thought the split
rules that have been automatically generated for a datatype are already
registered to be taken into account by the Simplifier, analogously to
the datatype’s simplification rules already being part of the simpset.
Is this not the case?
No.
Tobias
All the best,
Wolfgang
Last updated: Apr 29 2024 at 01:08 UTC