The Coq mailing list

[Yannick Zakowski <zakowski AT seas.upenn.edu>]

Hello Agnishom,

You need to bind you metavariable "?t" to the subterm in your goal with a match construct.

You can do so with the following for instance. Notice the question mark in front of your meta-variables in the pattern, but not afterwards.

match goal with
|- ?lhs + ?rhs = _ => replace (lhs + rhs) with (rhs + lhs)
end.

To avoid having to add this "= _" bit, you may use the "context" command:

match goal with
|- context[?lhs + ?rhs] => replace (lhs + rhs) with (rhs + lhs)
end.

Best,
Yannick

On 7/15/20 12:48 PM, Agnishom Chattopadhyay wrote:

Hi;

I want to understand how to use pattern variables to manipulate expressions inside proofs. A google search did not help very much.

Let's say I have an _expression_ 2 + <bigExp> and I want to rewrite it as <bigExp> + 2. I do not want to mention <bigExp> explicitly in my proof. How do I achieve this?

Here is my attempt.

Goal 2 + (3 + 1) = 6.
Proof.
  replace (2 + ?t1) with (?t1 + 2).

But it doesn't work.

--Agnishom