The Coq mailing list

[Sean Wilson <sean.wilson AT ed.ac.uk>]

On Wednesday 04 June 2008 11:25:48 Vladimir Komendantsky wrote:
> Is this possible to write a tactic in the Ltac language that would match
> goals of the kind
>
> |- (f ...) <= (g ...)
>
> where arities of f and g are arbitrary? Also I have the same question
> regarding goals like

I've very sure you can't do this in Ltac. I've seen other people work around 
this by using several match clauses that match against functions with 
increasing numbers of parameters e.g.

f x => idtac f x
f x y => idtac f x y
f x y z => idtac f x y z
...

This will obviously fail if a function comes along with too many parameters. 
You can add clause at the end that matches all patterns with a helpful "fail" 
message to help locate this problem if this happens.

> |- (match x with ...) <= (match y with ...)
>
> where the bodies of match clauses are not cared about. 

I'm fairly sure this isn't possible either. You need to give the exact 
structure of the match clause to look for or the pattern won't match.

> I'm writing my tactic in OCaml but I'd be grateful if someone suggests me 
how to use Ltac for this purpose.

I've found that issues like the above in Ltac, and others including easy ways 
of accessing a database of rules, means you really need the extra power that 
OCaml gives you to write more involved tactics.

Regards,

Sean