Coq:为什么我需要手动展开一个值，即使它上面有 `Hint Unfold`？

我想出了以下玩具证明脚本:

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？提示还不够吗？

最佳答案

那是因为(见 refman )



并且目标 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.

关于Coq:为什么我需要手动展开一个值，即使它上面有 `Hint Unfold`？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/44767744/