The Coq mailing list

[Michael<michaelschausten AT googlemail.com>]

Hello,

I have a function in a hypothesis, which I'd like to [replace] by something
else with Ltac. My goal looks like this:
x * func a (b+c) <= y * z

Manually, my next step would be:
replace (func a (b+c)) with (func a (b + c - 1 + 1)).

I tried to automatize it with Ltac like this:
Ltac myTac:=
match goal with
  |- func ?x (?y) =>
  replace (func x y) with (func x y - 1 + 1)
end.

However, Coq tells me that there are "No matching clauses for match goal". 
What
am I doing wrong?

Besides, I'm not very skilled with the syntax of Ltac, especially "match goal
with". Is there maybe a good tutorial with examples you can recommend?

Sincerely,