搜索Coq库

Question

我试图证明Coq中的n <= 2^n，我忽略了一个必须存在于某个地方的简单引理：

a <= b /\ c <= d -> a+c <= b+d

更广泛地说，我如何在Coq库中搜索像这样的引理？以下是我的完整代码：

(***********)
(* imports *)
(***********)
Require Import Nat.
Require Import Init.Nat.
Require Import Coq.Arith.PeanoNat.

(************************)
(* exponential function *)
(************************)
Definition f (a : nat) : nat := 2^a.

(**********************)
(* inequality theorem *)
(**********************)
Theorem a_leq_pow_2_a: forall a, a <= f(a).
Proof.
  induction a as[|a' IHa].
  - apply le_0_n.
  - unfold f.
    rewrite Nat.pow_succ_r.
    * rewrite Nat.mul_comm.
      rewrite Nat.mul_succ_r.
      rewrite Nat.mul_1_r.
      unfold f in IHa.
      (* stuck here *)
Qed.

Answer 1

搜索引理的命令称为Search。(对于较早的Coq版本，它被拆分为SearchAbout、SearchPattern等)有关所有可能的变体，请参见文档。

在您的例子中，您正在寻找一个带有形式_+_ <= _+_的结果的引理。因此，您可以键入以下内容，这将给出六种结果，包括您要寻找的结果：

Search (_ + _ <= _ + _).
(*
Nat.add_le_mono_r: forall n m p : nat, n <= m <-> n + p <= m + p
Nat.add_le_mono: forall n m p q : nat, n <= m -> p <= q -> n + p <= m + q
...
*)