pattern-matching on a `pexpr`

Stream: metaprogramming / tactics

[Damiano Testa]

This is a continuation of understanding how to make the parser do what I want. The context is still sort_summands in #13483.

Right now, writing sort_summands [f, g] finds f, g in the goal and does something with them. For instance

sort_summands [x * y, g]  --works

works, if the goal is g + x * y.

I would like to be able to pattern-match on the arguments that are passed to sort_summands. For instance, in the case above, I would like

sort_summands [_ * y, g] -- currently does not work

to have the same effect (assuming, of course, that the pattern does not also match for g).

Is it possible to achieve this?

[Damiano Testa]

If I understand the expressions correctly, I would like to find the first time that the given pattern unifies with the type of something in the goal and, if it finds a match, I would like to bind the incomplete pattern with the resulting term and use that as an argument for sort_summands.

[Damiano Testa]

I know that you can do this in the situation below:

import data.nat.basic

example {a b c d : ℕ} (h : c + a * b + d = 0) : a * b + c + d = 0 :=
begin
--  rwa add_comm _, -- uncommenting this does not prove the goal
--  rwa add_comm (_ * _),  -- uncommenting this does prove the goal
end

[Damiano Testa]

As an outcome of (this discussion)[https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics], I now think that I have way of making Lean pattern-match on the input that the user provides.