Coq: pourquoi ai-je besoin de déplier manuellement une valeur même si elle contient un `Hint Unfold`?

Question

Je suis venu avec le script preuve de jouet suivant:

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. 

Pourquoi ai-je besoin de déployer manuellement myValue ici? L'indice ne devrait-il pas suffire?

Answer 1

En effet, (voir refman)

Ce [Hint Unfold <qualid>] ajoute la tactique unfold qualid à la liste d'indices qui ne sera utilisé lorsque la constante de la tête de l'objectif est ident.

Et le but myProp myValue a myProp dans la position de la tête, et non myValue.

Il y a plusieurs façons de traiter ceci:

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

ou

Hint Extern 4 => unfold myValue. 

ou même

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

Answer 2

@AntonTrunov est correct dans son explication sur les raisons Hint Unfold n'est pas utilisé ici. Il y a l'alternative Hint Transparent qui fait fonctionner l'application modulo delta pour certaines constantes spécifiques. Il ne semble pas être encore pris en charge par trivial et auto mais est pris en charge par eauto comme vous pouvez le voir dans ce qui suit:

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.