1
$\begingroup$

The data I'm referring to is just an easy to understand JSON format of objects / arrows and the styling information about the arrows.

For example, if an arrow is two-headed I need in Coq locally to declare an epimorphism in the given category (also part of the data).

These usually will be "Let $f: A\to B$ be a morphism in $C$" type declarations but also sometimes the data will contain previously proved theorems or at least information on how to locate those theorems in the file system.

So my naive thinking tells me I should just create a Coq file that the user is not supposed to edit, I have standalone client running on their machine that updates this file, and then the user imports this file into their main file. So I would name the file probably the same thing as the diagram's name on the web.

Would this be possible in Coq? Or do you have a better way?

How far along am I? See this video to get a rough estimate:

Relevant YT video

It's a Django + Neo4j + Bootstrap Studio site for mathematicians.

Improve this question
$\endgroup$
1
  • 3
    $\begingroup$ I would really recommend writing an external tool in a different programming language (e.g. a shell script) rather than trying to get one piece of software (Coq, a theorem prover) to do something that's not in its job description (a HTTP client+JSON processor). $\endgroup$
    – HTNW
    May 24 at 2:08

1 Answer 1

Reset to default
2
$\begingroup$

Naïvely, the answer is no: Coq's programming language is not effectful, meaning in particular that there is no way to do input-output, either over http and otherwise.

As you remark, there is a slightly smarter solution: you can have an external program which grabs the data over http, and writes it into a file, which Coq can then import and work with. This sounds like a reasonable solution, and there already exists a flurry of tools that work in a more or less similar way. The ones that come to my mind are Ott and AutoSubst2 for syntax boilerplate, but I am pretty sure there are other examples for other use cases. If you go for such an approach I would recommand delegating as much work as possible to the external tool, ie letting it handle parsing and any needed transformation from the format used for communication to one that looks mathematically reasonable inside of Coq.

As for the difficulty of the task, it depends greatly of how much work there is to transform the data. If the transformation is a very simple syntactic one (for instance, turning JSON data representing a bunch of definitions like "Let $f : A \to B$ be a morphism in $C$" to an equivalent Coq definition), I don't expect the task to be too daunting. If you want to have more complex things (handling references/paths to theorems, generate theorems, etc.), you might have more work…

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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