Add convoy_destruct

1 files changed, 32 insertions, 0 deletions

diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index ea5d2e5e1..128fdcfd0 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -487,3 +487,35 @@ Ltac idtac_context :=
        idtac_goal;
        lazymatch goal with |- ?G => idtac "Context:" G end;
        fail).
+
+(** Destruct the convoy pattern ([match e as x return x = e -> _ with _ => _ end eq_refl] *)
+Ltac convoy_destruct_gen T change_in :=
+  let e' := fresh in
+  let H' := fresh in
+  match T with
+  | context G[?f eq_refl]
+    => match f with
+       | match ?e with _ => _ end
+         => pose e as e';
+            match f with
+            | context F[e]
+              => let F' := context F[e'] in
+                 first [ pose (eq_refl : e = e') as H';
+                         let G' := context G[F' H'] in
+                         change_in G';
+                         clearbody H' e'
+                       | pose (eq_refl : e' = e) as H';
+                         let G' := context G[F' H'] in
+                         change_in G';
+                         clearbody H' e' ]
+            end
+       end;
+       destruct e'
+  end.
+
+Ltac convoy_destruct_in H :=
+  let T := type of H in
+  convoy_destruct_gen T ltac:(fun T' => change T' in H).
+Ltac convoy_destruct :=
+  let T := get_goal in
+  convoy_destruct_gen T ltac:(fun T' => change T').