为什么"欧米茄"策略不能解决这样的简单问题

Question

我有两个定理tst4和tst3，为什么"omega"能解tst4而不能解tst3？这对我来说毫无意义。

Theorem tst4 : forall (a b c : nat), 
(a = b + 1 / b = 0) -> (False / a >= 1).
Proof. 
intros.
omega.
Qed.
Theorem tst3 : forall (a b c : nat), 
(a = b + 1 / b = 0) -> (False / (a >= 1 / True)).
Proof. 
intros.
omega.
Qed.

Answer 1

omega(或lia，正如@Anton Trunov所指出的，您应该使用它(对整数进行运算，并试图证明它们的性质，或从它们之间的矛盾中推断出虚假。因此，它能够在您的目标中处理False。然而True与此无关。omega不应该被认为是一种万能的策略，它实际上是处理自然数或整数。

事实上，lia能够解决你的目标，但我不会依赖任何一个来处理与数字无关的事情。在你的情况下，假设你坚持使用omega(或者切换到lia，最终达到另一个它无法解决的类似目标(，你可以将其与另一种战术相结合，比如战术intuition:

Theorem tst3 : 
forall (a b c : nat), 
(a = b + 1 / b = 0) -> 
(False / (a >= 1 / True)).
Proof. 
intros.
intuition omega.
Qed.