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: Jun 16 2024 at 01:42 UTC