为什么 "奥妙 "战术不能解决这样一个简单的问题？

Question

我有两个定理tst4和tst3，为什么 "omega "能解tst4而不能解tst3？这对我来说是没有意义的，我有两个定理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.