Sami Liedes (Oct 09 2021 at 21:45): Sami Liedes (Oct 09 2021 at 21:45):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?
Pierre-Marie Pédrot (Oct 09 2021 at 22:08):First things first, modules are probably not the right abstraction tool for this kind of problem.
Pierre-Marie Pédrot (Oct 09 2021 at 22:09):Most of the uses of modules from the ML world are subsumed by dependent records in dependent type theory.
Pierre-Marie Pédrot (Oct 09 2021 at 22:10):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
Pierre-Marie Pédrot (Oct 09 2021 at 22:11):Back to your precise issue: you can export a transparency constraint on a signature using the with Definition condition := ... syntax.
Pierre-Marie Pédrot (Oct 09 2021 at 22:12):See the with_declaration field from https://coq.inria.fr/refman/language/core/modules.html#grammar-token-with_declaration
Sami Liedes (Oct 09 2021 at 22:18):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.)
Pierre-Marie Pédrot (Oct 09 2021 at 22:20):Well, there are "dependent types" and "dependent types".
Pierre-Marie Pédrot (Oct 09 2021 at 22:21):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.
Sami Liedes (Oct 09 2021 at 22:21):Ok.
Pierre-Marie Pédrot (Oct 09 2021 at 22:22):(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)
Pierre-Marie Pédrot (Oct 09 2021 at 22:23):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.
Sami Liedes (Oct 09 2021 at 22:27):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.
Sami Liedes (Oct 09 2021 at 22:27):Thanks a lot :)
Notification Bot (Oct 09 2021 at 22:27):Sami Liedes has marked this topic as resolved.
Karl Palmskog (Oct 09 2021 at 22:41):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.
Paolo Giarrusso (Oct 10 2021 at 00:32):@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.
Pierre-Marie Pédrot (Oct 10 2021 at 08:53):@Karl Palmskog computation is not first-class in HOL, so you have to pass through weird hoops to get something akin to extraction
Karl Palmskog (Oct 10 2021 at 09:01):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