Coq：为什么我需要手动展开一个值，即使它上面有一个“ Hint 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到提示列表中，该列表仅在标识目标的开头常量时才使用。

而目标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.