The Coq mailing list

[Patrick Loiseleur <Patrick.Loiseleur AT lri.fr>]

I'm not sure I've exactly understood what you mean. What gets you
confused is probably the difference between "Defined" and "Save", or
the difference between opaque and transparent constants. Please check
the manual for full explanations on this subject. Briefly :
transparent constants can be unfolded, when the opaque cannot.

The point here is not wether "my_eq_refl" is opaque or not, it's not
wether "my_eq_refl" has type "(reflexive nat my_eq)" or 
"(x:nat)(my_eq x x)", the point here it wether "reflexive" is opaque
or not.

In the following context :

<<<<<<<<<<<<<<<<<
Require Relations.
Section c.
Definition my_eq [x,y:nat] := True.
Lemma my_eq_refl : (reflexive nat my_eq).
Red; Intro; Unfold my_eq; Trivial. 
Save.
Hints Resolve my_eq_refl.
Lemma t : (my_eq O O).
>>>>>>>>>>>>>>>>>>>

The command "Info Auto" will solve the Goal and print out 

 == Apply my_eq_refl.

If now I type "Undo. Opaque reflexive. Apply my_eq_refl" I get an error:

Error: Impossible to unify reflexive with my_eq

(Of course Auto fails to solve the goal in this case)
The difference is that now Apply will not try to unfold the constant
"reflexive" during unification between the goal and "my_eq_refl",
because "reflexive" is opaque now.

That explains why it works when you make "reflexive" a syntactic
definition : a syntactic definition is a kind of super-transparent
constant : actually, it is systematically unfolded during the parsing.

I hope I understand your problem and gave the right answer.

Patrick



Dans son message du 3 février, Randy Pollack a écrit : 
> 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
> 

-- 
Patrick.Loiseleur AT lri.fr