为什么Coq在“Top”前加上？为了我的条件？

Question

为什么我会收到以下错误消息：

The term "H1" has type
 "C Top.d2 w21"
while it is expected to have type
 "C d2 w21".

"d2“在我的代码中定义如下：

Inductive D : Type := 
  | d1 : D
  | d2 : D
  | d3 : D
.

完整的错误消息如下：

Error:
In environment
w, w1, w2, w3 : W
H : hide s0 =
    (w1 :: w2 :: w3 :: nil)%list
H1C : C d1 w1
H2C : C Top.d2 w2
H3C : C Top.d3 w3
w11 : W
H11 : pick d1 w1 =
      (w11 :: nil)%list
H11P : P d1 w11
w21 : W
H21 : pick d1 w2 =
      (w21 :: nil)%list
H21P : P d1 w21
w31 : W
H31 : pick d1 w3 =
      (w31 :: nil)%list
H31P : P d1 w31
H0 : C d1 w11
H1 : C Top.d2 w21
H2 : C Top.d3 w31
w112, w113 : W
d2, d3 : D
H11Open : open w11 =
          (w112 :: w113 :: nil)%list
D21 : d2 <> d1
D31 : d3 <> d1
D23 : d2 <> d3
H112O : O d2 w112
H113O : O d3 w113
The term "H1" has type
 "C Top.d2 w21"
while it is expected to have type
 "C d2 w21".

我不明白为什么只有"d2“和"d3”才能得到“顶级”。前缀并引起问题。对于"d2“和"d3”，我做的并没有什么不同，即使是d1也没有。

为什么Coq错误地添加了这个前缀？

编辑：

这是我的证明脚本：

Lemma changeprob: [ (At s0 (probPred Vic (cons hide (cons (pick d1) (cons open (cons (pick d2) nil) ) ) ) (2 # 3))) ].
Proof. mv.
unfold At.
unfold probPred.
unfold prob.
destruct (hide2 s0) as [w1 [w2 [w3 H ]]].  (* H : hide s0 =
(w1 :: w2 :: w3 :: nil)%list /\
C d1 w1 /\ C d2 w2 /\ C d3 w3 *)
destruct H as [H [H1C [H2C H3C]]].
rewrite H. simpl.
destruct (pick2 w1 d1) as [w11 [H11 H11P]].
destruct (pick2 w2 d1) as [w21 [H21 H21P]].
destruct (pick2 w3 d1) as [w31 [H31 H31P]].
rewrite H11; rewrite H21; rewrite H31; simpl.
assert (C d1 w11). (* H0 *)
  apply (frame w1 d1 d1 H1C); unfold r; unfold is_in; rewrite H11; left; reflexivity.

  assert (C d2 w21). (* H1 *)
    apply (frame w2 d2 d1 H2C); unfold r; unfold is_in; rewrite H21; left; reflexivity.

    assert (C d3 w31). (* H2 *)
      apply (frame w3 d3 d1 H3C); unfold r; unfold is_in; rewrite H31; left; reflexivity.


  destruct (open1 w11 d1 H0 H11P) as [w112 [w113 [d2 [d3 [H11Open [D21 [D31 [D23 [H112O H113O]]]]] ]]]].
  destruct (open2 w21 d2 d1 H1 H21P) as [w213 HNN]. (* This line throws the error *)

“框架”、"hide2“、"pick2”、"open1“和"open2”是公理(如下所示)。

请注意，H0、H1和H2是通过“断言”以完全相同的方式创建的。同样，H1C、H2C和H3C是通过“析构”以完全相同的方式创建的。但是，出于某种原因，Coq添加了“顶端”。前缀在d2和d3之前，而在d1之前。“顶上”仅在错误消息中显示。它不会出现在CoqIDE右上面板显示的输出中.

还要注意的是，上面的证明脚本中的第二个“破坏”策略非常好，因为Coq没有添加“Top”。前缀为d1在H0中。另一方面，最后一种“毁灭”策略会触发错误，因为Coq添加了“Top”。前缀为d2在H1中。

那么，为什么Coq要添加“顶端”。前缀？为什么它只对我的一些条款这样做，即使我以同样的方式创造了这些条款？什么是“顶级”？前缀？如何防止Coq添加它？

附录：

“框架”、"hide2“、"pick2”、"open1“和"open2”是公理：

Axiom hide2: forall w, exists w1 w2 w3, (hide w) = (cons w1 (cons w2 (cons w3 nil))) /\ (C d1 w1) /\ (C d2 w2) /\ (C d3 w3). 

Axiom pick2: forall w, forall d, exists w1, (pick d w) = (cons w1 nil) /\ (P d w1).

Axiom frame: [mforall d, mforall dp, (C d) m-> (box (pick dp) (C d)) ].

Axiom open1: forall w, forall d, ((C d) w) -> ((P d) w) -> exists w1 w2 d1 d2, (open w) = (cons w1 (cons w2 nil)) /\ ~(d1 = d) /\ ~(d2 = d) /\ ~(d1 = d2) /\ (O d1 w1) /\ (O d2 w2).

Axiom open2: forall w, forall d, forall dd, ((C d) w) -> ((P dd) w) -> exists w1, (open w) = (cons w1 nil) /\ exists do, ~(do = d) /\ ~(do = dd) /\ (O do w1).

Answer 1

这通常是由于名称空间重叠造成的。如果没有完整的示例，很难猜测，这段代码说明了这个问题：

Module A.

  Definition u := 3.
  Lemma v : u = u.
  Proof. reflexivity. Qed.

End A.

Import A.
Definition u := 4.
Print v.