1

玩 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

当我specialize (H2 eq_refl).在加载其他逻辑基础文件的 IndProp.v 中运行时，它可以工作。不知何故，它明白需要将“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)).

我认为这与专业无关。它是什么？怎么修？

4

1 回答 1

3

问题是导入PeanoNat.Nat。

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

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

Arith/PeanoNat.v（静态链接）包含模块1 Nat。在该模块中，我们发现2看起来不寻常的线

Include NBasicProp <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.

所有这些意味着NBasicProp,UsualMinMaxLogicalProperties和中的每一个UsualMinMaxDecProperties都被包含在内，这反过来又意味着这些模块中定义的所有内容都包含在当前模块中。将这一行分成三个Include命令，我们可以确定哪一个是重新定义eq_refl. 原来是NBasicProp，在这个文件中找到（静态链接）。我们还没有完成：eq_refl 的重新定义还没有出现。然而，我们看到了 的NBasicProp定义NMaxMinProp。

这将我们引向 NMaxMin.v，而 NSub.v 又将我们引向 NMulOrder.v，进而将我们引向 NAddOrder.v，进而将我们引向 NOrder.v，进而将我们引向 NAdd.v，这将我们引向 NBase.v，...

我会在这里切入正题。最终，我们在Structures/Equality.v（静态链接）中结束了该模块，该模块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（不带任何参数）有 type Reflexive eq，Reflexive类在哪里

Class Reflexive (R : relation A) :=
  reflexivity : forall x : A, R x x.

（在 Classes/RelationClasses.v 中找到）

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

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

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

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

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

于 2019-07-02T05:21:37.337 回答