[Coq-Club] Why doesn't there exist a 'patterns' tactic?

[Chris Dams]

Dear all,

We all know the 'pattern' tactic but I was looking for something that takes
multiple terms and does the same but came up empty. The idea is that we
have, for instance the goal a + b = b + a and then can do 'patterns a b' to
get the goal (fun a0 b0 : nat => a0 + b0 = b0 + a0) a b. Or have I missed
something?

Have a nice day,
Chris

[Dominique Larchey-Wendling]

Post by Chris Dams
Dear all,
We all know the 'pattern' tactic but I was looking for something that
takes multiple terms and does the same but came up empty. The idea is
that we have, for instance the goal a + b = b + a and then can do
'patterns a b' to get the goal (fun a0 b0 : nat => a0 + b0 = b0 + a0) a
b. Or have I missed something?

pattern a, b ?

D.

[Chris Dams]

Hello Dominique,

Thanks! That is funny, I had been trying 'pattern a b' but that did not
work....

Kind regards,
Chris

[Laurent Thery]

pattern can take multiple terms:

https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.pattern

Post by Chris Dams
Dear all,
We all know the 'pattern' tactic but I was looking for something that
takes multiple terms and does the same but came up empty. The idea is
that we have, for instance the goal a + b = b + a and then can do
'patterns a b' to get the goal (fun a0 b0 : nat => a0 + b0 = b0 + a0) a
b. Or have I missed something?
Have a nice day,
Chris