Warum Coq vor "Top". zu meinen Bedingungen?

Question

Warum erhalte ich folgende Fehlermeldung:

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

"d2" definiert ist, wie in meinem Code folgt:

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

Die vollständige Fehlermeldung ist folgende:

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

Ich verstehe nicht, warum nur "d2" und "d3" das "Top" erhalten. Präfix und Ursache Probleme. Ich habe nichts anderes gemacht als "d2" und "d3", was ich für d1 noch nicht gemacht habe.

Warum fügt Coq fälschlicherweise dieses Präfix hinzu?

Edit:

Hier ist mein Beweis Skript:

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

"Rahmen", "hide2", "pick2", "open1" und "open2" sind Axiome (siehe unten) .

Beachten Sie, dass H0, H1 und H2 in genau der gleichen Weise durch "assert" erstellt wurden. Ebenso wurden H1C, H2C und H3C auf genau die gleiche Weise durch "Zerstörung" erzeugt. Aber aus irgendeinem Grund fügt Coq das "Top" hinzu. Präfix vor d2 und d3, aber nicht vor d1. Die Spitze." erscheint nur in Fehlermeldungen. Es erscheint nicht in der Ausgabe, die oben rechts im CoqIDE angezeigt wird.

Beachten Sie auch, dass die vorletzte "Destruct" -Taktik im obigen Proofskript vollkommen in Ordnung ist, weil Coq das "Top" nicht hinzugefügt hat. Präfix zu d1 in H0. Auf der anderen Seite löst die letzte "Destruct" -Taktik den Fehler aus, weil Coq das "Top" hinzugefügt hat. Präfix zu d2 in H1.

Also, warum Coq die "Top" hinzufügen. Präfix? Und warum macht es das nur für einige meiner Begriffe, obwohl ich die Begriffe auf die gleiche Weise erstelle? Was ist das "Top"? Präfix? Wie kann ich verhindern, dass Coq es hinzufügt?

Anhang:

"Rahmen", "hide2", "pick2", "open1" und "open2" sind Axiome:

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

Dies ist in der Regel aufgrund eines Namensraum überlappen. Es ist schwer zu erraten, ohne ein vollständiges Beispiel, dieser Code veranschaulicht das Problem:

Module A. 

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

End A. 

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