I want to apply some Ltac everywhere except inside the branches of matches.
Here's a (non-working) example.
(* apply this tactic everywhere except inside match *) Ltac destr c := match c with context [ ?_a =? ?_b ] => destruct (_a =? _b) end. (* find occurrences of matches, avoid applying it inside the branches of the match *) Ltac test_m z := lazymatch z with | context C [ match ?_a with _ => _ end ] => destr _a | _ => destr z end. Parameter n m : nat. Goal (if n =? m then match n with 5 => if 6 =? n then m else m+1 | _ => n end else 6) = if m =? 9 then 7 else 9. repeat match goal with |- ?_Q => idtac _Q ; test_m _Q end. (* didn't apply it on the right hand side of equality :(( *)
Is there a reasonable simple & efficient way to achieve this?
My current idea is to do this:
Ltac destr c := match c with context [ ?_a =? ?_b ] => destruct (_a =? _b) end. Ltac test_m z := match z with | match ?_a with _ => _ end => idtac _a ; destr _a | ?_f ?_a => first [ test_m _f | test_m _a ] end.
But I'm worried it won't scale
Last updated: Oct 03 2023 at 02:34 UTC