The Coq mailing list

[t x <txrev319 AT gmail.com>]

Thanks for everyone's patient help. I think the problem here is that I'm confused about how ltac / goal states are working and thus unable to properly formulate a clear question.

Thus:

1) In Coq, just like how I can "Print" the definition of a function, can I also "Print" the definitions of tactics? (like: rewrite, refine, replace, exact) and see how they're implemented.

2) Is "refine" a Coq primitive (i.e. written in ocaml), or is it written in ltac? [and if so, where can I read the source]

Thanks!

On Thu, Jul 4, 2013 at 1:34 AM, Enrico Tassi <enrico.tassi AT inria.fr> wrote:

On Wed, Jul 03, 2013 at 10:24:14AM -0700, t x wrote:
> assert ( _statement_ ) as H0 by _tactic_ .
> pose proof (lemma ... H0 ...).

In ssreflect this could be expressed as

  have tmp : _statement_ by _tactic_.
  have {tmp} := lemma ... tmp ... .

where {tmp} is the syntax for clear, and have := is the anonymous
cut resulting in a new implication on top of your goal.

I see more compact ways only if know what you want to do with "lemma".
For example, if lemma proves an equality and you want to rewrite with it
you could even do that

  have -> := lemma ... (_ : _statement_) ...; last by _tactic_.

or

  rewrite (lemma ... (_ : _statement_) ...); last by _tactic_.

that follows Pierre's idea of using type inference to open a new goal.

Cheers
--
Enrico Tassi