The Coq mailing list

[Math Prover <mathprover AT gmail.com>]

In which case, why did Coq accept the Ltac, but not apply it? It seems to me if it didn't recognize the syntax, then the error should have happened when I defined tac00"

On Sat, May 25, 2013 at 2:15 AM, Math Prover <mathprover AT gmail.com> wrote:

Gabriel: I want to destruct the product, not the and. Thanks for pointing me at https://github.com/trefis/coquille

Auger: this fixed it, thanks!

So I guess my problem was: "*" notation syntax is not supported in Ltac?

On Sat, May 25, 2013 at 2:06 AM, AUGER Cédric <sedrikov AT gmail.com> wrote:

Le Sat, 25 May 2013 10:39:06 +0200,
Gabriel Scherer <gabriel.scherer AT gmail.com> a écrit :

> > 1) What am I doing wrong in this particular example?
>
> Given that your hypothesis is (A = (3,4) /\ (x,y) = A), you apparently
> want to destruct over (foo /\ bar) rather than (foo * bar). Changing
> your tactic from
>
> match goal with
>   | p: ?K * ?V |- _ => ...
>
> to
>
> match goal with
>   | p: ?K /\ ?V |- _ => ...
>
> works fine on my machine.

Well, I guess that he wants to destruct (A : prod nat nat) rather than
(H : A = (3, 4) ∧ (x, y) = A).

I did not tested it, but what happens if you replace "p : ?K * ?V" with
"p : prod ?K ?V"?

I do not know if in these conditions type_scope is active, or if it is
nat_scope.

>
> > I don't know emacs. I don't know proof general. Is there any other
> > way to debug ltac?
>
> I'm not sure what you mean by "debug Ltac", but regarding coq-modes,
> you may consider giving Emacs a try (it is rather easy to use in a
> simple way, and I know some long-time vimers use Emacs just for
> Proof-General). There is also a fairly young project or providing a
> proof-general-like interface for Vim, named "Coquille" (
> https://github.com/trefis/coquille ). It's in an early stage of
> development, but you may give it a try.
>
> On Sat, May 25, 2013 at 10:19 AM, Math Prover <mathprover AT gmail.com>
> wrote:
> > There are two separate questions here:
> >
> > 1) What am I doing wrong in this particular example and
> >
> > 2) What should I use in general?
> >
> > ### What am I doing wrong in this example?
> >
> > I want a tactic that destructs pairs (this is not what I want to
> > do, this is my minimal failure case). Yet, when I type in "tac00",
> > I get:
> >
> > |Error: No matching clauses for match goal
> > |       (use "Set Ltac Debug" for more info).
> >
> >
> > ### How do I debug Ltac?
> >
> > I have used Vim for 10+ years. I have used both CoqIde and Matthieu
> > Cartier's http://www.vim.org/scripts/script.php?script_id=4388 .
> >
> > I don't know emacs. I don't know proof general. Is there any other
> > way to debug ltac?
> >
> > Thanks!