Jonas Oberhauser (Jan 14 2022 at 04:02): Jonas Oberhauser (Jan 14 2022 at 04:02):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