The Coq mailing list

["JAEGER, Eric (SGDN)" <eric.jaeger AT sgdn.gouv.fr>]

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.

 

If on the contrary I write:

 

repeat (match goal with | Hfr:f(_)=_ => try (generalize (my_simpl _ _ Hfr); clear Hfr; intros Hfr))

 

That is, looking for ANY hypothesis f(t) then trying to apply my-simpl (and failing if t is not of the form f(CONS t)), it is more efficient... But can cause Coq crashes when I've hypothesis of the form "H:f(_)=g(_)". Again apparently there are too many conversions (beta-reduction, unfolding, etc.) going on.

 

I'm sorry to be unclear, I've not been able to replay the same scenario in a simple example (I need a rather complex mix of notations, coercions and functions).

 

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

 

I've investigated possible solutions. I've identified three "fixes" that would be ok:

1/ Making opaque the function "f" to prevent conversions, applying the tactic, then making f transparent again; yet "Opaque" and "Transparent" are not part of the Ltac language.

2/ Marking those hypotheses that my tactic has already tried to simplify just to avoid never ending loops; but I do not know how to do that efficiently and elegantly using the Ltac language.

3/ Identifying that a simplification has been without effect (using a tactic "simpl" failing when doing nothing - as "progress" works - OR being able to compare two hypothesis to see if they are equal - not equivalent, convertible, but really equal) in the Ltac language.

4/ Being able to use a form of "string match" on strings mixing notations, coercions, functions to prevent conversions.

 

Is any of those possible using only the LTAC language?

 

    Thanks in advance,

    Regards, Eric