Почему «Омега» Такти c не может решить такую ​​простую проблему, как эта

Question

У меня есть две теоремы tst4 и tst3, почему "омега" может решить 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 не следует рассматривать как универсальную тактику c, она действительно имеет дело с натуральными числами или целыми числами.

На самом деле lia может решить вашу цель, но я бы не стал полагаться на то, чтобы иметь дело с вещами, которые не имеют ничего общего с числами. В вашем случае, если вы придерживаетесь omega (или переключаетесь на lia и в конечном итоге получаете еще одну похожую цель, которую он не может решить), вы можете комбинировать ее с другой тактикой c, такой как тактическая intuition :

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