Deep matching like Ltac's context

[awalterschulze]

quote4 is amazing at pattern matching in hypotheses and the goal.
Thank you so much for creating this library.
It is already a huge help.

I was wondering if would be possible to extend quote4's matching to do deeper matching, something like how context works in Coq's Ltac.

This way we can apply rewrite rules to anywhere in a hypothesis or goal that they are possible.
For example in Coq we can write:

match goal with
| [ H: context [[] ++ _] |- _ ] =>
  rewrite app_nil_l in H
  (* [] ++ xs = xs *)
end.

This way the following hypothesis will all be rewritten with one pattern match

H1: [] ++ xs = ys
H2: x :: ([] ++ xs) = y :: ys
H3: xs ++ ([] ++ ys) = zs
H4: xs ++ (x :: ([] ++ ys)) = z :: zs
H4: x :: xs ++ (x :: ([] ++ ys)) = z :: z :: zs

Maybe this feature already exists and I missed it?

If it doesn't exist maybe not to break backwards compatibility there could be a new syntax, maybe using square brackets, but that is totally up to you:

...
    match hypProp with
    | ~q[[] ++ $xs] =>
      -- rewrite [] ++ xs anywhere
      Lean.Elab.Tactic.evalTactic <- `(tactic| rw list_app_nil_l at $name )
...