如何编译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中删除，我就能够编译该文件。

希望这会有所帮助。 （更完整的答案会在启动过程中发生这种情况解释究竟在何处。）