coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Sean Wilson <sean.wilson AT ed.ac.uk>
- To: Vladimir Komendantsky <Vladimir.Komendantsky AT sophia.inria.fr>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] contextual match on goals
- Date: Wed, 4 Jun 2008 11:46:53 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
- Organization: School of Informatics, The University of Edinburgh
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
- [Coq-Club] contextual match on goals, Vladimir Komendantsky
- Re: [Coq-Club] contextual match on goals, Sean Wilson
- Re: [Coq-Club] contextual match on goals, Adam Chlipala
- Re: [Coq-Club] contextual match on goals, Sean Wilson
Archive powered by MhonArc 2.6.16.