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 <= _).
