The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Here are some examples which might elucidate the differences between [appcontext] and [context]:

Set Printing All.

Goal 1 + 1 = 2.

match goal with

  | [ |- context[plus 1] ] => pose 1 (* fails *)

  | [ |- appcontext[plus 1] ] => pose 2 (* this one *)

end.

match goal with

  | [ |- context[plus 1 1] ] => pose 1 (* this one succeeds *)

end.

match goal with

  | [ |- context[_ 1] ] => pose 1 (* succeeds *)

end.

match goal with

  | [ |- appcontext[_ 1] ] => pose 2 (* succeeds *)

end.

The difference is that [context[?f]] only matches things where you have an [f] which is not applied to any arguments, for example, in [eq (plus 1 1) (plus 2 2)], [plus 1 1] is not applied to anything, but [plus 1] is.

There is an oddity when your head is a hole; I'm not sure what to make of it.  For example,

Goal 1 + 2 = 3.

match goal with

  | [ |- context[_ 2] ] => pose 0 (* succeeds *)

end.

Goal 1 + (id 2) = 3.

match goal with

  | [ |- context[_ (id 2)] ] => pose 0 (* fails *)

end.

Note that it does not matter whether or not you have [context] or [appcontext] here.

-Jason

On Mon, Mar 11, 2013 at 1:19 PM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

On 03/11/2013 01:17 PM, Dmitry Grebeniuk wrote:

Require Import Arith.
Goal (plus 1 (id 2)) = 3.
match goal with
| |- appcontext [ _ (id _) ] =>  idtac "found"
end.
(* Error: No matching clauses for match goal *)

   "context [ _ _ (id _) ]" matches the goal, and I thought
that "appcontext" could be used exactly in these
situations, since "plus 1 (id 2)" can be seen as partial
application: "(plus 1) (id 2)", so it could be matched
by "[ _ (id _) ]".
   It seems that I don't understand "appcontext", right?
   

I believe [appcontext] only matches against genuine Gallina terms, not, say, sequences of arguments as in your example.  You could think of [appcontext] as matching _prefixes_ of applications, whereas your example tries to match a strict _suffix_.