Ssreflect Users Discussion List

[Giovanni Mascellani <>]

Hi,

is it possible to use the "rewrite" tactic by specifying the target term
instead of the rewriting theorem? For example, suppose I want to prove

Lemma test (m n : nat) : m + n = n + m.

I know that I can do this:

Proof.
    by rewrite addnC.
Qed.

(ok, this is trivial, but it is an example)

Suppose that I don't remember the name "addnC" and I cannot find it with
the "Search" tool. Is there a way to ask rewrite: "Please, find a
theorem that makes you able to rewrite m+n to n+m and use it"?

I know the syntax

rewrite -[something]/(something else)

but AFAIU this only works when "something" and "something else"
trivially simplify to the same thing.

Thanks, Giovanni.
-- 
Giovanni Mascellani 
<>
Postdoc researcher - Université Libre de Bruxelles

Attachment: signature.asc
Description: OpenPGP digital signature