Andrey Klaus (Oct 15 2021 at 17:29): Andrey Klaus (Oct 15 2021 at 17:29):Hello everyone.
I would like to build verified boolean formula solver. It looked to me like it is a good idea to use mathcomp for this task because it would allow me to understand mathcomp a bit better. Now when I've spent several days working on this task I'm not sure what should I do now.
I think that my way might be a bit 'too programming' for selected task and mathcomp together. And before continue or stop the working I would like to hear opinions of people who worked with mathcomp: do you think the task can be solved as described below using mathcomp or it is better to leave this idea?
Formula is
Definition var := nat.
Inductive formula : Set :=
Flit of var | Fneg of formula | Fcon of formula & formula | Fdis of formula & formula.
The idea is quite straightforward:
- build a full set of functions from formula variables to bool:
+ each finite function represents one possible assignment of all formula's variables (so, type is kind of var -> bool)
+ all possible assigments is a finite set of such functions
- write function evalFormula : (var -> bool) -> formula -> bool which use one such function to evaluate formula to boolean true or false
- filter full set of assigments using evalFormula. If we have no elements after filtering this means there is no solutions otherwise return the first one.
What I would like to have in result is something like definitions below.
Inductive variables_of : formula -> seq var -> Prop :=
(* Inductive relation which relates formula and it's set of variables *).
Definition evalFormula
(f : formula)
(xs : seq var)
(fxs : variables_of f xs)
(fn : {ffun (elements of xs) -> bool})
(* fn - function which maps all elements of xs (so, formula variables)
to bool.
*)
) : bool.
Definition buildFullSet
(f : formula)
(xs : seq var)
(fxs : variables_of f xs) : [set: {ffun (elements of xs) -> bool}].
Definition solveFormula'
(f : formula)
(xs : seq var)
(fxs : variables_of f xs) :=
filter (evalFormula f xs fxs) (buildFullSet f xs fxs).
Definition solveFormula f xs fxs : option {fn | evalFormula f xs fxs fn} :=
let res := solveFormula' f xs fxs in
if size res == 0 then None else Some ({head res | _})
Task is inspired by tasks for A.Chlipala's Certified Programming with Dependent Types book.
Any comments are welcome.
Emilio Jesús Gallego Arias (Oct 17 2021 at 19:49):Hi @Andrey Klaus , for sure that task is super interesting and I think using the math-comp methodology should yield very interesting results!
Emilio Jesús Gallego Arias (Oct 17 2021 at 19:49):I'm a bit short on time right now, but I'd be happy to try to help if its on my hand around mid-week
Emilio Jesús Gallego Arias (Oct 17 2021 at 19:50):There are already similar solvers for example in the verified work of Datalog by S. Dumbrava, and in math-comp there are a few elements that use this, for example Cyril was pointing out presentation.v
Emilio Jesús Gallego Arias (Oct 17 2021 at 20:05):For example I'd start from this, then you can easily refine it so you provide a computational version of enum {: valuation v}
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Section F.
Implicit Types (v : finType).
Inductive form v :=
| Var of v
| And of form v & form v
| Or of form v & form v.
Definition valuation v := {ffun v -> bool}.
Fixpoint eval v (env : valuation v) (f : form v) : bool :=
match f with
| Var v => env v
| And f1 f2 => eval env f1 && eval env f2
| Or f1 f2 => eval env f1 || eval env f2
end.
Definition solver v f : seq (valuation v) :=
[seq e <- enum {: valuation v} | eval e f ].
End F.
There are many approaches to do so I'd say
Emilio Jesús Gallego Arias (Oct 17 2021 at 20:06):You can also remove the finType constrain, indeed, that's the reason I generalized already over vars
Emilio Jesús Gallego Arias (Oct 17 2021 at 20:07):so actually yes you almost sure want this instead
Emilio Jesús Gallego Arias (Oct 17 2021 at 20:09):Section Form.
Implicit Types (v : Type).
Inductive form v :=
| Var of v
| And of form v & form v
| Or of form v & form v.
Fixpoint eval v (env : v -> bool) (f : form v) : bool :=
match f with
| Var v => env v
| And f1 f2 => eval env f1 && eval env f2
| Or f1 f2 => eval env f1 || eval env f2
end.
End Form.
Section Solver.
Implicit Types (v : finType).
Definition valuation v := {ffun v -> bool}.
Definition solver (v : finType) (f : form v) : seq (valuation v) :=
[seq e : valuation v <- enum {: valuation v} | eval e f ].
End Solver.
etc, etc...
Emilio Jesús Gallego Arias (Oct 17 2021 at 20:13):I think IMVHO the key here is to use at first a more general type than {ffun elements of xs -> bool}
Emilio Jesús Gallego Arias (Oct 17 2021 at 20:13):Then you place the refinement slightly "lower"
Emilio Jesús Gallego Arias (Oct 17 2021 at 20:13):Yeah I know, that's annoying, it is actually like building a pretty tricky puzzle, as it changes the shape depending on what pieces you mash together
Andrey Klaus (Oct 18 2021 at 07:15):Hello Emilio, thank you very much for the answer! It is very encouraging. I will try to go the way you have described.
Emilio Jesús Gallego Arias (Oct 18 2021 at 10:18):Yup, the idea is that now you can relate satisifibily by rewriting on eval e f where v has different types
Emilio Jesús Gallego Arias (Oct 18 2021 at 10:19):That's actually a refinement [in the program verification sense] so it may help to write a small ref. infrastructure
Emilio Jesús Gallego Arias (Oct 18 2021 at 10:19):For example assume your variables are of type nat
Emilio Jesús Gallego Arias (Oct 18 2021 at 10:19):you can prove that there is an upper bound
Emilio Jesús Gallego Arias (Oct 18 2021 at 10:20):and next you can indeed tranform every formula form nat -> form 'I_bound
Emilio Jesús Gallego Arias (Oct 18 2021 at 10:20):[the bound is strict]
Emilio Jesús Gallego Arias (Oct 18 2021 at 10:20):you use this transformation not for computing, but for proving
Emilio Jesús Gallego Arias (Oct 18 2021 at 10:20):you still want to compute over it
Emilio Jesús Gallego Arias (Oct 18 2021 at 10:21):you could similarly use the set of variables as you tryied first
Emilio Jesús Gallego Arias (Oct 18 2021 at 10:21):then you want to rewrite eval such that you prove it is invariant over the "general set" [which is nice for proving] vs the subset [which is more efficient]
Last updated: Apr 20 2024 at 04:02 UTC