diff options
| -rw-r--r-- | src/Util/Tactics.v | 32 |
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'). |