为什么 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”收到“Top”。前缀并导致问题。对于“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 *)

“frame”、“hide2”、“pick2”、“open1”和“open2”是公理（如下所示）。

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

还要注意，上面证明脚本中倒数第二个“destruct”策略工作得很好，因为 Coq 没有添加“Top”。 H0 中 d1 的前缀。另一方面，最后一个“destruct”策略会触发错误，因为 Coq 添加了“Top”。 H1 中 d2 的前缀。

那么，Coq 为什么要添加“顶部”。字首？为什么它只对我的某些条款这样做，即使我以相同的方式创建条款？什么是“顶”。字首？如何阻止 Coq 添加它？

附录：

“frame”、“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.