coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] contextual match on goals

From: Adam Chlipala <adamc AT hcoop.net>
To: Sean Wilson <sean.wilson AT ed.ac.uk>
Cc: Vladimir Komendantsky <Vladimir.Komendantsky AT sophia.inria.fr>, coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] contextual match on goals
Date: Wed, 04 Jun 2008 08:33:34 -0400
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Sean Wilson wrote:

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.

I think that depends on your definition of "more involved." I've been able to get a completely automated proof of CPS translation correctness for almost-core-ML, using just Ltac, so my default Ltac optimism level is high. Context patterns can help a lot for getting around inability to crawl variable-arity AST nodes.

[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