Coq：强制定义错误

【问题标题】：Coq: Error in coercion definitionCoq：强制定义错误
【发布时间】：2016-07-19 06:14:13
【问题描述】：

你能修复错误吗：

Parameter Arg: Type.
Parameter F X XP: Arg.
Parameter Sen Phy Leg Inf: Arg -> Prop.
Parameter tree car: Phy X.
Parameter mary john: Phy XP /\ Leg XP /\ Sen XP.
Fail Coercion c (u:Arg) (x y z: Arg -> Prop) (t:x u /\ y u /\ z u): x u := fun t => @proj1 (x u) (y u /\ z u) t.
(*The type of this term is a product while it is expected to be "x u".*)

当我使用这个词时，我遇到了同样的错误

Coercion f (u:Arg) (x y z: Arg -> Prop) (t:x u /\ y u /\ z u): x u. tauto. Defined. Print f.

【问题讨论】：

标签： definition coq coercion

【解决方案1】：

部分答案：您的fun t => @proj1 (x u) (y u /\ z u) t 术语的类型为x u /\ y u /\ z u -> x /\ u。您希望整个强制转换具有x u 类型，因此您需要为您的函数提供x u /\ y u /\ z u 类型的术语，以便获得x u。

我认为您因为fun t => proj1 t 而感到困惑。为避免混淆，您可以使用新名称重命名此变量，例如 fun foobar => proj1 foobar，您会发现您实际上从未使用过您的 t 参数。

因此，整个术语是(fun t => @proj1 (x u) (y u /\ z u) t) t，它适用于Definition。但在Coercion 的情况下，我收到以下消息：

c is defined
Warning: c does not respect the uniform inheritance condition

Error: Cannot find the target class.

【讨论】：