Coq: why do I need to manually unfold a value even though it has a `Hint Unfold` on it?

Question

I've come up with the following toy proof script:

Inductive myType : Type :=
| c : unit -> myType.

Inductive myProp : myType -> Type :=
| d : forall t, myProp (c t).
Hint Constructors myProp.

Definition myValue : myType := c tt.
Hint Unfold myValue.

Example test: myProp myValue.
Proof.
  auto 1000. (* does nothing *)
  unfold myValue.
  trivial.
Qed.

Why do I need to manually unfold myValue here? Shouldn't the hint suffice?

Obscuration

Answer 1

That's because (see refman)

This [Hint Unfold <qualid>] adds the tactic unfold qualid to the hint list that will only be used when the head constant of the goal is ident.

And the goal myProp myValue has myProp in the head position, not myValue.

There are several ways of dealing with this:

Hint Extern 4 => constructor.   (* change 4 with a cost of your choice *)

or

Hint Extern 4 => unfold myValue.

or even

Hint Extern 1 =>
  match goal with
  | [ |- context [myValue]] => unfold myValue
  end.

Enrika

Answer 2

@AntonTrunov is correct in his explanation on why Hint Unfold is not used here. There is the alternative Hint Transparent that makes the application work modulo delta for some specific constants. It seems not to be yet supported by trivial and auto but is supported by eauto as you can see in the following:

Inductive myType : Type :=
| c : unit -> myType.

Inductive myProp : myType -> Type :=
| d : forall t, myProp (c t).
Hint Constructors myProp.

Definition myValue : myType := c tt.
Hint Transparent myValue.

Example test: myProp myValue.
Proof.
  eauto.
Qed.

Sword