The Coq mailing list

[t x <txrev319 AT gmail.com>]

(apologies if I'm misunderstanding your idea)

Technique1 = refine ((fun ... )) described above

Technique2 = 

  "extracting the proof term generated by

    assert(_statement_) as H0 by _tactic_ "

stylistically (perhaps this reflects my lack of experience), I'd really like to do:

Command1 = pose proof ... [somehow extract the term generated by assert(_statement_) ... by _tactic_]

To me, this seems easier to debug -- in that suppose I fail to solve the goal. Then, in T1, I end up having an extra goal (and when dealing with large proofs with 20 subgoal and handling them in parappel, it's not obvious to me where it's coming from. In T2, hopefully I get an type error directly at Command1 because I couldn't provide the term.

Furthermore, as I do more proof manipulation, I feel that I more and more want something of T2 -- to be able to say: "generate a type of this form for me using this tactic."

On Wed, Jul 3, 2013 at 10:44 AM, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

On 03/07/2013 19:26, t x wrote:

With apologies for 2 emails in rapid succession -- I realized what I wanted
in the first case is "replace ... with .... by ... ". However, I'm still
not sure how to solve the 2nd case (inlining with pose proof ... ).

To do the following:

assert ( _statement_ ) as H0 by _tactic_ .
pose proof (lemma ... H0 ...).

I would use the following trick:

refine
  ((fun (H0 : _statement_) => _ (lemma ... H0 ...)) _); [ |_tactic_].

You can use a tactic notation to do this more neatly, but it should work anyway.

PMP