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.

Hi @Andrey Klaus , for sure that task is super interesting and I think using the math-comp methodology should yield very interesting results!

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

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`

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

You can also remove the finType constrain, indeed, that's the reason I generalized already over vars

so actually yes you almost sure want this instead

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

I think IMVHO the key here is to use at first a more general type than {ffun elements of xs -> bool}

Then you place the refinement slightly "lower"

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

Hello Emilio, thank you very much for the answer! It is very encouraging. I will try to go the way you have described.

Yup, the idea is that now you can relate satisifibily by rewriting on `eval e f`

where `v`

has different types

That's actually a refinement [in the program verification sense] so it may help to write a small ref. infrastructure

For example assume your variables are of type `nat`

you can prove that there is an upper bound

and next you can indeed tranform every formula `form nat -> form 'I_bound`

[the bound is strict]

you use this transformation not for computing, but for proving

you still want to compute over it

you could similarly use the set of variables as you tryied first

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: Jan 29 2023 at 18:03 UTC