Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: pattern-matching on a `pexpr`


Damiano Testa (Apr 20 2022 at 09:07):

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 (Apr 20 2022 at 09:11):

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 (Apr 20 2022 at 09:26):

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 (Apr 22 2022 at 11:15):

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.


Last updated: Dec 20 2023 at 11:08 UTC