The Coq mailing list

[Math Prover <mathprover AT gmail.com>]

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!

Attachment: fail.v
Description: Binary data