The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

Yes, basically "tac1 ; tac2 ; tac3." is not equivalent to "tac1 ; body_of_tac2; tac3", but "tac1; (body_of_tac2); tac3." and the parenthesis are important.


Definition eqb (x y : bool) : Prop := if x then if y then True else False else if y then False else True.

Lemma test1 : forall x y, eqb x y -> x = y.
Proof.
  intros x y.
  case x; (case y; [intros []; split|intros []; split]).
Qed.

Lemma test2 : forall x y, eqb x y -> x = y.
Proof.
  intros x y.
  (case x; case y); [intros []; split|intros []; split|intros []; split|intros []; split].
Qed.

As far as I know, the default behaviour of ";" is to be left associative (cf test2).
=====================================
Thus a "idtac; [idtac|fail..]" tactic defined in Ltac would be equivalent to inserting "(idtac; [idtac|fail..])" which is pretty useless as "idtac" cannot generate goals.

I wonder if TacticNotations could deal with it, though…

2014-06-13 17:34 GMT+02:00 Jason Gross <jasongross9 AT gmail.com>:

It doesn't actually work for the same reason "idtac; []" doesn't work; it fails with "Not enough subgoals" if you have no goals left.  The "bug" is that some things, like square brackets, have special behavior with respect to semicolons, which are lost if you stick them inside a tactic.

-Jason

On Fri, Jun 13, 2014 at 4:31 PM, Jonathan <jonikelee AT gmail.com> wrote:

On 06/13/2014 11:25 AM, Jonathan wrote:

How about:

idtac; [idtac|fail..].

Oh - that doesn't work when defined as a tactic, but does if it's inlined.  Weird.  How can that not be a bug?

On 06/13/2014 11:16 AM, Jason Gross wrote:

Actually, my [at_most_one_goal_left] tactic doesn't work.  Is there a way
to detect "zero or one goals"?


On Fri, Jun 13, 2014 at 4:11 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

Hi,
Is there a standard way of asking the question "are all goals solved?" and
"is there at most one goal left?" in Ltac?

I can use "; solve [ idtac ]" to mean "fail if there are any goals left",
and I have been using "; []" to detect "exactly one goal left", and and I
can define a tactic
   Ltac at_most_one_goal_left := idtac; [].
so that "; at_most_one_goal_left" will fail if there is more than one
goal.  But is seems poor that inlining a tactic definition changes its
behavior; am I simply exploiting a bug?

-Jason

--
.../Sedrikov\...