## Stream: math-comp users

### Topic: build verified boolean formula solver

#### 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.
``````

#### Emilio Jesús Gallego Arias (Oct 17 2021 at 20:06):

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: Jul 23 2024 at 20:01 UTC