Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] coqide / ltac support

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] coqide / ltac support


Chronological Thread 
  • From: Pierre Casteran <pierre.casteran AT labri.fr>
  • To: Math Prover <mathprover AT gmail.com>
  • Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] coqide / ltac support
  • Date: Sun, 16 Jun 2013 17:07:51 +0200

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!






Require Import List . 

Section assocList.

  Variable K: Type.
  Variable V: Type.
  Variable Keq: forall k1 k2: K, {k1 = k2} + {k1 <> k2}.
  Variable Veq: forall v1 v2: V, {v1 = v2} + {v1 <> v2}.
  
  Function assocList_r (lst: list (K * V)) (k: K) (d: V) : V :=
    match lst with
    | nil => d
    | (k',v') :: xs => if Keq k k' then v' else assocList_r xs k d
    end.

  Function assocList_del (lst: list (K * V)) (k: K) : list (K * V) :=
    match lst with
    | nil => nil
    | (k',v') :: xs => if Keq k k' then assocList_del xs k else (k',v') :: assocList_del xs k
    end.

  Function assocList_w (lst: list (K * V)) (k: K) (v: V) : list (K * V) :=
    (k,v) :: assocList_del lst k.


  Ltac break_if :=
    match goal with
    | [ |- context [if ?tst then _ else _]] => destruct tst
    end.

  Ltac break_pair1 :=
    match goal with
    | [ |- context [ (_, _) = ?a ]] => destruct a
    end.

  Ltac break_pair2 :=
    match goal with
    | [ |- context [ prod _ _ = ?a ]] => destruct a
    end.


  Lemma lem1:
    forall (k1: K)
           (k2: K)
           (d: V)
           (lst: list (K * V)),
      k1 <> k2 ->
        assocList_r lst k1 d =
          assocList_r (assocList_del lst k2) k1 d.
  intros; induction lst.
    (* case 1 *)
    reflexivity.
    (* case 2 *)
      simpl.
destruct a;break_if.
break_if.
destruct H;transitivity k;eauto.
simpl.
break_if;auto.
destruct n0;auto.
break_if.
auto.
rewrite IHlst.
simpl.
break_if.
destruct n;auto.
auto.
Qed.






Archive powered by MHonArc 2.6.18.

Top of Page