Email Gateway (Aug 22 2022 at 12:54): Email Gateway (Aug 22 2022 at 12:54):From: Thomas Sewell <thomas.sewell@nicta.com.au>
A note of caution.
The if_split/split_if rule caused some headaches for us in l4v, and is
globally removed from the split set for a number of the theories (which
causes secondary headaches). It's possible if_split_asm would be the
same, though, as you've probably observed, if statements in assumptions
are probably a lot rarer than in conclusions in any case.
Cheers,
Thomas.
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 13:00):From: Tobias Nipkow <nipkow@in.tum.de>
Currently simp/auto split if-then-else terms if they occur in the conclusion by
default but not if they occur in the assumptions of a goal. The motivation was
the following: inductive proofs of propositions involving "if" often go astray
if the "if" in the IH is split. However, this situation is not very frequent
(the "if" is typically hidden in some definition) but I frequently need to
modify my simp/auto calls with
split: if_split_asm (* was named split_if_asm until recently *)
Hence I intend to enable "if_split_asm" by default, just like "if_split", and
would like your feedback on this, if you have any.
Why is this not clear cut? According to my tests, the effect is largely positive
(see below). But there is the following usage aspect:
Realizing that if_split_asm should be added is much easier than realizing that
it should be removed: the presence of "if" in an assumption is the indicator.
Of course this only applies if the user is aware of the existence of if_split_asm!
The empirical side look like this. I have converted all of HOL (locally) with
the following results:
The number of lines deleting if_split_asm has gone up from 18 to 54
In about 15 theories if_split_asm had to be disabled globally because it broke
too much. Typically these are long apply-style proofs.
Otherwise local "split del" modifiers did the job.
In a few places proofs became simpler.
In the AFP I only tested 2 articles.
Launchbury: the 4 occurrences of if_split_asm could be removed, that's all.
Jinja: the 56 occurrences of if_split_asm could be removed, 1 local split del
had to be added.
Any views?
Tobias
smime.p7s
Last updated: Apr 27 2024 at 01:05 UTC