The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I do not know much about style 1, though I think there is a style of proof using [proof.] (with a lowercase "p"), and things like [have].  Parhaps someone else can say more.

I do not think about style 2 the same way that you do.  For me, it is a failure if my tactic is not robust to goal reordering.  I generally use [match goal with ... end] to determine what the goal looks like sufficiently well to figure out what tactics to use.  I tend to look at Ltac as a brute force hammer; ideally, I give Coq a bunch of ways to solve goals, and have it apply them brute-force to all the goals until they are discharged.

I hope this helps.

-Jason

On Jul 3, 2013 3:42 PM, "t x" <txrev319 AT gmail.com> wrote:

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