# Define “vector space” from scratch in Coq

I just want to learn how to use Coq better.

Supposing I wanted to prove a statement like “a vector space is naturally isomorphic to its dual”.

I would like to see how to define the concepts used in this statement, and then the statement proven, from scratch, in Coq. I do not wish to use a pre-existing library which has such objects already defined. I would like to see it done from the lowest level possible. I am pretty sure I read that Coq, based on the calculus of inductive constraints, has some sort of “core library”, its absolutemost primitives, vs. a number of concepts and definitions it commonly comes supplied with, like a “standard library”. My wish is to see the definitions constructed from the minimal base; the former instead of the latter.

• Typo: dual $\to$ double dual
– Trebor
Commented Feb 6 at 19:21
• At the risk of stating the obvious, if you find a library with such objects already defined, you can look at the library (and recursively at every other library it uses) in order to see how to do it from scratch. Commented Feb 6 at 23:23
• “lowest level possible” Basically if you don’t want to use a standard library definition you can just redefine it and use your version. It is common for people to do this with the natural numbers, and you can even do this for basic logical operations like equality if you like. Commented Feb 6 at 23:30
• Quite a large body of mathematics goes into defining vector spaces, their duals, and natural isomorphism. I do not think that reproducing all that body of mathematics, just to answer a stack exchange question, is a reasonable thing to ask for. As Ana says, the reasonable thing to do is to look at libraries that have this kind of concepts available, and then you can inspect how they are defined, and if you wish so recreate your own minimalistic definition. I'm sure people here would be happy to point you to such libraries. Commented Feb 7 at 10:06
• To reiterate @AnaBorges's point: if we point you to a specific location in a specific library and say "read this", that's going to be a valid answer to your question, correct? And also, you do not mean "from scratch", or else you need to first define logic. Commented Feb 7 at 10:24