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）

This [Hint Unfold <qualid>] adds the tactic unfold qualid to the hint list that will only be used when the head constant of the goal is 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 is not used here. There is the alternative Hint Transparent that makes the application work modulo delta for some specific constants. It seems not to be yet supported by trivial and auto but is supported by 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.

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

Coq: why do I need to manually unfold a value even though it has a `Hint Unfold` on it?

coq

coq-tactic