The Coq mailing list

[Math Prover <mathprover AT gmail.com>]

Hi Pierre,

  With apologies for not making this clear: it does not work on the fail.v I attached. I'm using Coq 8.4pl2.

  In particular, on line 79, if I try to use either "break_if" or "break_pair1", Coq complains and says it can't match the pattern.

  "break_pair2" is me being stupid and misreading the constructor for pair.

On Sun, Jun 16, 2013 at 5:01 AM, Pierre Casteran <pierre.casteran AT labri.fr> wrote:

Hi,

  I looked at your attached file:

On which  kind of examples break_if doesn't work ?

On a small example, it works, as well as some variants I attached to this mail.

break_pair1 seems to work to, although it works only on goals containing an equality  (?x,?y)=t

But I don't understand how to use break_pair2 :

  It would need an equality of the form (T1 * T2) = T3, but how to destruct T3 ??


Pierre

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