The Coq mailing list

["Woon Ming" <woon_ming AT comp.nus.edu.sg>]

Hi Matthieu,

Thank you very much for your prompt reply. I have seen that pattern
construction when I was reading the reference manual (under Chapter 9.1
Syntax). However, the reason why I didn't use it is because there is no
worked examples on it.

Thus may I ask you to give me a simple example on how it is done so that?

Thank you in advance.

Best Regards, 
Woon Ming

-----Original Message-----
From: Matthieu Sozeau 
[mailto:Matthieu.Sozeau AT lri.fr]
 
Sent: Thursday, January 29, 2009 2:55 AM
To: Woon Ming
Cc: 
coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Occurrence of keyword in conclusion


Le 29 janv. 09 à 23:43, Woon Ming a écrit :

> Hi all,

Hi,

> In my Ltac,  I would like to detect the occurrence of a particular  
> keyword in the conclusion and apply the appropriate hypothesis.
> ( e.g.
> My conclusion consists of “a * b = keyword * b”.
> And my ltac is something like this:
>
> Ltac simplify :=
> match goal with
> | [id:(_=?key) |- (_ = key * b)] => rewrite id.
> end.
> )
> In the example given, it is workable only because I specified the  
> operator (*). However, in the case where I don’t specify any  
> operator (e.g. (_ =key_)), this is completely not workable. Is there  
> any way I can perform regex matching in a generalized manner (e.g.  
> without specifying the operator)?

Yes, using the [context [ pat ]] pattern construction.
It is documented in the reference manual.

-- Matthieu