The Coq mailing list

[Christine Paulin <paulin AT lri.fr>]

Dear Randy,

Actually, because the type of my_reflexive does not start with a 
product, the tactic Apply my_reflexive is expected to perform head
reduction until we get one product.
Also Hint Resolve my_reflexive should save both 
Apply my_reflexive (when the current goal is (my_eq a b) 
and Exact my_reflexive when the current goal is (reflexive ..)

So if you don't get this behavior it is a bug, please send us the 
example.

On the other hand it is true that except in this case, no constant
expansion is performed by the Apply tactic in order to get a succesful
match. In your second example s_refl has type 
(S:Setoid)(reflexive s_eq) , it starts with a product such that reflexixe is 
not expanded. 
One thing could be to adapt the Apply tactic such that it performs
expansion in order to succeed (as in LEGO if I remember correctly)
I would like to know what is your feeling on that point.

A more explicit way would be to have a tactic 
  Apply lemma [reduction_tactic]
which performs expansion of the type of lemma following the expansion
  strategy indicated by the reduction_tactic before performing
  application.

Then using reduction on the goal and on the type of the lemma should
allow the user to obtain the adequate formulation such that the
limited Coq unification succeeds.

Then there is no need to expanse the Hint grammar because the Hint
Extern facility can be used for that.

It should not be too much work to write such a tactic. 
(adapt the res_pf tactic such that it takes a reduction strategy as argument)
Freek seems to be willing to try ?

Best regards,
Christine.


In his message of Wed March 3, 1999, Randy Pollack writes: 
> Say I have some lemma:
> 
>   Lemma my_reflexive: (reflexive my_eq).
> 
> I want to use it as in "Apply my_reflexive" or 
> "Hints Resolve my_reflexive".
> 
> However, due to the defined term "reflexive" these uses of
> "my_reflexive" don't work as desired.  I have been writing:
> 
>   Definition my_reflexive_unfolded : (x:S)(my_eq x x) := my_reflexive.
> 
> This gives an unfolded version of the lemma for use in Hints, and
> still guarantees that the unfolded form *really is* the correct
> meaning of reflexive (the human reader doesn't have to check
> "(x:S)(my_eq x x)" against "reflexive").
> 
> I want some way to avoid the need for the definition
> "my_reflexive_unfolded".  What do you suggest?  Is there
> 
> One answer I see is to use "Syntactic Definition" for "reflexive"
> 
>   Syntactic Definition reflexive := (x: A)(R x x).
> 
> Now "reflexive" is always expanded.  But this isn't very nice.  Is
> there some way to expand the head constant of the type of a Hint
> without actually writing the expanded form down?
> 
> Randy

-- 
  Christine Paulin-Mohring             mailto : 
Christine.Paulin AT lri.fr
  LRI, URA 410 CNRS, Bat 490, Université Paris Sud,   91405 ORSAY Cedex 
  LRI   tel : (+33) (0)1 69 15 66 35       fax : (+33) (0)1 69 15 65 86
  INRIA tel : (+33) (0)1 39 63 54 60       fax : (+33) (0)1 39 63 56 84
  Tatoo tel : 06 04 24 44 75