The Coq mailing list

[Samuel Gruetter <gruetter AT mit.edu>]

Dear coq-club,

I have two questions about Ltac's match with "context".
I often write code like this:


Goal forall a b c, a + (1 + b) = c -> (1 + a) + b = c.
  intros.
  repeat match goal with
  | _: context [1 + ?x] |- _ => change (1 + x) with (S x) in *
  | |- context [1 + ?x]      => change (1 + x) with (S x) in *
  end.
Abort.


There are two things I'd like to improve, but don't know how to do it:

1) I write the same line twice, once for matching in the hypotheses, once
   for matching in the goal. Can this be unified?
2) On the right-hand side of "=>", I have to repeat the term (1 + x), just
   without the question marks. This is bad because it's code duplication,
   and it gets even worse if the term contains implicit arguments: It
   happens often to me that the implicit arguments inferred on the right-
   hand side of "=>" don't match the original ones, so that "change" does
   nothing. Therefore, I wonder if there's a way to refer to the
   "term matched inside context"?
   (I'm aware that I can write "context C[1 + ?x]", but C gives me the
   context *around* the term, i.e. everything *except* what I want)

Thanks in advance,

Sam