The Coq mailing list

[t x <txrev319 AT gmail.com>]

1) Thanks for the "refine" suggestion -- the tactic makes more sense now.

2) This isn't what I want. I tried to write out a block of code showing the "difference"

https://gist.github.com/anonymous/da4717b490952d2414fb

These are the distinctions in my mind:

  ## style 1:

  * functional: this function call will create a proof of the style you want (i.e. "gen")

  * function used to generate tactic is inline

  ## style 2:

  * imperative: let's assume this and add it as a subgoal

  * we generate lots of sub goals, and we have to track which subgoal we're dealing with and which tactic to use (admittedly, in this case, all of them uses "reflexivity"; but in a world where we're using different tactics for the branches, this is harder to read / keep track of [like if we added an extra subgoal in the middle, and now everything has to shift by one]).

If what I'm doing here is against the grain, please call me out on it. It seems that most Coq techniques is built around "let's assume this, and prove it as a subgoal", whereas what I want is a bit more functional "let's construct this, then use it."

Does this distinction make sense, or am I being pedantic? :-)

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

On 03/07/2013 20:28, t x wrote:

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.

I if understand correctly, you want to be sure to solve the generated goal. To this intent, you may use the [solve] tacticial. This gives:

refine ((fun (H0 : _statement_) => _ (lemma ... H0 ...)) _);

[ | solve[_tactic_] ].

Is that what you want ?

PMP