欧米茄真的在这里做什么？

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.