The Coq mailing list

[Math Prover <mathprover AT gmail.com>]

Pierre, Jason:

  This makes sense now. My failure in understanding was exactly this:

Pierre:

>> Anyway, your fail.v example works with your break_if tactic once I destruct the

a in the "let (k',v') := a in <term> "

Jason:

>> The problem is that k' and v' are meaningless at top level; a manual [destruct Keq k1 k'] will fail because Coq doesn't know what k' is.

I can best phrase my previous failure as follows: "Those variables don't exist until you break the let; therefore you can't destruct on them until you destruct the let first."

Anyway, thanks for everyone's help in debugging my confusing question.

On Sun, Jun 16, 2013 at 9:09 AM, Jason Gross <jasongross9 AT gmail.com> wrote:

The problem is that k' and v' are meaningless at top level; a manual [destruct Keq k1 k'] will fail because Coq doesn't know what k' is.

You could do something like

repeat match goal with | [ |- appcontext[match ?E with _ => _ end] ] => destruct E end

to destruct both the lets and the ifs, though it might be a bit more powerful than you want.

-Jason

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

Hu,

 I'm not sure the "context" notion in Ltac captures subterms of
match or destructuring let expressions (Perhaps someone in the list will confirm ?)

Anyway, your fail.v example works with your break_if tactic once I destruct the
a in the "let (k',v') := a in <term> "

I attach a solution that works. It is not well written in cpdt's sense, but writing
Coq scripts while listening at John Coltrane's music is a quite difficult exercise :-)

Pierre




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