The Coq mailing list

[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-----