coq Searching for an existing fact with Search and variants Searching for a pattern
Example
Search for all facts involving a pattern in an hypothesis or conclusion:
Coq < Search (_ + O).
plus_n_O: forall n : nat, n = n + 0
The _ character serves as a wildcard, it can be used multiple times:
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
You can also search for non-linear patterns:
Coq < Search (?x <= ?x).
le_n: forall n : nat, n <= n
