Что здесь делает «омега»?

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

Если вы ищете omega в руководстве Coq, вы увидите ссылку на 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.