The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

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_if':=
    match goal with
    | [ |- context [if ?tst then _ else _]] => case_eq tst
    end.


Ltac break_if'' tst :=
    match goal with
    | [ |- context [if tst then _ else _]] => case_eq 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.

Goal forall b:bool, (if b then 1 else 2) = (if (negb b) then 2 else 1).
intro b.
break_if.
break_if'' (negb true).
discriminate.
auto.
auto.
Qed.

Goal forall (n p:nat) x, (n,p) = x -> n = fst x.
intros n p x; break_pair1.
now injection 1.
Qed.