The Coq mailing list

[Wojciech Meyer <wojciech.meyer AT gmail.com>]

As a side comment (nothing to do with the excellent Gabriel's comment):

So in general, I don't like to use pattern of Ltac, I rather use bare
(well, let's say basic) tactics to do this. Ltac should be used in most
general cases where you want automated decisions rather than whole
tactic language. Surely that does not work always, but works for me. And
that's not because that Ltac is not simple enough, it's because it has
to be used for high level proofs. Also although Ltac is just very
pleasant to use, but should one should not fell into this trap so, it's
just even much better to do this for the other single or collection of
proofs even in the other module that needed automated decisions and
separate carefully the Ltac bits.

--
Wojciech


Gabriel Scherer 
<gabriel.scherer AT gmail.com>
 writes:

>> 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.
>
>> 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!