The Coq mailing list

[Matthieu Sozeau <Matthieu.Sozeau AT lri.fr>]

Le 2 févr. 09 à 10:03, JAEGER, Eric (SGDN) a écrit :

> Hi,
>
> (Warning : my text IS confusing, sorry for that, so you can skip it  
> and go below the line to see the real question).
>
> I've encountered a small difficulty when dealing with tactics in a  
> development using intensively notations, coercions, and decision  
> functions. Basically, I'm trying to write a tactic looking for  
> hypothesis of the form "f(CONS t)" where f is a transparent function  
> and CONS a constructor - to simplify this hypothesis into a simpler  
> one (or several simpler ones). I have a proof of "my_simpl:forall  
> (t:T)(s:S), f(CONS t)=s->f(t)=s".
>
> However, when I'm trying to write s.t. like:
>
> repeat (match goal with | Hfr:f(CONS _)=_ => generalize (my_simpl _  
> _ Hfr); clear Hfr; intros Hfr)
>
> This does not work... Probably because my function f defined as a  
> fixpoint can be simplified such that f(CONS t)=f(COER t)=f'(t) (COER  
> being a coercion). So it seems that there are conversions going on  
> preventing the match.

I don't think [match goal] involves any conversion but it does not  
typecheck patterns either.
You may want to use the [Debug On] command to investigate the bug  
further. After this command,
you have to switch to the *coq* buffer (in ProofGeneral, don't know  
about coqide) to enter the
debug mode of Ltac. You have to reissue a [Debug Off] command to get  
out of it, it has a
non-undoable side-effect.

Hope this helps,
-- Matthieu