正在搜索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等。）有关所有可能的变体，请参见documentation。

在您的情况下，您要寻找因果形式为_+_ <= _+_的引理。因此，您可以键入以下内容，这将给出六个结果，包括您要查找的结果：

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
...
*)