[Coq] search lemma on the fly

CoqSearchLemmaOnTheFly.md

Search lemma on the fly in ProofGeneral

A helm extension for Search command.

/disambiguation/

• in the text, helm means Emacs-helm
• not means the HELM library of mathematics.

DEMO

Let's prove the commutative law of add.

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit.

Goal forall x y, x + y = y + x.
  move=> x y.
  rewrite [x + _] (** we need some lemma about the commutative property here **)

1. invoke helm-coq-search to look up the lemma.
2. type add at the Search prompt, then candidates (the name of lemma which has add as a substring) are displayed.
   • we can select some candidates by arrow keys
3. continue typing [SPACE]commutative to look up lemmas which contains of both add and commutative.
4. select item by arrow key and then hit [RETURN].
5. finally, the name of the lemma is inserted.

You can use key bind such as M-n or C-n instead of arrow key.

At the present moment, the library helm-coq-search has not been appeared at GitHub. Any comments and feedback are appreciated. Thanks.

---

Daisuke IKEGAMI

helm-coq-search.gif