The Coq mailing list

[Math Prover <mathprover AT gmail.com>]

Figured it out. I want:

    match goal with

      | |- context [if ?tst then _ else _ ]  => destruct tst

    end.

instead.

However, 1) I have no idea why this works; and 2) I still don't know how to use proof-general/ltac. :-)

On Sun, Jun 16, 2013 at 1:20 AM, Math Prover <mathprover AT gmail.com> wrote:

Hi,

  I've installed proof-general and set "Set Ltac Debug." This is the results from just hitting <enter>. Can someone help me get started on debugging this? (This is installed on a separate machine; it has Coq 8.4pl2 compiled from source; but not access to CpdtTactics).

The details of what I'm using:

x@ubuntu:~$ proofgeneral --version

GNU Emacs 23.4.1

Copyright (C) 2012 Free Software Foundation, Inc.

GNU Emacs comes with ABSOLUTELY NO WARRANTY.

You may redistribute copies of Emacs

under the terms of the GNU General Public License.

For more information about these matters, see the file named COPYING.

x@ubuntu:~$ coqtop -v

The Coq Proof Assistant, version 8.4pl2 (June 2013)

compiled on Jun 16 2013 00:41:24 with OCaml 3.12.1

On Sat, Jun 15, 2013 at 11:52 PM, Math Prover <mathprover AT gmail.com> wrote:

Hi,

  I'm clearly doing something very stupid with ltac / match goal. However, it's not clear to me where my stupidity lies.

  Attached is a minimal example of failure.

  In particular, I can't:

  (*) break ifs

  (*) break pairs

  Please let me know what I'm mis-using. To help debug my error, here is my mental model of how things *should* work

Take for example

  Ltac break_if :=

    match goal with

    | [ |- context [if ?tst then _ else _]] => destruct tst

    end.

when I run "break_if" I expect the following to happen:

  1. Coq looks at my current state.

  2. It tries to find a "sub _expression_" of the goal that looks like "if ?tst then _ else _"

  3. I expect ?tst to be binding against either " Keq k1 k' " or " Keq k2 k' " (I actually don't care which).

  4. Then, I expect coq to do a " destruct (Keq k1 k') " or a " destruct (Keq k2 k') "

Thanks!