如何編譯Logic.v在勒柯克

Question

我使用勒柯克8.4pl6，並希望在勒柯克編譯Logic.v（Coq的標準庫），並看到它作爲模塊的編譯一個例子，打印輸出，但失敗了。

更具體地，在tauto的Logic.v 107系失敗：

104 Theorem and_cancel_l : forall A B C : Prop, 
    105 (B -> A) -> (C -> A) -> ((A /\ B <-> A /\ C) <-> (B <-> C)). 
    106 Proof. 
    107 intros; tauto. 
    108 Qed. 

我嘗試的過程如下：

1. 我試圖從控制檯，它在生產線生產Error: tauto failedcoqc Logic.v 107.我想這是因爲勒柯克初始環境已經導入Logic.vo，所以裝在同一個模塊的兩倍所造成的誤差。

2. 接下來，我試圖與空初始狀態編譯通過運行coqc -nois Logic.v，這產生以下錯誤。我不明白這個錯誤的意思......

   File ".../Logic.v", line 107, characters 10-15: 
   Anomaly: Incorrect tactic expression. Received exception is: 
   Anomaly: Uncaught exception Nametab.GlobalizationError(_). Please report.. 
   Please report. 
   

有什麼辦法來編譯Logic.v沒有錯誤？

Answer 1

編譯Logic.v的問題似乎是由於它重新定義了歸納類型True, False, and, or, ex, ex2, eq和常量not, iff, IF_then_else, all, eq_ind_r, eq_rec_r, eq_rect_r, subrelation, unique, uniqueness。

自動化的策略必須考慮（和治療），這些「新」的類型，並不斷從第一次被加載的情況不同，當勒柯克啓動。

一旦這些Definition和Inductive語句從Logic.v中刪除，我就能夠編譯該文件。

希望這會有所幫助。 （更完整的答案會在啓動過程中發生這種情況解釋究竟在何處。）