Bug 2998 - "match goal with context" can't find some terms under lambda abstraction
: "match goal with context" can't find some terms under lambda abstraction
Status: NEW
Product: Coq
Classification: Unclassified
Component: Tactics
: 8.4
: PC Linux
: P5 normal
: ---
Assigned To: nobody
Depends on:
Blocks:
  Show dependency treegraph
 
Reported: 2013-03-10 10:16 CET by Dmitry Grebeniuk
Modified: 2013-07-30 17:58 CEST (History)
2 users (show)

See Also:


Attachments

Note You need to log in before you can comment on or make changes to this bug.
Description Dmitry Grebeniuk 2013-03-10 10:16:57 CET
Suppose I have:

    Goal (fun x => 1 + id x) 2 = 3.

Then I do

    match goal with
    | |- context [id ?x] => idtac "found"
    end.

And I see

    Error: No matching clauses for match goal
           (use "Set Ltac Debug" for more info).

I'd prefer to think that this is a bug rather than documentation issue, since an ability to manipulate terms under lambda abstraction looks useful for me, and it's more "generic" ("no matter where the term is, it can be processed").
Comment 1 Dmitry Grebeniuk 2013-03-10 11:57:07 CET
In this case exists the workaround (thanks to robbert from #coq irc): "match goal with | |- context [id _] => ..." with obvious limitations (can't use "x" in RHS of this match case), but it doesn't work under fixpoints:

    Goal (fix f x := 1 + id x) 2 = 3.

    match goal with
    | |- context [id _] => idtac "found"
    end.

  ->

    Error: No matching clauses for match goal
           (use "Set Ltac Debug" for more info).
Comment 2 Pierre-Marie Pédrot 2013-07-30 17:58:12 CEST
The fixpoint part is fixed in trunk.

The original issue is still there, although I'm pretty sure that "it's not a bug, it's a feature"®. Indeed, we do not want to capture bound variables in Ltac match, or at least not this way.

That said, we can still ramble about the lack of Ltac primitives to manipulate open terms...