coq - 代数表达式的基本操作

Question

我仍然缺少通过向两边添加相同值来操作代数表达式的基本技术。例如，如果当前目标是 a + b < a + 5 ，如何将其转换为b < 5就像在纸笔校样中所做的那样？感谢您的帮助。

Answer 1

对于这种事情，你需要使用已经证明这一点的引理。其中大部分已在 Arith 中得到证明。 。如果您输入

From Coq Require Import Arith.
Search "+" "<".

Coq 会告诉您有关加法和“小于”关系的引理。特别是你会发现

plus_lt_compat_l: forall n m p : nat, n < m -> p + n < p + m

所以

Goal forall a b, a + b < a + 5.
  intros a b.
  apply plus_lt_compat_l.

确实会让你证明b < 5 .

通常情况下，您并不真正想要进行搜索，而是使用一些自动化操作。为此lia推荐。

From Coq Require Import Lia.

Goal forall a b, a + b < a + 5.
  intros a b.
  cut (b < 5).
  { lia. }
  (* The remaining goal is b < 5 *)

lia是解决许多此类算术问题的策略。