如何为构造函数设置隐式参数
How to set implicit parameters for constructor
玩 nostutter 练习时我发现了另一个奇怪的行为。这是代码：
Inductive nostutter {X:Type} : list X -> Prop :=
| ns_nil : nostutter []
| ns_one : forall (x : X), nostutter [x]
| ns_cons: forall (x : X) (h : X) (t : list X), nostutter (h::t) -> x <> h -> nostutter (x::h::t).
Example test_nostutter_manual: not (nostutter [3;1;1;4]).
Proof.
intro.
inversion_clear H.
inversion_clear H0.
unfold not in H2.
(* We are here *)
specialize (H2 eq_refl).
apply H2.
Qed.
展开后的状态是这样的：
1 subgoal (ID 229)
H1 : 3 <> 1
H : nostutter [1; 4]
H2 : 1 = 1 -> False
============================
False
当我在 IndProp.v 中 运行 specialize (H2 eq_refl). 加载其他逻辑基础文件时，它起作用了。它以某种方式理解它需要将“1”作为参数。 IndProp.v的Header是这样的：
Set Warnings "-notation-overridden,-parsing".
From LF Require Export Logic.
Require Import String.
Require Coq.omega.Omega.
当我将代码移动到另一个文件 "nostutter.v" 时，同样的代码给出了预期的错误：
The term "eq_refl" has type "RelationClasses.Reflexive Logic.eq" while
it is expected to have type "1 = 1".
Header 共 nostutter.v:
Set Warnings "-notation-overridden,-parsing".
Require Import List.
Import ListNotations.
Require Import PeanoNat.
Import Nat.
Local Open Scope nat_scope.
我必须明确地向 eq_refl 添加一个参数：specialize (H2 (eq_refl 1)).
我认为这与专门化无关。它是什么？如何修复？
问题是导入 PeanoNat.Nat。
当您导入 PeanoNat 时，模块类型 Nat 进入作用域，因此导入 Nat 会引入 PeanoNat.Nat。如果您打算导入 Coq.Init.Nat，则必须在导入 PeanoNat 之前导入它，或者使用 Import Init.Nat..
导入它
为什么在这种情况下导入 PeanoNat.Nat 会造成麻烦？
Arith/PeanoNat.v (static link) 包含模块1 Nat。在该模块中，我们发现2 看起来不寻常的行
Include NBasicProp <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
All this means is that each of NBasicProp, UsualMinMaxLogicalProperties and UsualMinMaxDecProperties are included, which in turn means that everything defined in those modules is included in the current module. Separating this line out into three Include commands, we can figure out which one is redefining eq_refl. It turns out to be NBasicProp, which is found in this file (static link)。我们还没有到那里： eq_refl 的重新定义不在这里。但是，我们根据 NMaxMinProp.
来查看 NBasicProp 的定义
这将我们引向 NMaxMin.v，进而将我们引向 NSub.v，将我们引向 NMulOrder.v，将我们引向 NAddOrder.v，进而将我们引向 NAddOrder.v到 NOrder.v，这导致我们 NAdd.v，这导致我们 NBase.v，...
我将切入正题。最终我们在 Structures/Equality.v (static link) 中以模块 BackportEq 结束，它最终给了我们对 eq_refl.
的重新定义
Module BackportEq (E:Eq)(F:IsEq E) <: IsEqOrig E.
Definition eq_refl := @Equivalence_Reflexive _ _ F.eq_equiv.
Definition eq_sym := @Equivalence_Symmetric _ _ F.eq_equiv.
Definition eq_trans := @Equivalence_Transitive _ _ F.eq_equiv.
End BackportEq.
这种定义方式，eq_refl（不带任何参数）的类型为 Reflexive eq，其中 Reflexive 是 class
Class Reflexive (R : relation A) :=
reflexivity : forall x : A, R x x.
（在 Classes/RelationClasses.v 中找到）
所以这意味着我们总是需要提供一个额外的参数来获得类型 x = x 的东西。这里没有定义隐式参数。
为什么导入像 PeanoNat.Nat 这样的模块通常不是一个好主意？
如果上面的徒劳无功还不够令人信服，我只想说像这样的模块，它扩展和导入其他模块和模块类型，通常不应该被导入。它们通常有短名称（如 N、Z 或 Nat），因此您可以轻松访问要从中使用的任何定理，而无需输入长名称。它们通常有很长的进口链，因此包含大量物品。如果你导入它们，现在大量的项目正在污染你的全局命名空间。正如您在 eq_refl 中看到的那样，这可能会导致您认为熟悉的常量发生意外行为。
在这次冒险中遇到的大部分模块都是“模块 type/functor”类型。可以说，它们很难完全理解，但可以找到简短的指南 here。
我的侦查是通过在 CoqIDE 中打开文件和 运行 命令 Locate eq_refl.（或者更好的是，ctrl+shift+L）在可能从其他地方导入的任何东西之后完成的. Locate 还可以告诉您常量是从哪里导入的。我希望有一种更简单的方法来查看模块类型中的导入路径，但我不这么认为。根据覆盖的 eq_refl 类型，您可能会猜到我们最终会进入 Coq.Classes.RelationClasses，但这并不准确。
玩 nostutter 练习时我发现了另一个奇怪的行为。这是代码：
Inductive nostutter {X:Type} : list X -> Prop :=
| ns_nil : nostutter []
| ns_one : forall (x : X), nostutter [x]
| ns_cons: forall (x : X) (h : X) (t : list X), nostutter (h::t) -> x <> h -> nostutter (x::h::t).
Example test_nostutter_manual: not (nostutter [3;1;1;4]).
Proof.
intro.
inversion_clear H.
inversion_clear H0.
unfold not in H2.
(* We are here *)
specialize (H2 eq_refl).
apply H2.
Qed.
展开后的状态是这样的：
1 subgoal (ID 229)
H1 : 3 <> 1
H : nostutter [1; 4]
H2 : 1 = 1 -> False
============================
False
当我在 IndProp.v 中 运行 specialize (H2 eq_refl). 加载其他逻辑基础文件时，它起作用了。它以某种方式理解它需要将“1”作为参数。 IndProp.v的Header是这样的：
Set Warnings "-notation-overridden,-parsing".
From LF Require Export Logic.
Require Import String.
Require Coq.omega.Omega.
当我将代码移动到另一个文件 "nostutter.v" 时，同样的代码给出了预期的错误：
The term "eq_refl" has type "RelationClasses.Reflexive Logic.eq" while it is expected to have type "1 = 1".
Header 共 nostutter.v:
Set Warnings "-notation-overridden,-parsing".
Require Import List.
Import ListNotations.
Require Import PeanoNat.
Import Nat.
Local Open Scope nat_scope.
我必须明确地向 eq_refl 添加一个参数：specialize (H2 (eq_refl 1)).
我认为这与专门化无关。它是什么？如何修复？
问题是导入 PeanoNat.Nat。
当您导入 PeanoNat 时，模块类型 Nat 进入作用域，因此导入 Nat 会引入 PeanoNat.Nat。如果您打算导入 Coq.Init.Nat，则必须在导入 PeanoNat 之前导入它，或者使用 Import Init.Nat..
为什么在这种情况下导入 PeanoNat.Nat 会造成麻烦？
Arith/PeanoNat.v (static link) 包含模块1 Nat。在该模块中，我们发现2 看起来不寻常的行
Include NBasicProp <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
All this means is that each of NBasicProp, UsualMinMaxLogicalProperties and UsualMinMaxDecProperties are included, which in turn means that everything defined in those modules is included in the current module. Separating this line out into three Include commands, we can figure out which one is redefining eq_refl. It turns out to be NBasicProp, which is found in this file (static link)。我们还没有到那里： eq_refl 的重新定义不在这里。但是，我们根据 NMaxMinProp.
NBasicProp 的定义
这将我们引向 NMaxMin.v，进而将我们引向 NSub.v，将我们引向 NMulOrder.v，将我们引向 NAddOrder.v，进而将我们引向 NAddOrder.v到 NOrder.v，这导致我们 NAdd.v，这导致我们 NBase.v，...
我将切入正题。最终我们在 Structures/Equality.v (static link) 中以模块 BackportEq 结束，它最终给了我们对 eq_refl.
Module BackportEq (E:Eq)(F:IsEq E) <: IsEqOrig E.
Definition eq_refl := @Equivalence_Reflexive _ _ F.eq_equiv.
Definition eq_sym := @Equivalence_Symmetric _ _ F.eq_equiv.
Definition eq_trans := @Equivalence_Transitive _ _ F.eq_equiv.
End BackportEq.
这种定义方式，eq_refl（不带任何参数）的类型为 Reflexive eq，其中 Reflexive 是 class
Class Reflexive (R : relation A) :=
reflexivity : forall x : A, R x x.
（在 Classes/RelationClasses.v 中找到）
所以这意味着我们总是需要提供一个额外的参数来获得类型 x = x 的东西。这里没有定义隐式参数。
为什么导入像 PeanoNat.Nat 这样的模块通常不是一个好主意？
如果上面的徒劳无功还不够令人信服，我只想说像这样的模块，它扩展和导入其他模块和模块类型，通常不应该被导入。它们通常有短名称（如 N、Z 或 Nat），因此您可以轻松访问要从中使用的任何定理，而无需输入长名称。它们通常有很长的进口链，因此包含大量物品。如果你导入它们，现在大量的项目正在污染你的全局命名空间。正如您在 eq_refl 中看到的那样，这可能会导致您认为熟悉的常量发生意外行为。
在这次冒险中遇到的大部分模块都是“模块 type/functor”类型。可以说，它们很难完全理解，但可以找到简短的指南 here。
我的侦查是通过在 CoqIDE 中打开文件和 运行 命令
Locate eq_refl.（或者更好的是，ctrl+shift+L）在可能从其他地方导入的任何东西之后完成的.Locate还可以告诉您常量是从哪里导入的。我希望有一种更简单的方法来查看模块类型中的导入路径，但我不这么认为。根据覆盖的eq_refl类型，您可能会猜到我们最终会进入 Coq.Classes.RelationClasses，但这并不准确。