Stream: Coq users

Topic: Elementary proofs


view this post on Zulip 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).

view this post on Zulip 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: Jan 31 2023 at 14:03 UTC