歐米茄真的在這裏做什麼？

Question

這個證明可以用一個omega完成：

a : Z 
    b : Z                        
    H : a > 1 
    H0 : b > 1 
    H1 : b = 1                       
    H2 : a mod b = 0 
    ============================ 
    False 

這是爲什麼？ omega真的在這裏做什麼？而且由於H0和H1相互矛盾，難道不可能證明什麼嗎？另外，這可以證明沒有omega？怎麼樣？

Answer 1

1-這裏，omega認識到H0和H1是矛盾的，並用它們來產生False的證明。通過將H1重寫爲H0（其結果爲1 > 1），然後應用一些表示a > b -> a <> b，導致1 <> 1，然後應用於我們的目標，導致新目標1 = 1，這應該不難直接顯示這一點。可以通過reflexivity排出。很難形容如何omega作品的細節，因爲它背後複雜的算法，可以處理一大類類似的目標（粗略地講，Presburger arithmetic）

2 - 是的。 H0和H1可以用來證明任何東西，包括False。這有時被稱爲Principle of explosion。但是請注意，您只能在該特定背景內證明任何。否則，這不是因爲你在一些證明上下文中有矛盾，你可以證明其他任何。

Answer 2

如果您在Coq手冊中查找omega，您會看到對Bill Pugh's "The Omega Test: a fast and practical integer programming algorithm for dependence analysis"的引用，這應該可以粗略地解釋omega正在做什麼。

Answer 3

你可以通過顯示它生成的證明術語來找出任何策略已經完成了。

Require Import Omega. 

Definition how : forall (a : Z), (a > 1)%Z -> (a = 1)%Z -> False. 
intros. 
omega. 
Qed. 

Print how. 

(* Here are the library functions "how" uses on my machine: *) 

Check fast_Zplus_assoc_reverse. 
Check fast_Zred_factor0. 
Check fast_OMEGA15. 
Check fast_Zred_factor5. 
Check OMEGA6. 
Check Zegal_left. 
Check Zgt_left. 

您也可以證明這一點你自己，沒有任何花哨的機器：

Locate "_ > _". 
Print Z.gt. 
Locate "_ ?= _". 
Print Z.compare. 

Definition this : forall (a : Z), (a > 1)%Z -> (a = 1)%Z -> False. 
Proof with (subst; simpl in *; auto). 
intros... 
unfold Z.gt in * ... 
unfold Pos.compare in * ... 
inversion H. 
Qed. 

Print this.