如何为构造函数设置隐式参数

Question

玩 nostutter excersizes 我发现了另一种奇怪的行为。代码如下：

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 的标头是这样的：

Set Warnings "-notation-overridden,-parsing".
From LF Require Export Logic.
Require Import String.
Require Coq.omega.Omega.

当我将代码移动到另一个文件“nostutter.v”时，同样的代码会给出预期的错误：

术语“eq_refl”的类型为“RelationClasses.Reflexive Logic.eq”，而 它的类型应该是“1 = 1”。

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)).

我认为这与专业无关。它是什么？如何解决？

Answer 1

问题在于导入PeanoNat.Nat。

当您导入PeanoNat 时，模块类型Nat 会进入范围，因此导入Nat 会引入PeanoNat.Nat。如果您打算导入Coq.Init.Nat，则必须在导入PeanoNat 之前导入它，或者使用Import Init.Nat. 导入它。

为什么在这种情况下导入PeanoNat.Nat会导致麻烦？

Arith/PeanoNat.v (static link) 包含模块¹Nat。在该模块中，我们发现²不寻常的线条

Include NBasicProp <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.

All this means 是包含NBasicProp、UsualMinMaxLogicalProperties 和UsualMinMaxDecProperties 中的每一个，这反过来意味着这些模块中定义的所有内容都包含在当前模块中。将这一行分成三个Include 命令，我们可以找出哪一个是重新定义eq_refl。原来是NBasicProp，可以在this file (static link) 中找到。我们还没有完成：eq_refl 的重新定义还没有出现。但是，我们看到NBasicProp 的定义为NMaxMinProp。

这将我们引向 NMaxMin.v，它又将我们引向 NSub.v，NSub.v 将我们引向 NMulOrder.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 Reflexive (R : relation A) :=
  reflexivity : forall x : A, R x x.

（在 Classes/RelationClasses.v 中找到）

这意味着我们总是需要提供一个额外的参数来获得x = x 类型的东西。这里没有定义隐式参数。

为什么导入像 PeanoNat.Nat 这样的模块通常是个坏主意？

如果上面的野鹅追逐还不够令人信服，我只想说像这个扩展和导入其他模块和模块类型的模块通常不意味着要导入。它们通常有短名称（如N、Z 或Nat），因此您想从它们中使用的任何定理都可以轻松访问，而无需输入长名称。它们通常有很长的进口链，因此包含大量物品。如果您导入它们，那么现在大量的项目正在污染您的全局命名空间。正如您在 eq_refl 中看到的那样，这可能会导致您认为熟悉的常量出现意外行为。

---

1. 在这次冒险中遇到的大多数模块都是“模块类型/函子”种类。可以说，它们很难完全理解，但可以在here 找到一个简短的指南。

2. 我的侦查是通过在 CoqIDE 中打开文件并在可能从其他地方导入的任何内容之后运行命令 Locate eq_refl.（或者更好的是，ctrl+shift+L）来完成的。 Locate 还可以告诉您常量是从哪里导入的。我希望有一种更简单的方法来查看模块类型中的导入路径，但我不这么认为。您可能会根据被覆盖的eq_refl 的类型猜测我们最终会进入 Coq.Classes.RelationClasses，但这并不准确。