What is "omega" doing here?
This proof can be completed with one omega
:
a : Z
b : Z
H : a > 1
H0 : b > 1
H1 : b = 1
H2 : a mod b = 0
============================
False
Why? What is omega
really doing here? And since H0
they H1
contradict each other, isn't it possible to prove something? Also, can you prove it without omega
? How?
source to share
1- Here omega
understands that they are H0
both H1
contradictory and use them to prove proof False
. It is not hard to show this directly by rewriting H1
in H0
(which leads to 1 > 1
), then we apply some lemma that shows what a > b -> a <> b
, resulting in 1 <> 1
, and then apply to our goal, resulting in a new goal 1 = 1
that can be discharged to reflexivity
. It is difficult to describe how it omega
works in detail, as it has a complex algorithm that can deal with a large class of similar targets (roughly Presburger arithmetic )
2- Yes. H0
and H1
can be used to prove anything, including False
. This is sometimes called the Explosion Principle . Please note, however, that you can only prove anything within that particular context. In other words, the point is not that in some evidential context you have a contradiction, that you can prove something else.
source to share
You can understand what a tactic has done by showing proven results.
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.
You can also prove it yourself without any fancy technique:
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.
source to share
If you look omega
in the Coq manual, you will see a link to Bill Pugh "The Omega Test: A Fast and Practical Integer Programming Algorithm for Dependency Analysis" , which should explain what it does omega
roughly.
source to share