在構建腳本中驗證coq定理？

Question

我使用coq來研究編程語言的元理論。

在IDE中交互式編寫和驗證定理非常好，但我需要自動化（重新）驗證。我看到手冊頁，但是我沒有看到這個用例在任何地方拼寫出來。

如何將coq驗證合併到構建腳本中？

Answer 1

如果我們有這樣的metatheory/hello_world.v：

$ cat metatheory/hello_world.v 
Theorem hello_world : forall a b:Prop, a /\ b -> b /\ a. 
intros a b H. 
split. 
destruct H as [H1 H2]. 
exact H1. (* A bug: We actually need H2 here. *) 
intuition. 

然後我們就可以看到錯誤（與失敗的退出代碼）有：

$ coqtop -batch -silent -l metatheory/hello_world.v 
Error while reading metatheory/hello_world.v: 
File "/vagrant/metatheory/hello_world.v", line 5, characters 6-8: 
Error: In environment 
a : Prop 
b : Prop 
H1 : a 
H2 : b 
The term "H1" has type "a" while it is expected to have type 
"b". 

如果我們解決這個問題：

$ coqtop -batch -silent -l metatheory/hello_world.v 

..帶有成功的退出碼。