The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi,
I think you are asking for the "as" pattern inside contexts ltac. I
don't think it
is implemented but would be a valid feature wish imho.

repeat match goal with
  | _: context [(1 + ?x) as foo] |- _ => change foo with (S x) in *
...

Regarding factorization of tactics you can do it like you would in a
standard functional programming language, with a let binding:

  repeat
    let oneplusx :=
      (match goal with
       | H: context [1 + ?x] |- _ => constr:(1 + x)
       | |- context [1 + ?x]      => constr:(1 + x)
       end) in
    match oneplusx with
    | context [1 + ?x] => change oneplusx with (S x) in *
    end.

Best regards
P.



2017-11-13 16:10 GMT+01:00 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