Tutorial by Examples

To see all the facts involving the le relation from the prelude: Coq < Search le. le_n: forall n : nat, n <= n le_S: forall n m : nat, n <= m -> n <= S m ... max_l: forall n m : nat, m <= n -> Nat.max n m = n max_r: forall n m : nat, n <= m -> Nat.max n m = m ... ...

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...

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 &...