Add KnuckleDragger like API

CHANGES.md

@@ -5,6 +5,12 @@
 
   * Turn on support for floats and uninterpreted sorts/functions in Bitwuzla.
 
+  * Add Data.SBV.Tools.KnuckleDragger, modeled after Philip Zucker's tool by the same
+    name: https://github.com/philzook58/knuckledragger.
+
+  * Add Documentation.SBV.Examples.KnuckleDragger.Kleene, as an example of the Knuckle-dragger
+    proofs.
+
 ### Version 10.12, 2024-08-11
 
   * Fix a few custom-floating-point format conversion bugs. Thanks to Sirui Lu for the patch.

Data/SBV/Tools/KnuckleDragger.hs

@@ -0,0 +1,104 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module    : Data.SBV.Tools.KnuckleDragger
+-- Copyright : (c) Levent Erkok
+-- License   : BSD3
+-- Maintainer: [email protected]
+-- Stability : experimental
+--
+-- A lightweight theorem proving like interface, built on top of SBV.
+-- Modeled after Philip Zucker's tool with the same name, see <http://github.com/philzook58/knuckledragger>
+-----------------------------------------------------------------------------
+
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE FlexibleInstances      #-}
+
+{-# OPTIONS_GHC -Wall -Werror #-}
+
+module Data.SBV.Tools.KnuckleDragger (
+        axiom, lemma, theorem, qb, ChainLemma(..)
+       ) where
+
+import Data.SBV
+import Control.Monad(void)
+
+-- | Tag the start of an axiom or lemma. The ribbon-length is roughly
+-- the width of the line you want printed. Perhaps it should be configurable,
+-- but for now, this is good enough.
+tag :: Int -> String -> String -> String
+tag tab s w = s ++ replicate (ribbonLength - length s - tab) ' ' ++ w
+  where ribbonLength :: Int
+        ribbonLength = 40
+
+-- | Tag the start of an axiom/lemma.
+start :: String -> String -> IO Int
+start knd nm = do let tab = 2 * length (filter (== '.') nm)
+                  putStr $ replicate tab ' ' ++ knd ++ nm
+                  pure tab
+
+-- | Accept the given definition as a fact. Usually used to introduce definitial axioms,
+-- giving meaning to uninterpreted symbols.
+axiom :: QuantifiedBool a => String -> a -> IO SBool
+axiom nm p = do putStrLn $ "Axiom: " ++ tag 0 nm "Admitted."
+                pure (qb p)
+
+-- | Helper to generate lemma/theorem statements.
+lemmaGen :: QuantifiedBool a => String -> String -> a -> [SBool] -> IO SBool
+lemmaGen what nm p by = do
+    tab <- start what nm
+    t <- isTheorem (quantifiedBool (sAnd by .=> qb p))
+    if t
+       then putStrLn $ drop (length nm) $ tag tab nm "Q.E.D."
+       else do putStrLn $ "\n*** Failed to prove " ++ nm ++ ":"
+               print =<< proveWith z3{verbose=True} (quantifiedBool p)
+               error "Failed"
+    pure (qb p)
+
+-- | Prove a given statement, using auxiliaries as helpers.
+lemma :: QuantifiedBool a => String -> a -> [SBool] -> IO SBool
+lemma = lemmaGen "Lemma: "
+
+-- | Prove a given statement, using auxiliaries as helpers. Essentially the same as lemma, except for the name.
+theorem :: QuantifiedBool a => String -> a -> [SBool] -> IO SBool
+theorem = lemmaGen "Theorem: "
+
+-- | Synonym for 'quantifiedBool', shorter to type.
+qb :: QuantifiedBool a => a -> SBool
+qb = quantifiedBool
+
+-- | A class for doing equational reasoning style chained proofs. Use 'chainLemma' to prove a given theorem
+-- as a sequence of equalities, each step following from the previous.
+class ChainLemma steps step | steps -> step where
+  chainLemma :: QuantifiedBool a => String -> a -> steps -> [SBool] -> IO SBool
+  makeSteps  :: steps -> [step]
+  makeInter  :: steps -> step  -> step -> SBool
+
+  chainLemma nm result steps base = do
+        void (start "Chain: " (nm ++ "\n"))
+        go (1 :: Int) base (makeSteps steps)
+     where go _ sofar []         = lemma nm result sofar
+           go _ sofar [_]        = lemma nm result sofar
+           go i sofar (a:b:rest) = do let intermediate = makeInter steps a b
+                                      _step <- lemma (nm ++ "." ++ show i) intermediate sofar
+                                      go (i+1) (qb intermediate : sofar) (b:rest)
+
+-- | Chaining lemmas that depend on a single quantified varible.
+instance (SymVal a, EqSymbolic z) => ChainLemma (SBV a -> [z]) (SBV a -> z) where
+   makeSteps steps = [\x -> steps x !! i | i <- [0 .. length (steps undefined) - 1]]
+   makeInter _ a b = qb $ \(Forall x) -> a x .== b x
+
+-- | Chaining lemmas that depend on two quantified varibles.
+instance (SymVal a, SymVal b, EqSymbolic z) => ChainLemma (SBV a -> SBV b -> [z]) (SBV a -> SBV b -> z) where
+   makeSteps steps = [\x y -> steps x y !! i | i <- [0 .. length (steps undefined undefined) - 1]]
+   makeInter _ a b = qb $ \(Forall x) (Forall y) -> a x y .== b x y
+
+-- | Chaining lemmas that depend on three quantified varibles.
+instance (SymVal a, SymVal b, SymVal c, EqSymbolic z) => ChainLemma (SBV a -> SBV b -> SBV c -> [z]) (SBV a -> SBV b -> SBV c -> z) where
+   makeSteps steps = [\x y z -> steps x y z !! i | i <- [0 .. length (steps undefined undefined undefined) - 1]]
+   makeInter _ a b = qb $ \(Forall x) (Forall y) (Forall z) -> a x y z .== b x y z
+
+-- | Chaining lemmas that depend on four quantified varibles.
+instance (SymVal a, SymVal b, SymVal c, SymVal d, EqSymbolic z) => ChainLemma (SBV a -> SBV b -> SBV c -> SBV d -> [z]) (SBV a -> SBV b -> SBV c -> SBV d -> z) where
+   makeSteps steps = [\x y z w -> steps x y z w !! i | i <- [0 .. length (steps undefined undefined undefined undefined) - 1]]
+   makeInter _ a b = qb $ \(Forall x) (Forall y) (Forall z) (Forall w) -> a x y z w .== b x y z w

Documentation/SBV/Examples/KnuckleDragger/Kleene.hs

@@ -0,0 +1,140 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module    : Documentation.SBV.Examples.KnuckleDragger.Kleene
+-- Copyright : (c) Levent Erkok
+-- License   : BSD3
+-- Maintainer: [email protected]
+-- Stability : experimental
+--
+-- Example use of the KnuckleDragger layer, proving some Kleene algebra theorems.
+--
+-- Based on <http://www.philipzucker.com/bryzzowski_kat/>
+-----------------------------------------------------------------------------
+
+{-# LANGUAGE DeriveAnyClass       #-}
+{-# LANGUAGE DeriveDataTypeable   #-}
+{-# LANGUAGE FlexibleInstances    #-}
+{-# LANGUAGE ScopedTypeVariables  #-}
+{-# LANGUAGE StandaloneDeriving   #-}
+{-# LANGUAGE TemplateHaskell      #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+
+{-# OPTIONS_GHC -Wall -Werror -Wno-unused-matches #-}
+
+module Documentation.SBV.Examples.KnuckleDragger.Kleene where
+
+import Prelude hiding((<=))
+
+import Data.SBV
+import Data.SBV.Tools.KnuckleDragger
+
+-- | An uninterpreted sort, corresponding to the type of Kleene algebra strings.
+data Kleene
+mkUninterpretedSort ''Kleene
+
+-- | Star operator over kleene algebras. We're leaving this uninterpreted.
+star :: SKleene -> SKleene
+star = uninterpret "star"
+
+-- | The 'Num' instance for Kleene makes it easy to write regular expressions
+-- in the more familiar form.
+instance Num SKleene where
+  (+) = uninterpret "par"
+  (*) = uninterpret "seq"
+
+  abs    = error "SKleene: not defined: abs"
+  signum = error "SKleene: not defined: signum"
+  negate = error "SKleene: not defined: signum"
+
+  fromInteger 0 = uninterpret "zero"
+  fromInteger 1 = uninterpret "one"
+  fromInteger n = error $ "SKleene: not defined: fromInteger " ++ show n
+
+-- | The set of strings matched by one regular expression is a subset of the second,
+-- if adding it to the second doesn't change the second set.
+(<=) :: SKleene -> SKleene -> SBool
+x <= y = x + y .== y
+
+-- | A sequence of Kleene algebra proofs. See <http://www.cs.cornell.edu/~kozen/Papers/ka.pdf>
+--
+-- We have:
+--
+-- >>> example
+-- Axiom: par_assoc                               Admitted.
+-- Axiom: par_comm                                Admitted.
+-- Axiom: par_idem                                Admitted.
+-- Axiom: par_zero                                Admitted.
+-- Axiom: seq_assoc                               Admitted.
+-- Axiom: seq_zero                                Admitted.
+-- Axiom: seq_one                                 Admitted.
+-- Axiom: rdistrib                                Admitted.
+-- Axiom: ldistrib                                Admitted.
+-- Axiom: unfold                                  Admitted.
+-- Axiom: least_fix                               Admitted.
+-- Lemma: par_lzero                               Q.E.D.
+-- Lemma: par_monotone                            Q.E.D.
+-- Lemma: seq_monotone                            Q.E.D.
+-- Chain: star_star_1
+--   Lemma: star_star_1.1                         Q.E.D.
+--   Lemma: star_star_1.2                         Q.E.D.
+--   Lemma: star_star_1.3                         Q.E.D.
+--   Lemma: star_star_1.4                         Q.E.D.
+-- Lemma: star_star_1                             Q.E.D.
+-- Lemma: subset_eq                               Q.E.D.
+-- Lemma: star_star_2_2                           Q.E.D.
+-- Lemma: star_star_2_3                           Q.E.D.
+-- Lemma: star_star_2_1                           Q.E.D.
+-- Lemma: star_star_2                             Q.E.D.
+example :: IO ()
+example = do
+
+  -- Kozen axioms
+  par_assoc <- axiom "par_assoc" $ \(Forall (x :: SKleene)) (Forall y) (Forall z) -> x + (y + z) .== (x + y) + z
+  par_comm  <- axiom "par_comm"  $ \(Forall (x :: SKleene)) (Forall y)            -> x + y       .== y + x
+  par_idem  <- axiom "par_idem"  $ \(Forall (x :: SKleene))                       -> x + x       .== x
+  par_zero  <- axiom "par_zero"  $ \(Forall (x :: SKleene))                       -> x + 0       .== x
+
+  seq_assoc <- axiom "seq_assoc" $ \(Forall (x :: SKleene)) (Forall y) (Forall z) -> x * (y * z) .== (x * y) * z
+  seq_zero  <- axiom "seq_zero"  $ \(Forall (x :: SKleene))                       -> x * 0       .== 0
+  seq_one   <- axiom "seq_one"   $ \(Forall (x :: SKleene))                       -> x * 1       .== x
+
+  rdistrib  <- axiom "rdistrib"  $ \(Forall (x :: SKleene)) (Forall y) (Forall z) -> x * (y + z) .== x * y + x * z
+  ldistrib  <- axiom "ldistrib"  $ \(Forall (x :: SKleene)) (Forall y) (Forall z) -> (y + z) * x .== y * x + z * x
+
+  unfold    <- axiom "unfold"    $ \(Forall e) -> star e .== 1 + e * star e
+
+  least_fix <- axiom "least_fix" $ \(Forall x) (Forall e) (Forall f) -> ((f + e * x) <= x) .=> ((star e * f) <= x)
+
+  -- Collect the basic axioms in a list for easy reference
+  let kleene = [ qb par_assoc,  qb par_comm, qb par_idem, qb par_zero
+               , qb seq_assoc,  qb seq_zero, qb seq_one
+               , qb ldistrib,   qb rdistrib
+               , qb unfold
+               , qb least_fix
+               ]
+
+  -- Various proofs:
+  par_lzero    <- lemma "par_lzero" (\(Forall (x :: SKleene)) -> 0 + x .== x) kleene
+  par_monotone <- lemma "par_monotone" (\(Forall (x :: SKleene)) (Forall y) (Forall z) -> x <= y .=> ((x + z) <= (y + z))) kleene
+  seq_monotone <- lemma "seq_monotone" (\(Forall (x :: SKleene)) (Forall y) (Forall z) -> x <= y .=> ((x * z) <= (y * z))) kleene
+
+  -- This one requires a chain of reasoning: x* x* == x*
+  star_star_1  <- chainLemma "star_star_1" (\(Forall (x :: SKleene)) -> star x * star x .== star x)
+                                           (\x -> [ star x * star x
+                                                  , (1 + x * star x) * (1 + x * star x)
+                                                  , (1 + 1) + (x * star x + x * star x)
+                                                  , 1 + x * star x
+                                                  , star x
+                                                  ])
+                                           kleene
+
+  subset_eq   <- lemma "subset_eq" (\(Forall x) (Forall y) -> (x .== y) .== (x <= y .&& y <= x)) kleene
+
+  -- Prove: x** = x*
+  star_star_2 <- do _1 <- lemma "star_star_2_2" (\(Forall x) -> ((star x * star x + 1) <= star x) .=> star (star x) <= star x) kleene
+                    _2 <- lemma "star_star_2_3" (\(Forall x) -> star (star x) <= star x)                                             (kleene ++ [_1])
+                    _3 <- lemma "star_star_2_1" (\(Forall x) -> star x        <= star (star x))                                      kleene
+
+                    lemma "star_star_2" (\(Forall (x :: SKleene)) -> star (star x) .== star x) [subset_eq, _2, _3]
+
+  pure ()

sbv.cabal

@@ -122,6 +122,7 @@ Library
                   , Data.SBV.Tools.BoundedFix
                   , Data.SBV.Tools.CodeGen
                   , Data.SBV.Tools.GenTest
+                  , Data.SBV.Tools.KnuckleDragger
                   , Data.SBV.Tools.NaturalInduction
                   , Data.SBV.Tools.Overflow
                   , Data.SBV.Tools.Polynomial
@@ -151,6 +152,7 @@ Library
                   , Documentation.SBV.Examples.Lists.Fibonacci
                   , Documentation.SBV.Examples.Lists.BoundedMutex
                   , Documentation.SBV.Examples.Lists.CountOutAndTransfer
+                  , Documentation.SBV.Examples.KnuckleDragger.Kleene
                   , Documentation.SBV.Examples.Misc.Definitions
                   , Documentation.SBV.Examples.Misc.Enumerate
                   , Documentation.SBV.Examples.Misc.FirstOrderLogic