coq - 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到提示列表中，该策略仅在目标的头部常量为 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.