The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

The problem is that [*] is, by default, interpreted as [mult], unless it occurs in [type_scope].  You can find this out by [Locate "*".].  You can fix this by replacing [?K * ?V] with [(?K * ?V)%type], or with [Local Open Scope type_scope.], or with [Local Close Scope nat_scope.].  Read http://coq.inria.fr/V8.4/refman/Reference-Manual014.html#hevea_default785 for more information about interpretation scopes.

So your tactic was looking for things of the type [x * y] where [x] and [y] are both [nat]ural numbers, and no hypothesis has such a type (because natural numbers are not types).  I have submitted an enhancement request at https://coq.inria.fr/bugs/show_bug.cgi?id=3050 to default to [type_scope] for Ltac hypotheses.  I suspect that this is not currently done because Ltac code is untyped.

-Jason

On Sat, May 25, 2013 at 5: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!