The Coq mailing list

[Samuel Gruetter <gruetter AT mit.edu>]

On Mon, 2017-11-13 at 17:58 +0100, Pierre Courtieu wrote:
> 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 *
> ...

Yes, that's exactly what I meant.
Actually, this might also be useful outside "context", e.g.

repeat match goal with
  | H: myFunc ((1 + ?x) as foo) |- _ => apply (myLemma foo) in H
end


> 
> 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.


I see... So let's apply this to a case with 2 actual branches:
I start with this:


Require Import Coq.Arith.PeanoNat.

Goal forall a b c, (a + 1) + (1 + b) = c -> (1 + a) + (b + 1) = 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 *
  | _: context [?x + 1] |- _ => rewrite (Nat.add_comm x 1) in *
  | |- context [?x + 1]      => rewrite (Nat.add_comm x 1) in *
  end.
Abort.


and to avoid the duplication, I turn it into this:


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


This works fine in this simple example, but it won't work any more when the
choice of which branch to take depends on whether the tactic on the right-
hand side of "=>" succeeds.
So I'd have to change it to something like the following I guess?


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


This is not very satisfactory to me because it's too complex.
What I'd really like to write is this:


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


Are there any good reasons for not supporting this?


> 
> 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