搜尋模式

在假設或結論中搜尋涉及模式的所有事實：

Coq < Search (_ + O).
plus_n_O: forall n : nat, n = n + 0

_ 字元用作萬用字元，可以多次使用：

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

你還可以搜尋非線性模式：

Coq < Search (?x <= ?x).
le_n: forall n : nat, n <= n