Add destruct_or tactics to (possibly repeatedly) split disjunctions in an assumption

Following split_and, the new tactics are split_or H, split_or? H and split_or! H. The name H is reused for the assumptions that are produced by destructing the disjunction (no fresh name is introduced).

I was pondering whether the tactic should be split_or H or split_or in H. The second one follows the usual pattern of in+assumption, but at the same time there is not going to be a split_or tactic that works on the goal, so...

Thanks for the MR. Some comments:

• The name should be destruct_or (similarly, destruct_and eliminates conjunctions, split_and introduces them).
• I really like the version with the argument. I think we should have such a version for destruct_and! too. (Of course, it cannot reuse the name, but it can repeatedly destruct conjunctions in just that hypothesis.)
• I think we should also have a version of the destruct_or tactic without the argument that destructs all disjunctions in the context.
• The tactic destruct_and also does do stuff with Is_true (bool_decide _) and False. Similarly, destruct_or should do stuff with Is_true (bool_decide _) and dually with True (namely, just remove it).

Thanks for the suggestions. Btw, is there a good place where to put tests for these kind of tactics? Should I create a new file tests/tactics.v maybe?

added 55 commits

• ec37608e...7d705c84 - 53 commits from branch iris:master
• 03b166ab - Slight update to the documentation of [split_and{!,?}]
• 44e45145 - Add destruct_or{?,!} tactics to (possibly repeatedly) destruct disjunctions in an assumption

Compare with previous version

changed title from Add split_or tactics to (possibly repeatedly) split disjunctions in an assumption to Add destruct_or tactics to (possibly repeatedly) split disjunctions in an assumption

changed the description

I updated the MR:

• renamed the tactic to destruct_or
• added a version of destruct_or? and destruct_or! that do not take any argument (and work on all hypothesis of the context)
• implemented support for Is_true (bool_decide _) and True.

I have not yet generalized destruct_and to work on a single hypothesis. I believe the implementation of the tactic would have to change somewhat, since what we want is in fact to call it recursively on both sub-goals every time we destruct a and. So a simple repeat match goal is not enough.

The tactic destruct_and also does do stuff with Is_true (bool_decide _) and False. Similarly, destruct_or should do stuff with Is_true (bool_decide _) and dually with True (namely, just remove it).

Hmm, thinking more about this, the handling of True and False makes very little sense.

When writing repeated disjunctions we end up with P1 ∨ P2 ∨ ... Pn ∨ False, so it makes sense that destruct_or also takes care of False. Likewise, for repeated conjunctions we end up with P1 ∧ P2 ∧ ... ∧ Pn ∧ True, so it seems like destruct_and should also take care of True. IMHO, to preserve backwards compatibility it makes most sense that both take care of False and True.

Opinions?

added 1 commit

• 40bf5c02 - Add destruct_or{?,!} tactics to (possibly repeatedly) destruct disjunctions in an assumption

Compare with previous version

added 1 commit

• b6955644 - Add destruct_or{?,!}, and generalize destruct_and{?,!} to handle an explicit assumption argument

Compare with previous version

New version of the patch. I think it should address all of the previous comments.

New version of the patch. I think it should address all of the previous comments.

Thanks. Looks good. I left some minor comments.