The Coq mailing list

[Gyesik Lee <gslee AT ropas.snu.ac.kr>]

Hi Florent,

what I learned last time is that it is not possible to write down a
tactic which "universally" destructs all kind of inductive types.
(I am not sure if I understood it correctly)
Instead a different tactic should be used for each inductive type on
which you apply the pattern matching.
In your case,

Ltac case_at_head :=
  match goal with
    | |- context [ match ?X with
                  | Some _ => _
                  | None   => _
                end ]
    => case_eq X
  end.

does what you want. (That is, the part in "context [ ... ]" should be
changed depending on the inductive type.)

=========================

Parameter a : nat -> Prop.
Parameter b : Prop.

Goal forall (f:nat -> option nat) (n: nat)(H1 : forall k, a k)(H2 : b),
  match f n with
  | Some k => a k
  | None => b
  end.
Proof.
intros; case_at_head; auto.
Qed.

==========================

Cheers,

Gyesik





10/9/16 Florent Becker 
<florent.becker AT ens-lyon.org>:
> -----BEGIN PGP SIGNED MESSAGE-----
> Hash: SHA1
>
> Le 02/07/2010 15:08, Adam Chlipala a écrit :
>> Gyesik Lee wrote:
>>> Then I tried with
>>>
>>> Ltac toto :=
>>>    match goal with
>>>       | |- context [ match ?T with | _ =>  _ end ] =>  idtac
>>>    end
>>>
>>> The error message now:
>>>
>>> Error: Non supported pattern.
>>>
>>
>> For now, you need to supply every pattern-match case, in enough detail
>> to make clear which type you're matching on.  It gets bothersomely
>> verbose and prevents genericity, but it makes some sense if you look at
>> the internal representation of Gallina terms.
>>
>
> I have run into the same problem while trying to define the following
> tactic:
>
> Ltac case_at_head :=
>    match goal with
>       | |- [ match ?T with | _ =>  _ end ] =>  case_eq T
>    end
>
>
> Does an equivalent tactic exist somewhere? I'd like to be able to solve
> goals like this:
>
>    f : nat -> option nat
>    n : nat
>    H1 : forall k, a k
>    H2 : b
>  ============================
>   match f n with
>   | Some k => a k
>   | None => b
>   end
>
> without having to mention (f n), so that i can solve them automatically
> (by 'case_at_head; auto')
>
> As far as I can tell, I'd need to implement that tactic as an ocaml
> plugin, but I've not been able to find documentation on how to do that.
>
> Thanks for any pointers,
>
> Florent
> -----BEGIN PGP SIGNATURE-----
> Version: GnuPG v1.4.10 (GNU/Linux)
> Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
>
> iEYEARECAAYFAkySDtEACgkQTCPcDztjGo7ffACeOx/QL9XLBrLKrsjWa/608HV4
> BKgAoJF+k7kQa/QN0TnhadIqLCtRrdU1
> =KNiH
> -----END PGP SIGNATURE-----
>