coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club] coqide / ltac support, Math Prover, 06/16/2013
- Message not available
- [Coq-Club] Re: coqide / ltac support, Math Prover, 06/16/2013
- Message not available
- Re: [Coq-Club] coqide / ltac support, Pierre Casteran, 06/16/2013
- Re: [Coq-Club] coqide / ltac support, Math Prover, 06/16/2013
- Re: [Coq-Club] coqide / ltac support, Pierre Casteran, 06/16/2013
- Re: [Coq-Club] coqide / ltac support, Jason Gross, 06/16/2013
- Re: [Coq-Club] coqide / ltac support, Math Prover, 06/17/2013
- Re: [Coq-Club] coqide / ltac support, Pierre Courtieu, 06/17/2013
- Re: [Coq-Club] coqide / ltac support, Math Prover, 06/17/2013
- Re: [Coq-Club] coqide / ltac support, Jason Gross, 06/16/2013
- Re: [Coq-Club] coqide / ltac support, Pierre Casteran, 06/16/2013
- Re: [Coq-Club] coqide / ltac support, Math Prover, 06/16/2013
Archive powered by MHonArc 2.6.18.