2
$\begingroup$

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.

Improve this question
$\endgroup$
5
  • 1
    $\begingroup$ Typo: dual $\to$ double dual $\endgroup$
    – Trebor ♦
    Commented Feb 6 at 19:21
  • 2
    $\begingroup$ 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. $\endgroup$
    – Ana Borges
    Commented Feb 6 at 23:23
  • $\begingroup$ “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. $\endgroup$
    – Jason Rute
    Commented Feb 6 at 23:30
  • 1
    $\begingroup$ 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. $\endgroup$
    – Meven Lennon-Bertrand ♦
    Commented Feb 7 at 10:06
  • $\begingroup$ 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. $\endgroup$
    – Andrej Bauer
    Commented Feb 7 at 10:24

1 Answer 1

Reset to default
3
$\begingroup$

Reading complicated code is the wrong approach to learning Coq, or any proof assistant, or any programming language. You should start with simple formalization that you attempt to do yourself, following a tutorial.

The Coq Documentation page lists a number of tutorials. For the mathematically inclined I would recommend the Mathematical Components book. The book comes accompanied with a web interface that allows you to use Coq in your browser and try it on the samples from the book.

Improve this answer
$\endgroup$

Not the answer you're looking for? Browse other questions tagged or ask your own question.