a version of every_case_tac that does case splits in order

[xrchz]

every_case_tac uses a search procedure for case expressions that claims (in the signature of BasicProvers) to be looking for the "smallest" case split first. It would often be useful to instead do the first (in top-down left-to-right order) case split first. There is BasicProvers.TOP_CASE_TAC for doing this once. An analogous every_case_tac (maybe every_top_case_tac?) would probably avoid many unnecessary splits in various proofs.

---

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

[tanyongkiam]

Hi Ramana,

Thanks for pointing this out! top_case_tac seems very useful. As a related question: do you also know if there is a way to force the case splitter to split on the first matched pattern?

For example, in my word_alloc proofs (especially in Call), I always get terrible default case splits (I think top_case_tac might help). This leads to a lot of Cases_on... where ... is a huge block of text that is annoying to type and breaks often because it uses fixed names.

One way I've used was:

qpat_abbrev_tac A=... >> Cases_onA>> fs[Abbrev_def]

or if I need to equality the correct way around, something like

Cases_onA>>pop_assum(assume_tac o SYM o REWRITE_RULE[markerTheory.Abbrev_def]) >>fs[]

[xrchz]

You could try something like:

(fn g => subterm (fn tm => Cases_on`^(assert some_condition tm)`) (#2 g) g)

where you define some_condition to pick out the thing you want. I use has_pair_type sometimes there, but you could also do a pattern match. You would usually want to do a pattern match in the context of the goal, though, and I forgot what function does that (but you have g around there, so it should be possible).

[thtuerk]

@tanyongkiam I of course don't know your exact situation, but this kind of case split on the first matched pattern was part of the motivation behind having a different representation of pattern matches. It is possible with my framework to essentially do this split, but lifting the case expression to the next boolean level. You might want to look in patternMatchesLib at

• PMATCH_LIFT_BOOL_ss
• PMATCH_TO_TOP_RULE
• PMATCH_INTRO_CONV

and related functions.

P.S.: I hope over the Christmas holidays, I finally fine enough time to work on the branch patternMatches again.