CODEWITHSUNDEEP
coq
OrenIshShalom
OrenIshShalom

Reputation: 7112

Searching Coq libraries

I'm trying to prove that n <= 2^n in Coq, and I'm missing a simple lemma that must exist somewhere:

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

Even more generally, how can I search Coq libraries for lemmas like this one? Here is my code for completeness:

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

Upvotes: 2

Views: 1268

Answers (1)

Guillaume Melquiond
Guillaume Melquiond

Reputation: 1263

The command for searching lemmas is called Search. (For older Coq versions, it was split into SearchAbout, SearchPattern, etc.) See the documentation for all the possible variants.

In your case, you are looking for a lemma with a consequent of the form _+_ <= _+_. So, you can type the following, which will give six results, including the one you are looking for:

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

Upvotes: 2

Related Questions