A boolean algebra solver buried in `Algebra.Lattice.Properties.BooleanAlgebra.Expression`

[onestruggler]

This file gives a boolean algebra solver:
src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda

It's probably better to put them in a dedicated file like "BooleanAlgebra.Solver.agda" for general use.

edit2: sorry, it is not a solver per se, but reminiscent of a solver.

[onestruggler]

We can slightly modify this file to work with more levels insteand of only

{b} (B : BooleanAlgebra b b)

as follows (only two places are modified, and it's checked) :

module Algebra.Lattice.Properties.BooleanAlgebra.Expression
{b c} (B : BooleanAlgebra b c)
where

...

open import Agda.Primitive using (⊔)
lift : ℕ → BooleanAlgebra b (b ⊔ c)

...

[jamesmckinna]

👍 to comment about Levels involved in this module... evidence of it not having been looked at too closely since it was first committed (itself as part of a refactoring which reorganised the Algebra hierarchy... so these design decision probably go back a lot longer)

[jamesmckinna]

As for Expression modelling 'the free BooleanAlgebra over n variables', as the basis for any potential Solver infrastructure, sure, so maybe you might like to work that up into a more detailed proposal/PR, including (or not) deprecation/modification of this module as needed? Although see also #1962 and #2539 ...

Seems as though that would be a good contribution!

[MatthewDaggitt]

Yes, agreed, moving this file up to the Algebra.Lattice.Solver.BooleanAlgebra file seems like a sensible move.

[onestruggler]

As for Expression modelling 'the free BooleanAlgebra over n variables', as the basis for any potential Solver infrastructure, sure, so maybe you might like to work that up into a more detailed proposal/PR, including (or not) deprecation/modification of this module as needed? Although see also #1962 and #2539 ...

Seems as though that would be a good contribution!

I am working on a solver. This is not hard, and I wonder why no one has done it before. I looked up this in Coq and Lean a little bit. In Coq, I didn't even find the definition of a boolean algebra. But Coq does have some tactics that works for Prop. In Lean, the definition of boolean algebra is there, but I didn't find related solvers. Leans does have tactics for Prop too.

[jamesmckinna]

NB, if we move the module up the hierarchy, and deprecate Algebra.Properties.BooleanAlgebra.Expression, we would have room to reconsider the syntax of Expr n, namely to employ the 'backtick' convention for quoted syntax, first proposed ... (by @gallais ? somewhere? ... I need to look this up!) so that _∧_ is quoted as _‵∧_ rather than infix ASCII _and_ etc.

There are separate questions (in my mind at least) about modelling Expr n (so fixing the 'variable' set to be Fin n) vs. fully-functorial syntax Expr (A : Set a) : Set (suc a) etc. and indeed whether we model the Free Algebra, or instead the Free Extension of a given BooleanAlgebra (with the free algebra as the degenerate instance at Fin 0/⊥... etc.)

[onestruggler]

Expr is just a datatype for manipulating expressions like "a + b * c" e.g. in a ring. Right now we have to define such a data type for every structure that needs a solver. We also have the reflection method to get the syntax of such expressions, but manipulating the syntax datatype is too complicated. I wonder if it is useful to have for each structure, an associated Expr? adding a fourth to the triple: IsX --- X --- RawX.

One use case is: Expr modulo out the laws of the structure is a "free" or "initial" object of the structure. E.g:

1. for monoid (the following is checked in Agda):

infixr 7 •
data Expr (X : Set) : Set where
var : X → Expr X
ε : Expr X
• : Expr X → Expr X → Expr X

infix 4 ≈
data ≈ {X} : (w v : Expr X) -> Set where
-- ≈ is a congruence.
refl : ∀ w -> w ≈ w
sym : ∀ w v -> w ≈ v -> v ≈ w
trans : ∀ w v u -> w ≈ v -> v ≈ u -> w ≈ u
cong : ∀ w v w' v' -> w ≈ w' -> v ≈ v' -> w • v ≈ w' • v'

-- The monoid axioms: asociativity and the left and right unit laws.
assoc : ∀ w v u -> (w • v) • u ≈ w • (v • u)
left-unit : ∀ w -> ε • w ≈ w
right-unit : ∀ w -> w • ε ≈ w

open import Level
open import Data.Product
open import Algebra.Bundles

free-monoid : Set -> Monoid 0ℓ 0ℓ
free-monoid X = record { Carrier = Expr X ; ≈ = ≈ {X} ; ∙ = • ; ε = ε ;
isMonoid = record {
isSemigroup = record {
isMagma = record { isEquivalence = record
{ refl = λ {x} → refl x
; sym = λ {x} {y} → sym x y
; trans = λ {i} {j} {k} → trans i j k
} ; ∙-cong = λ {x} {y} {u} {v} → cong x u y v } ; assoc = assoc } ;
identity = left-unit , right-unit } }

In this case, perhaps, the triple becomes the quadruple: IsX --- X --- RawX --- FreeX (ExprX). A solver uses the fact that if an expression hold in a free structure on X, then it holds in any other instance M of such structure under any given interpretation set function g : X -> M. That is, a solver uses the congruence requirement (well-definedness) of the unique morphism f prescribed by the universal property of free object for function g.

The remaining part of a solver is just to compute equalities on Expr the free object. The module Relation.Binary.Reflection then can be better parameterised to take only a semidecidable equality test on Expr, or be replaced by a different module that is less ad hoc, and is basically taking care of the "free boilerplate part" of a solver.

Anyone knows any paper about formalizing solvers in this way? If this is a new, is it worth to write a paper clarifying the idea?

[jamesmckinna]

Regarding papers, I guess that @oisdk might be the best person to ask here, but the idea for particular structures is already documented (though never quite in such explicit terms, as I read them) in eg. the papers I cite in #2629 (comment) ... but the architecture of the various existing Solver modules suggests that the technique was somehow already 'well-known'/'folklore' (probably there's some real archeology in the early automated reasoning papers on rewriting/unification-modulo-associative/associative-commutative laws, but that's outside my current expertise).

But it is also worth asking the members of the FREX project (mostly working in Idris, not Agda), including eg @gallais for pointers... that project site does include a link to 'Frex for Agda' but I still haven't had time to study exactly what's going on (despite frequent references and hints on this GitHub to others to look at this material... ;-)).

NB. As also mentioned elsewhere, I think the library is also missing a Solver specifically for AbelianGroup (via the free ℤ-module, which would, I hope, clear up existing problems in the RingSolvers about normalising away coefficients of the form r - r, and tackling Rings by viewing them as module-over-itself, together with the unique Ring/ℤ-module homomorphism from ℤ via initiality... but, again, I stress that I haven't really looked at this in detail, nor know any canonical reference to this)