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

tests/tactics.ref

+The command has indeed failed with message:
+Failed to progress.
+The command has indeed failed with message:
+Ltac call to "destruct_or !" failed.
+Failed to progress.
+The command has indeed failed with message:
+Ltac call to "destruct_and !" failed.
+Failed to progress.

tests/tactics.v

+From stdpp Require Import tactics.
+
+Goal forall P1 P2 P3 P4 (P: Prop),
+  P1 ∨ (Is_true (P2 || P3)) ∨ P4 →
+  (P1 → P) →
+  (P2 → P) →
+  (P3 → P) →
+  (P4 → P) →
+  P.
+Proof.
+  intros * HH X1 X2 X3 X4.
+  destruct_or? HH; [ exact (X1 HH) | exact (X2 HH) | exact (X3 HH) | exact (X4 HH) ].
+Qed.
+
+Goal forall P1 P2 P3 P4 (P: Prop),
+  P1 ∨ P2 →
+  P3 ∨ P4 →
+  (P1 → P3 → P) →
+  (P1 → P4 → P) →
+  (P2 → P3 → P) →
+  (P2 → P4 → P) →
+  P.
+Proof.
+  intros * HH1 HH2 X1 X2 X3 X4.
+  destruct_or?; [ exact (X1 HH1 HH2) | exact (X3 HH1 HH2) | exact (X2 HH1 HH2) | exact (X4 HH1 HH2) ].
+Qed.
+
+Goal forall P1 P2 P3 P4 (P: Prop),
+  id (P1 ∨ P2) →
+  id (P3 ∨ P4) →
+  (P1 → P3 → P) →
+  (P1 → P4 → P) →
+  (P2 → P3 → P) →
+  (P2 → P4 → P) →
+  P.
+Proof.
+  intros * HH1 HH2 X1 X2 X3 X4.
+  Fail progress destruct_or?.
+  Fail progress destruct_or!.
+  destruct_or! HH1; destruct_or! HH2;
+  [ exact (X1 HH1 HH2) | exact (X2 HH1 HH2) | exact (X3 HH1 HH2) | exact (X4 HH1 HH2) ].
+Qed.
+
+Goal forall P1 P2 P3 P4,
+  P1 ∧ (Is_true (P2 && P3)) ∧ P4 →
+  P1 ∧ P2 ∧ P3.
+Proof.
+  intros * HH. split_and!; [ destruct_and? HH; assumption | destruct_and?; assumption | ].
+  destruct_and?. Fail destruct_and!. assumption.
+Qed.

theories/tactics.v

@@ -91,7 +91,17 @@ Tactic Notation "etrans" := etransitivity.
   conjunction.
 
 Note that [split_and] differs from [split] by only splitting conjunctions. The
-[split] tactic splits any inductive with one constructor. *)
+[split] tactic splits any inductive with one constructor.
+
+
+- [destruct_and? H] : destruct assumption [H] repeatedly (perhaps zero times)
+  while it is of the shape [_ ∧ _].
+- [destruct_and! H] : works similarly, but at least one destruct should succeed.
+  In order to do so, it will head normalize the goal first to possibly expose a
+  conjunction.
+- [destruct_and?] iterates [destruct_or? H] on every matching assumption [H].
+- [destruct_and!] works similarly, but at least one destruct should succeed.
+*)
 Tactic Notation "split_and" :=
   match goal with
   | |- _ ∧ _ => split
@@ -100,14 +110,56 @@ Tactic Notation "split_and" :=
 Tactic Notation "split_and" "?" := repeat split_and.
 Tactic Notation "split_and" "!" := hnf; split_and; split_and?.
 
+Ltac destruct_and_go H :=
+  try lazymatch type of H with
+  | False => destruct H
+  | _ ∧ _ =>
+    let H1 := fresh in
+    let H2 := fresh in
+    destruct H as [ H1 H2 ];
+    destruct_and_go H1; destruct_and_go H2
+  | Is_true (bool_decide _) =>
+    apply (bool_decide_unpack _) in H;
+    destruct_and_go H
+  | Is_true (_ && _) =>
+    apply andb_True in H;
+    destruct_and_go H
+  end.
+
+Tactic Notation "destruct_and" "?" ident(H) :=
+  destruct_and_go H.
+Tactic Notation "destruct_and" "!" ident(H) :=
+  hnf in H; progress (destruct_and? H).
+
 Tactic Notation "destruct_and" "?" :=
-  repeat match goal with
-  | H : False |- _ => destruct H
-  | H : _ ∧ _ |- _ => destruct H
-  | H : Is_true (bool_decide _) |- _ => apply (bool_decide_unpack _) in H
-  | H : Is_true (_ && _) |- _ => apply andb_True in H; destruct H
+  repeat match goal with H : _ |- _ => progress (destruct_and? H) end.
+Tactic Notation "destruct_and" "!" :=
+  progress destruct_and?.
+
+(** Tactics for splitting disjunctions in an assumption:
+
+- [destruct_or? H] : destruct the assumption [H] repeatedly (perhaps zero times)
+  while it is of the shape [_ ∨ _].
+- [destruct_or! H] : works similarly, but at least one destruct should succeed.
+  In order to do so, it will head normalize the goal first to possibly
+  expose a disjunction.
+- [destruct_or?] iterates [destruct_or? H] on every matching assumption [H].
+- [destruct_or!] works similarly, but at least one destruct should succeed.
+*)
+Tactic Notation "destruct_or" "?" ident(H) :=
+  repeat match type of H with
+  | True => clear H
+  | _ ∨ _ => destruct H as [H|H]
+  | Is_true (bool_decide _) => apply (bool_decide_unpack _) in H
+  | Is_true (_ || _) => apply orb_True in H; destruct H as [H|H]
   end.
-Tactic Notation "destruct_and" "!" := progress (destruct_and?).
+Tactic Notation "destruct_or" "!" ident(H) := hnf in H; progress (destruct_or? H).
+
+Tactic Notation "destruct_or" "?" :=
+  repeat match goal with H : _ |- _ => progress (destruct_or? H) end.
+Tactic Notation "destruct_or" "!" :=
+  progress destruct_or?.
+
 
 (** The tactic [case_match] destructs an arbitrary match in the conclusion or
 assumptions, and generates a corresponding equality. This tactic is best used