Stream: Coq users

Topic: Code organization


view this post on Zulip Carl Patenaude-Poulin (Jun 29 2020 at 16:38):

Howdy! I'm playing around with formalizing generalized sudoku in Coq. "Generalized" in the sense that the game is parameterized by two nat values describing grid size. So I'm going to have a big chunk of (interdependent, type-heavy) code with those parameters. I'm going to want to instantiate that chunk of code by providing the parameters once, and receiving an object representing the specialized sudoku library.

Would you recommend using type classes? Modules? Sections? Something else? If you know of a relevant code example I could look at I would love that.

view this post on Zulip Enrico Tassi (Jun 29 2020 at 16:42):

What do you mean by code? It is just definitions and lemmas, or Ltac, Notations, ...

view this post on Zulip Carl Patenaude-Poulin (Jun 29 2020 at 16:51):

Minimally, definitions and lemmas; ideally, all of the above.

view this post on Zulip Enrico Tassi (Jun 29 2020 at 16:58):

Functors can abstract almost anything over a module, that would be the most "generic" abstraction you have. Type Classes and co are nice because instances are found automatically, while you have to manually apply functors. But for your use case this does not seem to be a big issue, I guess.

view this post on Zulip Karl Palmskog (Jun 29 2020 at 17:13):

@Carl Patenaude-Poulin are you aware of this? https://github.com/coq-contribs/sudoku

view this post on Zulip Karl Palmskog (Jun 29 2020 at 17:14):

most people use a combination of (1) sections + ltac + notations and (2) one of: modules, type classes, canonical structures

view this post on Zulip Carl Patenaude-Poulin (Jun 29 2020 at 17:17):

Nice, I'll try functors. Much appreciated.

view this post on Zulip Carl Patenaude-Poulin (Jun 29 2020 at 17:19):

@Karl Palmskog I've heard of the sudoku library, I plan on looking at it once I get stuck


Last updated: Feb 08 2023 at 22:03 UTC