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