coq Searching for an existing fact with Search and variants Searching for a pattern in the conclusion of a lemma


Example

Search for a lemma when you know what its conclusion ought to be:

Coq < SearchPattern (S _ <= _).
le_n_S: forall n m : nat, n <= m -> S n <= S m

You can also search on a partial conclusion (the conclusion and one or several last hypotheses).

Coq < Require Import Arith.
Coq < SearchPattern (?x <= ?y -> ?y <= _ -> ?x <= _).
Nat.le_trans: forall n m p : nat, n <= m -> m <= p -> n <= p

Warning: if you mix up the order of the hypotheses, you won't find anything:

Coq < SearchPattern (?y <= _ -> ?x <= ?y -> ?x <= _).