Hi, I'm trying to figure out if I'm using modules wrong by including lemmas in them, or if there's another a way to do what I am trying to do. I want to capture the notion of a solver that promises to work on a subset of our problem states:

```
Definition Solver_is_complete_given (f : State -> option Solution) (condition : State -> Prop) :=
forall (st : State), condition st -> isSome (f st).
Module Type Solver.
Parameter condition : State -> Prop. (* For which states the solver promises to work? *)
Parameter solve : State -> option Solution.
Parameter complete : Solver_is_complete_given solve condition.
Parameter correct : Solver_is_correct solve.
End Solver.
```

If our problem was e.g. the 3x3 Tic-Tac-Toe (and the solution the optimal move in the given state), the idea here is that a partial solver could e.g. promise (and prove) to work on all problem states where 1) it's X's turn to play, and 2) which are immediately winnable by that single move. Then there could be a functor that turns any (X_to_play st /\ some_other_conditions st) Solver into a more generic solver by swapping X and O if it's O's turn to move. This I essentially have working for my problem, but only if I make everything transparent using `<:`

.

The problem I'm encountering is that no matter what I do, `condition`

is opaque if I derive a module using `:`

. My mental model of modules may be wrong, but I'd like that to be part of the "public interface" of the module so that I can reason about that proposition outside the module, while ideally I'd keep the other stuff opaque (which I don't get if I use `<:`

) so that I don't accidentally rely on implementation details. Is there a way to accomplish this?

First things first, modules are probably not the right abstraction tool for this kind of problem.

Most of the uses of modules from the ML world are subsumed by dependent records in dependent type theory.

There are a few exceptions, including but not limited to: 1. namespacing, 2. non-logical contents (e.g. tactics / hints) and 3. higher-order universe polymorphism

Back to your precise issue: you can export a transparency constraint on a signature using the `with Definition condition := ...`

syntax.

See the `with_declaration`

field from https://coq.inria.fr/refman/language/core/modules.html#grammar-token-with_declaration

Ok, thanks :) So far I've mostly avoided dependent types because I think I heard somewhere that they make things tricky in some unspecified way, but I guess I'll need to look into it! (I've really only been looking at coq for a week or so.)

Well, there are "dependent types" and "dependent types".

It's clear that the basic example of length-indexed vector is probably a total antipattern in Coq, but that does not mean you should just eschew dependent types altogether.

Ok.

(Otherwise there is little point in using Coq, you could just stick to some flavour of Fω that could even be encoded in, say, OCaml)

From what I gather from your excerpt, you're likely to be better off splitting the solver in a couple of simply-typed functions + theorems proving that they preserve whatever they're supposed to.

That could be true, and that's what I in fact had before I started to work on the module. But there's something I intend to reuse there too in the functor to generalize stuff; I have a solution for a special case of the problem (like "Xs only, trivially solvable, play on left side of the board"), and I anticipate having to reuse at least the Xs only -> Os too logic also in the future. But it's probably true that modules don't help there that much, I can just use the correctness and completeness proofs of the function that does that and not embed it in any module.

Thanks a lot :)

Sami Liedes has marked this topic as resolved.

Pierre-Marie Pédrot said:

(Otherwise there is little point in using Coq, you could just stick to some flavour of Fω that could even be encoded in, say, OCaml)

hmm, isn't constructive type theory considered useful in itself even without the dependent stuff? I believe Isabelle/CTT is maintained to this day, so it may be a better choice than bootstrapping from plain OCaml.

@Sami Liedes abstracting over records is probably simplest; sometimes those records can be made typeclasses or canonical structures, but both options have large learning curves.

@Karl Palmskog computation is not first-class in HOL, so you have to pass through weird hoops to get something akin to extraction

but in Isabelle/CTT, only the *meta logic* is HOL, right? Shouldn't one be able to define extraction at the object logic level? I agree it seems hoop-jumping is needed.

(this is the main ref: https://link.springer.com/content/pdf/10.1007%2FBFb0030561.pdf)

Last updated: Sep 28 2023 at 11:01 UTC