Jean-Pierre Messager (Oct 21 2020 at 10:10): Jean-Pierre Messager (Oct 21 2020 at 10:10):Hi all!
I'm looking for some kind of catalog of elementary proofs made in Coq I remember to have spotted once. For instance things like x*y = 0 => x=0 or y=0 (on integers, rationals, real numbers).
Christian Doczkal (Oct 21 2020 at 14:24):I guess for things that are "elementary" in the sense of your example, no such catalog exists, nor would it be useful given that there are probably thousands of them, if not tens of thousands. If you are looking for something specific, the Search command is your friend. However, it only searches in libraries that are currently loaded (via Require, not necessarily imported). For instance, if you have loaded ssrnat from mathcomp, then
Search (_ * _ == 0). returns:
muln_eq0: forall m n : nat, (m * n == 0) = (m == 0) || (n == 0)
as one of two results.
Last updated: Oct 05 2023 at 02:01 UTC