Stream: math-comp users

Topic: build verified boolean formula solver


view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 20:06):

There are many approaches to do so I'd say

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 20:07):

so actually yes you almost sure want this instead

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 20:09):

etc, etc...

view this post on Zulip 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}

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2021 at 20:13):

Then you place the refinement slightly "lower"

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2021 at 10:19):

For example assume your variables are of type nat

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2021 at 10:19):

you can prove that there is an upper bound

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2021 at 10:20):

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2021 at 10:20):

[the bound is strict]

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2021 at 10:20):

you use this transformation not for computing, but for proving

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2021 at 10:20):

you still want to compute over it

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2021 at 10:21):

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

view this post on Zulip 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: Jan 29 2023 at 18:03 UTC