From 8eac9d423a80e34d1fa6bf8633a579cef6e72d2b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 7 Nov 2016 14:30:39 -0500 Subject: Add convoy_destruct --- src/Util/Tactics.v | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) (limited to 'src/Util/Tactics.v') 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'). -- cgit v1.2.3