The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

JAEGER, Eric (SGDN) wrote:
> 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
>   
1/ If you want to prevent computation on some function, you may want to 
control how
values are computed:

For instance,

match goal with Hfr : f(CONS ?x) = ?w =>
  let v := eval lazy beta iota zeta delta -[g g'] in x in assert (Hfr' 
: f x = w)
      by exact (my_simpl _ _ Hfr)
end

This would compute on (f x), but keep control on the functions that are 
allowed to get
reduced.  This may help you get closer to playing with transparent and 
opaque.

2/ Whenever you try an hypothesis, you can move it to the goal, by 
generalizing it and clearing it. At the end of your process, you move 
everything back to the context.

You probably thought about these, but just in case.


Yves