The Coq mailing list

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

Sure, but I'm also not very accustomed with Ltac yet. That was a general
comment.

> Given that your hypothesis is (A = (3,4) /\ (x,y) = A), you apparently
> want to destruct over (foo /\ bar) rather than (foo * bar).

Wouldn't `split' or `elim' tactic combined with `destruct' work?

It does not mean it's the only way however.

best,
Wojciech

Math Prover 
<mathprover AT gmail.com>
 writes:

> On Sat, May 25, 2013 at 5:45 PM, Wojciech Meyer
> <wojciech.meyer AT gmail.com>
>  wrote:
>
>     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.
>
>
> I'm new to Ltac / automated proving. Can you provide an example of how
> "bare tactics" would work in the above example? [It's likely that I'm
> doing terribly un-idiomatic things without even realizing that they're
> stupid.]
>
>
>  
>
>     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!
>
>

--
Wojciech