Coq：爲什麼我需要手動展開一個值，即使它有一個'提示Unfold`？

Question

我已經想出了下面玩具證明腳本：

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. 

爲什麼我需要手動展開myValue這裏？不應該提示足夠嗎？

Answer 1

這是因爲（見refman）

這[Hint Unfold <qualid>]增加了戰術unfold qualid當目標的頭常數的ident將只使用提示列表。

而且目標myProp myValue具有myProp在頭部位置，不會myValue。

有處理這幾種方法：

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

或

Hint Extern 4 => unfold myValue. 

甚至

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

Answer 2

@AntonTrunov是正確的，他的解釋，爲什麼不使用Hint Unfold這裏。還有一個替代方案Hint Transparent，它使應用程序對某些特定的常量以模數增量運行。看起來還沒有trivial和auto的支持，但支持eauto，你可以在下面看到：

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.