代数表达式的基本操作

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是解决诸如此类的许多算术问题的策略。

Answer 2

确定，我们设定这个目标。尽管nat和<是预定义的，但有关算术的许多基本定理仍需要Require Import Arith。

Require Import Arith.
Goal forall a b : nat, b < 5 -> a + b < a + 5.
  intros.

首先，我们来看看如何从库中手动找到正确的引理。我们可以搜索结论正确的可用引理。

SearchPattern (_+_ < _+_).

这将返回许多引理，其中之一恰好具有正确的形状（如果+运算符的左侧在两侧相同）：plus_lt_compat_l。因此，我们可以应用此引理。

  apply plus_lt_compat_l.
  assumption.
Qed.

请注意，有时<可能有引理，但<=可能没有引理，而SearchPattern找不到。在这种情况下，unfold lt in *.将<的所有用法扩展到<=可能会有所帮助，可能需要进行其他重写以移动S。

当然，每次都找到正确的引理很繁琐，因此有多种方法可以自动执行此搜索。一种方法是使用提示数据库。有一个名为arith的内置数据库，其中包含此引理。 auto with arith尝试将arith数据库中的引理的任何组合应用到特定深度。此处不需要的变量eauto with arith也将尝试发明中间变量。

Require Import Arith.
Goal forall a b : nat, b < 5 -> a + b < a + 5.
  intros.
  auto with arith.
Qed.

对于具体的算术，有“解决这个问题”的目标，例如lia（或旧版本的Coq中的omega，可以解决涉及变量和常量相加的任何不等式。

Require Import Omega.
Goal forall a b : nat, b < 5 -> a + b < a + 5.
  intros.
  omega.
Qed.